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

Yannick Moy moy at adacore.com
Thu Mar 14 12:18:02 CET 2013

Was there was some progress on this issue at the last design meetings?
Thanks in advance.

On 02/27/2013 11:27 AM, Yannick Moy wrote:
> Steve, Trevor, did you make any progress on how the user should express
> that parts of his/her code are in SPARK? Is there an agreement that a
> Boolean aspect called "SPARK" on declarations is the chosen solution?
> Looking at the online LRM
> (http://docs.adacore.com/spark2014-lrm-docs/index.html), there is
> nothing new apparently.

More information about the Spark2014-discuss mailing list