[Spark2014-discuss] [M122-037] mark code in or out SPARK

Arnaud Charlet charlet at adacore.com
Mon Mar 25 17:39:44 CET 2013

> Why not "Spark_Section" to designate a piece of text?

Note that we don't want to designate a piece of text, we really want to mark
some entities. The two special cases are the private part and the
elab body, but these are not just piece of text, these are two well identified
package parts.

In other words, we don't want some generic mechanism such as pragma Warnings

Also pragma SPARK_Section; as a global configuration pragma does not read very
nicely IMO.


More information about the Spark2014-discuss mailing list