[Spark2014-discuss] [M122-037] specifying SPARK sources for analysis

Yannick Moy moy at adacore.com
Thu Mar 14 16:01:19 CET 2013


On 03/14/2013 03:56 PM, Tucker Taft wrote:

> What I mean is that if at least part of a subprogram is worth
> attempting to prove, then it would be listed in the configuration
> file (perhaps using some kind of "wildcarding" pattern).
> If a subprogram is not listed in the configuration file,
> then it would be skipped in its entirety as far as proof.
>
> Note that whether or not you want something proved is somewhat
> different from whether you restrict yourself to SPARK-compatible
> constructs within it.  You might enforce the restrictions,
> but realize that proof is hopeless at a given state of
> development, and want to just rely on run-time checks.

ok I see your distinction now. At first, we plan to simply attempt proof 
on everything in SPARK, hence the need to be able to identify which code 
is in SPARK according to the user. What I meant is that this information 
needs to be in the code, and I think we agree.

We can always add more control on the tool side, if needed, possibly 
with patterns as you suggest. These may not be in the code, and in any 
case they are not part of SPARK 2014.
-- 
Yannick Moy, Senior Software Engineer, AdaCore


More information about the Spark2014-discuss mailing list