5.1. Language Restrictions

5.1.1. Excluded Ada Features

To facilitate formal verification, SPARK enforces a number of global simplifications to Ada 2012. The most notable simplifications are:

  • The use of access types and allocators is not permitted. Formal verification of programs with pointers requires tracking which memory is allocated and which memory has been freed, as well as separation between different blocks of memory, which are not doable precisely without a lot of manual work. As a replacement, SPARK provides rich generic data structures in the Formal Containers Library.
  • All expressions (including function calls) are free of side-effects. Functions with side-effects are more complex to treat logically and may lead to non-deterministic evaluation due to conflicting side-effects in sub-expressions of an enclosing expression. Functions with side-effects should be written as procedures in SPARK.
  • Aliasing of names is not permitted. Aliasing may lead to unexpected interferences, in which the value denoted locally by a given name changes as the result of an update to another locally named variable. Formal verification of programs with aliasing is less precise and requires more manual work. See Absence of Interferences.
  • The goto statement is not permitted. Gotos can be used to create loops, which require a specific treatment in formal verification, and thus should be precisely identified. See Loop Invariants and Loop Variants.
  • The use of controlled types is not permitted. Controlled types lead to the insertion of implicit calls by the compiler. Formal verification of implicit calls makes it harder for users to interact with formal verification tools, as there is no source code on which information can be reported.
  • Handling of exceptions is not permitted. Exception handling gives raise to numerous interprocedural control-flow paths. Formal verification of programs with exception handlers requires tracking properties along all those paths, which is not doable precisely without a lot of manual work. But raising exceptions is allowed (see Raising Exceptions and Other Error Signaling Mechanisms).

The features listed above are excluded from SPARK because, currently, they defy formal verification. As formal verification technology advances the list will be revisited and it may be possible to relax some of these restrictions. There are other features which are technically feasible to formally verify but which are currently not supported in SPARK, such as access-to-subprogram types.

Uses of these features in SPARK code are detected by GNATprove and reported as errors. Formal verification is not possible on subprograms using these features. But these features can be used in subprograms in Ada not identified as SPARK code, see Identifying SPARK Code.

5.1.2. Partially Analyzed Ada Features

SPARK reinforces the strong typing of Ada with a stricter initialization policy (see Data Initialization Policy), and thus provides no means currently of specifying that some input data may be invalid. As a result, the following features are allowed in SPARK, but only partially analyzed by GNATprove:

  • The result of a call to Unchecked_Conversion is assumed to be a valid value of the resulting type.
  • The evaluation of attribute Valid is assumed to always return True.

This is illustrated in the following example:

1
2
3
4
5
6
7
package Validity with
  SPARK_Mode
is

   procedure Convert (X : Integer; Y : out Float);

end Validity;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
with Ada.Unchecked_Conversion;

package body Validity with
  SPARK_Mode
