SPARK 22 Release Notes¶

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

Improved Support of Language Features ¶

Extended Support for Access Types ¶

SPARK now uses a simpler model for dynamic memory allocation and deallocation, in which allocators and instances of Ada.Unchecked_Deallocation neither read nor write a special abstract state as was done previously. This change makes it possible to deallocate memory inside functions, to allocate memory inside nonvolatile functions, and to use allocators more liberally inside expressions. For example, an array of pointers to integers can be initialized with an aggregate:

V : Arr := (others => new Integer'(42));

In addition to the existing support for pool-specific access types, SPARK now supports:

named access-to-constant types:
```
type Const_Ptr is access constant Integer;
```
The data they designate is constant all the way down, even through dereferences of access-to-variable parts. Objects of a named access-to-constant type are not subjected to ownership checking.
general access types:
```
type General_Ptr is access all Integer;
```
Objects of a general access type are subjected to ownership checking to prevent aliasing and they cannot be deallocated, as they could designate memory on the stack.
attribute 'Access of an anonymous access type:
```
Variable_Handle : access T := Variable'Access;
Const_Handle    : access constant T := Const'Access;
```
The 'Access attribute of an anonymous access-to-variable type, like for Variable_Handle above, allows borrowing a part of an object temporarily, like Variable here. The 'Access attribute of an anonymous access-to-constant type, like for Const_Handle above, allows observing a part of an object temporarily, like Const here.
attribute 'Access of a general access-to-variable type:
```
type General_Ptr is access all T;
General_Handle : General_Ptr := Variable'Access;
```
The 'Access attribute of a general access-to-variable type, like for General_Handle above, allows moving the ownership of a local object, like Variable here, into a pointer. Ownership cannot be reclaimed back by Variable which should not be read or written directly afterwards.
attribute 'Access of a named access-to-constant type:
```
type Const_Ptr is access constant T;
Const_Handle : Const_Ptr := Const'Access;
```
The 'Access attribute of a named access-to-constant type, like for Const_Handle above, allows sharing a read-only access to a constant part of an object, like Const here.
owning components in tagged root types

SPARK now supports components of an owning type in the root type of a tagged hierarchy. Such components are still not allowed in tagged extensions.

Support for Address Clauses and Overlays ¶

SPARK now takes into account aliases created by address clauses of the form with Address => Obj'Address. If some variable X is overlaid on the address of Y, then any read or write of X will be considered a read or write of Y, and vice versa. Objects with such an address clause cannot appear in global contracts; one has to refer to the overlaid object instead.

Access Elements in Formal Containers Without Copy ¶

The formal containers library now provides Constant_Reference and Reference functions which provide read-only and read-write access to specific elements inside formal containers without copy. They use the ownership policy of SPARK to ensure that the container is not tampered with while the reference is valid.

Support for Iterator Filters ¶

GNATprove now supports disabling selected iterations inside loops and quantified expressions using an iterator filter, a new feature of Ada 2022. The filter is introduced by the keyword when to specify values that are subject to the iteration of quantification:

for J in 1 .. 10 when F(J) loop
   ...
end loop;

pragma Assert (for all J in 1 .. 10 when F(J) => Prop(J));

Program Specification ¶

Functional Contracts on Standard Library Units ¶

Preconditions and postconditions have been added to the subprograms of Ada.Characters.Handling, Ada.Strings.Bounded, Ada.Strings.Fixed and Ada.Strings.Maps. As a result, GNATprove can detect incorrect use of these libraries (through precondition failures) and analyse more precisely the effect of calling them (thanks to postconditions).

The body of these units has been proven with GNATprove to implement the specified contracts, thanks to the use of suitable ghost code (loop invariants and ghost lemmas mostly).

Tool Automation ¶

New Warnings by Flow Analysis ¶

Flow analysis now issues warnings in more cases:

When it detects statically dead code in IF and CASE statements.
When it detects that a loop exit condition is stable, i.e. when the variables used in the condition are not modified in the loop body.

Improved Reporting of Data Races for Abstract State ¶

If an abstract state is potentially subject to data-race conditions (because the state is accessed by different tasks), then GNATprove attempts to report this at the level of the common state abstraction rather than at the level of the state constituents. This used to only work for one “level” of state abstraction. Now the report is provided against the most abstract level of state that contains all contested constituents.

Additional Automatic Prover COLIBRI ¶

A new automatic prover called COLIBRI has been added to the existing three provers distributed with SPARK Pro: Alt-Ergo, CVC4 and Z3. COLIBRI is a constraint solver, rather than an SMT solver like the other three, which brings benefits for proving properties that involve mixed arithmetic (e.g. floating-point and integer arithmetic) or non-linear arithmetic (e.g. uses of rem and mod operators). COLIBRI can be used alone with the switch --prover=colibri or together with other provers, for example --prover=all for calling all provers.

New Prover Versions ¶

The Alt-Ergo prover shipped with SPARK was updated to version 2.4.0. The Z3 prover shipped with SPARK was updated to version 4.8.12.

Tool Interaction ¶

Distinguished Error Messages With “error:” Tag ¶

Error messages in GNATprove are now flagged with the error: tag after the location prefix, to make it easier to distinguish them from warnings (starting with warning: tag), check messages (starting with a tag denoting their severity: high:, medium: or low:) and information messages (starting with info: tag).

Better Display of Messages on the Command Line ¶

When using GNATprove from the command line, the location for the message (error, check, warning or info) is displayed precisely with characters that outline the span for the faulty expression. GNATprove also uses SGR (Select Graphic Rendition) to highlight different parts of messages, using colors and bold font. This is enabled by default, or when explicitly choosing --output=pretty switch.

More Precise Identification of Failed Proofs ¶

In various cases, GNATprove can now identify more precisely the part of a property that it fails to prove:

For unproved range and overflow checks, GNATprove now reports which bound (lower or upper bound) is not proved.
For predicate checks which consist in a conjunction of several properties, GNATprove now reports which property is not proved.
For calls to Boolean expression functions inside assertions, when the expression function is defined as a conjunction of several properties, GNATprove now reports which property is not proved, when it cannot prove the call.

Improved Suggestions for a Fix on Unproved Checks ¶

GNATprove generates better suggestions as part of unproved check messages in three cases:

When recommending the use of an expression function instead of a regular function, GNATprove indicates when it should be in the spec unit (for a client unit to see).
When a check is on the right-hand side of an “and” expression in a precondition, and the left-hand side of the “and” refers to some of the same variables, GNATprove recommends using “and then” instead, so that the evaluation of the right-hand side is guarded by the condition on the left-hand side.
When GNATprove can determine a sufficient precondition that would allow a check to pass, it suggests this precondition as possible fix. Note that the suggested precondition may be stricter than necessary. This concerns range-related checks (overflow, range, index and length checks) for which GNATprove suggests preconditions of the form:
```
add precondition (X < Integer'Last - 1) to subprogram at line xxx
```
as well as division-by-zero checks (on mod, rem, / and other operations) for which GNATprove suggests preconditions of the form:
```
add precondition (X /= 0) to subprogram at line xxx
```

Improved Counterexamples on Unproved Checks ¶

Counterexamples for unproved checks were previously enabled by default, and disabled explicitly with the switch --no-counterexample. As counterexamples can be spurious, especially at low levels of proof, they are now disabled by default and enabled either through the new switch --counterexamples=on or when switch --level is used with a value of 2, 3 or 4. The switch --counterexamples=off can be used to disable counterexamples explicitly at these levels.

Additionally, prior to being displayed, counterexamples are validated by a special simulation of the corresponding execution, taking into account the specificities of loops and calls, so that GNATprove can report when the error likely originates in a missing contract or annotation. More information on the technique used is available from the scientific article published at F-IDE 2021 Workshop.

Finally, for the case of array values displayed in counterexamples, GNATprove checks that these values contain only those indexes which fit in the array bounds, and avoids stating a value for the others index when none is needed. Values inside arrays are also pretty-printed, so for example Integer'Last is displayed instead of 2147483647.

Display of Generated Global Contracts in GNAT Studio ¶

A new contextual menu SPARK ‣ Globals ‣ Show generated Globals allows users to display generated Global contracts inside code panels. GNATprove flow analysis should have been run previously to generate the necessary information. More information can be found in this blog post.