2.166 Pragma SPARK_Mode ¶

Syntax:

pragma SPARK_Mode [(On | Off)] ;

In general a program can have some parts that are in SPARK 2014 (and follow all the rules in the SPARK Reference Manual), and some parts that are full Ada 2012.

The SPARK_Mode pragma is used to identify which parts are in SPARK 2014 (by default programs are in full Ada). The SPARK_Mode pragma can be used in the following places:

• As a configuration pragma, in which case it sets the default mode for all units compiled with this pragma.
• Immediately following a library-level subprogram spec
• Immediately within a library-level package body
• Immediately following the private keyword of a library-level package spec
• Immediately following the begin keyword of a library-level package body
• Immediately within a library-level subprogram body

Normally a subprogram or package spec/body inherits the current mode that is active at the point it is declared. But this can be overridden by pragma within the spec or body as above.

The basic consistency rule is that you can’t turn SPARK_Mode back On, once you have explicitly (with a pragma) turned if Off. So the following rules apply:

If a subprogram spec has SPARK_Mode Off, then the body must also have SPARK_Mode Off.

For a package, we have four parts:

• the package public declarations
• the package private part
• the body of the package
• the elaboration code after begin

For a package, the rule is that if you explicitly turn SPARK_Mode Off for any part, then all the following parts must have SPARK_Mode Off. Note that this may require repeating a pragma SPARK_Mode (Off) in the body. For example, if we have a configuration pragma SPARK_Mode (On) that turns the mode on by default everywhere, and one particular package spec has pragma SPARK_Mode (Off), then that pragma will need to be repeated in the package body.