5. 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.

5.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 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.

5.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.
divide by zero Second operand of a divide, mod or rem operation could be zero (CWE 369).
tag check A tag check (incorrect tag value on a tagged object) may fail (CWE 136, 137).
discriminant check A field for the wrong variant/discriminant is accessed (CWE 136, 137).
access check Attempting to dereference a reference that could be null (CWE 476).
range check A calculation may generate a value outside the bounds of an Ada type or subtype and generate an invalid value (CWE 682).
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).
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. NOTE: 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.
precondition A subprogram call that might violate the subprogram’s preconditions. NOTE: in the details associated with the message, the precondition being checked is expressed in terms of the variables of the called subprogram, rather than the calling one. On the HTML output, you can click on the link provided to view the preconditions and local parameter names of the called subprogram, and then click the Back button (“<<”), before trying to understand in what way the caller might be violating the precondition. In GPS, you can use the Goto body of xxx capability instead. 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 all messages above).

5.1.2. User Checks

CodePeer will analyze checks inserted manually by the programmer either as an explicit Assert or Precondition pragma:

pragma Assert (Condition_that_should_be_True);

or via code of the form:

if Condition_that_should_be_False then
   raise Some_Exception;
end if;
Message Description
assertion A user assertion (using e.g. pragma Assert or precondition) could fail. The precondition may be written as a pragma Precondition, or as a Pre aspect in Ada 2012 syntax.
conditional check An exception could be raised depending on the outcome of a conditional test in user code.
raise exception An exception is being raised on a reachable path.
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. The message will only show up in certain complex cases where CodePeer is unable to propagate the precondition (for example, when the condition is a quantified expression). The message is issued on the precondition expression.
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.

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.

For both pragmas (as with any run-time check), analysis of subsequent code assumes the success of the preceding run-time check. Pragma Assume can, therefore, be used to prevent generation of unwanted messages about subsequent code. No message will be generated about a possible division by zero in the following example (provided that CodePeer is unable to deduce that failure of the assumption is a certainty):

declare
   Num : Natural := Some_Function;
   Den : Natural := Some_Other_Function;
   pragma Assume (Den /= 0);
   Quo : Natural := Num / Den;
begin
   ...
end;

In this respect, one might think of pragma Assume as an alternative to “pragma Annotate (CodePeer, False_Positive, ...);”. It is important to be aware of two important differences between these two approaches to avoiding unwanted messages. First, an Assume pragma (unlike an Annotate pragma) can affect the run-time behavior of a program - an Annotate pragma has no effect on run-time behavior. Second, an incorrect Assume pragma can invalidate CodePeer’s analysis, possibly to an extent that is not obvious, while an Annotate pragma has no effect on CodePeer’s analysis of subsequent constructs. The user-visible effects (with respect to both run-time behavior and to CodePeer’s analysis) of an Assume pragma are more like those of an Assert pragma followed by an Annotate pragma that suppresses any message about the possibility that the assertion might fail.

5.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).

5.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).
test predetermined Indicates redundant conditionals, which could flag logical errors (CWE 570, 571).
test always true Same as above, with an additional indication that the test always evaluates to true (CWE 571).
test always false Same as above, with an additional indication that the test always evaluates to false (CWE 570).
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).
loop does not complete normally Indicates loops that either run forever or fail to terminate normally (CWE 835).
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).
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).
unused out parameter Indicates that an actual parameter of a call is ignored (either never used or overwritten) (CWE 563).
useless self assignment Indicates when an assignment does not modify the value stored in the variable being assigned (CWE 563).
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.
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.
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.
unassigned parameter A parameter of a scalar type of mode in out is never assigned, and so could be declared with 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.
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.
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.

5.1.5. GNAT Warning Messages

When called with the --gnat-warnings switch, CodePeer will also report 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 Integrating GNAT Warnings.

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)

5.1.6. Race Condition Messages

CodePeer produces three sorts of race condition messages. See Identify Possible Race Conditions for details on using CodePeer to perform race condition analysis. 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. See Identify Possible Race Conditions for more information on the handling of local locks. See above for an explanation of the CWE references.

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).

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 titlebar. 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. See Identify Possible Race Conditions for more information on how to interpret this report. Note that the current release of CodePeer does not detect deadlocks between tasks (sometimes called deadly embraces). Rather it identifies data objects that are potentially referenced without adequate synchronization.

5.1.7. Information Messages

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

Message Description
call too complex; analysis skipped 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. These should be reviewed to be sure they are appropriate.
subp not available; call not analyzed Indicates that CodePeer cannot analyze the call because the called subprogram is not available. There are two possible reasons for this: the .scil file for the called subprogram is not supplied in the library file, or the called subprogram is analyzed in a different partition. CodePeer will report any presumptions it makes about the results/effects of the otherwise unanalyzed call. These should be reviewed to be sure they are appropriate.
subp not analyzed Indicates that Codepeer encountered a problem while analyzing this subprogram and skipped its analysis as well as its nested subprograms.
module not analyzed Indicates that Codepeer could not analyze any of the subprograms in this module.
module analyzed Indicates that Codepeer completed analysis of this module

