7. CodePeer by Example

CodePeer is very different from most static analyzers, which execute symbolically the program until a safe approximation is reached. Instead, CodePeer works bottom-up from callees to callers, generating a contract for each subprogram along the way. Contracts are the basis for generating error messages related to possible run-time errors and logic errors, and they can be inspected during code reviews to detect further errors. Thus, it is essential to understand how CodePeer generates contracts, and how it uses contracts to detect errors. This section aims at providing a deeper insight into how CodePeer static analyzer engine works, through a step-by-step exploration of simple code examples. The code for these examples is available in the distribution of CodePeer, under <codepeer install>/share/examples/codepeer/codepeer_by_example, and in GPS and GNATbench through menu Help ‣ CodePeer ‣ Examples ‣ Codepeer by Example.

7.1. Basic Examples

This section presents the results of running CodePeer on simple subprograms composed of assignments, branchings and calls.

7.1.1. Scalar Assignment

Assign

CodePeer is able to follow very precisely the assignments to scalar variables throughout the program. Take a very simple program Assign that assigns the value Y+1 to the variable X:

1
2
3
4
procedure Assign (X : out Integer; Y : in Integer) is
begin
   X := Y + 1;
end Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
assign.adb:1: (pre)- assign:(overflow check) Y <= 2_147_483_646
assign.adb:1: (post)- assign:X = Y + 1
assign.adb:1: (post)- assign:X >= -2_147_483_647

The precondition on line 1 requires that the value of Y passed in argument to Assign be less than the maximal integer value. This is good advice indeed, because otherwise the addition on line 3 of Assign overflows.

The postcondition on line 2 indicates that the value of X after the call is equal to Y+1. The postcondition on line 3 indicates that this value is greater than the minimal integer value.

On this first example, CodePeer is able to generate the most precise contract for subprogram Assign. On more complex subprograms, CodePeer will generate a comprehensive and safe approximation.

Bad_Assign

Consider a version of Assign where X is read inside the subprogram before it is assigned a value:

1
2
3
4
procedure Bad_Assign (X : out Integer; Y : in Integer) is
begin
   X := X + 1;
end Bad_Assign;

CodePeer detects that X is not initialized when it is read on line 3, and thus it generates an error:

1
bad_assign.adb:3:9: high: validity check: X is uninitialized here

Assign_To_Pos

When constrained types are used, for example the type Positive of positive integers in Ada, then CodePeer uses this information in the contracts it generates. Take a variation of Assign where parameter X is a positive integer:

1
2
3
4
procedure Assign_To_Pos (X : out Positive; Y : in Integer) is
begin
   X := Y + 1;
end Assign_To_Pos;

On this subprogram, CodePeer generates the following contract:

1
2
3
assign_to_pos.adb:1: (pre)- assign_to_pos:(range check) Y in 0..2_147_483_646
assign_to_pos.adb:1: (post)- assign_to_pos:X = Y + 1
assign_to_pos.adb:1: (post)- assign_to_pos:X'Initialized

Note how the range of Y in the precondition on line 1 has been restricted to positive integers less than the maximal integer value. Note also that the postcondition on line 3 only indicates now that X is initialized on exit, which is the most precise information here given that the type of X already excludes all negative values. The attribute 'Initialized is not an actual Ada attribute. It is used to denote that a location has been initialized. This is different from the Ada attribute 'Valid which only denotes that a location has a valid bit representation. For example, a variable of a machine integer type is always valid, even if it is not initialized.

Bad_Assign_To_Pos

Consider a version of Assign_To_Pos where the assignment to X always results in a constraint error, whatever the precondition:

1
2
3
4
procedure Bad_Assign_To_Pos (X : out Positive; Y : in Positive) is
begin
   X := -Y + 1;
end Bad_Assign_To_Pos;

CodePeer detects that no suitable precondition can be generated for this subprogram, and it generates errors:

1
2
bad_assign_to_pos.adb:1:1: high warning: subp always fails: bad_assign_to_pos fails for all possible inputs
bad_assign_to_pos.adb:3:12: high: range check fails here

Self_Assign

As shown in the examples above, the precondition refers to values of variables before a call, while the postcondition refers to values of variables after a call. In general, though, postconditions may relate values on entry to a subprogram and values on exit to the same subprogram. Consider the code of Self_Assign which increments the value of its parameter X:

1
2
3
4
procedure Self_Assign (X : in out Integer) is
begin
   X := X + 1;
end Self_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
self_assign.adb:1: (pre)- self_assign:(overflow check) X <= 2_147_483_646
self_assign.adb:1: (post)- self_assign:X = X'Old + 1
self_assign.adb:1: (post)- self_assign:X >= -2_147_483_647

The precondition on line 1 indeed refers to the value of X before the call, and the postcondition on line 3 refers to the value of X after the call. The interesting case is the postcondition on line 2, which relates the value of X before the call, denoted X'Old, and the value of X after the call.

Bad_Self_Assign

Consider a version of Self_Assign where X is assigned its current value previously copied:

1
2
3
4
5
procedure Bad_Self_Assign (X : in out Integer) is
   Y : Integer := X - 1;
begin
   X := Y + 1;
end Bad_Self_Assign;

CodePeer detects that the assignment is useless, and it generates a warning:

1
bad_self_assign.adb:4:6: medium warning: useless self assignment into X

7.1.2. Aggregate Assignment

Assign_Rec

CodePeer is able to follow assignments to variables of composite type as precisely as assignments to scalar variables. Take for example a record type Rec aggregating an integer and a Pair, which is itself aggregating two integers:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
package Assign_Rec is
   type Pair is record
      A, B : Integer;
   end record;
   type Rec is record
      C : Integer;
      D : Pair;
   end record;
   procedure Assign (X : out Rec; Y : in Integer);
end Assign_Rec;

The subprogram Assign_Rec.Assign updates some components of its record parameter X:

1
2
3
4
5
6
7
package body Assign_Rec is
   procedure Assign (X : out Rec; Y : in Integer) is
   begin
      X.C := Y + 1;
      X.D.B := Y - 1;
   end Assign;
end Assign_Rec;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
assign_rec.adb:2: (pre)- assign_rec.assign:(overflow check) Y in -2_147_483_647..2_147_483_646
assign_rec.adb:2: (post)- assign_rec.assign:X.C = Y + 1
assign_rec.adb:2: (post)- assign_rec.assign:X.C >= -2_147_483_646
assign_rec.adb:2: (post)- assign_rec.assign:X.D.B <= 2_147_483_645
assign_rec.adb:2: (post)- assign_rec.assign:X.D.B = Y - 1

The postconditions on lines 2-5 correspond exactly to the most precise postconditions on this subprogram, which one would also get with assignments to scalar variables.

Bad_Assign_Rec

Consider a version of Assign_Rec where Y is multiplied and divided by one million, instead of being incremented and decremented by one:

1
2
3
4
5
6
with Assign_Rec; use Assign_Rec;
procedure Bad_Assign_Rec (X : out Rec; Y : in Integer) is
begin
   X.C := Y * 1_000_000;
   X.D.B := Y / 1_000_000;
end Bad_Assign_Rec;

CodePeer detects that the expression Y / 1_000_000 on line 5 always evaluates to zero, and it issues a warning:

1
bad_assign_rec.adb:5:15: medium warning: suspicious constant operation Y/1_000_000 always evaluates to 0

Indeed, since Y is multiplied by one million, its absolute value should be less than 2147, as indicated by the contract generated by CodePeer:

1
2
3
4
bad_assign_rec.adb:2: (pre)- bad_assign_rec:(overflow check) Y in -2_147..2_147
bad_assign_rec.adb:2: (post)- bad_assign_rec:X.C = Y*1_000_000
bad_assign_rec.adb:2: (post)- bad_assign_rec:X.C in -2_147_000_000..2_147_000_000
bad_assign_rec.adb:2: (post)- bad_assign_rec:X.D.B = 0

Then, dividing Y by one million always gives the value zero.

Assign_Arr

Similarly, take an array type Arr aggregating ten integers:

1
2
3
4
package Assign_Arr is
   type Arr is array (1 .. 10) of Integer;
   procedure Assign (X : out Arr; Y : in Integer);
end Assign_Arr;

The subprogram Assign_Arr.Assign updates some elements of its array parameter X:

