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 variables

  • flow dependencies (aspect Depends) stating that the final value of parameter X only depends on its input value

  • a precondition (aspect Pre) stating that parameter X should be less than Integer'Last on entry

  • a postcondition (aspect Post) stating that parameter X 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.