5.2. 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. With guidance from your CodePeer support, this MessagePatterns.xml file may be used to tune the categorization of messages to the needs of a particular project; see also Format of MessagePatterns.xml File for more information about the format of that 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 (even if not necessarily a bug, e.g. dead code)
Medium Moderate likelihood there is a defect on this line of code. It may cause a problem on some executions.
Low There is a small chance there is a defect on the given line of code. It is worth investigating 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.
Suppressed The message is very likely uninteresting and was suppressed automatically by CodePeer. Suppression of messages is controlled by the MessagePatterns.xml file, and is used to e.g. suppress messages about internally generated variables or constructs, not directly relevant to the source code.

The following terms are used to distinguish between different reviews and messages when an historical database is being maintained for a body of code.

Message Description
current (now)

A current message is one that appears in the current review, regardless of whether it appeared in any prior review. If no historical database is being kept, all messages are current.

The current review is always the review currently being viewed though the CodePeer browser interface.

new (added) A new (or added) message is one that appears in the current review but not the base one. New messages have a + indicator in the left column in the File Source view and in the +/- column in the Per-File Message Status Window. If no historical database is being kept, the new designation is not made.
dropped A dropped message is one that appears in the base review but not in the current review. Dropped messages have a - indicator in the +/- column in the Per-File Message Status window. If no historical database is being kept, no dropped messages will be displayed.
base (baseline)

A base message is one that appears in the base code review, regardless of whether it appears in the current review.

The base review is a prior review against which the current review is compared, in the CodePeer Overview. Any CodePeer Overview has exactly one base review, or none, if no historical database is specified.

A baseline review is a review run with the -baseline run time option. This makes the review eligible for being used as the default base review for future analyses, in the absence of an explicit -cutoff parameter. A previous review can become the new default baseline review if specified by the -set-baseline-id option.

deltas The deltas column contains the count of messages dropped (-) and/or added (+) between the base and the current review.

Where an historical database is specified, the CodePeer Overview‘s Base Code Review defaults to be the second most recent baseline review, one run with the -baseline or -set-baseline-id command-line flag. Use the -cutoff flag to override the default Base Code Review by assigning the review ID of an arbitrary review to be the base.

CodePeer uses the historical database, the message type, and the line number on which the message is associated to determine whether a base message matches a current message or the current message is new. Each new message is assigned a unique identifier, and that identifier is maintained across subsequent runs. If the source file has been modfied significantly between base and Current Code Reviews, CodePeer may not be able to determine that a current message matches a base message. In this case it will designate the current message as new. Similarly, if CodePeer cannot read the historical database for any reason, it will determine that all current messages are new.

5.3. 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. See Use Annotations for Code Reviews for more details on how annotations can be used to aid in source code review.

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

  • Preconditions (aka “pre”) 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.
    • The notation X’Initialized means that X is expected to be initialized prior to calling the subprogram, but no further requirement 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. In particular, CodePeer issues the same precondition if X is default-initialized, because, in many cases, the default value of a variable is not a correct value for the subprogram analyzed. In that case, the precondition serves as a reminder that X should be set to a correct value prior to calling the subprogram.
    • The notation (soft) means that the precondition is associated with code that might not be executed on certain calls to the subprogram, 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.
    • The notation 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).
    • The notation X in (a..b | c | d) 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.
    • Floating point ranges are expressed using the mathematical notation: X in (1.1 .. 5.2] 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.
    • The notation Global_Var@package_name’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 package_name that captures the value of a global variable declared in some other packge, during elaboration of package_name.
    • The notation Package.Variable’Body refers to a variable defined in the body of a given package.
    • Precondition messages include in parenthesis a list of the checks involved in the requirements.
  • Presumptions (aka “presumption”) display what CodePeer presumes about the results of an external subprogram whose code is unavailable for review, 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.
  • Postconditions (aka “post”) characterize the behavior of the subprogram in terms of its outputs and the presumptions made.
    • The notation X’Old in a postcondition refers to the value X had on entry to the subprogram, as defined in Ada 2012.
    • The notation Func’Result in a postcondition refers to return value of the given function Func, as defined in Ada 2012.
    • The notation X’Initialized means that X is initialized by a call to the subprogram. CodePeer displays this notation when it cannot indicate more precisely the value of X on exit to the subprogram.
    • The notation possibly_updated(X) is used to convey that X is a possible output, but there is no specific set of values that it is known to have after the subprogram completes.
    • The notation possibly_init’ed(X) is used to convey that X is initialized on some but not all paths through the subprogram.
    • The notation 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.
  • Unanalyzed Calls (aka “unanalyzed”) 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 (aka “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 (aka “global outputs”) comprise a list of all global variables (objects and components) modified by each subprogram.
  • New Objects (aka “new obj”) 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: the notation Pkg’Body in messages and annotations 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.

5.4. 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.

5.5. Support for CWE

5.5.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 assignement 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.

5.5.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.

5.5.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_Dependence => Ada.Unchecked_Deallocation);
pragma Restrictions (No_Dependence => Unchecked_Deallocation);
pragma Restrictions (No_Dependence => Ada.Unchecked_Conversion);
pragma Restrictions (No_Dependence => Unchecked_Conversion);

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).