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

Arnaud Charlet 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
point first.

>   - 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):

pragma In_SPARK;
pragma Mix_Ada_Spark;

what does the above mean? It doesn't mean anything to me, since it's
ambiguous. Hence the need for a single pragma IMO.

> 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

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
wants.

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
Auto allowed.

Arno


More information about the Spark2014-discuss mailing list