[Spark2014-discuss] [M122-037] specifying SPARK sources for analysis
moy at adacore.com
Thu Mar 14 17:08:55 CET 2013
On 03/14/2013 05:00 PM, Tucker Taft wrote:
> Well then "Analyze => On" if that is more appropriate. This
> ticket is supposedly asking how to specify which sources to
I still don't think it should be written like that in the code. I don't
find it clear to have entities marked as "Analyze => On" to mean that
"some" analysis by "some" formal tool can be performed. I much prefer
the firm SPARK / not SPARK distinction.
>> I don't really understand why the simple SPARK / non SPARK distinction
>> is not relevant. I
>> see there are issues with tool configuration and code profiles, but to
>> me they only add to
>> the SPARK / non SPARK distinction.
> Mixing these two together is what has created the problem in
> my mind.
So if we clearly separate those, and we say we are mostly interested for
now in the SPARK / non SPARK distinction, is it clear for you then? The
fact that we can exploit this distinction to have a better usability of
our tools is indeed a separate issue (although that's the one I'm most
Yannick Moy, Senior Software Engineer, AdaCore
More information about the Spark2014-discuss