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

Yannick Moy 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
> analyze.

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 
interested in).
-- 
Yannick Moy, Senior Software Engineer, AdaCore


More information about the Spark2014-discuss mailing list