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

Cyrille Comar comar at adacore.com
Thu Mar 14 14:41:54 CET 2013


Le 14/03/2013 14:28, Tucker Taft a écrit :
> 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. -Tuck

just for the record, I fundamentally disagree with this conclusion. A
lexical on/off mechanism doesn't make any sense to me. Using an aspect
could make more sense to me but doesn't seem very urgent. I still think
that defining the scope of the formal analysis is mainly an issue of
providing the right input files and parameters to the toolset.

Furthermore, I don't understand what relation there is between "control
which features are permitted" and "specifying SPARK sources for analysis".


More information about the Spark2014-discuss mailing list