SPARK 26 Release Notes¶

We present here a few highlights of the new features in SPARK 26. You can access the complete list here.

Language Extensions ¶

Multiple Levels of Ghost Code ¶

SPARK now offers multiple levels of ghost code. Ghost entities, assertion expressions, and specification pragmas can be associated with named assertion levels. Assertion levels, defined using the Assertion_Level pragma can then be enabled or disabled through an Assertion_Policy pragma.

Two levels of ghost code are predefined: Runtime and Static. Ghost code marked Runtime is always enabled; ghost code marked Static is never enabled.

Assertion Levels for SPARKlib Containers ¶

The SPARK library introduces several assertion levels that are used in the container libraries.

The assertion level SPARKlib_Defensive` allows enabling preconditions on container operations. This level is useful in particular if these operations are called from unproved code.

The assertion level SPARKlib_Logic` is for models of formal containers. It can be enabled in the full runtime. In the light runtime, it is also used for the ghost versions of the big numbers library and functional Containers library. As these libraries require finalization, the assertion level SPARKlib_Logic` cannot be enabled in the light runtime.

New Program_Exit Aspect for Abrupt Program Termination ¶

SPARK now offers a new Program_Exit aspect for specifying that the subprogram will terminate the whole program abruptly. The boolean expression given with this aspect, if any, shall be true when the program is terminated, which permits reasoning about intended program termination.

New Exit_Cases for Termination Conditions ¶

SPARK now offers a new Exit_Cases aspect for specifying subprogram termination conditions.

A subprogram can terminate by returning normally, by propagating an exception or by abruptly terminating the program. If a subprogram does not always terminate normally, then it can be annotated with an Exit_Cases aspect. This aspect allows partitioning the input state into cases and specifying for each case what the expected termination kind is:

Normal_Return, the subprogram shall return normally;

Program_Exit, the subprogram shall abruptly terminate the program;

Exception_Raised, the subprogram shall raise an (unspecified) exception; or

(Exception_Raised => E), the subprogram shall raise the exception E.

Support for Invalid Values ¶

SPARK now supports invalid values via a new Potentially_Invalid aspect. The Potentially_Invalid aspect can be used to annotate standalone objects, subprogram parameters, function result, and instances of Ada.Unchecked_Conversion to specify that they might have values that do not abide by the constraints of their type. A validity check is introduced whenever such objects are evaluated. The ‘Valid and ‘Valid_Scalars attributes can be used to assess their validity both in the code and in contracts.

Support for the finally Construct ¶

SPARK now supports the finally` keyword, a GNAT extension, which makes it possible to have a sequence of statements be executed when another sequence of statements is completed, whether normally or abnormally.

User Experience ¶

Success Message After Full Verification ¶

Previously, when all checks were proved (or annotated), GNATprove exited quietly with no explicit success message. Now, SPARK outputs a success message and prints the number of checks that were proved.

Support for Generics when Using –limit Switches ¶

Similar to the –limit-subp switch, the switches –limit-line and –limit-region now also support prefixing the location by a generic instantiation. The same is true for locations specified in a file passed to the –limit-lines switch.

No Resource-Leak Checks in Nonexecutable Ghost Code ¶

Taking advantage of the new support for multiple levels of ghost code, GNATprove no longer emits checks for resource leaks inside assertion pragmas, specification aspects, and ghost code that is associated with an assertion level that cannot be enabled at run time.

Warning Management via the Command Line ¶

In addition to the existing warning management capabilities, such as pragma Warnings and the –warnings switch, GNATProve now supports three switches -W, -A and -D, which allow users to enable warnings, suppress them, and promote them to errors, respectively. This can be done for predefined warning categories, which are identified by names appended to the warnings by default.

SARIF Output ¶

GNATProve now generates a gnatprove.sarif file at the same location as the gnatprove.out file that contains a summary of the run in SARIF format.

Improved Message with the –info Switch ¶

Previously, the –info switch could be used to enable a number of additional info messages, mostly related to proof. Now, a small number of these messages have been enabled by default (the messages related to inlining and loop unrolling), and the other info messages have been promoted into warnings that are disabled by default. Being warnings, they can be controlled by the -A, -W and -D switches and pragma Warnings (Off). The –info switch remains available to enable these warnings collectively.

Revised –no-global-generation Switch Behavior ¶

In previous versions of SPARK, the –no-global-generation switch prevented flow analysis from automatically generating Global contracts for subprograms without explicit global contracts. In this version of SPARK, the –no-global-generation switch has been modified to emit warnings when non-null Global contracts are generated for a subprogram with no explicit Global contracts. This change improves the stability of the feature, making it usable in more contexts.

Improved Documentation of Proof Limitations ¶

The section on proof limitations in the SPARK User’s Guide has been extended to include cases where the verification might fail due to the tool imprecision. The GNATprove tool has also been extended to detect more of these cases and to emit warnings when the –info switch is used.

Incompatible Changes in the SPARK Library ¶

Renaming of Insertion Primitives in Formal Vectors ¶

Similarly to Ada standard containers, the Containers.Formal.Vectors and Containers.Formal.Unbounded_Vectors packages of the SPARK library provide versions of the Append, Insert, and Prepend primitives taking a vector as a new item. These primitives have been renamed Append_Vector, Insert_Vector, and Prepend_Vector to match what has been done for the standard vector packages of Ada.

Simplification of Reference Function in Formal Containers ¶

The mode of the first parameters of the Reference functions declared in the Containers.Formal.Vectors, Containers.Formal.Doubly_Linked_Lists, Containers.Formal.Hashed_Maps, and Containers.Formal.Ordered_Maps packages of the SPARK library has been modified to simplify its usage. It is now an aliased parameter of mode IN OUT instead of an access parameter.

Similarly, the mode of the first parameters of the Reference functions declared in the Containers.Formal.Unbounded_Vectors, Containers.Formal.Unbounded_Doubly_Linked_Lists, Containers.Formal.Unbounded_Hashed_Maps, and Containers.Formal.Unbounded_Ordered_Maps packages of the SPARK library is now a parameter of mode IN instead of an access parameter.

Change in Generic Instances for Models of Formal Containers ¶

The actual parameter supplied for equality over elements of functional sequences and maps has been changed in the generic instances introduced for the various models of all formal containers. It is now the user-supplied equality function over keys or elements instead of a non-executable function standing for the logical equality. It makes it possible to enable these ghost models at run time, but it changes the meaning of comparison operators ("=", "<=", and "<") over these models, since they make use of this equality function. This change cannot modify the execution of a SPARK program in any way, as this is non-executable ghost code. However, it might affect the provability of user code if it uses these operators in its contracts. The ghost functions Equal, and Equal_Prefix on sequences, and Equal and Elements_Equal on functional maps are used as a replacement for these operators in the contracts of the container library so as to avoid degrading provability. User code might need to be changed in a similar way.

Executable Ghost Code in Containers ¶

It is now possible to execute most preconditions in the functional and formal container library. Ghost models in the formal container library are also executable in the full runtime. As a result, enabling all assertions and ghost code, for example using -gnata, now has the result of enabling these preconditions and ghost models as well. It is possible to disable them globally by adding pragma Check_Policy (SPARKlib_Defensive => Ignore); and pragma Check_Policy (SPARKlib_Logic => Ignore); to the global configuration switch of the user project.