7.9.1. Basic Examples
The examples in this section have no loops, and do not use more complex features of SPARK like Ghost Code, Interfaces to the Physical World, or Object Oriented Programming and Liskov Substitution Principle.
7.9.1.1. Increment
Consider a simple procedure that increments its integer parameter X
:
1procedure Increment (X : in out Integer) with
2 SPARK_Mode
3is
4begin
5 X := X + 1;
6end Increment;
As this procedure does not have a contract yet, GNATprove only checks that
there are no possible reads of uninitialized data and no possible run-time
errors in the procedure. Here, it issues a message about a possible overflow
check failure on X + 1
:
increment.adb:5:11: high: overflow check might fail, cannot prove upper bound for X + 1
5 | X := X + 1;
| ~~^~~
e.g. when X = Integer'Last
reason for check: result of addition must fit in a 32-bits machine integer
possible fix: subprogram at line 1 should mention X in a precondition
1 |procedure Increment (X : in out Integer) with
|^ here
The counterexample displayed tells us that Increment
could be called on
value Integer'Last
for parameter X
, which would cause the increment to
raise a run-time error. As suggested by the possible fix in the message
issued by GNATprove, one way to eliminate this vulnerability is to add a
precondition to Increment
specifying that X
should be less than
Integer'Last
when calling the procedure:
1procedure Increment_Guarded (X : in out Integer) with
2 SPARK_Mode,
3 Pre => X < Integer'Last
4is
5begin
6 X := X + 1;
7end Increment_Guarded;
As this procedure has a contract now, GNATprove checks like before that there
are no possible reads of uninitialized data and no possible run-time errors in
the procedure, including in its contract, and that the procedure implements its
contract. As expected, GNATprove now proves that there is no possible
overflow check failure on X + 1
:
increment_guarded.adb:6:11: info: overflow check proved
The precondition is usually the first contract added to a subprogram, but there
are other Subprogram Contracts. Here is a version of Increment
with:
global dependencies (aspect
Global
) stating that the procedure reads and writes no global variablesflow dependencies (aspect
Depends
) stating that the final value of parameterX
only depends on its input valuea precondition (aspect
Pre
) stating that parameterX
should be less thanInteger'Last
on entrya postcondition (aspect
Post
) stating that parameterX
should have been incremented by the procedure on exit
1procedure Increment_Full (X : in out Integer) with
2 SPARK_Mode,
3 Global => null,
4 Depends => (X => X),
5 Pre => X < Integer'Last,
6 Post => X = X'Old + 1
7is
8begin
9 X := X + 1;
10end Increment_Full;
GNATprove checks that Increment_Full
implements its contract, and that it
cannot raise run-time errors or read uninitialized data. By default,
GNATprove’s output is empty in such a case, but we can request that it prints
one line per check proved by using switch --report=all
, which we do here:
increment_full.adb:3:03: info: data dependencies proved
increment_full.adb:4:03: info: flow dependencies proved
increment_full.adb:6:14: info: postcondition proved
increment_full.adb:6:24: info: overflow check proved
increment_full.adb:9:11: info: overflow check proved
As subprogram contracts are used to analyze callers of a subprogram, let’s
consider a procedure Increment_Calls
that calls the different versions of
Increment
presented so far:
1with Increment;
2with Increment_Guarded;
3with Increment_Full;
4
5procedure Increment_Calls with
6 SPARK_Mode
7is
8 X : Integer;
9begin
10 X := 0;
11 Increment (X);
12 Increment (X);
13
14 X := 0;
15 Increment_Guarded (X);
16 Increment_Guarded (X);
17
18 X := 0;
19 Increment_Full (X);
20 Increment_Full (X);
21end Increment_Calls;
GNATprove proves all preconditions expect the one on the second call to
Increment_Guarded
:
increment_calls.adb:8:04: info: initialization of "X" proved
increment_calls.adb:15:04: info: precondition proved
increment_calls.adb:16:04: medium: precondition might fail
16 | Increment_Guarded (X);
| ^~~~~~~~~~~~~~~~~~~~
e.g. when X = Integer'Last
possible fix: call at line 15 should mention X (for argument X) in a postcondition
15 | Increment_Guarded (X);
| ^ here
increment_calls.adb:19:04: info: precondition proved
increment_calls.adb:20:04: info: precondition proved
Increment
has no precondition, so there is nothing to check here except the
initialization of X
when calling Increment
on lines 11 and 12. But
remember that GNATprove did issue a message about a true vulnerability on
Increment
’s implementation.
This vulnerability was corrected by adding a precondition to
Increment_Guarded
. This has the effect of pushing the constraint on
callers, here procedure Increment_Calls
. As expected, GNATprove proves
that the first call to Increment_Guarded
on line 15 satisfies its
precondition. But it does not prove the same for the second call to
Increment_Guarded
on line 16, because the value of X
on line 16 was set
by the call to Increment_Guarded
on line 15, and the contract of
Increment_Guarded
does not say anything about the possible values of X
on exit.
As suggested by the possible fix in the message issued by GNATprove,
a postcondition like the one on Increment_Full
is needed so that
GNATprove can check the second call to increment X
. As expected,
GNATprove proves that both calls to Increment_Full
on lines 19 and 20
satisfy their precondition.
In some cases, the user is not interested in specifying and verifying a
complete contract like the one on Increment_Full
, typically for helper
subprograms defined locally in a subprogram or package body. GNATprove allows
performing Contextual Analysis of Subprograms Without Contracts for these
local subprograms. For example, consider a local definition of Increment
inside procedure Increment_Local
:
1procedure Increment_Local with
2 SPARK_Mode
3is
4 procedure Increment (X : in out Integer) is
5 begin
6 X := X + 1;
7 end Increment;
8
9 X : Integer;
10
11begin
12 X := 0;
13 Increment (X);
14 Increment (X);
15 pragma Assert (X = 2);
16end Increment_Local;
Although Increment
has no contract (like the previous non-local version),
GNATprove proves that this program is free from run-time errors, and that the
assertion on line 15 holds:
increment_local.adb:6:14: info: overflow check proved, in call inlined at increment_local.adb:13
increment_local.adb:6:14: info: overflow check proved, in call inlined at increment_local.adb:14
increment_local.adb:9:04: info: initialization of "X" proved
increment_local.adb:15:19: info: assertion proved
7.9.1.2. Swap
Consider a simple procedure that swaps its integer parameters X
and Y
,
whose simple-minded implementation is wrong:
1procedure Swap_Bad (X, Y : in out Integer) with
2 SPARK_Mode
3is
4begin
5 X := Y;
6 Y := X;
7end Swap_Bad;
As this procedure does not have a contract yet, GNATprove only checks that there are no possible reads of uninitialized data and no possible run-time errors in the procedure. Here, it simply issues a warning:
swap_bad.adb:1:21: warning: unused initial value of "X"
1 |procedure Swap_Bad (X, Y : in out Integer) with
| ^ here
But we know the procedure is wrong, so we’d like to get an error of some sort!
We could not detect it with GNATprove because the error is functional, and
GNATprove cannot guess the intended functionality of
Swap_Bad
. Fortunately, we can give this information to GNATprove by
adding a contract to Swap_Bad
.
One such contract is the flow dependencies introduced by aspect
Depends
. Here it specifies that the final value of X
(resp. Y
)
should depend on the initial value of Y
(resp. X
):
1procedure Swap_Bad_Depends (X, Y : in out Integer) with
2 SPARK_Mode,
3 Depends => (X => Y, Y => X)
4is
5begin
6 X := Y;
7 Y := X;
8end Swap_Bad_Depends;
GNATprove issues 3 check messages (and a warning) on Swap_Bad_Depends
:
swap_bad_depends.adb:1:29: warning: unused initial value of "X"
1 |procedure Swap_Bad_Depends (X, Y : in out Integer) with
| ^ here
swap_bad_depends.adb:3:03: medium: missing dependency "null => X"
3 | Depends => (X => Y, Y => X)
| ^~~~~~~~~~~~~~~~~~~~~~~~~~
swap_bad_depends.adb:3:23: medium: missing self-dependency "Y => Y"
3 | Depends => (X => Y, Y => X)
| ^ here
swap_bad_depends.adb:3:28: medium: incorrect dependency "Y => X"
3 | Depends => (X => Y, Y => X)
| ^ here
The last message informs us that the dependency Y => X
stated in
Swap_Bad_Depends
’s contract is incorrect for the given implementation. That
might be either an error in the code or an error in the contract. Here this is
an error in the code. The two other messages are consequences of this error.
Another possible contract is the postcondition introduced by aspect
Post
. Here it specifies that the final value of X
(resp. Y
) is
equal to the initial value of Y
(resp. X
):
1procedure Swap_Bad_Post (X, Y : in out Integer) with
2 SPARK_Mode,
3 Post => X = Y'Old and Y = X'Old
4is
5begin
6 X := Y;
7 Y := X;
8end Swap_Bad_Post;
GNATprove issues one check message on the unproved postcondition of
Swap_Bad_Post
(and a warning), with a counterexample giving concrete values
of a wrong execution:
swap_bad_post.adb:1:26: warning: unused initial value of "X"
1 |procedure Swap_Bad_Post (X, Y : in out Integer) with
| ^ here
swap_bad_post.adb:3:25: high: postcondition might fail, cannot prove Y = X'Old
3 | Post => X = Y'Old and Y = X'Old
| ^~~~~~~~~
e.g. when X'Old = 1
and Y = 0
Both the check messages on Swap_Bad_Depends
and on Swap_Bad_Post
inform
us that the intended functionality as expressed in the contracts is not
implemented in the procedure. And looking again at the warning issued by
GNATprove on Swap_Bad
, this was already pointing at the same issue:
swapping the values of X
and Y
should obviously lead to reading the
initial value of X
; the fact that this value is not used is a clear sign
that there is an error in the implementation. The correct version of Swap
uses a temporary value to hold the value of X
:
1procedure Swap (X, Y : in out Integer) with
2 SPARK_Mode,
3 Depends => (X => Y, Y => X),
4 Post => X = Y'Old and Y = X'Old
5is
6 Tmp : constant Integer := X;
7begin
8 X := Y;
9 Y := Tmp;
10end Swap;
GNATprove proves both contracts on Swap
and it informs us that the
postcondition was proved:
swap.adb:3:03: info: flow dependencies proved
swap.adb:4:14: info: postcondition proved
Let’s now consider a well-known in place implementation of Swap
that
avoids introducing a temporary variable by using bitwise operations:
1with Interfaces; use Interfaces;
2
3procedure Swap_Modulo (X, Y : in out Unsigned_32) with
4 SPARK_Mode,
5 Post => X = Y'Old and Y = X'Old
6is
7begin
8 X := X xor Y;
9 Y := X xor Y;
10 X := X xor Y;
11end Swap_Modulo;
GNATprove understands the bitwise operations on values of modular types, and
it proves here that the postcondition of Swap_Modulo
is proved:
swap_modulo.adb:5:11: info: postcondition proved
GNATprove’s flow analysis issues warnings like the one on Swap_Bad
whenever it detects that some variables or statements are not used in the
computation, which is likely uncovering an error. For example, consider
procedure Swap_Warn
which assigns X
and Tmp_Y
out of order:
1procedure Swap_Warn (X, Y : in out Integer) with
2 SPARK_Mode
3is
4 Tmp_X : Integer;
5 Tmp_Y : Integer;
6begin
7 Tmp_X := X;
8 X := Tmp_Y;
9 Tmp_Y := Y;
10 Y := Tmp_X;
11end Swap_Warn;
On this wrong implementation, GNATprove issues a high check message for the certain read of an uninitialized variable, and three warnings that point to unused constructs:
swap_warn.adb:1:25: warning: unused initial value of "Y"
1 |procedure Swap_Warn (X, Y : in out Integer) with
| ^ here
swap_warn.adb:8:09: high: "Tmp_Y" is not initialized
8 | X := Tmp_Y;
| ^~~~~
In general, warnings issued by GNATprove’s flow analysis should be carefully reviewed, as they may lead to the discovery of errors in the program.
7.9.1.3. Addition
Consider a simple function Addition
that returns the sum of its integer
parameters X
and Y
. As in Increment, we add a suitable
precondition and postcondition for this function:
1function Addition (X, Y : Integer) return Integer with
2 SPARK_Mode,
3 Depends => (Addition'Result => (X, Y)),
4 Pre => X + Y in Integer,
5 Post => Addition'Result = X + Y
6is
7begin
8 return X + Y;
9end Addition;
We also added flow dependencies to Addition
for illustration purposes, but
they are the same as the default generated ones (the result of the function
depends on all its inputs), so are not in general given explicitly.
GNATprove issues a check message about a possible overflow in the
precondition of Addition
:
addition.adb:4:16: high: overflow check might fail, cannot prove lower bound for X + Y
4 | Pre => X + Y in Integer,
| ~~^~~
e.g. when X = Integer'First
and Y = -1
reason for check: result of addition must fit in a 32-bits machine integer
possible fix: use pragma Overflow_Mode or switch -gnato13 or unit SPARK.Big_Integers
Indeed, if we call for example Addition
on values Integer'Last
for
X
and 1
for Y
, the expression X + Y
evaluated in the
precondition does not fit in a machine integer and raises an exception at run
time. In this specific case, some people may consider that it does not really
matter that an exception is raised due to overflow as the failure of the
precondition should also raise a run-time exception. But in general the
precondition should not fail (just consider the precondition X + Y not in
Integer
for example), and even here, the different exceptions raised may be
treated differently (Constraint_Error
in the case of an overflow,
Assertion_Error
in the case of a failing precondition).
One way to avoid this vulnerability is to rewrite the precondition so that no overflow can occur:
1function Addition (X, Y : Integer) return Integer with
2 SPARK_Mode,
3 Depends => (Addition'Result => (X, Y)),
4 Pre => (X >= 0 and then Y <= Integer'Last - X) or else (X < 0 and then Y >= Integer'First - X),
5 Post => Addition'Result = X + Y
6is
7begin
8 return X + Y;
9end Addition;
Although GNATprove proves that Addition
implements its contract
and is free from run-time errors, the rewritten precondition is not so readable
anymore:
addition.adb:1:10: info: implicit aspect Always_Terminates on "Addition" has been proved, subprogram will terminate
addition.adb:3:03: info: flow dependencies proved
addition.adb:4:49: info: overflow check proved
addition.adb:4:97: info: overflow check proved
addition.adb:5:14: info: postcondition proved
addition.adb:5:34: info: overflow check proved
addition.adb:8:13: info: overflow check proved
A better way to achieve the same goal without losing in readability is to use the Big Numbers Library for arithmetic operations which could overflow:
1with SPARK.Big_Integers;
2use SPARK.Big_Integers;
3
4function Addition (X, Y : Big_Integer) return Big_Integer with
5 SPARK_Mode,
6 Depends => (Addition'Result => (X, Y)),
7 Post => Addition'Result = X + Y
8is
9begin
10 return X + Y;
11end Addition;
In that case, GNATprove proves that there are no run-time errors in function
Addition
, and that it implements its contract:
addition.adb:4:10: info: implicit aspect Always_Terminates on "Addition" has been proved, subprogram will terminate
addition.adb:6:03: info: flow dependencies proved
addition.adb:7:14: info: postcondition proved
addition.adb:7:22: info: predicate check proved
addition.adb:7:32: info: predicate check proved
addition.adb:7:36: info: predicate check proved
addition.adb:10:11: info: predicate check proved
addition.adb:10:15: info: predicate check proved
Finally, we can choose to expand the range of applicability of the function, by
accepting any values of inputs X
and Y
, and saturating when the
addition would overflow the bounds of machine integers. That’s what the
rewritten function Addition
does, and its saturating behavior is expressed
in Contract Cases:
1function Addition (X, Y : Integer) return Integer with
2 SPARK_Mode,
3 Contract_Cases => ((X + Y in Integer) => Addition'Result = X + Y,
4 X + Y < Integer'First => Addition'Result = Integer'First,
5 X + Y > Integer'Last => Addition'Result = Integer'Last)
6is
7begin
8 if X < 0 and Y < 0 then -- both negative
9 if X < Integer'First - Y then
10 return Integer'First;
11 else
12 return X + Y;
13 end if;
14
15 elsif X > 0 and Y > 0 then -- both positive
16 if X > Integer'Last - Y then
17 return Integer'Last;
18 else
19 return X + Y;
20 end if;
21
22 else -- one positive or null, one negative or null, adding them is safe
23 return X + Y;
24 end if;
25end Addition;
GNATprove proves that Addition
implements its contract and is free from
run-time errors:
addition.adb:1:10: info: implicit aspect Always_Terminates on "Addition" has been proved, subprogram will terminate
addition.adb:3:03: info: disjoint contract cases proved
addition.adb:3:03: info: complete contract cases proved
addition.adb:3:44: info: contract case proved
addition.adb:4:44: info: contract case proved
addition.adb:5:44: info: contract case proved
addition.adb:9:28: info: overflow check proved
addition.adb:12:19: info: overflow check proved
addition.adb:16:27: info: overflow check proved
addition.adb:19:19: info: overflow check proved
addition.adb:23:16: info: overflow check proved
Note that we analyzed this function in ELIMINATED overflow mode, using the
switch -gnato13
, otherwise there would be possible overflows in the guard
expressions of the contract cases.