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

Yannick Moy moy at adacore.com
Thu Mar 14 16:12:17 CET 2013

On 03/14/2013 04:09 PM, Cyrille Comar wrote:
> Le 14/03/2013 15:31, Arnaud Charlet a écrit :
>> - being able to mark elaboration in/out spark
>> Is the above a correct summary of our needs/requirements, or am I completely
>> off?
> What is the rational for marking specially elaboration stuff?

In SPARK 2005, the elaboration of a package can be hidden. And, if we 
provide the ability to state on each subprogram if it's in SPARK or not, 
we should do the same for the implicit subprogram of the elaboration, no?
Yannick Moy, Senior Software Engineer, AdaCore

More information about the Spark2014-discuss mailing list