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 potentially exhaustive, which means that CodePeer can be configured to consider all cases of e.g. array out of bounds or integer overflow and report them, with an associated ranking. See Provide Evidence for Program Verification for more details.

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.2 released on January 3, 2019. 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 (CWE 628). 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 GNAT Studio, 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:20: low: raise exception unconditional raise

user precondition

A call might violate a subprogram’s specified precondition (CWE 628). 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 (CWE 682). 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 := States'Val (States'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 reassignment

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 reassignment of 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:20: 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, 667, 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, 667, 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, 667, 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. Infer messages

In addition to the backend messages, CodePeer reports messages issued by Infer (unless Infer is deactivated). See Infer Integration for more details.

First, Infer emits messages for most standard Ada checks. Those correspond to the corresponding messages emitted by by the backend, and won’t be described further: assertion, discriminant check, access check, array index check, range check, test always true, test always false.

Second, the following checkers are specific to Infer:

Message

Description

same operands, same logic

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

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

function Same_Logic (A, B : Boolean) return Boolean is
begin
   return A or else B or else A;
end Same_Logic;

CodePeer will flag:

infer.adb:3:22: medium warning: same operands (Infer): operands of '/' are identical
infer.adb:8:34: medium warning: same operands (Infer): 'A' duplicated at line 10

duplicate branches

Duplicated code has been detected, which might point to an unintentional copy/paste (CWE 1041). 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:

infer.adb:4:10: medium warning: duplicate branches (Infer): code duplicated at line 16

test duplication

A certain expression is tested multiple times as part of successive if ... elsif ... elsif ... tests.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
procedure Same_Test (Str : String) is
   A : constant String := "toto";
   B : constant String := "titi";
begin
   if Str = A then
      Ada.Text_IO.Put_Line("Hello, tata!");
   elsif Str = B then
      Ada.Text_IO.Put_Line("Hello, titi!");
   elsif Str = A then
      Ada.Text_IO.Put_Line("Hello, toto!");
   else
      Ada.Text_IO.Put_Line("Hello, world!");
   end if;
end Same_Test;

CodePeer will flag:

infer.adb:9:13: medium warning: same test (Infer): test 'Str = A' duplicated at line 42

length check

Infer uses the category length check to emit checks for array operations in which the two operands may not have the same size. The backend analysis uses the category range check for such messages.

1
2
3
4
5
6
7
8
type A is array (Integer range <>) of Natural;

   procedure Arr is
   X : A (1 .. 10) := (others => 0);
   Y : A (2 .. 12);
begin
   Y := X;
end Arr;

CodePeer will flag:

infer.adb:7:12: medium: length check (Infer): requires (Y'Length = X'Length)

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)

components without representation (-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 Remediation_Effort, e.g:

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

The remediation effort (Medium in the message above) gives an indication of the effort needed to fix a typical error of the kind corresponding to this message. This metric is used by SonarQube (through GNAThub), see SonarQube’s documentation for more details.

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

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.

Note that the global inputs and global outputs annotations are by default limited in length and may be truncated as a result. In order to generate these annotations fully, you can use the -dbg-off inout_limit switch.

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.

X’Accessibility_Level

Every entity has an associated number called its accessibility level. CodePeer tracks this number and makes reference to it using the attribute X’Accessibility_Level. This number relates to the accessibility rules of Ada. Every access type also has an underlying accessibility level. When needed, there is a check between the accessibility level of the object and the accessibility level of the access type. When the object has a greater accessibility level than the access type, a PROGRAM_ERROR is raised at run time. CodePeer tracks these levels and reports on possible exceptions using this attribute notation.

(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.2]

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 names IEEE_32_Float and IEEE_64_Float are used as the prefix of an attribute. For example, 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. The names “IEEE_32_Float’First”, “IEEE_64_Float’Last” and “IEEE_64_Float’First” are used analogously. A name such as “IEEE_32_Float’Succ(0.0)” refers to the successor (or predecessor, if Succ is replaced with Pred) of the argument value in the given IEEE representation; for example, the name “IEEE_64_Float’Pred(1.0) refers to the predecessor of 1.0 in the 64-bit IEEE representation. The Succ/Pred notation may be used in cases where this choice shortens the resulting message text.

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 GNAT Studio 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 reassignment, use useless_reassignment.

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 is very unlikely to be a false positive.

Medium

Moderate likelihood there is a bug on this line of code, or a definite occurrence of a code pattern that is in some contexts considered 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 look for 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 reassignment

CWE-570

Expression is always false

test always false

CWE-571

Expression is always true

test always true

CWE-628

Incorrect arguments in call

precondition failure

CWE-667

Improper locking

unprotected access, unprotected shared access, mismatched protected access

CWE-682

Incorrect calculation

range check, postcondition failure

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. CWE Top 25 Most Dangerous Software Errors

The Common Weakness Enumeration (CWE) Top 25 Most Dangerous Software Errors (CWE Top 25) list is continuously updated to maintain the latest trends in dangerous and widespread software weaknesses that exist in the wild. Please visit http://cwe.mitre.org/top25/ for the most up-to-date information.

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

The 2019 list includes ‘parent’ CWE classes that encompass many smaller CWE that were included on the 2011 list (Support for 2011 CWE/SANS Top 25 Most Dangerous Software Errors). For example, CWE-119 (Improper Restriction of Operation within the Bounds of Memory Buffer), ranked [1] on the 2019 list, is the parent of CWE-120 (Classic Buffer Overflow) which was ranked [3] in the 2011 list. For more information about these new rankings, please visit the 2019 CWE/SANS Top 25 List

CodePeer supports the following list of from 2019 CWE/SANS Top 25 most dangerous software errors as well as two errors considered “Weaknesses On the Cusp” just outside the Top 25:

Rank

ID

CodePeer Message

5

CWE-125

array index check

8

CWE-190

overflow check

14

CWE-476

access check

26

CWE-835

loop does not complete normally

29

CWE-362

unprotected access

The other errors listed in the Top 25 are either parents of other errors, or 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.2. Support for 2011 CWE/SANS Top 25 Most Dangerous Software Errors

CodePeer supports the following from 2011 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.3. 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).