Previous: No_Wide_Characters, Up: Program Unit Level Restrictions

5.2.12 SPARK_05

[GNAT] This restriction checks at compile time that some constructs forbidden in SPARK 2005 are not present. Error messages related to SPARK restriction have the form:

    violation of restriction "SPARK_05" at <source-location>
     <error message>

The restriction SPARK is recognized as a synonym for SPARK_05. This is retained for historical compatibility purposes (and an unconditional warning will be generated for its use, advising replacement by SPARK).

This is not a replacement for the semantic checks performed by the SPARK Examiner tool, as the compiler currently only deals with code, not SPARK 2005 annotations, and does not guarantee catching all cases of constructs forbidden by SPARK 2005.

Thus it may well be the case that code which passes the compiler with the SPARK restriction is rejected by the SPARK Examiner, e.g. due to the different visibility rules of the Examiner based on SPARK 2005 inherit annotations.

This restriction can be useful in providing an initial filter for code developed using SPARK 2005, or in examining legacy code to see how far it is from meeting SPARK restrictions.

The list below summarizes the checks that are performed when this restriction is in force:

The following restrictions are enforced, but note that they are actually more strict that the latest SPARK 2005 language definition:

This list summarises the main SPARK 2005 language rules that are not currently checked by the SPARK_05 restriction:

Note that if a unit is compiled in Ada 95 mode with the SPARK restriction, violations will be reported for constructs forbidden in SPARK 95, instead of SPARK 2005.