[GNAT] This restriction checks at compile time that some constructs forbidden in SPARK are not present. The SPARK version used as a reference is the same as the Ada mode for the unit, so a unit compiled in Ada 95 mode with SPARK restrictions will be checked for constructs forbidden in SPARK 95. Error messages related to SPARK restriction have the form:
violation of restriction "SPARK" at <file>
<error message>
This is not a replacement for the semantic checks performed by the SPARK Examiner tool, as the compiler only deals currently with code, not at all with SPARK annotations and does not guarantee catching all cases of constructs forbidden by SPARK.
Thus it may well be the case that code which
passes the compiler in SPARK mode is rejected by the SPARK Examiner,
e.g. due to the different visibility rules of the Examiner based on
SPARK inherit annotations.
This restriction can be useful in providing an initial filter for code developed using SPARK, or in examining legacy code to see how far it is from meeting SPARK restrictions.