Previous: , Up: Program Unit Level Restrictions   [Contents][Index]

5.2.15 SPARK_05

[GNAT] This restriction checks at compile time that some constructs forbidden in SPARK 2005 are not present. Note that SPARK 2005 has been superseded by SPARK 2014, whose restrictions are checked by the tool GNATprove. To check that a codebase respects SPARK 2014 restrictions, mark the code with pragma or aspect SPARK_Mode, and run the tool GNATprove at Stone assurance level, as follows:

gnatprove -P project.gpr --mode=stone

or equivalently:

gnatprove -P project.gpr --mode=check_all

With restriction SPARK_05, error messages related to SPARK 2005 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_05).

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 2005 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 2005 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 2005 restriction, violations will be reported for constructs forbidden in SPARK 95, instead of SPARK 2005.

Previous: , Up: Program Unit Level Restrictions   [Contents][Index]