1
2
3
4
5
6
7
package body Assign_Arr is
   procedure Assign (X : out Arr; Y : in Integer) is
   begin
      X (1) := Y + 1;
      X (4) := Y - 1;
   end Assign;
end Assign_Arr;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
assign_arr.adb:2: (pre)- assign_arr.assign:(overflow check) Y in -2_147_483_647..2_147_483_646
assign_arr.adb:2: (post)- assign_arr.assign:X(1) = Y + 1
assign_arr.adb:2: (post)- assign_arr.assign:X(1) >= -2_147_483_646
assign_arr.adb:2: (post)- assign_arr.assign:X(4) <= 2_147_483_645
assign_arr.adb:2: (post)- assign_arr.assign:X(4) = Y - 1

The postconditions on lines 2-5 correspond exactly to the most precise postconditions already shown for Assign_Rec.Assign.

Bad_Assign_Arr

Consider a version of Assign_Arr where X is assigned at indexes Y and Y + 10:

1
2
3
4
5
6
with Assign_Arr; use Assign_Arr;
procedure Bad_Assign_Arr (X : out Arr; Y : in Integer) is
begin
   X (Y) := 1;
   X (Y + 10) := -1;
end Bad_Assign_Arr;

CodePeer detects that the expression Y + 10 on line 5 is outside of the bounds of X, which ranges from 1 to 10, and it issues an error:

1
2
3
bad_assign_arr.adb:2:1: high warning: subp always fails: bad_assign_arr fails for all possible inputs
bad_assign_arr.adb:4:4: medium: array index check might fail: requires Y in 1..10
bad_assign_arr.adb:5:4: high: array index check fails here: requires Y in -9..0

Indeed, since index Y is used to access X, its value should be between 1 and 10. Then, Y + 10 is greater than the upper bound of X.

Assign_Arr_Unk

Finally, take an array type Arr aggregating an unknown number of integers:

1
2
3
4
package Assign_Arr_Unk is
   type Arr is array (Integer range <>) of Integer;
   procedure Assign (X : out Arr; Y : in Integer);
end Assign_Arr_Unk;

The subprogram Assign_Arr_Unk.Assign updates some elements of its array parameter X:

1
2
3
4
5
6
7
package body Assign_Arr_Unk is
   procedure Assign (X : out Arr; Y : in Integer) is
   begin
      X (1) := Y + 1;
      X (4) := Y - 1;
   end Assign;
end Assign_Arr_Unk;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
6
7
assign_arr_unk.adb:2: (pre)- assign_arr_unk.assign:(array index check) X'First <= 1
assign_arr_unk.adb:2: (pre)- assign_arr_unk.assign:(array index check) X'Last >= 4
assign_arr_unk.adb:2: (pre)- assign_arr_unk.assign:(overflow check) Y in -2_147_483_647..2_147_483_646
assign_arr_unk.adb:2: (post)- assign_arr_unk.assign:X(1) = Y + 1
assign_arr_unk.adb:2: (post)- assign_arr_unk.assign:X(1) >= -2_147_483_646
assign_arr_unk.adb:2: (post)- assign_arr_unk.assign:X(4) <= 2_147_483_645
assign_arr_unk.adb:2: (post)- assign_arr_unk.assign:X(4) = Y - 1

The postconditions on lines 4-7 correspond exactly to the most precise postconditions already shown.

7.1.3. Branching

Cond_Assign

A common limitation of static analyzers is that they cannot follow precisely disjunctions that occur due to branches in the program. CodePeer uses advanced techniques to overcome this difficulty and actually follow these branches. Take a simple subprogram Cond_Assign that assigns a different value to parameter X depending on the value of another parameter B:

1
2
3
4
5
6
7
8
procedure Cond_Assign (X : out Integer; Y : in Integer; B : in Boolean) is
begin
   if B then
      X := Y + 1;
   else
      X := Y - 1;
   end if;
end Cond_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
cond_assign.adb:1: (pre)- cond_assign:(overflow check) B or Y >= -2_147_483_647
cond_assign.adb:1: (pre)- cond_assign:(overflow check) not B or Y <= 2_147_483_646
cond_assign.adb:1: (post)- cond_assign:X = One-of{Y + 1, Y - 1}
cond_assign.adb:1: (post)- cond_assign:X'Initialized

The preconditions on line 1 and 2 precisely represent the conditions that input parameters should respect to avoid an integer negative overflow (on line 6 of Cond_Assign) or positive overflow (on line 4 of Cond_Assign). Note how these preconditions are expressed as disjunctions. This is because the negative or positive overflow is only possible for a fixed value of B (which differs between the negative overflow and the positive overflow).

The postcondition on line 2 indicates that the value of X on exit either comes from the assignment on line 4, or the one on line 6. This is not the most precise postcondition, as one could state that, on exit:

(B = True and X = Y + 1) or (B = False and X = Y - 1)

As seen with the Call_Assign example below, CodePeer actually generates internally this more precise postcondition, from which it outputs on line 3 a more user-friendly postcondition. The internal more precise postcondition is used for analyzing callers of Cond_Assign.

Bad_Cond_Assign

Consider a version of Cond_Assign with a modified test:

1
2
3
4
5
6
7
8
procedure Bad_Cond_Assign (X : out Integer; Y : in Integer; B : in Boolean) is
begin
   if B or not B then
      X := Y + 1;
   else
      X := Y - 1;
   end if;
end Bad_Cond_Assign;

CodePeer detects that the test on line 3 is always true and it issues a warning:

1
2
bad_cond_assign.adb:3:9: medium warning: test always true because B or not B
bad_cond_assign.adb:6:9: medium warning: dead code because B or not B

Multi_Cond_Assign

The precise analysis of branches seen on Cond_Assign is performed by CodePeer on any number of if statements, as shown on Multi_Cond_Assign:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
procedure Multi_Cond_Assign (X : out Integer; Y : in Integer; B1, B2 : in Boolean) is
begin
   if B1 then
      X := Y + 1;
   else
      if B2 then
	 X := Y - 1;
      else
	 X := Y * 2;
      end if;
   end if;
end Multi_Cond_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
multi_cond_assign.adb:1: (pre)- multi_cond_assign:(overflow check) B1 or B2 or Y*2 in -2_147_483_648..2_147_483_647
multi_cond_assign.adb:1: (pre)- multi_cond_assign:(overflow check) B1 or not B2 or Y >= -2_147_483_647
multi_cond_assign.adb:1: (pre)- multi_cond_assign:(overflow check) not B1 or Y <= 2_147_483_646
multi_cond_assign.adb:1: (post)- multi_cond_assign:X = One-of{Y + 1, Y - 1, Y*2}
multi_cond_assign.adb:1: (post)- multi_cond_assign:X'Initialized

The postcondition on line 4 is similar to the one obtained for Cond_Assign, except here it deals with two if statements. Our comment about CodePeer generating internally a contract more precise than the one displayed for Cond_Assign is also applicable here.

Bad_Multi_Cond_Assign

Consider a version of Multi_Cond_Assign with modified tests:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
procedure Bad_Multi_Cond_Assign (X : out Integer; Y : in Integer; B1, B2 : in Boolean) is
begin
   if B1 or Y < 10 then
      X := Y + 1;
   else
      if B2 and not (Y > 0) then
	 X := Y - 1;
      else
	 X := Y * 2;
      end if;
   end if;
end Bad_Multi_Cond_Assign;

CodePeer detects that the test on line 6 is always false and it issues a warning:

1
2
bad_multi_cond_assign.adb:6:13: low warning: test always false because not B2 or Y >= 1
bad_multi_cond_assign.adb:7:12: medium warning: dead code because not B2 or Y >= 1

Case_Assign

The analysis of case statements is similar to the analysis of if statements. Consider the subprogram Case_Assign.Assign which takes an operation Op in parameter, among three possibilities:

1
2
3
4
package Case_Assign is
  type Oper is (Incr, Decr, Double);
  procedure Assign (X : out Integer; Y : in Integer; Op : in Oper);
end Case_Assign;

It does the obvious assignment in each case:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
package body Case_Assign is
  procedure Assign (X : out Integer; Y : in Integer; Op : in Oper) is
  begin
     case Op is
        when Incr =>
           X := Y + 1;
        when Decr =>
           X := Y - 1;
        when Double =>
           X := Y * 2;
     end case;
  end Assign;
