4. Messages and Annotations

CodePeer output is comprised of messages and annotations. The types of messages and annotations produced are described below. For an overview of CodePeer’s output, refer to the How to View CodePeer Output section.

4.1. Description of Messages

CodePeer uses static analysis to track possible run-time values of all variables, parameters, and components at each point in the source code. Using this information, it identifies conditions under which an Ada run-time check might fail (null pointer, array out of bounds, etc.), an exception might be raised, a user-written assertion might fail, or a numeric calculation might overflow or wraparound.

The messages that CodePeer emits, when it detects one of the above conditions, are referred to as Check-Related Messages.

Some messages that CodePeer emits do not fall into the Check-Related category (see tables below: the check-related messages are in the categories Run-Time Checks, User Checks and Uninitialized and Invalid Variables).

The messages produced by CodePeer indicate particular lines of source code that could cause a crash, questionable behavior at run time or suspicious coding. The kind of check as well as the run-time expression that might not be satisfied (or that CodePeer is not able to prove statically) is given (such as array index check might fail: requires i in 1..10), along with a ranking corresponding to a rough indication (based on heuristics) taking into account both the severity (likelihood that this message identifies a defect that could lead to incorrect results during execution), and the certainty of the message.

The analysis performed on Check-Related categories is designed to be sound (messages reported with high rank are certain) and complete (all possible errors are reported). This means that CodePeer will consider all cases of e.g. array out of bounds or integer overflow and report them, with an associated ranking. In other words, if you do not have any messages reported for a given category of check, this means such check will not fail at run-time during the program execution, assuming CodePeer did a complete, global analysis (via e.g. -level 4) of all your sources.

