5.1. Language Restrictions
5.1.1. Excluded Ada Features
To facilitate formal verification, SPARK enforces a number of global simplifications to Ada. The most notable simplifications are:
Uses of access types and allocators must follow an ownership policy, so that only one access object has read-write permission to some allocated memory at any given time, or only read-only permission for that allocated memory is granted to possibly multiple access objects. See Memory Ownership Policy.
All expressions (including function calls) are free of side effects, at the exception of calls to so-called functions with side effects (see Aspect Side_Effects) which can only appear as the right-hand side of assignments. Allowing functions with side effects everywhere could lead to non-deterministic evaluation due to conflicting side effects in sub-expressions of an enclosing expression. Allowing all functions to have side effects would conflict with the need to treat functions mathematically in specifications.
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 backward goto statement is not permitted. Backward 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.
Functions should always terminate when called on inputs satisfying the precondition, at the exception of so-called functions with side effects (see Aspect Side_Effects). While care is taken in GNATprove to detect possibilities of unsoundness resulting from nonterminating functions, it is possible that axioms generated for infeasible contracts may lead to unsoundness. See Infeasible Subprogram Contracts.
Generic code is not analyzed directly. Doing so would require lengthy contracts on generic parameters, and would restrict the kind of code that can be analyzed, e.g. by forcing the variables read/written by a generic subprogram parameter. Instead, instantiations of generic code are analyzed in SPARK. See Analysis of Generics.
As formal verification technology advances the list will be revisited and it may be possible to relax some of these restrictions.
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. Sizes of Objects
GNATprove generally only knows the values of the Size
and Object_Size
attributes in simple cases such as scalar objects. For any more complex types
such as arrays and records, the value of these attributes is unknown, and e.g.
assertions referring to them remain unproved.
The user can indicate the values of these attributes to SPARK via confirming
representation clauses, using for Type'Size use ...
or the aspect syntax
with Size => ...
. Only static values can be used in these
representation aspects or clauses, which can only be used on type declarations
and not on subtype declarations.
Note that for an object X
of type T
, the value of X'Size
is not
necessarily equal to T'Size
, but equal to T'Object_Size
. So it is
generally more useful to specify Object_Size
on types to be able to know
the value the Size
attribute of the type’s objects. However, to compute the
size of T'Object_Size
for composite types, the value of C'Size
is
generally used, C
being the type of a component. The value of
Object_Size
must be 8, 16, 32 or a multiple of 64, while the Size
of a
type can be any value.
Attributes Size
and Object_Size
are specific to a subtype. As such, it
is not known if a subtype has the same value for these attributes as its base
type, including when the subtype does not introduce any constraint as in
subtype S is T
.
The following code example shows some simple representation clauses using the aspect syntax:
-- SPARK knows the 'Size and 'Object_Size of scalar types
type Short_Short is range -128 .. 127;
type U8 is mod 2 ** 8;
-- The following representation clauses are not needed, but serve to
-- illustrate that in the record type declaration below, U7'Size (and not
-- U7'Object_Size) is used to check the Object_Size of the record type.
type U7 is mod 2 ** 7
with Size => 7,
Object_Size => 8;
-- Without the packing instruction, the compiler would complain that
-- objects of type R do not fit into 8 bits.
type R is record
A : U7;
B : Boolean;
end record
with Pack, Object_Size => 8;
5.1.3. Data Validity
SPARK reinforces the strong typing of Ada with a stricter initialization policy (see Data Initialization Policy), and thus provides no means of specifying that some input data may be invalid. This has some impact on language features that process or potentially produce invalid values. SPARK issues checks specific to data validity on two language constructs:
Calls to instances of
Unchecked_Conversion
Objects with a supported address clause (so-called overlays). An address clause is supported if it is of the form
with Address => Y'Address
, whereY
is another object, andY
is part of a statically known object.
For occurences of these patterns, SPARK checks that no invalid values can be
produced. Given that no invalid values can be constructed in SPARK, the
evaluation of the attribute Valid
is assumed to always return True.
These validity checks are illustrated in the following example:
1package Validity with
2 SPARK_Mode
3is
4
5 procedure Convert (X : Integer; Y : out Float);
6
7end Validity;
1with Ada.Unchecked_Conversion;
2
3package body Validity with
4 SPARK_Mode
5is
6
7 function Int_To_Float is new Ada.Unchecked_Conversion (Integer, Float);
8
9 procedure Convert (X : Integer; Y : out Float) is
10 begin
11 pragma Assert (X'Valid);
12 Y := Int_To_Float (X);
13 pragma Assert (Y'Valid);
14 end Convert;
15
16end 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. It also issues
a “high” unproved check that the unchecked conversion to Float
may produce
invalid values (for example, if an Integer
is converted whose bit
representation corresponds to a NaN
float, which is not allowed in SPARK).
validity.adb:7:13: info: types in unchecked conversion have the same size
validity.adb:7:59: info: type is suitable as source for unchecked conversion
validity.adb:7:68: high: type is unsuitable as a target for unchecked conversion
7 | function Int_To_Float is new Ada.Unchecked_Conversion (Integer, Float);
| ^~~~~
possible explanation: floating-point types have invalid bit patterns for SPARK
validity.adb:11:22: warning: attribute Valid is assumed to return True
11 | pragma Assert (X'Valid);
| ^~~~~~~
validity.adb:11:22: info: assertion proved
validity.adb:13:22: warning: attribute Valid is assumed to return True
13 | pragma Assert (Y'Valid);
| ^~~~~~~
validity.adb:13:22: info: assertion proved
validity.ads:5:36: info: initialization of "Y" proved
When checking an instance of Unchecked_Conversion
, GNATprove also checks
that both types have the same Object_Size
. For non-scalar types,
GNATprove doesn’t know the Object_Size
of the types, so representation
clauses that specify Object_Size
are required to prove such checks (see
also Sizes of Objects). Similarly, for object declarations with an
Address clause or aspect that refers to the 'Address
of another object,
SPARK checks that both objects have the same known Object_Size
.
SPARK allows conversions from (suitable) integer types or
System.Address_Type
to general access-to-object types. When
calling such instances of Unchecked_Conversion
, GNATprove makes
some assumptions about the result of the call:
The designated data has no aliases if it is an access-to-variable type and no mutable aliases otherwise.
The returned object is a valid access and it designates a valid value of its type.
At each call to such Unchecked_Conversion
, GNATprove raises
warnings to notify the user that these assumptions need to be
ascertained by other means.
Conversions from integer types or System.Address_Type
to
pool-specific access-to-object types are still forbidden, as these
pointers should not be deallocated nor considered when checking for
memory leaks.
Conversions from access-to-object types to integer
types or System.Address_Type
are still forbidden, because SPARK
does not handle addresses.
1with Ada.Unchecked_Conversion;
2with Interfaces; use Interfaces;
3with System; use System;
4
5package UC_To_Access with SPARK_Mode => On is
6 type Int_Access is access all Integer;
7
8 function Uns_To_Int_Access is new Ada.Unchecked_Conversion (Unsigned_64, Int_Access);
9 -- Accepted with warnings
10 function Uns_From_Int_Access is new Ada.Unchecked_Conversion (Int_Access, Unsigned_64);
11 -- Rejected
12
13 C1 : constant Int_Access := Uns_To_Int_Access (30);
14
15 function Addr_To_Int_Access is new Ada.Unchecked_Conversion (Address, Int_Access);
16 -- Accepted with warnings
17 function Addr_From_Int_Access is new Ada.Unchecked_Conversion (Int_Access, Address);
18 -- Rejected
19
20 Addr : Address with Import;
21 C2 : constant Int_Access := Addr_To_Int_Access (Addr);
22
23 type PS_Access is access Integer;
24
25 function Uns_To_PS_Access is new Ada.Unchecked_Conversion (Unsigned_64, PS_Access);
26 -- Rejected
27end UC_To_Access;
uc_to_access.ads:10:13: error: unchecked conversion instance from a type with access subcomponents is not allowed in SPARK
uc_to_access.ads:10:13: error: violation of aspect SPARK_Mode at line 5
uc_to_access.ads:13:32: warning: call to "Uns_To_Int_Access" is assumed to return a valid access designating a valid value
uc_to_access.ads:13:32: warning: the value returned by a call to "Uns_To_Int_Access" is assumed to have no aliases
uc_to_access.ads:17:13: error: unchecked conversion instance from a type with access subcomponents is not allowed in SPARK
uc_to_access.ads:17:13: error: violation of aspect SPARK_Mode at line 5
uc_to_access.ads:21:32: warning: call to "Addr_To_Int_Access" is assumed to return a valid access designating a valid value
uc_to_access.ads:21:32: warning: the value returned by a call to "Addr_To_Int_Access" is assumed to have no aliases
uc_to_access.ads:25:13: error: unchecked conversion instance to a pool-specific access type is not allowed in SPARK
uc_to_access.ads:25:13: error: violation of aspect SPARK_Mode at line 5
gnatprove: error during flow analysis and proof
5.1.4. 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 modeInput
) 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 modeOutput
) 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 modeIn_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:
1package Data_Initialization with
2 SPARK_Mode
3is
4 type Data is record
5 Val : Float;
6 Num : Natural;
7 end record;
8
9 G1, G2, G3 : Data;
10
11 procedure Proc
12 (P1 : in Data;
13 P2 : out Data;
14 P3 : in out Data)
15 with
16 Global => (Input => G1,
17 Output => G2,
18 In_Out => G3);
19
20 procedure Call_Proc with
21 Global => (Output => (G1, G2, G3));
22
23end 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.
1package body Data_Initialization with
2 SPARK_Mode
3is
4
5 procedure Proc
6 (P1 : in Data;
7 P2 : out Data;
8 P3 : in out Data) is
9 begin
10 P2.Val := 0.0;
11 G2.Num := 0;
12 -- fail to completely initialize P2 and G2 before exit
13 end Proc;
14
15 procedure Call_Proc is
16 X1, X2, X3 : Data;
17 begin
18 X1.Val := 0.0;
19 X3.Num := 0;
20 G1.Val := 0.0;
21 G1.Num := 0;
22 -- fail to completely initialize X1, X3 and G3 before call
23 Proc (X1, X2, X3);
24 end Call_Proc;
25
26end 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" is not an input in the Global contract of subprogram "Call_Proc" at data_initialization.ads:20
23 | Proc (X1, X2, X3);
| ^~~~~~~~~~~~~~~~
either make "G3" an input in the Global contract or initialize it before use
data_initialization.adb:23:13: high: "X1.Num" is not initialized
23 | Proc (X1, X2, X3);
| ^~
data_initialization.adb:23:17: warning: "X2" is set by "Proc" but not used after the call
23 | Proc (X1, X2, X3);
| ^~
data_initialization.adb:23:21: warning: "X3" is set by "Proc" but not used after the call
23 | Proc (X1, X2, X3);
| ^~
data_initialization.adb:23:21: high: "X3.Val" is not initialized
23 | Proc (X1, X2, X3);
| ^~
data_initialization.ads:12:07: warning: unused variable "P1"
12 | (P1 : in Data;
| ^~
data_initialization.ads:13:07: high: "P2.Num" is not initialized in "Proc"
13 | P2 : out Data;
| ^~
reason for check: OUT parameter should be fully initialized on return
possible fix: initialize "P2.Num" on all paths, make "P2" an IN OUT parameter or annotate it with aspect Relaxed_Initialization
data_initialization.ads:14:07: warning: "P3" is not modified, could be IN
14 | P3 : in out Data)
| ^~
data_initialization.ads:14:07: warning: unused variable "P3"
14 | P3 : in out Data)
| ^~
data_initialization.ads:16:27: low: unused global "G1"
16 | Global => (Input => G1,
| ^~
data_initialization.ads:17:27: high: "G2.Val" is not initialized
17 | Output => G2,
| ^~
data_initialization.ads:18:27: warning: "G3" is not modified, could be INPUT
18 | In_Out => G3);
| ^~
data_initialization.ads:18:27: low: unused global "G3"
18 | In_Out => G3);
| ^~
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 low check messages and warnings that GNATprove issues on unused parameters, global items and assignments, also based on the stricter SPARK interpretation of parameter and global modes.
It is possible to opt out of the strong data initialization
policy of SPARK on a case by case basis using the aspect
Relaxed_Initialization
(see section Aspect Relaxed_Initialization and Ghost Attribute Initialized).
Parts of objects subject to this aspect only need to be initialized when
actually read. Using Relaxed_Initialization
requires specifying data
initialization through contracts that are verified by proof (as opposed to
flow analysis). Thus, Relaxed_Initialization
should only be used when
needed as it requires more effort to verify data initialization from both the
user and the tool.
5.1.5. Memory Ownership Policy
In SPARK, access values (a.k.a. pointers) are only allowed to alias in known ways, so that formal verification can be applied as if allocated memory pointed to by access values was a component of the access value seen as a record object.
In particular, assignment between access objects operates a transfer of ownership, where the source object loses its permission to read or write the underlying allocated memory.
For example, in the following example:
1procedure Ownership_Transfer with
2 SPARK_Mode
3is
4 type Int_Ptr is access Integer;
5 X : Int_Ptr;
6 Y : Int_Ptr;
7 Tmp : Integer;
8begin
9 X := new Integer'(1);
10 X.all := X.all + 1;
11 Y := X;
12 Y.all := Y.all + 1;
13 X.all := X.all + 1; -- illegal
14 X.all := 1; -- illegal
15 Tmp := X.all; -- illegal
16end Ownership_Transfer;
GNATprove correctly detects that X.all
can neither be read nor written
after the assignment of X
to Y
and issues corresponding messages:
ownership_transfer.adb:13:06: error: dereference from "X" is not writable
13 | X.all := X.all + 1; -- illegal
| ~~^~~
object was moved at line 11 [E0010]
11 | Y := X;
| ^ here
launch "gnatprove --explain=E0010" for more information
ownership_transfer.adb:13:15: error: dereference from "X" is not readable
13 | X.all := X.all + 1; -- illegal
| ~~^~~
object was moved at line 11 [E0010]
11 | Y := X;
| ^ here
launch "gnatprove --explain=E0010" for more information
ownership_transfer.adb:14:06: error: dereference from "X" is not writable
14 | X.all := 1; -- illegal
| ~~^~~
object was moved at line 11 [E0010]
11 | Y := X;
| ^ here
launch "gnatprove --explain=E0010" for more information
ownership_transfer.adb:15:15: error: dereference from "X" is not readable
15 | Tmp := X.all; -- illegal
| ~~^~~
object was moved at line 11 [E0010]
11 | Y := X;
| ^ here
launch "gnatprove --explain=E0010" for more information
gnatprove: error during flow analysis and proof
At call site, ownership is similarly transferred to the callee’s parameters for the duration of the call, and returned to the actual parameters (a.k.a. arguments) when returning from the call.
For example, in the following example:
1procedure Ownership_Transfer_At_Call with
2 SPARK_Mode
3is
4 type Int_Ptr is access Integer;
5 X : Int_Ptr;
6
7 procedure Proc (Y : in out Int_Ptr)
8 with Global => (In_Out => X)
9 is
10 begin
11 Y.all := Y.all + 1;
12 X.all := X.all + 1;
13 end Proc;
14
15begin
16 X := new Integer'(1);
17 X.all := X.all + 1;
18 Proc (X); -- illegal
19end Ownership_Transfer_At_Call;
GNATprove correctly detects that the call to Proc
cannot take X
in
argument as X
is already accessed as a global variable by Proc
.
possible fix: subprogram at line 7 should mention X in a precondition
7 | procedure Proc (Y : in out Int_Ptr)
| ^ here
It is also possible to transfer the ownership of an object temporarily, for
the duration of the lifetime of a local object. This can be achieved by
declaring a local object of an anonymous access type and initializing it with
a part of an existing object. In the following example, B
temporarily
borrows the ownership of X
:
1procedure Ownership_Borrowing with
2 SPARK_Mode
3is
4 type Int_Ptr is access Integer;
5 X : Int_Ptr := new Integer'(1);
6 Tmp : Integer;
7begin
8 declare
9 B : access Integer := X;
10 begin
11 B.all := B.all + 1;
12 X.all := X.all + 1; -- illegal
13 X.all := 1; -- illegal
14 Tmp := X.all; -- illegal
15 end;
16 X.all := X.all + 1;
17 X.all := 1;
18 Tmp := X.all;
19end Ownership_Borrowing;
During the lifetime of B
, it is incorrect to either read or modify X
,
but complete ownership is restored to X
when B
goes out of scope.
GNATprove correctly detects that reading or assigning to X
in the scope of
B
is incorrect.
ownership_borrowing.adb:12:09: error: object was borrowed at line 9
12 | X.all := X.all + 1; -- illegal
| ~~^~~
ownership_borrowing.adb:12:18: error: object was borrowed at line 9
12 | X.all := X.all + 1; -- illegal
| ~~^~~
ownership_borrowing.adb:13:09: error: object was borrowed at line 9
13 | X.all := 1; -- illegal
| ~~^~~
ownership_borrowing.adb:14:18: error: object was borrowed at line 9
14 | Tmp := X.all; -- illegal
| ~~^~~
gnatprove: error during flow analysis and proof
It is also possible to only transfer read access to a local variable. This happens when the variable has an anonymous access-to-constant type, as in the following example:
1procedure Ownership_Observing with
2 SPARK_Mode
3is
4 type Int_Ptr is access Integer;
5 X : Int_Ptr := new Integer'(1);
6 Tmp : Integer;
7begin
8 declare
9 B : access constant Integer := X;
10 begin
11 Tmp := B.all;
12 Tmp := X.all;
13 X.all := X.all + 1; -- illegal
14 X.all := 1; -- illegal
15 end;
16 X.all := X.all + 1;
17 X.all := 1;
18 Tmp := X.all;
19end Ownership_Observing;
In this case, we say that B
observes the value of X
. During the
lifetime of an observer, it is illegal to move or modify the observed object.
GNATprove correctly flags the write inside X
in the scope of B
as
illegal. Note that reading X
is still possible in the scope of B
:
ownership_observing.adb:13:09: error: object was observed at line 9
13 | X.all := X.all + 1; -- illegal
| ~~^~~
ownership_observing.adb:14:09: error: object was observed at line 9
14 | X.all := 1; -- illegal
| ~~^~~
gnatprove: error during flow analysis and proof
5.1.6. Absence of Interferences
In SPARK, an assignment to a variable cannot change the value of another variable. This is enforced by restricting 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 mutable parameters should never be aliased.
An immutable and a mutable parameters should not be aliased, unless the immutable parameter is always passed by copy.
A mutable parameter should never be aliased with a global variable referenced by the subprogram.
An immutable parameter should not be aliased with a global variable referenced by the subprogram, unless the immutable parameter is always passed by copy.
An immutable parameter is either an input parameter that is not of an access type, or an anonymous access-to-constant parameter. Except for parameters of access types, the immutable/mutable distinction is the same as the input/output one.
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:
1package Aliasing with
2 SPARK_Mode
3is
4 Glob : Integer;
5
6 procedure Whatever (In_1, In_2 : Integer; Out_1, Out_2 : out Integer) with
7 Global => Glob;
8
9end Aliasing;
Procedure Whatever
can only be called on arguments that satisfy the
following constraints:
Arguments for
Out_1
andOut_2
should not be aliased.Variable
Glob
should not be passed in argument forOut_1
andOut_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
:
1with Aliasing; use Aliasing;
2
3procedure Check_Param_Aliasing with
4 SPARK_Mode
5is
6 X, Y, Z : Integer := 0;
7begin
8 Whatever (In_1 => X, In_2 => X, Out_1 => X, Out_2 => X); -- illegal
9 Whatever (In_1 => X, In_2 => X, Out_1 => X, Out_2 => Y); -- correct
10 Whatever (In_1 => X, In_2 => X, Out_1 => Y, Out_2 => X); -- correct
11 Whatever (In_1 => Y, In_2 => Z, Out_1 => X, Out_2 => X); -- illegal
12end 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: error: writable actual for "Out_1" overlaps with actual for "Out_2"
8 | Whatever (In_1 => X, In_2 => X, Out_1 => X, Out_2 => X); -- illegal
| ^ here
check_param_aliasing.adb:11:45: error: writable actual for "Out_1" overlaps with actual for "Out_2"
11 | Whatever (In_1 => Y, In_2 => Z, Out_1 => X, Out_2 => X); -- illegal
| ^ here
gnatprove: error during generation of Global contracts
Here are other examples of correct and incorrect calls (according to SPARK
rules) to procedure Whatever
:
1with Aliasing; use Aliasing;
2
3procedure Check_Aliasing with
4 SPARK_Mode
5is
6 X, Y, Z : Integer := 0;
7begin
8 Whatever (In_1 => X, In_2 => X, Out_1 => X, Out_2 => Glob); -- incorrect
9 Whatever (In_1 => X, In_2 => Y, Out_1 => Z, Out_2 => Glob); -- incorrect
10 Whatever (In_1 => Glob, In_2 => Glob, Out_1 => X, Out_2 => Y); -- correct
11end Check_Aliasing;
GNATprove correctly detects the two incorrect calls and issues high check messages:
check_aliasing.adb:8:57: high: formal parameter "Out_2" and global "Glob" are aliased (SPARK RM 6.4.2)
8 | Whatever (In_1 => X, In_2 => X, Out_1 => X, Out_2 => Glob); -- incorrect
| ^~~~
check_aliasing.adb:9:57: high: formal parameter "Out_2" and global "Glob" are aliased (SPARK RM 6.4.2)
9 | Whatever (In_1 => X, In_2 => Y, Out_1 => Z, Out_2 => Glob); -- incorrect
| ^~~~
Note that SPARK currently does not detect aliasing between objects that arises due to the use of Address clauses or aspects.
5.1.7. Analysis of Generics
GNATprove does not directly analyze the code of generics. The following message is issued if you call GNATprove on a generic unit:
warning: no bodies have been analyzed by GNATprove
enable analysis of a non-generic body using SPARK_Mode
The advice given is to use SPARK_Mode
on non-generic code, for example an
instantiation of the generic unit. As SPARK_Mode
aspect cannot be attached
to a generic instantiation, it should be specified on the enclosing context,
either through a pragma or aspect.
For example, consider the following generic increment procedure:
1generic
2 type T is range <>;
3procedure Generic_Increment (X : in out T) with
4 SPARK_Mode,
5 Pre => X < T'Last,
6 Post => X = X'Old + 1;
1procedure Generic_Increment (X : in out T) with
2 SPARK_Mode
3is
4begin
5 X := X + 1;
6end Generic_Increment;
Procedure Instance_Increment
is a specific instance of
Generic_Increment
for the type Integer
:
1pragma SPARK_Mode;
2with Generic_Increment;
3
4procedure Instance_Increment is new Generic_Increment (Integer);
GNATprove analyzes this instantiation and reports messages on the generic code, always stating to which instantiation the messages correspond to:
generic_increment.ads:6:11: info: postcondition proved, in instantiation at instance_increment.ads:4
generic_increment.ads:6:21: info: overflow check proved, in instantiation at instance_increment.ads:4
generic_increment.adb:5:11: info: overflow check proved, in instantiation at instance_increment.ads:4
Thus, it is possible that some checks are proved on an instance and not on another one. In that case, the chained locations in the messages issued by GNATprove allow you to locate the problematic instantiation. In order to prove a generic library for all possible uses, you should choose extreme values for the generic parameters such that, if these instantiations are proved, any other choice of parameters will be provable as well.