is

   function Int_To_Float is new Ada.Unchecked_Conversion (Integer, Float);

   procedure Convert (X : Integer; Y : out Float) is
   begin
      pragma Assert (X'Valid);
      Y := Int_To_Float (X);
      pragma Assert (Y'Valid);
   end Convert;

end Validity;

GNATprove proves both assertions, but issues warnings about its assumptions that the evaluation of attribute Valid on both input parameter X and the result of the call to Unchecked_Conversion return True:

validity.adb:11:22: info: assertion proved
validity.adb:11:22: warning: attribute Valid is assumed to return True
validity.adb:13:22: info: assertion proved
validity.adb:13:22: info: initialization of "Y" proved
validity.adb:13:22: warning: attribute Valid is assumed to return True
validity.ads:5:36: info: initialization of "Y" proved

5.1.3. Data Initialization Policy

Modes on parameters and data dependency contracts (see Data Dependencies) in SPARK have a stricter meaning than in Ada:

  • Parameter mode in (resp. global mode Input) indicates that the object denoted in the parameter (resp. data dependencies) should be completely initialized before calling the subprogram. It should not be written in the subprogram.
  • Parameter mode out (resp. global mode Output) indicates that the object denoted in the parameter (resp. data dependencies) should be completely initialized before returning from the subprogram. It should not be read in the program prior to initialization.
  • Parameter mode in out (resp. global mode In_Out) indicates that the object denoted in the parameter (resp. data dependencies) should be completely initialized before calling the subprogram. It can be written in the subprogram.
  • Global mode Proof_In indicates that the object denoted in the data dependencies should be completely initialized before calling the subprogram. It should not be written in the subprogram, and only read in contracts and assertions.

Hence, all inputs should be completely initialized at subprogram entry, and all outputs should be completely initialized at subprogram output. Similarly, all objects should be completely initialized when read (e.g. inside subprograms), at the exception of record subcomponents (but not array subcomponents) provided the subcomponents that are read are initialized.

A consequence of the rules above is that a parameter (resp. global variable) that is partially written in a subprogram should be marked as in out (resp. In_Out), because the input value of the parameter (resp. global variable) is read when returning from the subprogram.

GNATprove will issue check messages if a subprogram does not respect the aforementioned data initialization policy. For example, consider a procedure Proc which has a parameter and a global item of each mode:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
package Data_Initialization with
  SPARK_Mode
is
   type Data is record
      Val : Float;
      Num : Natural;
   end record;

   G1, G2, G3 : Data;

   procedure Proc
     (P1 : in     Data;
      P2 :    out Data;
      P3 : in out Data)
   with
     Global => (Input  => G1,
                Output => G2,
                In_Out => G3);

   procedure Call_Proc with
     Global => (Output => (G1, G2, G3));

end Data_Initialization;

Procedure Proc should completely initialize its outputs P2 and G2, but it only initalizes them partially. Similarly, procedure Call_Proc which calls Proc should completely initalize all of Proc‘s inputs prior to the call, but it only initalizes G1 completely.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
package body Data_Initialization with
  SPARK_Mode
is

   procedure Proc
     (P1 : in     Data;
      P2 :    out Data;
      P3 : in out Data) is
   begin
      P2.Val := 0.0;
      G2.Num := 0;
      --  fail to completely initialize P2 and G2 before exit
   end Proc;

   procedure Call_Proc is
      X1, X2, X3 : Data;
   begin
      X1.Val := 0.0;
      X3.Num := 0;
      G1.Val := 0.0;
      G1.Num := 0;
      --  fail to completely initialize X1, X3 and G3 before call
      Proc (X1, X2, X3);
   end Call_Proc;

end Data_Initialization;

On this program, GNATprove issues 6 high check messages, corresponding to the violations of the data initialization policy:

data_initialization.adb:23:07: high: "G3.Num" is not an input in the Global contract of subprogram "Call_Proc" at data_initialization.ads:20
data_initialization.adb:23:07: high: "G3.Num" is not initialized
data_initialization.adb:23:07: high: "G3.Val" is not an input in the Global contract of subprogram "Call_Proc" at data_initialization.ads:20
data_initialization.adb:23:07: high: "G3.Val" is not initialized
data_initialization.adb:23:07: high: either make "G3.Num" an input in the Global contract or initialize it before use
data_initialization.adb:23:07: high: either make "G3.Val" an input in the Global contract or initialize it before use
data_initialization.adb:23:07: info: initialization of "G1.Num" proved
data_initialization.adb:23:07: info: initialization of "G1.Val" proved
data_initialization.adb:23:13: high: "X1.Num" is not initialized
data_initialization.adb:23:13: info: initialization of "X1.Val" proved
data_initialization.adb:23:17: warning: unused assignment to "X2"
data_initialization.adb:23:21: high: "X3.Val" is not initialized
data_initialization.adb:23:21: info: initialization of "X3.Num" proved
data_initialization.adb:23:21: warning: unused assignment to "X3"
data_initialization.ads:12:07: warning: unused variable "P1"
data_initialization.ads:13:07: high: "P2.Num" is not initialized in "Proc"
data_initialization.ads:13:07: info: initialization of "P2.Val" proved
data_initialization.ads:14:07: warning: "P3" is not modified, could be IN
data_initialization.ads:14:07: warning: unused variable "P3"
data_initialization.ads:16:27: low: unused global "G1"
data_initialization.ads:17:27: high: "G2.Val" is not an input in the Global contract of subprogram "Proc" at line 11
data_initialization.ads:17:27: high: "G2.Val" is not initialized
data_initialization.ads:17:27: high: either make "G2.Val" an input in the Global contract or initialize it before use
data_initialization.ads:17:27: info: initialization of "G2.Num" proved
data_initialization.ads:18:27: low: unused global "G3"
data_initialization.ads:18:27: warning: "G3" is not modified, could be INPUT
data_initialization.ads:21:28: info: initialization of "G1.Num" proved
data_initialization.ads:21:28: info: initialization of "G1.Val" proved
data_initialization.ads:21:32: info: initialization of "G2.Num" proved
data_initialization.ads:21:32: info: initialization of "G2.Val" proved
data_initialization.ads:21:36: info: initialization of "G3.Num" proved
data_initialization.ads:21:36: info: initialization of "G3.Val" proved

While a user can justify individually such messages with pragma Annotate (see section Justifying Check Messages), it is under her responsibility to then ensure correct initialization of subcomponents that are read, as GNATprove relies during proof on the property that data is properly initialized before being read.

Note also the various warnings that GNATprove issues on unused parameters, global items and assignments, also based on the stricter SPARK interpretation of parameter and global modes.

5.1.4. Absence of Interferences

In SPARK, an assignment to a variable cannot change the value of another variable. This is enforced by forbidding the use of access types (pointers) in SPARK, and by restricting aliasing between parameters and global variables so that only benign aliasing is accepted (i.e. aliasing that does not cause interference).

The precise rules detailed in SPARK RM 6.4.2 can be summarized as follows:

  • Two output parameters should never be aliased.
  • An input and an output parameters should not be aliased, unless the input parameter is always passed by copy.
  • An output parameter should never be aliased with a global variable referenced by the subprogram.
  • An input parameter should not be aliased with a global variable referenced by the subprogram, unless the input parameter is always passed by copy.

These rules extend the existing rules in Ada RM 6.4.1 for restricting aliasing, which already make it illegal to call a procedure with problematic (non-benign) aliasing between parameters of scalar type that are known to denote the same object (a notion formally defined in Ada RM).

For example, in the following example:

1
2
3
4
5
6
7
8
9
package Aliasing with
  SPARK_Mode
is
   Glob : Integer;

   procedure Whatever (In_1, In_2 : Integer; Out_1, Out_2 : out Integer) with
     Global => Glob;

end Aliasing;

Procedure Whatever can only be called on arguments that satisfy the following constraints:

  1. Arguments for Out_1 and Out_2 should not be aliased.
  2. Variable Glob should not be passed in argument for Out_1 and Out_2.

Note that there are no constraints on input parameters In_1 and In_2, as these are always passed by copy (being of a scalar type). This would not be the case if these input parameters were of a record or array type.

For example, here are examples of correct and illegal (according to Ada and SPARK rules) calls to procedure Whatever:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
with Aliasing; use Aliasing;

procedure Check_Param_Aliasing with
  SPARK_Mode
is
   X, Y, Z : Integer := 0;
begin
   Whatever (In_1 => X, In_2 => X, Out_1 => X, Out_2 => X);  --  illegal
   Whatever (In_1 => X, In_2 => X, Out_1 => X, Out_2 => Y);  --  correct
   Whatever (In_1 => X, In_2 => X, Out_1 => Y, Out_2 => X);  --  correct
   Whatever (In_1 => Y, In_2 => Z, Out_1 => X, Out_2 => X);  --  illegal
end Check_Param_Aliasing;

GNATprove (like GNAT compiler, since these are also Ada rules) correctly detects the two illegal calls and issues errors:

check_param_aliasing.adb:8:45: writable actual for "Out_1" overlaps with actual for "Out_2"
check_param_aliasing.adb:11:45: writable actual for "Out_1" overlaps with actual for "Out_2"

Here are other examples of correct and incorrect calls (according to SPARK rules) to procedure Whatever:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
with Aliasing; use Aliasing;

procedure Check_Aliasing with
  SPARK_Mode
is
   X, Y, Z : Integer := 0;
begin
   Whatever (In_1 => X, In_2 => X, Out_1 => X, Out_2 => Glob);     --  incorrect
   Whatever (In_1 => X, In_2 => Y, Out_1 => Z, Out_2 => Glob);     --  incorrect
   Whatever (In_1 => Glob, In_2 => Glob, Out_1 => X, Out_2 => Y);  --  correct
end Check_Aliasing;

GNATprove correctly detects the two incorrect calls and issues high check messages:

check_aliasing.adb:8:22: info: initialization of "X" proved
check_aliasing.adb:8:57: high: formal parameter "Out_2" and global "Glob" are aliased (SPARK RM 6.4.2)

5.1.5. Raising Exceptions and Other Error Signaling Mechanisms

Raising an exception is allowed in SPARK to signal an error, but handling the exception raised to perform recovery or mitigation actions is outside of the SPARK subset. Typically, such exception handling code should be added to top-level subprograms in full Ada, or to a last chance handler called by the runtime when an exception is raised, none of which is analyzed by GNATprove.

GNATprove treats raising an exception specially:

  • in flow analysis, the program paths that lead to a raise_statement are not considered when checking the contract of the subprogram, which is only concerned with executions that terminate normally; and
  • in proof, a check is generated for each raise_statement, to prove that no such program point is reachable.

Multiple error signaling mechanisms are treated the same way:

  • raising an exception
  • pragma Assert (X) where X is an expression statically equivalent to False
  • calling a procedure with an aspect or pragma No_Return that has no outputs (unless the call is itself inside such a procedure, in which case the check is only generated on the call to the enclosing error-signaling procedure)

For example, consider the artificial subprogram Check_OK which raises an exception when parameter OK is False:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
package Abnormal_Terminations with
  SPARK_Mode
is

   G1, G2 : Integer := 0;

   procedure Check_OK (OK : Boolean) with
     Global => (Output => G1),
     Pre    => OK;

end Abnormal_Terminations;
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
package body Abnormal_Terminations with
  SPARK_Mode
is

   procedure Check_OK (OK : Boolean) is
   begin
      if OK then
         G1 := 1;
      else
         G2 := 1;
         raise Program_Error;
      end if;
   end Check_OK;

end Abnormal_Terminations;

Note that, although G2 is assigned in Check_OK, its assignment is directly followed by a raise_statement, so G2 is never assigned on an execution of Check_OK that terminates normally. As a result, G2 is not mentioned in the data dependencies of Check_OK. During flow analysis, GNATprove verifies that the body of Check_OK implements its declared data dependencies.

During proof, GNATprove generates a check that the raise_statement on line 11 is never reached. Here, it is proved thanks to the precondition of Check_OK which states that parameter OK should always be True on entry:

abnormal_terminations.adb:11:10: info: raise statement proved unreachable
abnormal_terminations.ads:8:27: info: initialization of "G1" proved

GNATprove also checks that procedures that are marked with aspect or pragma No_Return do not return: they should either raise an exception or loop forever on any input.