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

Yannick Moy moy at adacore.com
Thu Mar 14 15:45:35 CET 2013


On 03/14/2013 03:31 PM, Arnaud Charlet wrote:

> So far as I understand, we have identified the potential need to mark
> the following either "in" or "out" SPARK:
>
> - being able to mark a whole package in/out spark
> - being able to mark a subprogram in/out spark
> - being able to mark all public types in/out spark

rather all the declarations in the public part

> - being able to mark all private types in/out spark

rather all the declarations in the private part

> - being able to mark elaboration in/out spark
>
> Is the above a correct summary of our needs/requirements, or am I completely
> off?

I'm happy with the above. But others have different views.
-- 
Yannick Moy, Senior Software Engineer, AdaCore


More information about the Spark2014-discuss mailing list