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

Arnaud Charlet charlet at adacore.com
Thu Mar 14 16:16:38 CET 2013

> I agree, there are two somewhat different issues here, one is
> where you want the "prover" to try to do its work, and the other
> is what features you want to restrict.

Simply put, yes.

And to remove some confusion, this ticket (M122-037) is about the
former issue (where you want to apply the toolset/prover).

The other issue (feature restriction) is M226-014.

With that very important clarification in mind, can we now focus on
the first issue only on this thread?

> I believe the first might
> best be handled with a configuration file, as it may vary over time
> and depending on the project.

That's an interesting thought. Not one I had in mind, but I can see how
indeed that could vary, although in a similar way, a project can vary and
corresponding changes are made to the sources (including in the form of
comments), so I do not necessarily agree with your conclusion that a
configuration file is best for that.

In particular, I find a configuration file OK for coarse grain (basically
on a file level, or set of files), but configuration files get quickly
out of hand by finer grain (e.g. subprogram level), and quite impractical
if you want something more precise (e.g. public part of this package only).

> It sounds like we may need two different mechanisms, though

Yes, we clearly need two different mechanisms.

> The point of a "SPARK Issue" is for someone to capture all of
> the alternatives, with rationale and trade-offs well documented,
> and with examples.  E-mail is a rather poor substitute for that
> kind of reasoned argument.  Trying to resolve these kinds of
> things in a conference call, without first having someone lay
> out the various alternatives in a clear fashion, is a mistake in
> my view.

OK well, I apparently wrongly assumed that this ground work had occurred
already, but indeed it hasn't yet, and this needs to happen sooner rather
later now.

Who should be in charge of doing that?


More information about the Spark2014-discuss mailing list