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

Arnaud Charlet charlet at adacore.com
Thu Mar 14 15:31:00 CET 2013


OK, I'll try to answer myself on the needs that have been identified so far,
please correct me/complete the list below, that will help clarify
things:

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
- being able to mark all private types in/out spark
- being able to mark elaboration in/out spark

Is the above a correct summary of our needs/requirements, or am I completely
off?

If I'm completely off, can someone list the precise needs/requirements
that have been identified as part of this ticket?

Arno


More information about the Spark2014-discuss mailing list