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

Arnaud Charlet charlet at adacore.com
Thu Mar 14 15:19:34 CET 2013

>   1. specifying that a given (subprogram) entity is intended to be in SPARK
>   2. specifying the scope of a given analysis.
> Sure we need a subprogram body to be in SPARK to be able to analyse it
> for proof but we don't necessarily wish to analyze all the time all
> entities that are in the SPARK subset.
> Are we talking of 1. or 2. in this TN? the subject implies 2. but
> everything that has been said makes me think that we mostly discuss 1.

Yes, if you review the comment file you'll see that this ticket is
mainly about 1 at this stage.

In other words, the comment file contains some useful input/data, so I'd
recommend reading it/getting familiar with it to participate to this


More information about the Spark2014-discuss mailing list