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

Tucker Taft taft at adacore.com
Thu Mar 14 17:00:45 CET 2013


On 3/14/13 11:42 AM, Yannick Moy wrote:
> On 03/14/2013 04:31 PM, Tucker Taft wrote:
>
>> Perhaps if we dropped the terms "SPARK" and "non SPARK" and focused
>> on whether we want to "attempt proof" or not, then this would clarify
>> things.  "SPARK" means too many things at this point, and using it
>> as a way to turn on or off proof seems like it has pushed things to
>> a breaking point.  How about "Proof => On" or "Proof => Off".  This
>> would be to some degree orthogonal to the "Code Profile" notion.
>> I think this might help to defuse the conflict.
>
> I would find it harder to explain to people, because:
>
> - as you say, which analysis you attempt to do on which code is ultimately a tool
> configuration issue. For example, do you want to do flow analysis, proof of absence of
> run-time errors, proof of contracts? This depends on the switches passed to gnatprove. So
> a code marked Proof => On might be simply flow analyzed.

Well then "Analyze => On" if that is more appropriate.  This
ticket is supposedly asking how to specify which sources to
analyze.


> ...
> 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.

-Tuck



More information about the Spark2014-discuss mailing list