These are the messages produced by CodePeer. NOTE: CWE refers to the Common Weakness Enumeration, a community-developed dictionary of common software weaknesses, hosted on the web by The MITRE Corporation (http://cwe.mitre.org/). The current version of CodePeer is based on CWE version 3.1 released on March 29, 2018. The numbers following CWE are the indices into the CWE dictionary, for weaknesses that correspond to the given CodePeer message. See CWE Categorization of Messages for a complete table of all CWE ids supported by CodePeer.

4.1.1. Run-Time Checks

These are language defined run-time checks that are searched exhaustively by CodePeer:

Message Description
array index check

Index value could be outside the array bounds (CWE 120, 124, 125-127, 129-131). This is also known as buffer overflow. For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
procedure Buffer_Overflow is
   type Int_Array is array (0 .. 2) of Integer;
   X, Y : Int_Array;
begin
   for I in X'Range loop
      X (I) := I + 1;
   end loop;

   for I in X'Range loop
      Y (X (I)) := I;  -- Bad when I = 2, since X (I) = 3
   end loop;
end Buffer_Overflow;

the buffer overflow will be flagged with:

buffer_overflow.adb:10:7: high: array index check fails here: requires (X (I)) in 0..2
divide by zero

The second operand of a divide, mod or rem operation could be zero (CWE 369). For example in the following code:

1
2
3
4
5
6
7
8
9
procedure Div is
   type Int is range 0 .. 2**32-1;
   A : Int := Int'Last;
   X : Integer;
begin
   for I in Int range 0 .. 2 loop
      X := Integer (A / I);  --  division by zero when I = 0
   end loop;
end Div;

CodePeer will detect the division by zero with:

div.adb:7:23: high: divide by zero fails here: requires I >= 1
access check

Attempting to dereference a reference that could be null (CWE 476). For example in the following code:

1
2
3
4
5
6
7
8
procedure Null_Deref is
   type Int_Access is access Integer;
   X : Int_Access;
begin
   if X = null then
      X.all := 1;  -- null dereference
   end if;
end Null_Deref;

the dereference at line 6 will generate:

null_deref.adb:6:7: high: access check fails here: requires X /= null
range check

A calculation may generate a value outside the bounds of an Ada type or subtype and generate an invalid value (CWE 682). For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
procedure Out_Of_Range is
   subtype Constrained_Integer is Integer range 1 .. 2;
   A : Integer;

   procedure Proc_1 (I : in Constrained_Integer) is
   begin
      A := I + 1;
   end Proc_1;

begin
   A := 0;
   Proc_1 (I => A);  --  A is out-of-range of parameter I
end Out_Of_Range;

the call at line 12 will generate:

out_of_range.adb:12:17: high: range check fails here: requires A in 1..2

because A is not in the range of Constrained_Integer.

overflow check

A calculation may overflow the bounds of a numeric type and wrap around. The likelihood this will affect operation of the program depends on how narrow is the range of the numeric value (CWE 190-191). For example in the following code:

 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
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;
with Ada.Text_IO; use Ada.Text_IO;

procedure Overflow is
   Attempt_Count : Integer := Integer'Last;
   --  Gets reset to zero before attempting password read
   PW            : Natural;
begin
   --  Oops forgot to reset Attempt_Count
   loop
      Put ("Enter password to delete system disk");
      Get (PW);
      if PW = 42 then
         Put_Line ("system disk deleted");
         exit;
      else
         Attempt_Count := Attempt_Count + 1;

         if Attempt_Count > 3 then
            Put_Line ("max password count reached");
            raise Program_Error;
         end if;
      end if;
   end loop;
end Overflow;

the expression Attempt_Count + 1 will overflow since Attempt_Count is initialized with the largest integer value (Integer'Last):

overflow.adb:17:41: high: overflow check fails here:
requires Attempt_Count <= Integer_32'Last-1
aliasing check

A parameter that can be passed by reference is aliased with another parameter or a global object and a subprogram call might violate the associated precondition by writing to one of the aliased objects and reading the other aliased object, possibly resulting in undesired behavior. Aliasing checks are generally expressed as a requirement that a parameter not be the same as some other parameter, or not match the address of some global object and will be flagged as a precondition check in the caller. For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
procedure Alias is
   type Int_Array is array (1 .. 10) of Integer;
   A, B : Int_Array := (others => 1);

   procedure In_Out
     (A : Int_Array;
      B : Int_Array;
      C : out Int_Array) is
   begin
      --  Read A multiple times, and write C multiple times:
      --  if A and C alias and are passed by reference, we are in trouble!
      C (1) := A (1) + B (1);
      C (1) := A (1) + B (1);
   end In_Out;

begin
   --  We pass A as both an 'in' and 'out' parameter: danger!
   In_Out (A, B, A);
end Alias;

the call to In_Out will be flagged with:

alias.adb:18:4: high: precondition (aliasing check) failure on call to alias.in_out:
requires C /= A
tag check

A tag check (incorrect tag value on a tagged object) may fail (CWE 136, 137). For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
procedure Tag is
   type T1 is tagged null record;

   package Pkg is
      type T2 is new T1 with null record;
      procedure Op (X : T2) is null;
   end Pkg;
   use Pkg;

   type T3 is new T2 with null record;

   procedure Call (X1 : T1'Class) is
   begin
      Op (T2'Class (X1));
   end Call;

   X1 : T1;
   X2 : T2;
   X3 : T3;
begin
   Call (X1); -- not OK, Call requires T2'Class
   Call (X2); -- OK
   Call (X3); -- OK
end Tag;

the first call will be flagged with:

tag.adb:21:4: high: precondition (tag check) failure on call to downward.call:
requires X1'Tag in {tag.pkg.t2, tag.t3}
discriminant check

A field for the wrong variant/discriminant is accessed (CWE 136, 137). For example in the following code:

 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
procedure Discr is

   subtype Length is Natural range 0 .. 10;
   type T (B : Boolean := True; L : Length := 1) is record
      I : Integer;
      case B is
         when True =>
            S : String (1 .. L);
            J : Integer;
         when False =>
            F : Float := 5.0;
      end case;
   end record;

   X : T (B => True, L => 3);

   function Create
     (L : Length;
      I : Integer;
      F : Float) return T is
   begin
      return (False, L, I, F);
   end Create;

begin
   X := Create (3, 2, 6.0);  -- discriminant check failure
end Discr;

the call to Create will generate the following message:

discr.adb:26:9: high: discriminant check fails here
precondition A subprogram call that might violate the subprogram’s preconditions. Checks (as listed above) associated with this precondition are listed as part of the message. In the expression associated with the message, the precondition being checked is expressed in terms of the variables of the called subprogram, rather than the calling one. In GPS, you can use the Goto body of xxx capability to view the called subprogram and its associated preconditions. A run-time check as listed above (e.g. range check) may add a precondition on a subprogram, which is then checked at all call sites and will generate a precondition message in case a failure of this precondition may occur. See Description of Annotations and Understanding the differences between preconditions and run-time errors for more information on preconditions. (Same CWE values as the associated checks). See aliasing check and tag check examples above.

4.1.2. User Checks

CodePeer will analyze checks inserted manually by the programmer either as an explicit Assert or via Ada 2012 aspects.

Message Description
assertion

A user assertion (using e.g. pragma Assert) could fail. For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
procedure Assert is

   function And_Or (A, B : Boolean) return Boolean is
   begin
      return False;
   end And_Or;

begin
   pragma Assert (And_Or (True, True));
end Assert;

CodePeer will detect that the pragma Assert will never be True:

assert.adb:9:19: high: assertion fails here
conditional check

An exception could be raised depending on the outcome of a conditional test in user code. For example in the following code:

 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
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;
with Ada.Text_IO; use Ada.Text_IO;

procedure Overflow is
   Attempt_Count : Integer := Integer'Last;
   --  Gets reset to zero before attempting password read
   PW            : Natural;
begin
   --  Oops forgot to reset Attempt_Count
   loop
      Put ("Enter password to delete system disk");
      Get (PW);
      if PW = 42 then
         Put_Line ("system disk deleted");
         exit;
      else
         Attempt_Count := Attempt_Count + 1;

         if Attempt_Count > 3 then
            Put_Line ("max password count reached");
            raise Program_Error;
         end if;
      end if;
   end loop;
end Overflow;

CodePeer will detect that Attempt_Count will always be greater than 3:

overflow.adb:21:13: high: conditional check raises exception here:
requires Attempt_Count <= 3
raise exception

An exception is being raised on a reachable path. This is similar to conditional check, but the exception is raised systematically instead of conditionally. For example:

1
2
3
4
5
 procedure Raise_Exc is
    X : Integer := raise Program_Error;
 begin
    null;
 end Raise_Exc;

will generate:

raise_exc.adb:2:19: low: raise exception unconditional raise
user precondition

A call might violate a subprogram’s specified precondition. This specification may be written as a pragma Precondition, or as a Pre aspect in Ada 2012 syntax. For example the following code:

1
2
3
4
5
6
7
8
procedure Pre is
   function "**" (Left, Right : Float) return Float
     with Import, Pre => Left /= 0.0;

   A : Float := 1.0;
begin
   A := (A - 1.0) ** 2.0;
end Pre;

will generate:

pre.adb:7:19: high: precondition (user precondition) failure on call to pre."**":
requires Left /= +0
postcondition

The subprogram’s body may violate its specified postcondition. This specification may be written as a pragma Postcondition, or as a Post aspect in Ada 2012 syntax. For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
procedure Post is

   type States is (Normal_Condition, Under_Stress, Bad_Vibration);
   State : States;

   function Stress_Is_Minimal return Boolean is (State = Normal_Condition);
   function Stress_Is_Maximal return Boolean is (State = Bad_Vibration);

   procedure Decrement with
     Pre  => not Stress_Is_Minimal,
     Post => not Stress_Is_Maximal;

   procedure Decrement is
   begin
      State := State'Val (State'Pos (State) + 1);
   end Decrement;

begin
   ...
end Post;

CodePeer detects that the postcondition of Decrement will always be violated, given the precondition:

post.adb:16:8: high: postcondition failure on call to post.decrement:
requires State <= Under_Stress

In addition, CodePeer treats the run-time check associated with an Assume pragma differently in this respect than other checks (notably, than the check associated with an Assert pragma). Pragma Assume is defined for the specific purpose of communicating assumptions to static-analysis tools (e.g., CodePeer or SPARK) that the tools can assume to be correct without any further analysis - the burden of ensuring the correctness of the assumption is on the user, not the tool, and misuse of Assume pragmas can invalidate CodePeer’s analysis.

Assert and Assume pragmas take the same arguments and have the same effect at run time (except that they are enabled/disabled by different assertion policies), but CodePeer does not generate a message if the check of an Assume pragma cannot be shown to always pass.

See Improve Your Code Specification for more details on pragma Assert and Assume.

4.1.3. Uninitialized and Invalid Variables

CodePeer attempts to detect as many cases of accessing uninitialized (or invalid, for example due to reading an external input) variables as possible, including accessing global uninitialized variables. This includes detecting cases of uninitialized components. In the case of out parameters of composite types, if there are components of an out parameter that are not initialized within the called subprogram, then detection of that will happen for references to the out parameter’s uninitialized components on the calling side. Note that no messages will be issued within the called subprogram if the formal out parameter or any of its components are not assigned (as it’s not an error in Ada to fail to assign to a composite out parameter’s components).

Message Description
validity check

The code may be reading an uninitialized or invalid value (e.g. corrupted data) (CWE 457). For example in the following code:

1
2
3
4
5
6
procedure Uninit is
   A : Integer;
   B : Integer;
begin
   A := B;  --  we are reading B which is uninitialized!
end Uninit;

CodePeer will flag the read of B:

uninit.adb:5:9: high: validity check: B is uninitialized here

4.1.4. Warning Messages

In addition to run-time checks, CodePeer will also attempt to detect many cases of logic errors, which often point to suspicious/possibly incorrect code. Unlike check-related messages, these messages do not always point to a real error if the message is correct, and are based on heuristics, so are not meant to be exhaustive.

Message Description
dead code

Also called “unreachable code.” Indicates logical errors as the programmer assumed the unreachable code could be executed (CWE 561). For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
procedure Dead_Code (X : out Integer) is
   I : Integer := 10;
begin
   if I < 4 then
      X := 0;
   elsif I >= 10 then
      X := 0;
   else
      X := 0;
   end if;
end Dead_Code;

CodePeer will flag:

dead_code.adb:5:9: medium warning: dead code because I = 10
dead_code.adb:9:9: medium warning: dead code because I = 10
test always false

Indicates redundant conditionals, which could flag logical errors where the test always evaluates to false (CWE 570). For example in the code above for dead code, CodePeer will also flag:

dead_code.adb:4:9: low warning: test always false because I = 10
test always true

Indicates redundant conditionals, which could flag logical errors where the test always evaluates to true (CWE 571). For example in the code above for dead code, CodePeer will also flag:

dead_code.adb:6:4: medium warning: test always true because I = 10
test predetermined

Indicates redundant conditionals, which could flag logical errors (CWE 570, 571). This is similar to test always true and test always false and is only emitted when there is no real polarity associated with the test such as in a case statement:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
procedure Predetermined is
   I : Integer := 0;
begin
   case I is
      when 0 =>
         ...
      when 1 =>
         ...
      when others =>
         ...
   end case;
end Predetermined;

CodePeer will flag:

predetermined.adb:4:4: low warning: test predetermined because I = 0
condition predetermined

Indicates redundant condition inside a conditional, like the left or right operand of a boolean operator which is always true or false (CWE 570, 571). For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
procedure Condition is
   type L is (A, B, C);

   procedure Or_Else (V : L) is
   begin
      if V /= A or else V /= B then
         return;
      else
         raise Program_Error;
      end if;
   end Or_Else;

CodePeer will flag:

condition.adb:6:25: medium warning: condition predetermined because
(V /= B) is always true
loop does not complete normally

Indicates loops that either run forever or fail to terminate normally (CWE 835). For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
procedure Loops is
   Buf : String := "The" & ASCII.NUL;
   BP  : Natural;
begin
   Buf (4) := 'a';   -- Eliminates null terminator
   BP := Buf'First;

   while True loop
      BP := BP + 1;
      exit when Buf (BP - 1) = ASCII.NUL;  -- Condition never reached
   end loop;
end Loops;

CodePeer will flag:

loops.adb:8:10: medium warning: loop does not complete normally
unused assignment

Indicates redundant assignment. This may be an indication of unintentional loss of result or unexpected flow of control (CWE 563). Note that CodePeer recognizes special variable patterns as temporary variables that will be ignored by this check: ignore, unused, discard, dummy, tmp, temp. This can be tuned via the MessagePatterns.xml file if needed. An object marked as unreferenced via an Unreferenced pragma is similarly ignored (see the Implementation Defined Pragmas section of the Gnat Pro Reference Manual for information about this pragma). For example in the following code:

1
2
3
4
5
procedure Unused_Assignment is
   C : Character := Get_Character;
begin
   null;  -- C is not used in this subprogram
end Unused_Assignment;

CodePeer will flag:

unused_assignment.adb:2:4: medium warning: unused assignment into C
unused assignment to global

Indicates that a subprogram call modifies a global variable, which is then overwritten following the call without any uses between the assignments. Note that the redundant assignment may occur inside another subprogram call invoked by the current subprogram (CWE 563). For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
package body Unused_Global is
   G : Integer;

   procedure Proc0 is
   begin
      G := 123;
   end Proc0;

   procedure Proc1 is
   begin
      Proc0;
   end Proc1;

   procedure Proc2 is
   begin
      Proc1;
      G := 456;  -- override effect of calling Proc1
   end Proc2;

end Unused_Global;

CodePeer will flag:

unused_global.adb:16:7: low warning: unused assignment to global G
in unused_global.proc1
unused out parameter

Indicates that an actual parameter of a call is ignored (either never used or overwritten) (CWE 563). For example in the following code:

1
2
3
4
5
6
7
8
9
with Search;

procedure Unused_Out is
   Table : Int_Array (1..10) := (others => 0);
   Found : Boolean;
   Index : Integer;
begin
   Search.Linear_Search (Table, 0, Found, Index);
end Unused_Out;

CodePeer will flag:

unused_out.adb:8:25: medium warning: unused out parameter Found
unused_out.adb:8:25: medium warning: unused out parameter Index
useless self assignment

Indicates when an assignment does not modify the value stored in the variable being assigned (CWE 563). For example in the following code:

1
2
3
4
5
6
procedure Self_Assign (A : in out Integer) is
   B : Integer;
begin
   B := A;
   A := B;
end Self_Assign;

CodePeer will flag:

self_assign.adb:5:6: medium warning: useless self assignment into A
suspicious precondition

The precondition has a form that indicates there might be a problem with the algorithm. If the allowable value set of a given input expression is not contiguous, that is, there are certain values of the expression that might cause a run-time problem inside the subprogram in between values that are safe, then this might be an indication that certain cases are not being properly handled by the code. In other situations, this might simply reflect the inherent nature of the algorithm involved. For example in the following code extracted from the CodePeer tutorial:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
package body Stack is

   procedure Push (S : in out Stack_Type; V : Value) is
   begin
      if S.Last = S.Tab'Last then
         raise Overflow;
      end if;

      S.Last := S.Last - 1;  --  Should be S.Last + 1
      S.Tab (S.Last) := V;
   end Push;

CodePeer will flag:

stack.adb:3:4: medium warning: suspicious precondition for S.Last:
not a contiguous range of values
suspicious input

Inputs mention a value reachable through an out-parameter of the suprogram before this parameter is assigned. Although the value may sometimes be initialized as the Ada standard allows, it generally uncovers a bug where the subprogram reads an uninitialized value or a value that the programmer did not mean to pass to the subprogram as an input value. For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
procedure In_Out is
   type T is record
      I : Integer;
   end record;

   procedure Take_In_Out (R : in out T) is
   begin
      R.I := R.I + 1;
   end Take_In_Out;

   procedure Take_Out (R : out T; B : Boolean) is
   begin
      Take_In_Out (R);  -- R is 'out' but used as 'in out'
   end Take_Out;

CodePeer will flag:

in_out.adb:13:7: medium warning: suspicious input R.I:
depends on input value of out-parameter
unread parameter

A parameter of an elementary type of mode in out is assigned on all paths through the subprogram before any reads, and so could be declared with mode out. For example in the following code:

1
2
3
4
procedure Unread (X : in out Integer) is
begin
   X := 0;  -- X is assigned but never read
end Unread;

CodePeer will flag:

unread.adb:1:1: medium warning: unread parameter X: could have mode out
unassigned parameter

A parameter of a scalar type of mode in out is never assigned, and so could be declared with mode in. For example in the following code:

1
2
3
4
procedure Unassigned (X : in out Integer; Y : out Integer) is
begin
   Y := X;  -- X is read but never assigned
end Unassigned;

CodePeer will flag:

unread.adb:1:1: medium warning: unassigned parameter X: could have mode in
suspicious constant operation

An operation computes a constant value from non-constant operands. This is characteristic of a typographical mistake, where a variable is used instead of another one, or a missing part in the operation, like the lack of conversion to a floating-point or fixed-point type before division. For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
procedure Constant_Op is
   type T is new Natural range 0 .. 14;

   function Incorrect (X : T) return T is
   begin
      return X / (T'Last + 1);
   end;
begin
   null;
end Constant_Op;

CodePeer will flag:

constant_op.adb:6:16: medium warning: suspicious constant operation X/15
always evaluates to 0
subp never returns

The subprogram will never return, presumably because of an infinite loop. There will typically be an additional message in the subprogram body (e.g. test always false) explaining why the subprogram never returns. For example in the following code:

1
2
3
4
5
6
7
procedure Infinite_Loop is
   X : Integer := 33;
begin
   loop
      X := X + 1;
   end loop;
end Infinite_Loop;

CodePeer will flag:

infinite_loop.adb:1:1: medium warning: subp never returns: infinite_loop
infinite_loop.adb:5:11: medium warning: loop does not complete normally
subp always fails

Indicates that a run-time problem is likely to occur on every execution of the subprogram. There will typically be an additional message in the subprogram body explaining why the subprogram always fails. For example in the following code:

1
2
3
4
5
procedure P is
   X : Integer := raise Program_Error;
begin
   null;
end P;

CodePeer will flag:

p.adb:1:1: high warning: subp always fails: p fails for all possible inputs
p.adb:3:19: low: raise exception unconditional raise

4.1.5. Race Condition Messages

CodePeer produces three sorts of race condition messages. Note that when CodePeer indicates that no lock is held, it actually means that no lock visible to multiple tasks is held. There may in fact be a local lock held.

Race condition messages are meant to be exhaustive, assuming knowledge about tasks and protected objects in the application are visible to CodePeer.

Message Description
unprotected access A reentrant task (e.g. task type) reads or writes a potentially shared object without holding a lock. The message is associated with places where the object is accessed in the absence of any lock, or with non-overlapping lock configuration (CWE 362, 366, 820).
unprotected shared access A task accesses a potentially shared object without holding a lock and this object is also referenced by some other task. The message is associated with places where the object is referenced in the absence of any lock, or with non-overlapping lock configuration (CWE 362, 366, 820).
mismatched protected access A task references a potentially shared object while holding a lock, and this object is also referenced by another task without holding the same lock. Messages are associated with the second task’s references (CWE 362, 366, 821).

For example given the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
package Race is

   procedure Increment;
   pragma Annotate (CodePeer, Multiple_Thread_Entry_Point, "Race.Increment");
   --  This is a task type: there will be multiple threads calling this subprogram

   procedure Decrement;
   pragma Annotate (CodePeer, Multiple_Thread_Entry_Point, "Race.Decrement");
   --  Ditto

end Race;
 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
package body Race is

   Counter : Natural := 0;

   procedure Acquire;
   pragma Import (C, Acquire);

   procedure Release;
   pragma Import (C, Release);

   pragma Annotate (CodePeer, Mutex, "Race.Acquire", "Race.Release");

   procedure Increment is
   begin
      Acquire;

      if Counter = Natural'Last then
         Counter := Natural'First;
      else
         Counter := Counter + 1;
      end if;

      Release;
   end Increment;

   procedure Decrement is
   begin
      if Counter = Natural'First then  --  reading Counter without any lock
         Counter := Natural'Last;      --  writing without any lock
      else
         Counter := Counter - 1;       --  reading and writing without any lock
      end if;
   end Decrement;

end Race;

CodePeer will generate the following messages:

race.adb:28:10: medium warning: mismatched protected access of shared object Counter via race.increment
race.adb:28:10: medium warning: unprotected access of Counter via race.decrement
race.adb:29:18: medium warning: mismatched protected access of shared object Counter via race.increment
race.adb:29:18: medium warning: unprotected access of Counter via race.decrement
race.adb:31:18: medium warning: mismatched protected access of shared object Counter via race.increment
race.adb:31:21: medium warning: mismatched protected access of shared object Counter via race.increment
race.adb:31:18: medium warning: unprotected access of Counter via race.decrement
race.adb:31:21: medium warning: unprotected access of Counter via race.decrement

If CodePeer indicates a race condition at a particular line in your program, it is best to refer to the Race Conditions report by clicking on the Race Conditions button in the title bar. The Race Conditions report is organized by the affected object, and gives an overall perspective on how the various task entry points are involved in creating the potential race condition on the given object. Note that CodePeer does not detect deadlocks between tasks (sometimes called deadly embraces). Rather it identifies data objects that are potentially referenced without adequate synchronization.

The following section gives more explanations on how to identify possible race conditions.

4.1.5.1. Identify Possible Race Conditions

CodePeer detects common forms of race conditions. A race condition may exist if there are two or more concurrent tasks that attempt to access the same object and at least one of them is doing an update. For example, if a Reader task makes a copy of a List Object at the same time a Writer task is modifying the List Object, the copy of the List Object may be corrupt. Languages such as Ada use synchronization or locking as a means to guard against race conditions. CodePeer identifies race conditions where synchronization is not used or is used incorrectly. (Note that the current release of CodePeer does not identify potential deadlocks, also known as deadly embraces, where two tasks are stuck waiting on locks held by the other.)

A lock is held during any protected subprogram or protected entry call. Any variable that can be accessed by more than one referencing task simultaneously must be locked at every reference to guard against race conditions. Furthermore, the referencing lock should match the lock used by other tasks to prevent updates during access. If locking is absent, or if one reference uses a different lock than some other reference, CodePeer identifies a possible race condition. Note that an identified race condition is not guaranteed to create problems on every execution, but it might cause a problem, depending on specific run time circumstances.

Note that if a lock is associated with an object that is newly created each time a subprogram is called, it does not actually provide any synchronization between distinct calls to that subprogram. A lock is only effective if it is associated with an object visible to multiple tasks. CodePeer ignores locks on objects that are not visible to multiple tasks since they have no synchronizing effect. This means CodePeer may indicate there are no locks held at the point of a reference to a potentially shared object even though there are in fact some local locks held. A future release will identify any potential problems associated with local locks more explicitly.

CodePeer must understand the tasking structure of the program being analyzed to detect race conditions. There are two types of entry points that are important to race condition analysis: Reentrant entry points and Daemon entry points. A Reentrant entry point represents code that can be invoked by multiple tasks concurrently (e.g. task types). A Daemon entry point (also called a singleton) is presumed to be invoked only by a single task at a time (e.g. task bodies).

Standard Ada tasking constructs (such as tasks and protected objects) are identified automatically by CodePeer as needed. In addition, you can manually identify reentrant entry points (aka task types) with the -reentrant “package.subp” option on the CodePeer command line. Use the -daemon “package.subp” to identify daemon entry points (aka tasks). See Command Line Invocation for the syntax for these options.

You may also identify tasks and task types for CodePeer by using the GNAT-defined pragma Annotate. This pragma has no effect on the code generated for the execution of a program: it only affects CodePeer’s race condition analysis. In this example:

package Pkg is
   procedure Single;
   pragma Annotate (CodePeer, Single_Thread_Entry_Point, "Pkg.Single");
   procedure Multiple;
   pragma Annotate (CodePeer, Multiple_Thread_Entry_Point, "Pkg.Multiple");
end Pkg;

CodePeer will assume that Pkg.Single is a single thread entry point (or “daemon”, or “task”) procedure and that Pkg.Multiple ia multiple thread entry point (or “reentrant”, or “task type”) procedure. An Annotate pragma used in this way must have exactly three operands: the identifier CodePeer, one of the identifiers Single_Thread_Entry_Point or Multiple_Thread_Entry_Point, and a string literal whose value is the fully qualified name of the procedure being identified.

To allow one pragma to apply to multiple subprograms, the final string literal may also have the same “wildcard” syntax supported by the -reentrant and -daemon command line options. In this example:

package Foo_Procs is
   procedure Foo_123;
   procedure Foo_456;
   pragma Annotate (CodePeer, Single_Thread_Entry_Point, "Foo_Procs.Foo*");
   procedure Foo_789;
end Foo_Procs;

the pragma would apply to the two procedures which precede it. If the same pragma were used as a configuration pragma in an associated configuration pragma file (described below), the pragma would apply to all three procedures.

Except when used as a configuration pragma (described below), the pragma must occur in the same immediately enclosing declarative_part or package_specification as the procedure declaration, not before the procedure’s declaration, and not after its completion. For a general description of pragma Annotate, see the GNAT Reference Manual.

Annotate pragmas may be used as configuration pragmas. In the preceding example, the same pragmas could have been present in an associated configuration pragma file (e.g., a codepeer.adc file).

You might need to specify your own entry points explicitly to include all relevant external entry points, including call backs from external subsystems and interrupt entry points.

For partitions that include one or more task entry points, an indication of zero detected race conditions ensures there is no path within that partition from one of these entry points to any of the three kinds of unsynchronized access to shared data objects identified by CodePeer.

CodePeer performs race condition analysis only at level 3 and above by default. This helps to ensure that potential race conditions are identified early. Locating race conditions with run-time testing can be difficult since they normally cause problems only intermittently or under heavy load. Note that you may use the -no-race-conditions command line parameter to suppress race condition analysis, or conversely -race-conditions to enable this analysis at level 1 or 2.

Some programs make use of user-defined mutual exclusion mechanisms instead of using language-defined protected actions. If a pair of procedures (often with names like Lock and Unlock, Acquire and Release, or P and V) are used to implement mutual exclusion, pragma Annotate may be used to communicate this information to CodePeer. This pragma has no effect on the code generated for the execution of a program; the pragma only affects CodePeer’s race condition analysis. Given this example:

package Locking is
    procedure Lock;
    procedure Unlock;
    pragma Annotate (CodePeer, Mutex, "Locking.Lock", "Locking.Unlock");
end Locking;

CodePeer will assume that a call to Lock acquires a lock and a call to Unlock releases it. If the following procedure is then called, for example, from the body of a task type:

procedure Increment_Global_Counters is
begin
    Counter_1 := Counter_1 + 1;
    Locking.Lock;
    Counter_2 := Counter_2 + 1;
    Locking.Unlock;
end Increment_Global_Counters;

CodePeer’s race condition analysis will flag only the use of Counter_1 as being potentially unsafe.

CodePeer trusts the accuracy of the pragma; no attempt is made to verify that the two procedures really do somehow implement mutual exclusion. An Annotate pragma used in this way must have exactly four operands: the identifier CodePeer, the identifier Mutex, a string literal whose value is the fully qualified name of (only) the lock-acquiring procedure, and a corresponding string literal for the lock-releasing procedure. Except when used as a configuration pragma (described below), the pragma must occur in the same immediately enclosing declarative_part or package_specification as the two procedure declarations, not before either procedure’s declaration, and not after either procedure’s completion.

The Race Condition report gives complete details about the shared objects in your program that might be subject to unsafe access. The Race Condition report is divided into three panes. The upper right pane, which runs horizontally, summarizes which subprograms CodePeer has determined are daemon-task entry points or reentrant entry points. The narrow pane which runs along the left shows the shared objects that might be involved in a race condition. The third pane, which is the large pane taking up the lower right of the report, has a table summarizing the kinds of race conditions associated with each object and provides further information below, viewed by clicking on the name of a particular object. For each shared object, there is a summary report and a detailed report. The summary report identifies which entry point is associated with each possible race condition. The detailed report goes further by identifying every reference to the object organized by task entry point, locks held (L1, L2, etc.), and whether it is a read (R) or a write (W) access. A key at the bottom indicates the actual Ada object associated with each lock.

As mentioned above, CodePeer only concerns itself with locks that are visible to multiple tasks, so an indication of None in the locks held column means no task-visible locks are held. There may be locks associated with locally created objects, but these provide no effective synchronization between distinct tasks.

4.1.6. Information Messages

These are extra information messages generated by CodePeer during analysis to complement existing warnings or check messages.

Message Description
call too complex Indicates that CodePeer skipped analyzing the subprogram call to avoid exhausting resources needed for analyzing the remainder of the system. CodePeer will report any presumptions it makes about the results/effects of the otherwise unanalyzed call. See also section Call Too Complex for more information on the possible causes of this message.
subp not available Indicates that CodePeer cannot analyze the call because the called subprogram is not available. There are two possible reasons for this: the body of the subprogram is not part of the project sources, or the called subprogram subprogram is analyzed in a different partition. CodePeer will report any presumptions it makes about the results/effects of the otherwise unanalyzed call.
subp not analyzed Indicates that Codepeer encountered a problem while analyzing this subprogram and skipped its analysis as well as its nested subprograms. These subprograms need to be reviewed manually instead.
module not analyzed Indicates that Codepeer could not analyze any of the subprograms in this module. These subprograms need to be reviewed manually instead.
module analyzed Indicates that Codepeer completed analysis of this module

4.1.7. External Messages

CodePeer can call external tools to collect their messages, display them and add them to its database.

4.1.7.1. Libadalang checkers messages

In addition to the backend messages, CodePeer reports by default messages issued by the Libadalang checkers. See Libadalang Checkers Integration for more details. The column “Checker” lists the (possibly multiple) checker(s) that report messages of the corresponding kind.

Message Checker Description
contract check invalid_contract

A user contract, either a pragma Assert or a pre/postcondition aspect in Ada 2012 syntax, could fail. For example on the following code:

1
2
3
4
5
procedure Check is
   X : Integer := 0;
begin
   pragma Assert (X > 0);
end Check;

CodePeer will flag:

check.adb:4:4: medium warning: contract check (LAL checker):
assertion failure
discriminant check invalid_discriminant

A field for the wrong variant/discriminant is accessed (CWE 136, 137). For example on the following code:

 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
function Variant return Integer is
   type RGB is (Red, Green, Blue);

   type Rec (Color : RGB := Red) is record
      case Color is
         when Red =>
            Red_Value : Integer;
         when Green =>
            Green_Value : Integer;
         when Blue =>
            Blue_Value : Integer;
      end case;
   end record;

   Value : Rec with Import;

begin
   case Value.Color is
      when Red =>
         return Value.Red_Value;
      when Green =>
         return Value.Green_Value;
      when Blue =>
         return Value.Green_Value;  --  Oops copy/paste error
   end case;
end Variant;

CodePeer will flag:

variant.adb:24:17: medium warning: discriminant check (LAL checker):
invalid field 'Green_Value'
access check null_dereference

Attempting to dereference a reference that could be null (CWE 476). For example in the following code:

1
2
3
4
5
6
7
8
9
procedure Null_Deref is
   type Int_Access is access Integer;
   X   : Int_Access;
   Var : Integer;
begin
   if X = null then
      Var := X.all;  -- null dereference
   end if;
end Null_Deref;

the dereference at line 6 will generate:

null_deref.adb:7:14: medium warning: access check (LAL checker):
null dereference of 'X'
same operands same_logic, same_operands

The two operands of a binary operation are syntactically equivalent and will always yield the same value. For example in the following code:

1
2
3
4
function Same_Op (X : Natural) return Integer is
begin
   return (X + 1) / (X + 1);  --  Copy/paste error? Always return 1
end Same_Op;

CodePeer will flag:

same_op.adb:3:11: medium warning: same operands (LAL checker):
operands of '/' are identical
code duplicated duplicate_branches

Indicates that duplicated code has been detected which might point to an unintentional copy/paste. For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
function Dup (X : Integer) return Integer is
begin
   if X > 0 then
      declare
         A : Integer := X;
         B : Integer := A + 1;
         C : Integer := B + 1;
         D : Integer := C + 1;
      begin
         return D;
      end;
   else
      declare
         A : Integer := X;
         B : Integer := A + 1;
         C : Integer := B + 1;
         D : Integer := C + 1;
      begin
         return D;  -- Suspicious duplicated code
      end;
   end if;
end Dup;

CodePeer will flag:

dup.adb:13:7: medium warning: code duplicated (LAL checker):
code duplicated with line 4
test always true test_always_true, bad_unequal

Indicates redundant conditionals, which could flag logical errors where the test always evaluates to true (CWE 571). For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
function Always (X : Integer) return Integer is
   procedure Compute with Import;
begin
   if X > 0 then
      Compute;

      if X > 0 then  --  Always True
         return 1;
      end if;
   end if;

   return 0;
end Always;

CodePeer will flag:

always.adb:7:10: medium warning: test always true (LAL checker):
'X > 0' is always true
test always false test_always_false, same_test

Indicates redundant conditionals, which could flag logical errors where the test always evaluates to false (CWE 570). For example in the following code:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
function Always (X : Integer) return Integer is
   procedure Compute with Import;
begin
   if X > 0 then
      Compute;

      if X < 0 then  --  Always false
         return 1;
      end if;
   end if;

   return 0;
end Always;

CodePeer will flag:

always.adb:7:10: medium warning: test always false (LAL checker):
'X < 0' is always false

4.1.7.2. GNAT Warnings

When called with the --gnat-warnings switch, CodePeer reports warnings issued by the GNAT front end. Their descriptions can be found in the GNAT user’s guide in the Warning Message Control section. For more details on this capability see GNAT Warnings Integration.

Message
default GNAT warnings (-gnatwn)
bad fixed value (-gnatwb)
constant conditional (-gnatwc)
implicit dereference (-gnatwd)
unreferenced formal (-gnatwf)
unrecognized pragma (-gnatwg)
hiding declarations (-gnatwh)
implementation unit (-gnatwi)
obsolescent feature (-gnatwj)
constant variable (-gnatwk)
elaboration problems (-gnatwl)
unused assignment (-gnatwm)
address clause overlay (-gnatwo)
ineffective inline (-gnatwp)
missing parenthesis (-gnatwq)
redundant construct (-gnatwr)
dead code (-gnatwt)
unused entity (-gnatwu)
unassigned variable (-gnatwv)
low bound assumption (-gnatww)
export/import mismatch (-gnatwx)
Ada compatibility (-gnatwy)
suspicious unchecked conversion (-gnatwz)
assertion failure (-gnatw.a)
biased representation (-gnatw.b)
unrepped components (-gnatw.c)
suspicious subprogram access (-gnatw.f)
record holes (-gnatw.h)
overlapping actuals (-gnatw.i)
late dispatching primitives (-gnatw.j)
standard redefinition (-gnatw.k)
suspicious modulus value (-gnatw.m)
unused out parameter assignment (-gnatw.o)
suspicious parameter order (-gnatw.p)
questionable layout (-gnatw.q)
object renaming function (-gnatw.r)
overridden size clause (-gnatw.s)
suspicious contract (-gnatw.t)
unordered enumeration (-gnatw.u)
ineffective Warnings Off (-gnatw.w)
non-local exception (-gnatw.x)
size/alignment mismatch (-gnatw.z)

4.1.7.3. GNATcheck Messages

When called with the --gnatcheck switch, CodePeer reports the messages issued by GNATcheck. The list of the message kinds and their descriptions can be found in GNATcheck reference manual in the List of Rules section, as well as by directly asking CodePeer the list of the message kinds (see Listing All Message Kinds). For more details on this capability see GNATcheck Integration.

4.1.8. Listing All Message Kinds

You can ask CodePeer to print a list of all message kinds it can generate along with a short description, by using the switch --list-categories. The format of the output is Message_Kind - Short_description, e.g:

overflow check - calculation may overflow the bounds of a numeric type (CWE 190-191)

This list contains the kinds described in this part of the user’s guide as well as all the external messages kinds.

For the libadalang checkers the message kind is followed, between parentheses, by the list of checkers that issue messages of this kind, e.g.:

same operands (same logic, same operands) - a binary operation uses the same two operands

4.2. Description of Annotations

In addition to messages, CodePeer also generates annotations on your source code. Annotations do not need to be reviewed like messages, and do not in general represent errors in the code. Instead, they express properties and assumptions of the code, and can be used to help reviewing the code manually and spot inconsistencies, and also to help understand messages generated by CodePeer.

4.2.1. Annotations

CodePeer generates the following kinds of annotations on each Ada subprogram:

pre Preconditions specify requirements that the subprogram imposes on its inputs. For example, a subprogram might require a certain parameter to be non-null for proper operation of the subprogram. These preconditions are checked at every call site. A message is given for any precondition that a caller might violate. Precondition messages include in parenthesis a list of the checks involved in the requirements.
presumption Presumptions display what CodePeer presumes about the results of an external subprogram whose code is unavailable, or are in a separate partition. There are separate presumptions for each call site, with a string in the form @<line-number-of-the-call> appended to the name of the subprogram. Presumptions are not generally used to determine preconditions of the calling routine, but they might influence postconditions of the calling routine. See below for further discussion of presumptions.
post Postconditions characterize the behavior of the subprogram in terms of its outputs and the presumptions made.
unanalyzed Unanalyzed Calls display the external calls to subprograms that the CodePeer has not analyzed, and so participate in the determination of presumptions. Note that these annotations include all directly unanalyzed calls as well as the unanalyzed calls in the call graph subtree that have an influence on the current subprograms.
global inputs Global Inputs comprise a list of all global variables referenced by each subprogram. Note that this only includes enclosing objects and not e.g. specific components. In the case of pointers, only the pointer is listed. Dereference to pointers may be implied by the pointer listed.
global outputs Global Outputs comprise a list of all global variables (objects and components) modified by each subprogram.
new obj New Objects comprise a list of heap-allocated objects, created by a subprogram, that are not reclaimed during the execution of the subprogram itself; these are new objects that are accessible after return from the subprogram.

See Use Annotations for Code Reviews for more details on how annotations can be used to aid in source code review.

4.2.2. Annotation Syntax

In the context of pre/post conditions and messages, a syntax close to Ada is used to express these conditions, including some CodePeer specific notations:

X’Initialized Means that X is expected to be initialized, but no further requirement or knowledge is imposed on its value. CodePeer issues a precondition X’Initialized whenever the value of X is read in the subprogram and it is not already mentioned in another precondition. As part of a postcondition, this means that X is known to be initialized when the subprogram exits, with no more precise information.
(soft) Means that a precondition is associated with code that might not be executed on certain paths, so violating the precondition might be safe under those circumstances. However, violating the precondition on every call would not be wise, as there are values for other inputs that could cause a violation of the precondition to lead to a run-time failure.
possibly_updated(X) Used to convey in a postcondition that X is a possible output, but there is no specific set of values that it is known to have after the subprogram completes.
possibly_init’ed(X) Used to convey in a postcondition that X is initialized on some but not all paths through the subprogram.
base...fld Refers to the fld component of any object accessible by following one or more levels of indirection starting at base, not including base.fld itself. This notation is used to handle iterative or recursive algorithms that walk recursive data structures. For example, in an algorithm that walks a linked list, a possible precondition might be (X...next)’Initialized meaning that the next component of any object reachable from X must be initialized (not including X.next itself: there will be a separate X.next’Initialized precondition if appropriate.
X in (a..b | c | d) This is the Ada 2012 set notation, and means that X is either in the range a..b, or equal to c, or equal to d.
X in (1.1 .. 5.5] Floating point ranges are expressed using this mathematical notation, where ( and ) mean that the value is excluded (not part of the range), and [ and ] mean that the value is included in the range. In other words, this is equivalent to X > 1.1 and X <= 5.2. In some cases the name IEEE_32_Float’Last is used to represent the largest (finite) value representable in the IEEE 754 single precision (i.e., 32-bit) representation. Similarly for the name IEEE_64_Float’Last and the double precision (i.e., 64-bit) representation. Finally, the names IEEE_32_Float’First and IEEE_64_Float’First may be used represent the corresponding negative values.
Global_Var@Pkg’Elab_Spec Refers to the value of a global variable at the time the specified package is elaborated. This might occur if there is a global constant in Pkg that captures the value of a global variable declared in some other packge, during elaboration of Pkg.
X’Old Refers to the value X had on entry to the subprogram, as defined in Ada 2012.
Func’Result Refers to the return value of the given function Func, as defined in Ada 2012.
new My_Type(in Subp)#N Refers to the My_Type object created by the Nth allocator within Subp. The notation new My_Type(in Subp)#N.<num objects> refers to the number of times this allocator might be invoked at run-time for each call of the subprogram. If an asterisk follows the index (e.g. new My_Type(Subp)#3*)) then the allocator arises from a nested call on Subp, which may represent a recursive call, or simply a nested call on a same-named subprogram.
Pkg’Body Refers to the package body of unit Pkg (as opposed to the spec or to the whole unit). This is used in particular to refer to variables declared in package bodies, e.g. Pkg1’Body.Global_Var1 points to the variable Global_Var1 declared in the body of package Pkg1.

4.2.3. Use Annotations for Code Reviews

Whether a formal team process or an ad-hoc, one-person activity, manually reviewing source code is a good way to identify problems early in the development cycle. Unfortunately, it can also be quite time consuming, especially when the reviewer is not the author of the code. CodePeer reduces the effort required for understanding source code by characterizing the input requirements and the net effect of each component of the code base.

Specifically, CodePeer determines preconditions and postconditions for every Ada subprogram it analyzes. It also makes presumptions about external subprograms it calls whose source code is not available, or which are so complex that they threaten to exhaust the available machine resources. CodePeer displays preconditions, presumptions, and postconditions within the GPS source editor and in its web-based source listings as an Ada comment block immediately preceding the first executable line of the subprogram. If a large number of conditions are found, the display list will be truncated and an ellipsis (...) substituted for the undisplayed messages. You may display all of the preconditions, presumptions, and postconditions in the bottom pane of the File Source view by clicking on the P/P link at the top of the comment block or on the ellipsis (...) at the bottom of a truncated comment block.

The preconditions displayed by CodePeer are implicit requirements that are imposed on the inputs to a subprogram, as determined by analyzing the algorithms used within the subprogram. Violating preconditions might cause the subprogram to fail or to give meaningless results. During code review, the reviewer can verify that the preconditions determined by CodePeer for the code as written are appropriate and meet the underlying requirements for the subprogram.

Early in a development cycle, system documentation might be missing or incomplete. Since CodePeer generates preconditions for each module without requiring the entire enclosing system to be available, it can be used before system integration to understand subprograms as they are developed. In a mature, maintained codebase the system documentation might no longer agree with current code’s behavior. In either case, CodePeer’s generated preconditions can be used to verify both the written and unwritten assumptions made by the codewriters.

Presumptions represent assumptions made by CodePeer about the results of a call on a subprogram whose code is unavailable for analysis. A separate presumption is made for each call site to the unanalyzed subprogram, with a string in the form @<line-number-of-the-call> appended to the name of the subprogram. Presumptions do not generally affect the preconditions of the calling routine, but they might influence postconditions of the calling routine.

Postconditions are characteristics of the output which a subprogram could produce, presuming its preconditions are satisfied and the presumptions made about unanalyzed calls are appropriate. Even in the absence of other documentation, postconditions can help a reviewer understand the purpose and effect of code. Likewise, postconditions can be helpful to software developers who use a subprogram. Comparing postconditions to either preconditions or the context of calling routines can provide valuable insight into the workings of the code which might not be obvious from solely a manual review.

4.3. Filtering Messages

You can provide to CodePeer a selection of message kinds and tell it to only issue and store a message if its kind is selected. This is done with the switch --be-messages=[...]. This switch expects a combination of message kinds and group of message kinds. The message kinds are the ones described in the Sections Description of Messages and Description of Annotations.

They are also listed with the --list-categories switch, see Listing All Message Kinds.

When giving a message kind to the switch you need to replace any space with an underscore. For example, to reference the conditional check category, use conditional_check, similarly for useless self assignment, use useless_self_assignment.

The group of messages are:

checks References all Run-Time Checks, User Checks and Uninitialized and Invalid Variables
warnings References all Warning Messages
race_conditions References all Race Condition Messages
info References all Information Messages
annotations References all Annotations.

Each of these arguments can be either positive (by default), or negative (by adding - in front of it). Positive arguments denote the ones that you want CodePeer to emit and store, negative ones are the ones that CodePeer should not emit.

For example, to tell CodePeer to not issue nor store any annotations, use:

--be-messages=-annotations

To tell CodePeer to only emit checks, except for precondition checks, use:

--be-messages=checks,-precondition

The polarity of the first argument determines if you start your selection from the full collection of the messages kinds or the empty one. Also note that CodePeer evaluates the arguments in the given order. Furthermore, if the arguments evaluate to an empty set of categories, CodePeer ignores the switch assuming that you made a mistake.

Note that this switch not only tells CodePeer to not issue the corresponding messages but also not store them in its database. This means in particular that you have to launch a new analysis to get the messages that were filtered out in the last analysis if you decide to change the filters.

4.4. Categorization of Messages

CodePeer makes conservative assumptions in order to avoid missing potential problems. Because of these assumptions, CodePeer might generate messages that a programmer would decide are not true problems, or that are problems that would not occur during a normal execution of the program. For example, a given numeric overflow might occur only if the program ran continuously for decades. Messages that are not true problems are called false positives.

To help deal with false positives, CodePeer categorizes messages into three levels of ranking, according to the potential severity of the problem and to the likelihood that the message corresponds to a true problem.

For example, a divide by zero error might be categorized as high. An overflow that only occurs near the limits of the maximum long integer value, however, might be categorized as medium, especially if there are intermediate exit points in the loop that would prevent the overflow. Use of a global pointer variable that is not explicitly initialized might be categorized as low because Ada provides well-defined default initial values for all pointers. These levels are determined by matching against patterns provided in a MessagePatterns.xml file.

Message Description
High High likelihood there is a defect on this line of code. It is likely to cause a problem on every execution, or the problem detected is known to be always true.
Medium Moderate likelihood there is a defect on this line of code, or a high likelihood associated with a message that may or may not be a bug. If a bug is present, it may cause a problem on some executions.
Low There is a small chance there is a defect on the given line of code or the message is potentially not very interesting. It is worth investigating only when other (high, medium) messages have been reviewed, or when trying to eliminate any possibility of incorrect execution.
Info Information about the code (e.g. subprogram not analyzed) or more details about the current message is provided via informational messages.

4.5. Understanding the differences between preconditions and run-time errors

One possibly surprising behavior of CodePeer is that potential run-time errors are not always flagged on the line that actually raises the exception. Using the following example:

Arr : array (Integer range 1 .. 10) of Integer := (others => 0);

function Get1 (X : Integer) return Integer is
begin
   return Arr (X + 10);
end Get1;

...

R := Get1 (-10);

There is a potential run-time error on the access to the array:

return Arr (X + 10);

However, CodePeer does not flag the potential problem here. Instead, it “protects” the calls to Get1 with a deduced precondition:

X in -9..0

This precondition has to be respected by callers. This is clearly not the case in the call:

R := Get1 (-10);

Which is why CodePeer flags a precondition violation here. This precondition violation is due to a potential run-time error, which is indicated in parentheses as part of the message generated by CodePeer:

bug.adb:13:12: high: precondition (array index check) failure on bug.get1: requires X in -9..0

Let’s look at a slightly (admittedly artificially) more complex example than the above:

Arr : array (Integer range 1 .. 10) of Integer := (others => 0);

function Get2 (X : Integer) return Integer is
   Index : Integer := 10;
begin
   for J in 1 .. X loop
      Index := Index + 1;
   end loop;

   return Arr (Index);
end Get1;

...

R := Get1 (-10);

Although the nature of the checks is very similar (array checks), the additional complexity of the code added by the loop leads CodePeer to report the potential errors on the array access, as opposed to the precondition. Therefore, in this case the message is reported directly on the line that may raise the exception, and not on the caller.

In summary, when looking for potential run-time errors it’s important to keep in mind that CodePeer may flag problems either on the actual line where the error may occur or in callers that may lead to the error. This is only the case for potential run-time errors: warnings on the other hand (e.g. dead code, unused assignments) are always flagged directly on the incriminated line.

Note that you can change this behavior (at the expense of additional false alarms) by enabling the -no-preconditions switch which will disable the generation and propagation of preconditions and will generate messages instead at the point of the potential failure.

4.6. Support for CWE

4.6.1. CWE Categorization of Messages

CodePeer has been designated as CWE-Compatible by the MITRE Corporation’s Common Weakness Enumeration (CWE) Compatibility and Effectiveness Program (cwe.mitre.org).

CodePeer will detect the following CWE weaknesses:

CWE weakness Description CodePeer Message
CWE 120, 124, 125, 126, 127, 129, 130, 131 Buffer overflow/underflow array index check
CWE 136, 137 Variant record field violation, Use of incorrect type in inheritance hierarchy discriminant check, tag check
CWE 190, 191 Numeric overflow/underflow overflow check
CWE 362, 366 Race condition unprotected access, unprotected shared access
CWE 369 Division by zero divide by zero
CWE 457 Use of uninitialized variable validity check
CWE 476 Null pointer dereference access check
CWE 561 Dead (unreachable) code dead code
CWE 563 Unused or redundant assignment unused assignment, unused out parameter, useless self assignment
CWE 570 Expression is always false test always false
CWE 571 Expression is always true test always true
CWE 682 Range constraint violation range check
CWE 820 Missing synchronization unprotected access, unprotected shared access
CWE 821 Incorrect synchronization mismatched protected access
CWE 835 Infinite loop loop does not complete normally

See Description of Messages for more details on the meaning of each CodePeer message.

4.6.2. Support for CWE/SANS Top 25 Most Dangerous Software Errors

CodePeer supports the following from CWE/SANS Top 25 most dangerous software errors:

Rank ID CodePeer Message
3 CWE 120 array index check
16 CWE 829 detected by the use of pragma Import and pragma Interface in Ada
18 CWE 676 see CWE-676 Use of Potentially Dangerous Function
20 CWE 131 array index check
24 CWE 190 overflow check

The other errors are typically not applicable to Ada software due to either the nature of the Ada language or the domains in which Ada applications are written.

4.6.2.1. CWE-676 Use of Potentially Dangerous Function

By design, most functions in Ada are safe to use. A notable exception are the predefined Ada functions Ada.Unchecked_Conversion and Ada.Unchecked_Deallocation.

CodePeer can check for the usage of these functions via the use of the following configuration pragmas:

pragma Restrictions (No_Unchecked_Conversion, No_Unchecked_Deallocation);

that you can put in a codepeer.adc file and reference this file in your project file via the Global_Configuration_Pragmas project attribute, as described in Configuration of System Package (system.ads).