[Spark2014-discuss] [M122-037] specifying SPARK sources for analysis
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