SPARK 24 Release Notes

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

Vulnerability Report

From 24.2, you can download the SPARK vulnerability report from the Release Download section. It will provide you the list of the CVEs that can impact this product and the corresponding impact analysis describing whether the product is concerned by each CVE.

Improved Support of Language Features

Conditional Termination

Previously, GNATprove was designed to support primarily programs that always return normally. For SPARK 24, we extended the SPARK language and GNATprove to make termination explicit, by allowing fine-grained annotation of subprograms that propagate exceptions (see below) or that failing to terminate.

The new Always_Terminates aspect allows users to specify procedures that only terminate (return normally) or that raise an exception conditionally, in a fine-grained manner. This aspect can be used to specify a boolean condition on procedure inputs such that, if the condition evaluates to True, then the procedure must terminate.

procedure P1 (...) with Always_Terminates;
--  P1 shall terminate on all its inputs

procedure P2 (...) with Always_Terminates => False;
--  P2 might terminate on some of its input, but it does not need
--  to.

procedure P3 (...) with Always_Terminates => Condition;
--  P3 shall terminate on all inputs for which Condition evaluates
--  to True.

Functions in SPARK should still always terminate and therefore cannot be annotated with this aspect.

Handling and Propagation of Exceptions

Previously, SPARK allowed exceptions to be raised but did not allow exceptions to be propagated or handled. GNATprove thus attempted to verify that raise statements could never be reached - i.e., that they were dead code.

For SPARK 24, we extended the SPARK language and GNATprove to support propagation of exceptions to outer secope and local handling of exceptions. Procedures that might propagate exceptions need to be annotated with the new Exceptional_Cases aspect, which allows the exceptions that might be propagated to be listed and associated with an exceptional postcondition. This postcondition is used both to restrict the set of inputs on which the exception might be propagated and to verify callers when the exception is handled in outer scopes.

procedure P1 (...) with
  Exceptional_Cases => (others => False);
--  P1 cannot propagate exceptions. It is the default.

procedure P2 (...) with
  Exceptional_Cases => (others => True);
--  P2 might propagate an unspecified exception

procedure P3 (X : T; Y : out T) with
  Exceptional_Cases =>
    (E1 => Cond1 (X),
     E2 => Cond2 (Y));
--  P3 might propagate E1 or E2. The exceptional postconditions are
--  used both to:
--   * specify in which cases the exception might be raised - E1
--     can only be propagated on inputs on which Cond1 evaluates to
--     True.
--   * describe the effect of the subprogram when the exception is
--     propagated - when E2 is propagated, Cond2 (Y) evaluates to True.
--  A mix of the two is also possible.

Functions in SPARK still cannot propagate exceptions, so the aspect cannot be specified for them.

Enhanced Support for Relaxed_Initialization

The Relaxed_Initialization aspect can now be used to relax the initialization policy of SPARK on a case-by-case basis. The support for this feature has been extended to support types annotated with subtype predicates.

Checks for Parameters of the Container Library

The formal parameters of the container library of SPARK are subject to requirements. For example, the provided equality function shall be an equivalence relation (symmetric, reflexive, and transitive). Previously, these requirements were treated as assumptions by the tool; the user was required to verify them by other means. The container library has been modified so these properties are now verified by the tool on every instance. If the verification is complex, users can provide lemmas to help the tool as additional parameters of the generic packages.

Program Specification

Functional Multisets in the SPARK Library

Functional multisets have been added to the SPARK Library. They are particularly useful in modeling permutations, e.g., when verifying sorting routines.

GNAT-specific Aspect Ghost_Predicate

Ghost functions cannot be used in subtype predicates for non-ghost types: the predicates may be evaluated as part of normal execution during, e.g., membership tests.To alleviate this restriction, it is now possible to supply a subtype predicate using the Ghost_Predicate aspect, making it possible to use ghost entities in its expression. Membership tests are not allowed if the right operand is a type with such a predicate.

Tool Automation

New Prover Versions

The Z3 prover shipped with SPARK was updated to version 4.12.2. The cvc5 prover shipped with SPARK was updated to version 1.0.5.

Better Provability with Containers

The container library of SPARK has been modified to improve provability. In particular, contracts on procedures used to modify these containers now use logical equality instead of Ada equality. This is notably more efficient when both equalities do not coincide because the logical equality, unlike the Ada one, is handled natively by the underlying solvers.

Better Provability when Using Size Attributes

GNATprove now calls GNAT to generate data representations in order to support more precisely size and alignment attributes in proof.

Tool Interaction

Explain Codes

GNATprove now has an option gnatprove --explain that prints to standard output a short explanation for emitted messages, similar to rustc --explain. This can be used for error messages, warnings, or check messages. When a message has a corresponding explanation, it includes an explanation code, such as [E0001], in the message. Using the command --gnatprove --explain E0001, users can display the corresponding explanation. Note that while the GNAT compiler may also issue messages with an “explain code” for messages related to the use of SPARK, the command to get the explanation is always gnatprove --explain.

Fine-grained Specification of Analysis Mode

For customers who are migrating large bodies of code to SPARK, having to choose between disabling analysis entirely (i.e., setting the SPARK_Mode to Off) or committing to proof at Silver level (proof of absence of runtime errors) may not always be satisfactory. Previously, the analysis level could be set only at the project level, which is too coarse in such cases.

To help customers who are migrating large bodies of code to SPARK, we introduced two new ways to set a more fine-grained analysis level. First, users can select the analysis level for each unit, by setting the --mode switch for specific units in the GPR project file. Second, users can annotate their subprograms with one of two new annotations:

pragma Annotate (GNATprove, Skip_Proof, Name_Of_Subprogram);
pragma Annotate (GNATprove, Skip_Flow_And_Proof, Name_Of_Subprogram);

These annotations disable proof on a per-subprogram basis. The annotation Skip_Proof allows users to benefit from flow analysis on a subprogram, without having to go to full proof.

Counterexamples for Floating Point Values

Counterexample checking now supports floating-point numbers, so that counterexamples computed by a prover can be checked before being displayed to the user, when a proof does not pass.

Better Messages for Initialization and Incomplete Data Dependency

Messages emitted for reads of uninitialized data and incomplete Global and Depends contracts have been improved. Redundant messages are removed, initialization checks are condensed, and more errors are reported at once in case of incomplete contracts.

Incompatible Changes

Termination Annotations

The Annotate pragmas that used to be defined for termination are no longer supported. This includes Always_Return, Might_Not_Return, and Terminating. The Always_Terminates aspect should be used instead on procedures. Termination of functions is now checked by default.

Command-line Switches

The switch --checks-as-errors now needs an argument on or off. Previous usage of the switch should be replaced by --checks-as-errors=on.