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

Arnaud Charlet charlet at adacore.com
Thu Mar 14 14:41:10 CET 2013


> Our general conclusion was to use a mechanism more like
> suppress/unsuppress or assertion policy or warning off/on than using an
> aspect to control which features are permitted at any point. The aspect
> approach is too tied to declarations, whereas something which can be turned
> off and on at various levels of granularity.

Can you clarify what use cases correspond to this need?

Also, what levels of granularity have been identified?

Certainly, we do not want to allow a hide-like capability, and we do not want
to start having to do proof on parts of subprograms only, so we need something
more "robust/controlled" than a general suppress/unsuppress mechanism.

In other words, we should keep the granularity at the package or subprogram
level (with I guess some provision to handle elaboration code/procedure),
and potentially allow granularity at the type level, although this part isn't
clear to me.

Arno


More information about the Spark2014-discuss mailing list