[Spark2014-discuss] [M122-037] mark code in or out SPARK

Cyrille Comar comar at adacore.com
Mon Mar 25 16:29:15 CET 2013


Le 25/03/2013 15:58, Yannick Moy a écrit :
> On 03/25/2013 03:18 PM, Arnaud Charlet wrote:
>> I've written a first draft of the updated SPARK in/out proposal:
>>
>> https://forge.open-do.org/plugins/moinmoin/spark2014/SPARK2014Issues/SPARKMode
>>
>>
>> So that we can discuss it tomorrow during the SPARK 2014 RM concall.
> 
> I think it strikes a good balance between simplicity and flexibility.
> Plus it allows an easy adoption for SPARK 2005 users, since they can use
> pragma SPARK_Mode almost everywhere they used the --#hide annotation. It
> also makes it possible to add some other parameters one day to the
> pragma, say to express the version of SPARK. In summary: I like it!

I like the general direction as well. I made a few changes after
discussing with Arno: the default for a package/subprogram body was the
same spark_mode as the spec when defined locally on the spec. I'm not
sure this is the best default: I prefer that the body keeps the
spark_mode of the outer scope so that only "exceptions" need to be
marked with a local spark_mode. It is somewhat of a detail...


Things that I haven't changed but would be good to discuss:

  - pragma name: I don't like Spark_Mode ('mode' is such a generic
term). I wonder if In_Spark (Status => Boolean) wouldn't be clearer

  - since the parameters on/off are treated differently from "auto", I
wonder if it should be a separate functionality, pragma, aspect. For
instance: Pragma Mix_Ada_Spark. Note also that if this remains the
default, we don't even need to materialize the pragma. THe functionality
just disappears locally or globally when it is overridden by In_Spark


More information about the Spark2014-discuss mailing list