end Case_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
case_assign.adb:2: (pre)- case_assign.assign:(overflow check) Op /= Decr or Y >= -2_147_483_647
case_assign.adb:2: (pre)- case_assign.assign:(overflow check) Op <= Decr or Y*2 in -2_147_483_648..2_147_483_647
case_assign.adb:2: (pre)- case_assign.assign:(overflow check) Op >= Decr or Y <= 2_147_483_646
case_assign.adb:2: (post)- case_assign.assign:X = One-of{Y + 1, Y - 1, Y*2}
case_assign.adb:2: (post)- case_assign.assign:X'Initialized

The postcondition on line 2 is the same as what is obtained for if statements in Multi_Cond_Assign. The same comment about the internally more precise contract still applies.

7.1.4. Call Statement

Call_Assign

The modular treatment of calls is a cornerstone of CodePeer analysis. Before a caller of subprogram S is analyzed, the body of S is analyzed and CodePeer generates a contract for S. Then, this contract is used to completely abstract the calls to S during the analysis of its callers. Direct and mutually recursive calls require that a coarser contract is used for bootstrapping. This coarser contract is then iteratively refined. Consider the subprogram Call_Assign.Call:

1
2
3
4
package Call_Assign is
   type Choice is (Simple, Conditional, Self);
   procedure Call (X : in out Integer; C : in Choice);
end Call_Assign;

It calls one of Assign, Cond_Assign or Self_Assign seen previously, depending on the value of its parameter C:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Assign, Cond_Assign, Self_Assign;
package body Call_Assign is
   procedure Call (X : in out Integer; C : in Choice) is
   begin
      case C is
         when Simple =>
            Assign (X, 1);
         when Conditional =>
            Cond_Assign (X, 2, True);
         when Self =>
            Self_Assign (X);
      end case;
   end Call;
