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

Yannick Moy moy at adacore.com
Mon Mar 25 15:58:33 CET 2013


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!
-- 
Yannick Moy, Senior Software Engineer, AdaCore


More information about the Spark2014-discuss mailing list