[Spark2014-discuss] [M122-037] mark code in or out SPARK
charlet at adacore.com
Mon Mar 25 16:37:27 CET 2013
> 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
This is obviously linked to your second point, so let's discuss the second
> - since the parameters on/off are treated differently from "auto", I
> wonder if it should be a separate functionality, pragma, aspect.
It can't be an aspect, since it's a global setting.
Introduce a different pragma seems overkill to me, and in particular, you
then need to resolve conflicting statements (using your syntax):
what does the above mean? It doesn't mean anything to me, since it's
ambiguous. Hence the need for a single pragma IMO.
> 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
I think it's better if users can express explicitly what a tool would do
automatically, even if it's redundant, so I think it's better if the
user can specify pragma SPARK_Mode (Auto); explicitly if this is what he
As for the name itself, 'SPARK' is even more generic than SPARK_Mode
I think, that's why I haven't proposed it, but I have no strong preference
on the name, except that In_SPARK doesn't work well if we keep the value
More information about the Spark2014-discuss