end Call_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
call_assign.adb:3: (pre)- call_assign.call:(overflow check) C <= Conditional or X <= 2_147_483_646
call_assign.adb:3: (post)- call_assign.call:X = One-of{2, 3, X'Old + 1}
call_assign.adb:3: (post)- call_assign.call:X >= -2_147_483_647

The precondition on line 1 only constrains the input value of X when C is equal to Self. Indeed, the generated preconditions for Assign and Cond_Assign are always satisfied by the values passed in parameters in Call_Assign, while the generated precondition for Self_Assign imposes that X is less than the maximal integer value.

The postcondition on line 2 enumerates the possible values for X on exit. The value 2 corresponds to the call to Assign. The value 3 corresponds to the call to Cond_Assign. Note here that CodePeer used the more precise internal contract for Cond_Assign instead of the one displayed, which would have lead to an additional possible value of 1 for X. The value X'Old + 1 corresponds to the call to Self_Assign.

The postcondition on line 3 is a common constraint on X on exit, whatever the procedure called.

Bad_Call_Assign

Consider a version of Call_Assign in which subprograms Assign, Cond_Assign and Self_Assign are all called in contexts that violate their generated preconditions:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Call_Assign; use Call_Assign;
with Assign, Cond_Assign, Self_Assign;
procedure Bad_Call_Assign (X : in out Integer; C : in Choice) is
begin
   case C is
      when Simple =>
	 Assign (X, Integer'Last);
      when Conditional =>
	 Cond_Assign (X, Integer'Last, True);
      when Self =>
	 X := Integer'Last;
	 Self_Assign (X);
   end case;
end Bad_Call_Assign;

CodePeer detects these violations and it issues corresponding precondition errors:

1
2
3
4
5
bad_call_assign.adb:3:1: high warning: subp always fails: bad_call_assign fails for all possible inputs
bad_call_assign.adb:3:1: medium warning: unread parameter X: could have mode out
bad_call_assign.adb:7:10: high: precondition (overflow check) failure on call to assign: requires Y <= Integer_32'Last-1
bad_call_assign.adb:9:10: high: precondition (overflow check) failure on call to cond_assign: requires not B or Y <= Integer_32'Last-1
bad_call_assign.adb:12:10: high: precondition (overflow check) failure on call to self_assign: requires X <= Integer_32'Last-1

Reverse_Call_Assign

You might be wondering whether CodePeer computed a more precise internal postcondition for the postcondition of Call_Assign displayed on line 2. This is indeed the case, as shown in the following example. Consider three subprograms for each value of the Choice enumeration:

1
2
3
4
5
package Reverse_Call_Assign is
   procedure Call_Simple (X : in out Integer);
   procedure Call_Conditional (X : in out Integer);
   procedure Call_Self (X : in out Integer);
end Reverse_Call_Assign;

Each subprogram calls Call_Assign.Call with the corresponding value for parameter C:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
with Call_Assign; use Call_Assign;
package body Reverse_Call_Assign is
   procedure Call_Simple (X : in out Integer) is
   begin
      Call (X, Simple);
   end Call_Simple;
   procedure Call_Conditional (X : in out Integer) is
   begin
      Call (X, Conditional);
   end Call_Conditional;
   procedure Call_Self (X : in out Integer) is
   begin
      Call (X, Self);
   end Call_Self;
end Reverse_Call_Assign;

On these subprograms, CodePeer generates the following contracts:

1
2
3
4
5
reverse_call_assign.adb:3: (post)- reverse_call_assign.call_simple:X = 2
reverse_call_assign.adb:7: (post)- reverse_call_assign.call_conditional:X = 3
reverse_call_assign.adb:11: (pre)- reverse_call_assign.call_self:(overflow check) X <= 2_147_483_646
reverse_call_assign.adb:11: (post)- reverse_call_assign.call_self:X = X'Old + 1
reverse_call_assign.adb:11: (post)- reverse_call_assign.call_self:X >= -2_147_483_647

The postcondition on line 1 is indeed the most precise contract on Call_Simple, as it is the same as the contract generated for Assign with the value of 1 for Y.

The postcondition on line 2 is indeed the most precise contract on Call_Conditional, as it is the same as the contract generated for Cond_Assign with the value of 2 for Y and True for B.

The precondition on line 3 and the postconditions on lines 4 and 5 are indeed the most precise contract on Call_Self, as they are the same as the contract generated for Self_Assign.

CodePeer could only generate these most precise contracts because it did not lose the relation between the input value of parameter C and the output value of parameter X in Call_Assign.Call. The internal most precise postcondition computed by CodePeer for Call_Assign.Call is really:

(C = Simple and X = 2) or (C = Conditional and X = 3) or (C = Self and X = X'Old + 1)

Top_Down

CodePeer completely works bottom-up on the call-graph, propagating information gathered from callees in their generated contracts to their callers. This strategy ensures that partial applications can be handled easily, and that the analysis is much faster than the classical top-down approach. Although CodePeer does not use knowledge of the calling context when analyzing a subprogram, in many cases it generates contracts precise enough to take this context into account.

Consider the local function Ident which is always called in a context where the content of array A is all ones:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Assign_Arr; use Assign_Arr;
procedure Top_Down (Y : out Integer) is
   A : Arr := (others => 1);
   function Ident (X : Integer) return Integer is
   begin
      if A (X) > 0 then
         return X;
      else
         return 0;
      end if;
   end Ident;
begin
   Y := A (Ident (3));
end Top_Down;

CodePeer does not use this information in the analysis of Ident, but instead generates a conditional precondition taking the value of X into account (even though this is not visible in the printable version, internally CodePeer knows that One-of{X, 0} really means X when A(X) > 0 and 0 otherwise):

1
2
3
4
top_down.adb:2: (post)- top_down:Y = 1
top_down.adb:4: (pre)- top_down.ident:(array index check) X in 1..10
top_down.adb:4: (post)- top_down.ident:top_down.ident'Result = One-of{X, 0}
top_down.adb:4: (post)- top_down.ident:top_down.ident'Result in 0..10

Thus, CodePeer can then check that the call to Ident(3) returns a non-null value since at this point it knows that X(3) > 0.

7.2. Loop Examples

This section presents the results of running CodePeer on subprograms containing loops.

7.2.1. Induction Variables

Induction

The first difficulty in analyzing loops is that it is not possible in general to completely unroll the loop, either because the number of iterations is very large, or because it is not known statically. Thus, the static analysis must analyze together all iterations beyond a certain point. This is a source of approximations, in particular for induction variables, that is, those variables assigned in the loop. However, CodePeer analyzes precisely those induction variables that are incremented or decremented at each run through the loop.

For example, take a simple subprogram incrementing a variable X 10 times:

1
2
3
4
5
6
7
procedure Induction (X : out Integer) is
begin
   X := 0;
   for J in 1 .. 10 loop
      X := X + 1;
   end loop;
end Induction;

On this subprogram, CodePeer generates the following contract:

1
induction.adb:1: (post)- induction:X = 10

CodePeer manages here to generate the most precise postcondition for the loop.

Bad_Induction

Consider a version of Induction in which X is not initialized before the loop:

1
2
3
4
5
6
procedure Bad_Induction (X : out Integer) is
begin
   for J in 1 .. 10 loop
      X := X + 1;
   end loop;
end Bad_Induction;

CodePeer detects that X might be uninitialized on line 4 and it issues an error:

1
bad_induction.adb:4:12: high: validity check fails here: requires X'Initialized (iteration 1 of 10)

Multi_Induction

In many cases, CodePeer can also follow precisely the relations between induction variables in a loop, as in subprogram Multi_Induction:

1
2
3
4
5
6
7
8
9
procedure Multi_Induction (X1, X2 : out Integer; Y : in Integer) is
begin
   X1 := 0;
   X2 := 0;
   while X1 < Y loop
      X1 := X1 + 2;
      X2 := X2 + 6;
   end loop;
end Multi_Induction;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
6
multi_induction.adb:1: (pre)- multi_induction:(validity check) Y <= 715_827_882
multi_induction.adb:1: (post)- multi_induction:X1 - Y in 0..2_147_483_648
multi_induction.adb:1: (post)- multi_induction:X1 in (0 | 2 | 4 | 6 | ... | 44..715_827_882)
multi_induction.adb:1: (post)- multi_induction:X2 - Y*3 in -2_147_483_646..6_442_450_944
multi_induction.adb:1: (post)- multi_induction:X2 = X1*3
multi_induction.adb:1: (post)- multi_induction:X2 in (0 | 6 | 12 | 18 | ... | 132..2_147_483_646)

Note how the postcondition on line 5 correctly indicates the relation between X1 and X2 after the loop.

Bad_Multi_Induction

Consider a version of Multi_Induction in which X1 is not assigned in the loop:

1
2
3
4
5
6
7
8
procedure Bad_Multi_Induction (X1, X2 : out Integer; Y : in Positive) is
begin
   X1 := 0;
   X2 := 0;
   while X1 < Y loop
      X2 := X2 + 6;
   end loop;
end Bad_Multi_Induction;

CodePeer detects that the loop never terminates, because the exit test on line 5 is always true:

1
2
3
4
bad_multi_induction.adb:1:1: high warning: subp never returns: bad_multi_induction
bad_multi_induction.adb:5:13: medium warning: loop does not complete normally
bad_multi_induction.adb:5:13: medium warning: test always true because X1 < Y
bad_multi_induction.adb:8:5: medium warning: dead code because X1 < Y

7.2.2. Array Scanning

The most frequent use of loops is to iterate over a collection, for example an array. Use of arrays introduces a new difficulty, namely that the static analysis must handle a large or unbounded number of memory locations. This requires performing some abstractions, to compute a safe approximation.

Search

Take a simple function Search scanning an array for a value. We are reusing here the type Assign_Arr.Arr from example Assign_Arr of arrays of ten integers.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
with Assign_Arr; use Assign_Arr;
function Search (X : in Arr; Y : in Integer) return Integer is
begin
   for J in X'Range loop
      if X (J) = Y then
         return J;
      end if;
   end loop;
   return 0;
end Search;

On this subprogram, CodePeer generates the following contract:

1
2
search.adb:2: (pre)- search:(validity check) (soft) X(1..10)'Initialized
search.adb:2: (post)- search:search'Result in 0..10

The precondition on line 1 is a safe approximation. Indeed, it requires that the array X is completely initialized upon entry to Search (the notation X(J..K) designates all elements of array X between J and K). In fact, it is sufficient that the array X is initialized up to the element whose value is Y. CodePeer detects that this precondition might be too strong, and it marks it as (soft) to notify the user.

Note that the postcondition on line 2 is also a safe approximation on Search. The most precise postcondition would have to state that either the array X does not contain Y, in which case Search returns 0, or the array X contains Y, in which case Search returns the smallest corresponding index.

Bad_Search

Consider a version of Search in which the final return statement is missing:

1
2
3
4
5
6
7
8
9
with Assign_Arr; use Assign_Arr;
function Bad_Search (X : in Arr; Y : in Integer) return Integer is
begin
   for J in X'Range loop
      if X (J) = Y then
         return J;
      end if;
   end loop;
end Bad_Search;

CodePeer generates an error if the loop is exited, because then the function raises Program_Error (as mandated by Ada standard) instead of returning a value to the caller:

1
bad_search.adb:4:4: low: conditional check might raise exception: checking that J < (10)

Call_Search

CodePeer also computes the set of inputs and outputs of Search, whether these are reachable from parameters or global variables. These inputs and outputs form a part of the generated contract not shown here. Now consider a caller of Search, that calls it twice on the same inputs:

1
2
3
4
5
6
7
with Assign_Arr; use Assign_Arr;
with Search;
procedure Call_Search (X : in Arr; Y : in Integer; U, V : out Integer) is
begin
   U := Search (X, Y);
   V := Search (X, Y);
end Call_Search;

On this subprogram, CodePeer generates the following contract:

1
2
3
call_search.adb:3: (pre)- call_search:(validity check) (soft) X(1..10)'Initialized
call_search.adb:3: (post)- call_search:U in 0..10
call_search.adb:3: (post)- call_search:V = U

CodePeer uses the knowledge that the same inputs produce the same outputs to compute the postcondition on line 3.

Bad_Call_Search

Consider a caller of Search which does not initialize the last element of parameter X before the call:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
with Assign_Arr; use Assign_Arr;
with Search;
function Bad_Call_Search return Integer is
   X : Arr;
begin
   for J in 1 .. 9 loop
      X (J) := J;
   end loop;
   return Search (X, 10);
end Bad_Call_Search;

Since the precondition is soft, CodePeer only generates an error when option -messages max is used:

1
bad_call_search.adb:9:11: low: precondition (validity check) might fail on call to search: requires (soft) X(1..10) to be initialized

Search_Unk

Take now a slightly different function Search_Unk. It also scans an array for a value, but we are reusing here the type Assign_Arr_Unk.Arr from example Assign_Arr_Unk of unconstrained arrays, which may contain an unbounded number of integers.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
with Assign_Arr_Unk; use Assign_Arr_Unk;
function Search_Unk (X : in Arr; Y : in Integer) return Integer is
begin
   for J in X'Range loop
      if X (J) = Y then
         return J;
      end if;
   end loop;
   return 0;
end Search_Unk;

On this subprogram, CodePeer generates the following contract:

1
search_unk.adb:2: (post)- search_unk:search_unk'Result'Initialized

CodePeer implicitly assumes that all inputs are initialized on entry to the subprogram, hence it does not generate a precondition that array X is completely initialized upon entry to Search_Unk.

Search_While

The same reasoning as above applies to other forms of loops. Suppose we rewrite Search using a while loop instead of a for loop:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
with Assign_Arr; use Assign_Arr;
function Search_While (X : in Arr; Y : in Integer) return Integer is
   J : Integer := X'First;
begin
   while J <= X'Last loop
      if X (J) = Y then
         return J;
      end if;
      J := J + 1;
   end loop;
   return 0;
end Search_While;

On this subprogram, CodePeer generates the following contract:

1
search_while.adb:2: (post)- search_while:search_while'Result in 0..10

This is the same contract as the one for Search_Unk.

Search_Loop

Now, we rewrite Search using an indefinite loop instead of a for loop:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
with Assign_Arr; use Assign_Arr;
function Search_Loop (X : in Arr; Y : in Integer) return Integer is
   J : Integer := X'First;
begin
   loop
      if J > X'Last then
         return 0;
      end if;
      if X (J) = Y then
         return J;
      end if;
      J := J + 1;
   end loop;
end Search_Loop;

On this subprogram, CodePeer generates the following contract:

1
search_loop.adb:2: (post)- search_loop:search_loop'Result in 0..10

Again, this is the same contract as the one for Search_Unk.

7.2.3. Array Increments

Assign_All_Arr

Let’s consider now subprograms that iterate over arrays to increment their elements. The procedure Assign_All_Arr increments each element of its array parameter X:

1
2
3
4
5
6
7
with Assign_Arr; use Assign_Arr;
procedure Assign_All_Arr (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J) + 1;
   end loop;
end Assign_All_Arr;

On this subprogram, CodePeer generates the following contract:

 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
27
28
29
30
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(1) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(10) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(2) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(3) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(4) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(5) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(6) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(7) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(8) <= 2_147_483_646
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(9) <= 2_147_483_646
assign_all_arr.adb:2: (post)- assign_all_arr:X(1) = X(1)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(1) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(10) = X(10)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(10) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(2) = X(2)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(2) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(3) = X(3)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(3) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(4) = X(4)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(4) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(5) = X(5)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(5) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(6) = X(6)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(6) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(7) = X(7)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(7) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(8) = X(8)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(8) >= -2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(9) = X(9)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(9) >= -2_147_483_647

The preconditions on lines 1 to 10 ensure that all additions on line 5 of Assign_All_Arr will not overflow. These preconditions are really the most precise ones for subprogram Assign_All_Arr, guaranteeing that no run-time error can be raised during subprogram execution.

Bad_Assign_All_Arr

Consider a version of Assign_All_Arr in which elements are shifted to the left of the array:

1
2
3
4
5
6
7
with Assign_Arr; use Assign_Arr;
procedure Bad_Assign_All_Arr (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J + 1);
   end loop;
end Bad_Assign_All_Arr;

CodePeer generates an index error because the last iteration of the loop will access past the upper bound of X:

1
2
bad_assign_all_arr.adb:2:1: high warning: subp always fails: bad_assign_all_arr fails for all possible inputs
bad_assign_all_arr.adb:5:16: high: array index check fails here: requires 10 + 1 <= 10 (iteration 10 of 10)

Assign_All_Arr_Incr

Take now a slight variation over example Assign_All_Arr that increments each element by a different amount:

1
2
3
4
5
6
7
with Assign_Arr; use Assign_Arr;
procedure Assign_All_Arr_Incr (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J) + J;
   end loop;
end Assign_All_Arr_Incr;

On this subprogram, CodePeer generates the following contract:

 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
27
28
29
30
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(1) <= 2_147_483_646
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(10) <= 2_147_483_637
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(2) <= 2_147_483_645
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(3) <= 2_147_483_644
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(4) <= 2_147_483_643
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(5) <= 2_147_483_642
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(6) <= 2_147_483_641
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(7) <= 2_147_483_640
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(8) <= 2_147_483_639
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(9) <= 2_147_483_638
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(1) = X(1)'Old + 1
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(1) >= -2_147_483_647
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(10) = X(10)'Old + 10
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(10) >= -2_147_483_638
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(2) = X(2)'Old + 2
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(2) >= -2_147_483_646
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(3) = X(3)'Old + 3
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(3) >= -2_147_483_645
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(4) = X(4)'Old + 4
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(4) >= -2_147_483_644
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(5) = X(5)'Old + 5
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(5) >= -2_147_483_643
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(6) = X(6)'Old + 6
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(6) >= -2_147_483_642
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(7) = X(7)'Old + 7
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(7) >= -2_147_483_641
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(8) = X(8)'Old + 8
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(8) >= -2_147_483_640
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(9) = X(9)'Old + 9
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(9) >= -2_147_483_639

Again, the preconditions on lines 1 to 10 ensure that all additions on line 5 of Assign_All_Arr_Incr will not overflow. These preconditions are really the most precise ones for subprogram Assign_All_Arr_Incr, guaranteeing that no run-time error can be raised during subprogram execution.

Assign_All_Arr_Incr_Unk

Take yet another variation over the previous example that uses arrays of unbounded size:

1
2
3
4
5
6
7
with Assign_Arr_Unk; use Assign_Arr_Unk;
procedure Assign_All_Arr_Incr_Unk (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J) + J;
   end loop;
end Assign_All_Arr_Incr_Unk;

On this subprogram, CodePeer generates the following contract:

1
assign_all_arr_incr_unk.adb:2: (post)- assign_all_arr_incr_unk:possibly_updated(X(-2_147_483_648..2_147_483_647))

Here, CodePeer generates no precondition to guarantee that the addition on line 5 of Assign_All_Arr_Incr_Unk cannot overflow. However, CodePeer does not issue any error on this subprogram. This is because these errors are suppressed by default, because they are likely false alarms. To display these errors, CodePeer must be run with the -messages max option:

1
assign_all_arr_incr_unk.adb:5:22: low: overflow check might fail: requires X.all(J) + J in Integer_32'First..Integer_32'Last

Bad_Assign_All_Arr_Unk

Now take the subprogram just seen, and use an unbounded array instead:

1
2
3
4
5
6
7
with Assign_Arr_Unk; use Assign_Arr_Unk;
procedure Bad_Assign_All_Arr_Unk (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J + 1);
   end loop;
end Bad_Assign_All_Arr_Unk;

CodePeer can still detect that the last iteration accesses the array at index X'Last + 1, because it treats array bounds symbolically:

1
2
3
bad_assign_all_arr_unk.adb:5:16: high: array index check fails here: requires X'First <= J + 1 and J + 1 <= X'Last
bad_assign_all_arr_unk.adb:5:16: medium: array index check might fail: requires J + 1 <= X'Last
bad_assign_all_arr_unk.adb:5:21: low: overflow check might fail: requires J <= Integer_32'Last-1

7.2.4. Array Treatments

Let’s consider now more general array treatments, in which subprograms iterate over arrays to update their content.

Map

Take the subprogram Map which stores in array Z an incremented version of array X:

1
2
3
4
5
6
7
with Assign_Arr; use Assign_Arr;
procedure Map (X : in Arr; Y : in Integer; Z : out Arr) is
begin
   for J in X'Range loop
      Z (J) := X (J) + Y;
   end loop;
end Map;

On this subprogram, CodePeer generates the following contract:

 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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
map.adb:2: (pre)- map:(validity check) X(1)'Initialized
map.adb:2: (pre)- map:(validity check) X(10)'Initialized
map.adb:2: (pre)- map:(validity check) X(2)'Initialized
map.adb:2: (pre)- map:(validity check) X(3)'Initialized
map.adb:2: (pre)- map:(validity check) X(4)'Initialized
map.adb:2: (pre)- map:(validity check) X(5)'Initialized
map.adb:2: (pre)- map:(validity check) X(6)'Initialized
map.adb:2: (pre)- map:(validity check) X(7)'Initialized
map.adb:2: (pre)- map:(validity check) X(8)'Initialized
map.adb:2: (pre)- map:(validity check) X(9)'Initialized
map.adb:2: (pre)- map:(overflow check) Y + X(1) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(10) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(2) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(3) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(4) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(5) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(6) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(7) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(8) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(9) in -2_147_483_648..2_147_483_647
map.adb:2: (post)- map:Z(1) = Y + X(1)
map.adb:2: (post)- map:Z(1)'Initialized
map.adb:2: (post)- map:Z(10) = Y + X(10)
map.adb:2: (post)- map:Z(10)'Initialized
map.adb:2: (post)- map:Z(2) = Y + X(2)
map.adb:2: (post)- map:Z(2)'Initialized
map.adb:2: (post)- map:Z(3) = Y + X(3)
map.adb:2: (post)- map:Z(3)'Initialized
map.adb:2: (post)- map:Z(4) = Y + X(4)
map.adb:2: (post)- map:Z(4)'Initialized
map.adb:2: (post)- map:Z(5) = Y + X(5)
map.adb:2: (post)- map:Z(5)'Initialized
map.adb:2: (post)- map:Z(6) = Y + X(6)
map.adb:2: (post)- map:Z(6)'Initialized
map.adb:2: (post)- map:Z(7) = Y + X(7)
map.adb:2: (post)- map:Z(7)'Initialized
map.adb:2: (post)- map:Z(8) = Y + X(8)
map.adb:2: (post)- map:Z(8)'Initialized
map.adb:2: (post)- map:Z(9) = Y + X(9)
map.adb:2: (post)- map:Z(9)'Initialized

The overflow check preconditions are sufficient to guarantee that the addition on line 5 of Map cannot overflow, so no messages are generated.

Filter

Consider the subprogram Filter which erases all non-positive elements of array parameter X:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
with Assign_Arr; use Assign_Arr;
procedure Filter (X : in out Arr) is
   K : Integer := X'First;
begin
   for J in X'Range loop
      if X (J) > 0 then
	 X (K) := X (J);
	 K := K + 1;
      end if;
   end loop;
end Filter;

On this subprogram, CodePeer generates the following contract:

1
2
filter.adb:2: (pre)- filter:(validity check) (soft) X(1..10)'Initialized
filter.adb:2: (post)- filter:possibly_init'ed(X(1..10))

Here, the precondition on line 1 guarantees that no run-time error can be raised during subprogram execution.

Concat

Consider the program Concat which takes two arrays of unbounded size in input, and returns their concatenation in array parameter Z:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
with Assign_Arr_Unk; use Assign_Arr_Unk;
procedure Concat (X, Y : in Arr; Z : out Arr) is
   K : Integer := 1;
begin
   for J in X'Range loop
      Z (K) := X (J);
      K := K + 1;
   end loop;
   for J in Y'Range loop
      Z (K) := Y (J);
      K := K + 1;
   end loop;
end Concat;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
6
concat.adb:2: (pre)- concat:(array index check) X'Last < X'First or X'Last - X'First < Z'Last
concat.adb:2: (pre)- concat:(array index check) X'Last < X'First or Z'First <= 1
concat.adb:2: (pre)- concat:(array index check) X'Last < X'First or Z'First <= X'Last - X'First + 1
concat.adb:2: (pre)- concat:(overflow check) X'Last <= X'First + 2_147_483_645
concat.adb:2: (pre)- concat:(validity check) Y'Last <= Y'First + 2_147_483_645
concat.adb:2: (post)- concat:possibly_updated(Z(1..2_147_483_647))

The precondition on line 1 guarantees that the assignment to Z(K) on line 6 of Concat is within bounds: either X is empty (then the loop is not executed), or it should fit in Z. The precondition on line 2 guarantees that the first assignment to Z on line 6 of Concat is within bounds.

This time, CodePeer issues errors for possible index checks and overflow checks failure:

1
2
3
concat.adb:10:7: medium: array index check might fail: requires K <= Z'Last
concat.adb:10:7: medium: array index check might fail: requires Z'First <= K
concat.adb:11:14: low: overflow check might fail: requires K <= Integer_32'Last-1

Concat_Op

Of course, the behavior of Concat can be obtained by simply using the Ada concatenation operator, as in subprogram Concat_Op:

1
2
3
4
5
with Assign_Arr_Unk; use Assign_Arr_Unk;
procedure Concat_Op (X, Y : in Arr; Z : out Arr) is
begin
   Z := X & Y;
end Concat_Op;

On this subprogram, CodePeer generates the following contract:

1
2
concat_op.adb:2: (pre)- concat_op:(overflow check) X'Length + Y'Length <= 4_294_967_296
concat_op.adb:2: (post)- concat_op:possibly_updated(Z(-2_147_483_648..2_147_483_647))

The preconditions above are not sufficient to guarantee that the bounds of Z allow such an assignment, hence the error message generated by CodePeer:

1
concat_op.adb:4:11: medium: array index check might fail: requires not (Z.all'Length - ((if X'length + Y'length = 0 then Y'first else if X'length /= 0 then X'first else Y'first)..(if X'length + Y'length = 0 then Y'last else if X'length /= 0 then X'first else Y'first + X'length + Y'length - 1))'Length /= 0)

7.2.5. Limitations

Rec_Constant

Although recursion and loops are in theory equivalent, CodePeer treats them very differently. While the analysis of loops is carefully designed to recognize invariants over induction variables, the analysis of recursive functions may be less precise. Take as a contrived example a simple recursive function returning a constant value:

1
2
3
4
5
6
7
8
function Rec_Constant (X : in Integer) return Integer is
begin
   if X < 10 then
      return 3;
   else
      return Rec_Constant (5);
   end if;
end Rec_Constant;

On this subprogram, CodePeer generates the following contract:

1
rec_constant.adb:1: (post)- rec_constant:rec_constant'Result'Initialized

The most precise postcondition would state that Rec_Constant always return the value 3.

Ident_Arr

CodePeer can follow quite precisely the value of individual elements in an array, as well as the possible values for all other elements which are not individually tracked. This is not the same as being able to handle arbitrary quantified expressions over arrays, although in the cases of loop with static bounds, CodePeer will automatically unroll these loops, leading to precise messages when the loop is not too large. Take for example a subprogram Ident_Arr that initializes an array to the identity function over its indexes:

1
2
3
4
5
6
procedure Ident_Arr (X : out Arr) is
begin
   for J in X'Range loop
      X (J) := J;
   end loop;
end Ident_Arr;

Using the aspect syntax of Ada 2012, the user can even specify a postcondition for this procedure stating the property above:

1
2
3
with Assign_Arr; use Assign_Arr;
procedure Ident_Arr (X : out Arr) with
  Post => (for all J in X'Range => X (J) = J);

which is proven by CodePeer.

Sum_All_Arr

CodePeer does not treat specially some quite useful abstractions over array content, like the sum/max/min over array elements, but again, as long as the loop has static bounds and is not too large, CodePeer is able to unroll such loops and produce the most precise analysis. Consider a subprogram Sum_All_Arr which computes the sum over the elements of an array:

1
2
3
4
5
6
7
8
9
with Assign_Arr; use Assign_Arr;
function Sum_All_Arr (X : in Arr) return Integer is
   Sum : Integer := 0;
begin
   for J in X'Range loop
      Sum := Sum + X (J);
   end loop;
   return Sum;
end Sum_All_Arr;

CodePeer will generate preconditions stating that this sum cannot overflow:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(10) + X(9) + X(8) + X(7) + X(6) + X(5) + X(4) + X(3) + X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(10)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(2)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(3) + X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(3)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(4) + X(3) + X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(4)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(5) + X(4) + X(3) + X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(5)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(6) + X(5) + X(4) + X(3) + X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(6)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(7) + X(6) + X(5) + X(4) + X(3) + X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(7)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(8) + X(7) + X(6) + X(5) + X(4) + X(3) + X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(8)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(9) + X(8) + X(7) + X(6) + X(5) + X(4) + X(3) + X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(9)'Initialized
sum_all_arr.adb:2: (post)- sum_all_arr:sum_all_arr'Result = X(10) + X(9) + X(8) + X(7) + X(6) + X(5) + X(4) + X(3) + X(1) + X(2)
sum_all_arr.adb:2: (post)- sum_all_arr:sum_all_arr'Result'Initialized

7.3. Pointer Examples

This section presents the results of running CodePeer on subprograms containing pointers.

7.3.1. Dereference

CodePeer assumes that the strong typing guarantees provided by Ada are not circumvented by the improper use of unchecked conversions and unchecked deallocation. In particular, it assumes that there are no dangling pointers. Thus, it is equivalent to state that pointer X can be dereferenced and that X is not null.

Deref

Consider an access type Ptr on integers, and a function Deref.Read which takes a parameter of type Ptr:

1
2
3
4
package Deref is
   type Ptr is access all Integer;
   function Read (X : in Ptr) return Integer;
end Deref;

It simply returns the value pointed to:

1
2
3
4
5
6
package body Deref is
   function Read (X : in Ptr) return Integer is
   begin
      return X.all;
   end Read;
end Deref;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
deref.adb:2: (pre)- deref.read:(access check) X /= null
deref.adb:2: (pre)- deref.read:(validity check) X.all'Initialized
deref.adb:2: (post)- deref.read:deref.read'Result = X.all
deref.adb:2: (post)- deref.read:deref.read'Result'Initialized

This is indeed the most precise contract for subprogram Deref.Read. The preconditions on lines 1 and 2 guarantee that no run-time error can be raised and that no uninitialized value can be read. The postcondition on line 3 completely summarizes the effect of calling Deref.Read.

Bad_Deref

Consider a version of Deref in which parameter X is an in out parameter that is always reset to null:

1
2
3
4
5
6
7
8
with Deref; use Deref;
function Bad_Deref (X : in out Ptr) return Integer is
begin
   if X /= null then
      X := null;
   end if;
   return X.all;
end Bad_Deref;

CodePeer detects that X is null at the point of dereference, and it generates an error:

1
2
bad_deref.adb:2:1: high warning: subp always fails: bad_deref fails for all possible inputs
bad_deref.adb:7:13: high: access check fails here: requires X /= null

Deref_Assign

Consider now subprogram Deref_Assign which updates the value of pointer X:

1
2
3
4
5
with Deref; use Deref;
procedure Deref_Assign (X : in Ptr; Y : in Integer) is
begin
   X.all := Y;
end Deref_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
deref_assign.adb:2: (pre)- deref_assign:(access check) X /= null
deref_assign.adb:2: (post)- deref_assign:X.all = Y
deref_assign.adb:2: (post)- deref_assign:X.all'Initialized

Again, this is the most precise contract for subprogram Deref_Assign. The precondition on line 1 guarantees that no run-time error can be raised. The postcondition on line 2 completely summarizes the effect of calling Deref_Assign.

Bad_Deref_Assign

Consider a version of Deref_Assign in which some defensive code wrongly returns when parameter X is not null:

1
2
3
4
5
6
7
8
with Deref; use Deref;
procedure Bad_Deref_Assign (X : in Ptr; Y : in Integer) is
begin
   if X /= null then
      return;
   end if;
   X.all := Y;
end Bad_Deref_Assign;

CodePeer detects that X is null at the point of dereference, and it generates an error:

1
bad_deref_assign.adb:7:6: high: access check fails here: requires X /= null

Self_Deref_Assign

Finally, consider the version of Self_Assign seen previously, where X is now a pointer:

1
2
3
4
5
with Deref; use Deref;
procedure Self_Deref_Assign (X : in out Ptr) is
begin
   X.all := X.all + 1;
end Self_Deref_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
self_deref_assign.adb:2: (pre)- self_deref_assign:(access check) X /= null
self_deref_assign.adb:2: (pre)- self_deref_assign:(overflow check) X.all <= 2_147_483_646
self_deref_assign.adb:2: (post)- self_deref_assign:X.all = X.all'Old + 1
self_deref_assign.adb:2: (post)- self_deref_assign:X.all >= -2_147_483_647

The preconditions on lines 1 and 2 guarantee that that no run-time error can be raised and that no uninitialized value can be read. Note that the precondition on line 2 implicitly states that X.all is initialized, since it expresses a relation involving X.all. The lines 2-4 are exactly the same as the contract previously seen for Self_Assign, where X has been replaced by X.all.

Bad_Self_Deref_Assign

Consider a version of Self_Deref_Assign in which the increment is missing:

1
2
3
4
5
with Deref; use Deref;
procedure Bad_Self_Deref_Assign (X : in out Ptr) is
begin
   X.all := X.all;
end Bad_Self_Deref_Assign;

CodePeer detects that the assignment is useless, and it generates a warning:

1
bad_self_deref_assign.adb:4:10: medium warning: useless self assignment into X.all

7.3.2. Aliasing

Pointer_Assign

What makes pointers so tricky to handle in static analysis is the possibility of aliasing, where two pointers point to the same memory location. Consider the subprogram Pointer_Assign:

1
2
3
4
5
with Deref; use Deref;
procedure Pointer_Assign (X, Y : in Ptr) is
begin
   X.all := Y.all + 1;
end Pointer_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
pointer_assign.adb:2: (pre)- pointer_assign:(access check) X /= null
pointer_assign.adb:2: (pre)- pointer_assign:(access check) Y /= null
pointer_assign.adb:2: (pre)- pointer_assign:(overflow check) Y.all <= 2_147_483_646
pointer_assign.adb:2: (post)- pointer_assign:X.all = Y.all + 1
pointer_assign.adb:2: (post)- pointer_assign:X.all >= -2_147_483_647

Preconditions are the expected ones. The interesting postcondition in the one on line 4, which states the relationship between the input value of Y.all and the output value of X.all. Indeed, this is true whether X and Y are equal or not. (Note that on this example, CodePeer displays Y.all for the input value pointed to by Y.)

Bad_Pointer_Assign

Consider a version of Pointer_Assign in which the user added an assertion that, after the assignment, X.all and Y.all should indeed be different:

1
2
3
4
5
6
with Deref; use Deref;
procedure Bad_Pointer_Assign (X, Y : in Ptr) is
begin
   X.all := Y.all + 1;
   pragma Assert (X.all = Y.all + 1);
end Bad_Pointer_Assign;

This is not true in the case where X and Y are equal. CodePeer detects this possibility, and it generates an error:

1
2
bad_pointer_assign.adb:5:19: low: assertion might fail: requires Y.all = Y.all
bad_pointer_assign.adb:5:33: low: overflow check might fail: requires Y.all <= Integer_32'Last-1

The message indicates that the value of Y.all at subprogram entry, and the value of Y.all after the assignment, may differ. This is the case precisely when X and Y are equal.

Call_Pointer_Assign

Let’s see how CodePeer handles a caller of Pointer_Assign which aliases its parameters X and Y:

1
2
3
4
5
6
with Deref; use Deref;
with Pointer_Assign;
procedure Call_Pointer_Assign (X : in Ptr) is
begin
   Pointer_Assign (X, X);
end Call_Pointer_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
call_pointer_assign.adb:3: (pre)- call_pointer_assign:(access check) X /= null
call_pointer_assign.adb:3: (pre)- call_pointer_assign:(overflow check) X.all <= 2_147_483_646
call_pointer_assign.adb:3: (post)- call_pointer_assign:X.all = X.all'Old + 1
call_pointer_assign.adb:3: (post)- call_pointer_assign:X.all >= -2_147_483_647

The postcondition of Pointer_Assign has lead to a similar postcondition for Call_Pointer_Assign, where Y.all has correctly been replaced with X.all'Old (and not X.all).

Double_Pointer_Assign

Consider now the subprogram Double_Pointer_Assign which assigns to both X and Y pointers:

1
2
3
4
5
6
with Deref; use Deref;
procedure Double_Pointer_Assign (X, Y : in Ptr) is
begin
   X.all := 1;
   Y.all := 2;
end Double_Pointer_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
double_pointer_assign.adb:2: (pre)- double_pointer_assign:(access check) X /= null
double_pointer_assign.adb:2: (pre)- double_pointer_assign:(access check) Y /= null
double_pointer_assign.adb:2: (post)- double_pointer_assign:X.all in 1..2
double_pointer_assign.adb:2: (post)- double_pointer_assign:Y.all = 2

Note the asymmetry between postconditions 3 and 4 which deal respectively with the output values of X.all and Y.all. Since Y.all is assigned last, its output value 2 comes from this last assignment. On the contrary, the output value of X.all can come either from the explicit assignment to X.all, or from the assignment to Y.all if X and Y are equal. Therefore, the postcondition on line 3 correctly considers the two output values for X.all.

The postcondition on line 3 is not the most precise postcondition, which would state in which case the value of X.all is 1 or 2:

(X /= Y and X.all = 1) or (X = Y and X.all = 2)

As already seen in section Basic Examples in the context of branchings, CodePeer generates internally this more precise postcondition, from which it outputs on line 3 a more user-friendly postcondition. The internal more precise postcondition is used for analyzing callers of Double_Pointer_Assign.

Diff_Pointer_Assign

Consider a version of Double_Pointer_Assign in which the user added an assertion that, after the assignment, X.all and Y.all should indeed be different:

1
2
3
4
5
6
7
with Deref; use Deref;
procedure Diff_Pointer_Assign (X, Y : in Ptr) is
begin
   X.all := 1;
   Y.all := 2;
   pragma Assert (X.all /= Y.all);
end Diff_Pointer_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
diff_pointer_assign.adb:2: (pre)- diff_pointer_assign:(assertion) X /= Y
diff_pointer_assign.adb:2: (pre)- diff_pointer_assign:(access check) X /= null
diff_pointer_assign.adb:2: (pre)- diff_pointer_assign:(access check) Y /= null
diff_pointer_assign.adb:2: (post)- diff_pointer_assign:X.all = 1
diff_pointer_assign.adb:2: (post)- diff_pointer_assign:Y.all = 2

Indeed, the assertion holds only if X and Y are not equal. Thus, CodePeer generates the precondition on line 1 that X and Y should be different.

Call_Double_Pointer_Assign

Take now such a caller Call_Double_Pointer_Assign, which calls Double_Pointer_Assign on non-aliased parameters:

1
2
3
4
package Call_Double_Pointer_Assign is
   X, Y : aliased Integer;   
   procedure Call;
end Call_Double_Pointer_Assign;
1
2
3
4
5
6
7
8
with Deref; use Deref;
with Double_Pointer_Assign;
package body Call_Double_Pointer_Assign is
   procedure Call is
   begin
      Double_Pointer_Assign (X'Access, Y'Access);
   end Call;
end Call_Double_Pointer_Assign;

On this subprogram, CodePeer generates the following contract:

1
2
call_double_pointer_assign.adb:4: (post)- call_double_pointer_assign.call:X = 1
call_double_pointer_assign.adb:4: (post)- call_double_pointer_assign.call:Y = 2

As mentioned before, CodePeer could use the more precise contract for Double_Pointer_Assign, which leads here to the precise postcondition that X has value 1 after the call.

7.4. Unknown Subprograms

This section presents the results of running CodePeer on partial applications. It is very common to analyze a partial application, where some units are not yet implemented. This may happen either when analyzing a library, or when not having access to parts of an application (third-party development) or when analyzing an application early on, before all the code has been developed. CodePeer handles these cases gracefully, by assuming that calling an unknown subprogram has some effects on its calling environment. These assumptions are precisely tuned to avoid false alarms, while keeping the analysis as precise as possible.

Call_Unknown

Take the unknown subprogram Unknown:

1
procedure Unknown (X : out Integer; Y : in Integer);

It is called by subprogram Call_Unknown:

1
2
3
4
5
with Unknown;
procedure Call_Unknown (X : out Integer) is
begin
   Unknown (X, 1);
end Call_Unknown;

On this subprogram, CodePeer generates the following contract:

1
call_unknown.adb:2: (post)- call_unknown:X'Initialized

Because the parameter X of Unknown is marked as out, CodePeer assumes that it is initialized by the call to Unknown, hence the corresponding postcondition of Call_Unknown.

Call_Unknown_Pos

Now consider a slight variation of Call_Unknown in which X is a positive integer:

1
2
3
4
5
with Unknown;
procedure Call_Unknown_Pos (X : out Positive) is
begin
   Unknown (X, 1);
end Call_Unknown_Pos;

On this subprogram, CodePeer generates the following contract:

1
2
call_unknown_pos.adb:2: (presumption)- call_unknown_pos:unknown.X@4 >= 1
call_unknown_pos.adb:2: (post)- call_unknown_pos:X'Initialized

The postcondition on line 2 is similar to the one seen previously. What is new here is the presumption on line 1, which states that CodePeer assumes that Unknown returns a positive value for X, as needed to avoid a possible run-time error in calling Unknown. Note the name X@4 is used instead of X to denote the value of X on line 4, after the call to Unknown. Since this presumption is relative to the call in Call_Unknown_Pos, it is part of the contract of Call_Unknown_Pos.

Call_Unknown_Rel

Presumptions can be more complex, for example in the subprogram Call_Unknown_Rel, an assertion requires that the value of X returned by Unknown respects a linear relation with Y:

1
2
3
4
5
6
with Unknown;
procedure Call_Unknown_Rel (X : out Integer; Y : in Integer) is
begin
   Unknown (X, Y);
   pragma Assert (X < 2 * Y + 1);
end Call_Unknown_Rel;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
call_unknown_rel.adb:2: (pre)- call_unknown_rel:(overflow check) Y in -1_073_741_824..1_073_741_823
call_unknown_rel.adb:2: (presumption)- call_unknown_rel:unknown.X@4 - Y*2 in -4_294_967_294..0
call_unknown_rel.adb:2: (presumption)- call_unknown_rel:unknown.X@4 <= 2_147_483_646
call_unknown_rel.adb:2: (post)- call_unknown_rel:X - Y*2 in -4_294_967_294..0
call_unknown_rel.adb:2: (post)- call_unknown_rel:X <= 2_147_483_646

The presumption on line 2 indeed propagates the desired assertion on the expected behavior of Unknown.

Call_Unknown_Arr

CodePeer tries as much as possible to keep precise information through calls to unknown subprograms. Take the unknown subprogram Unknown_Arr which takes an array as in out parameter:

1
2
with Assign_Arr; use Assign_Arr;
procedure Unknown_Arr (X : in out Arr);

It is called in a context where the value of some array elements is known:

1
2
3
4
5
6
7
8
with Assign_Arr; use Assign_Arr;
with Unknown_Arr;
procedure Call_Unknown_Arr (X : in out Arr) is
begin
   X (1) := 1;
   X (4) := 2;
   Unknown_Arr (X);
end Call_Unknown_Arr;

On this subprogram, CodePeer generates the following contract:

1
2
call_unknown_arr.adb:3: (post)- call_unknown_arr:X(1)'Initialized
call_unknown_arr.adb:3: (post)- call_unknown_arr:X(4)'Initialized

Since the array is passed as in out, CodePeer assumes that the value of X may change, but it keeps the information that elements at indexes 1 and 4 are initialized.

Call_Unknown_Ptr

This is even more visible in the way CodePeer analyzes calls to unknown subprograms which take pointers in parameter, like Unknown_Ptr:

1
2
with Deref; use Deref;
procedure Unknown_Ptr (X : in out Ptr);

It is called twice, first in a context where the value of parameter X.all is not known, then in a context where it is known:

1
2
3
4
5
6
7
8
9
with Deref; use Deref;
with Unknown_Ptr;
procedure Call_Unknown_Ptr (X, Y : in out Ptr) is
begin
   Unknown_Ptr (X);
   Y.all := 1;
   Unknown_Ptr (Y);
   pragma Assert (X.all < Y.all);
end Call_Unknown_Ptr;

On this subprogram, CodePeer generates the following contract:

1
2
3
4
5
6
call_unknown_ptr.adb:3: (pre)- call_unknown_ptr:(access check) Y /= null
call_unknown_ptr.adb:3: (presumption)- call_unknown_ptr:unknown_ptr.X@5 /= null
call_unknown_ptr.adb:3: (presumption)- call_unknown_ptr:unknown_ptr.X@7 /= null
call_unknown_ptr.adb:3: (post)- call_unknown_ptr:X /= null
call_unknown_ptr.adb:3: (post)- call_unknown_ptr:Y /= null
call_unknown_ptr.adb:3: (post)- call_unknown_ptr:Y.all = 1

Since Y.all has a value prior to the second call to Unknown_Ptr, CodePeer assumes that the call does not modify this value. This is a heuristic choice that in most cases increases precision and avoids false alarms, compared to the alternative of always assuming that a new unknown value has been written in Y.all. Hence the postcondition on line 6 which states that Y.all is equal to 1 on exit to Call_Unknown_Ptr.

Note that the postconditions on line 7 and 8 are derived from presumptions.

Above_Call_Unknown

In general, the exact constraint expected from a call to an unknown subprogram may not be given by its direct caller, but possibly by a caller higher in the call chain. CodePeer handles these cases by generating presumptions on unknown subprograms in the contract of these indirect callers. Consider a caller of the subprogram Call_Unknown, which expects X to be different from 10 after the call:

1
2
3
4
5
6
with Call_Unknown;
procedure Above_Call_Unknown (X : out Integer) is
begin
   Call_Unknown (X);
   pragma Assert (X /= 10);
end Above_Call_Unknown;

On this subprogram, CodePeer generates the following contract:

1
2
above_call_unknown.adb:2: (presumption)- above_call_unknown:unknown.X@4 /= 10
above_call_unknown.adb:2: (post)- above_call_unknown:X /= 10

The presumption on line 1 indeed requires that the call to Unknown inside Call_Unknown returns a value different from 10. Since this presumption is relative to the call in Call_Unknown inside a call in Above_Call_Unknown, it is part of the contract of Above_Call_Unknown.