11. GNAT SAS Messages Reference

GNAT SAS outputs analysis results from multiple integrated engines as "messages" in a consistent, uniform way. The types of messages produced are described below. For an overview of GNAT SAS' output, refer to Viewing Results.

GNAT SAS 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 GNAT SAS emits, when it detects one of the above conditions, are referred to as Check-Related Messages.

Some messages that GNAT SAS emits do not fall into the Check-Related category and rather signal a suspicious coding (e.g., dead code, memory leak, unreferenced formal parameter, or code style violation).

The messages produced by GNAT SAS 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 GNAT SAS is not able to prove statically) is given (such as array index check (Inspector): 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.

Note

CWE refers to the Common Weakness Enumeration, a community-developed dictionary of common software weaknesses, hosted on the web by The MITRE Corporation (https://cwe.mitre.org/). The current version of GNAT SAS 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 GNAT SAS message. See CWE to GNAT SAS Message Mapping for a complete table of all CWE ids supported by GNAT SAS.

11.1. Categorization of Messages

GNAT SAS makes conservative assumptions in order to avoid missing potential problems. Because of these assumptions, GNAT SAS 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, GNAT SAS 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 info messages.

11.2. CWE Categorization of Messages

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

11.2.1. CWE to GNAT SAS Message Mapping

GNAT SAS will look for the following CWE weaknesses:

CWE weakness	Description	GNAT SAS Message
CWE-120, 124, 125, 126, 127, 129, 130, 131, 787	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-416	Use after free	use after free
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 Inspector Messages and Infer Messages for more details on the meaning of each GNAT SAS message.

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

GNAT SAS 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 gnatsas.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).

11.2.3. 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 https://cwe.mitre.org/top25/ for the most up-to-date information.

Amongst the 2024 list, GNAT SAS supports the following CWEs:

Rank	ID	GNAT SAS Message
2	CWE-787	array index check
6	CWE-125	array index check
8	CWE-416	use after free
21	CWE-476	access check
23	CWE-190	overflow check

11.3. GNATcheck Messages

By default, GNAT SAS reports the messages issued by GNATcheck (unless GNATcheck is explicitly disabled). GNAT SAS enables five GNATcheck rules by default:

Message	Description
Suspicious_Equalities	Flag "or" expressions whose left and right operands are inequalities referencing the same entity and a literal and "and" expressions whose left and right operands are equalities referencing the same entity and a literal.
Duplicate_Branches	Flag a sequence of statements that is a component of an if statement or of a case statement alternative, if the same if or case statement contains another sequence of statements as its component (or a component of its case statement alternative) that is syntactically equivalent to the sequence of statements in question.
Same_Logic	Flags expressions that contain a chain of infix calls to the same boolean operator (and, or, and then, or else, xor) if an expression contains syntactically equivalent operands.
Same_Operands	Flags infix calls to binary operators /, =, /=, >, >=, <, <=, -, mod, rem (except when operating on floating point types) if operands of a call are syntactically equivalent.
Same_Tests	Flags condition expressions in if statements or if expressions if a statement or expression contains another condition expression that is syntactically equivalent to the first one.

The user may extend that list by specifying predefined rules, or custom rules as explained in Configuring GNATcheck.

The complete list of message kinds and their descriptions, along with examples, can be found in the GNATcheck reference manual in the Predefined Rules chapter.

11.4. Infer Messages

By default, GNAT SAS reports messages issued by Infer (unless Infer is explicitly disabled). See Configuring Infer for more details.

Certain limitations and heuristics can apply to infer messages. See Infer's Limitations and Heuristics for the list of these limitations and heuristics.

First, some messages correspond exactly to messages emitted by Inspector, and won't be described further: validity check (see Uninitialized and Invalid Variables) and unassigned parameter (see Warning Messages).

Second, the following checkers are specific to Infer:

Message	Description
access check	The main difference with Inspector messages is that Infer tries to find a path from the assignment to a null pointer (appearing as null in the source code), to its dereference. As a consequence, the example shown earlier is not flagged by Infer. Here is an example that is flagged: procedure P is type Int_Ptr is access Integer; Some_Cond : Boolean with Volatile; function Get_Ptr return Int_Ptr is begin if Some_Cond then return new Integer; else return null; end if; end Get_Ptr; X : Int_Ptr := Get_Ptr; begin X.all := 42; end P; Infer will flag: p.adb:17:12: high: access check (Infer): `X` could be null (from the call to `p.get_ptr` on line 15) and is dereferenced
memory leak	Memory leaks are reported when a variable is dynamically allocated with new and not deallocated with an instance of Ada.Unchecked_Deallocation. procedure P is X : access Integer := new Integer; begin null; end P; Infer will flag: p.adb:2:26: medium warning: memory leak (Infer): Memory dynamically allocated by `new` on line 2 is not freed after the last access at line 2, column 26
use after free	An error is emitted when a pointer is dereferenced after it has been freed. Here is a simple example: with Ada.Unchecked_Deallocation; procedure P is type Int_Ptr is access Integer; procedure Free is new Ada.Unchecked_Deallocation (Integer, Int_Ptr); X : Int_Ptr; Y : Int_Ptr; begin X := new Integer; Y := X; Free (X); Y.all := 42; end P; Infer will flag: p.adb:16:13: high: use after free (Infer): accessing memory that was invalidated by call to `p.free` on line 14
uninitialized value passed to call	A warning is emitted when uninitialized value of a composite type is passed to a call in an in or in out mode. The checker considers a value of a composite type uninitialized when the composite type and any of its components don't have default initialization, it is a value of a local variable or an out parameter, and any component of the value isn't written before the call. Here is an example: type Rec is record F1 : Integer; F2 : Integer; end record; function Compute (R : Rec) with Import; procedure Uninitialized_Value_Passed_To_Call (R : out Rec) return Integer is begin R.F2 := Compute (R); end Uninitialized_Value_Passed_To_Call; Infer will flag: p.adb:10:15: medium warning: uninitialized value passed to call (Infer): R not written before being passed to call to Compute This warning is not emitted for null records and for calls to primitives of Ada containers. In addition, as a heuristics, the warning is also not emitted for calls to primitives of tagged types.
write without open	A warning is emitted when a file handler not opened for a write access is used to write into a file. Here is an example: with Ada.Text_IO; use Ada.Text_IO; procedure Write_Without_Open is F : File_Type; begin Create (F, In_File, File_Name); Put_Line (F, "Hello World"); end Write_Without_Open; Infer will flag: a.adb:7:7: medium warning: write without open (Infer): file F is written and opened for read access
read without open	A warning is emitted when a file handler not opened for a read access is used to read from a file. Here is an example: with Ada.Text_IO; use Ada.Text_IO; procedure Read_Without_Open is F : File_Type; begin Create (F, Out_File, File_Name); declare S := Get_Line (F); begin ... end Read_Without_Open; Infer will flag: a.adb:8:24: medium warning: read without open (Infer): file F is read and opened for write access
double open	A warning is emitted when an open operation is called on a file handler that has already been opened. Here is an example: with Ada.Text_IO; use Ada.Text_IO; procedure Double_Open is F : File_Type; begin Create (F, Out_File, File_Name); Create (F, Out_File, File_Name); end Double_Open; Infer will flag: a.adb:7:7: medium warning: double open (Infer): file F is already opened at a.adb:6:4
close without open	A warning is emitted when a close operation is called on a file handler that hasn't been opened. Here is an example: with Ada.Text_IO; use Ada.Text_IO; procedure Close_Without_Open is F : File_Type; begin Close (F); end Close_Without_Open; Infer will flag: a.adb:6:7: medium warning: close without open (Infer): file F is closed without being opened
function with side effects	A warning is emitted when a function has side effects. This checker has to be explicitly enabled using the Infer-specific switch --side-effects. By default, the checker looks for side effects on global variables, uplevel variables (variables declared in some enclosing subprogram), and dereferences of parameters of access types passed in IN mode (e.g., updating P.all where P is an IN parameter). Infer switches --ignore-global-side-effects, --ignore-uplevel-side-effects, and --ignore-param-derefs-side-effects can be used to ignore global variable, uplevel variables, and dereferences of IN parameters respectively. The Infer switch --side-effects-ignore can be used to specify global or uplevel variables that will be ignored by the analysis, and can be repeated (e.g. --side-effects-ignore P1.G1 --side-effects-ignore P2.G2). Here is an example: package body P is G : Integer; function Side_Effects (I : Integer) return Integer is begin G := G + I; return G; end Side_Effects; Infer will flag: p.adb:5:4: medium warning: function with side effects (Infer): Function reprod.side_effects has side effects
function with side effects in conditional	A warning is emitted when function having side effects is used in the right hand side of a conditional. This checker has to be explicitly enabled using the Infer-specific switch --side-effects-in-conditionals. Infer switches --ignore-global-side-effects, --ignore-uplevel-side-effects, --ignore-param-derefs-side-effects, and --side-effects-ignore have the same effect as for the checker finding functions with side effects. Here is an example: package body P is G : Integer; function Side_Effects (I : Integer) return Integer is begin G := G + I; return G; end Side_Effects; procedure P is begin if G = 2 or else Side_Effects (2) = 2 then G := 1; end if; end P; Infer will flag: p.adb:15:24: medium warning: function with side effects in conditional (Infer): Impure function reprod.side_effects in conditional
write through global and parameter	Emitted on calls where a global variable is used as parameter to a subprogram that modifies said global both through its global reference and through the parameter reference. For example: procedure P is X : Integer := 0; procedure I (A : in out Integer) is begin X := 1; A := 2; end; begin I (X); end P; Infer will emit: p.adb:9:3: medium: write through global and parameter (Infe r): p.i may write to X through a global reference, but X may be overwritten by an out parameter copy

11.5. GNAT Warnings Messages

By default, GNAT SAS reports a selection of warnings from the GNAT compiler, as listed in the table below. The list of all available GNAT warnings and their description can be found in the GNAT user's guide in the Warning Message Control section. For more details on this capability see Configuring GNAT Warnings.

Message	GNAT switch	Description
normal warnings mode	-gnatwn	Assorted set of messages with no common theme.
bad fixed value	-gnatwb	Warnings for static fixed-point expressions whose value is not an exact multiple of Small.
unused assignment	-gnatwm	Warnings for variables that are assigned but whose value is never read.
missing parenthesis	-gnatwq	Warnings for expressions whose lack of parenthesis may be ambiguous from a reader's point of view.
redundant construct	-gnatwr	Warnings for redundant constructs.
unassigned variable	-gnatwv	Warnings on access to variables which may not be properly initialized.
low bound assumption	-gnatww	Warnings on accessing unconstrained string parameters with a literal or S'Length.
export/import mismatch	-gnatwx	Warnings on potential issues arising from interfacing with other programming languages.
assertion failure	-gnatw.a	Warnings on assertions the compiler can tell will always fail.
biased representation	-gnatw.b	Warnings on clauses that may force the compiler to use a biased representation for an integer type (e.g. using a single bit to represent the range 10..11).
overlapping actuals	-gnatw.i	Warnings on statically detectable overlapping actuals in a subprogram call.
suspicious modulus value	-gnatw.m	Warnings on modulus values matching the size of the type they're attached to.
suspicious parameter order	-gnatw.p	Warnings on subprogram calls where all parameters are variables whose name match the formals of the subprogram but are not in the same order.
object renaming function	-gnatw.r	Warnings on object renamings that rename function calls.

11.6. Inspector Messages

GNAT SAS reports messages issued by Inspector (unless Inspector is disabled). See Configuring Inspector for more details.

11.6.1. Understanding messages on generics

In some cases, Inspector messages are reported on an instance of a generic unit, but the message references entities by the names used in the generic template rather than in the instance. In such cases, it is important to understand that Inspector, like SPARK, only analyzes fully-instantiated code and the message was actually emitted on a given instantiation of the generic. When reading such messages, users should then look at the instantiation at the reported location, and compare with the generic code, to understand how the message applies.

Note that when messages are emitted on multiple instances, GNAT SAS will de-duplicate them and only report one message to avoid extra noise, as in most cases the issue comes from the generic's implementation.

11.6.2. Run-Time Checks

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

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: 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 (Inspector): 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: 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; Inspector will detect the division by zero with: div.adb:7:23: high: divide by zero (Inspector): check fails here; requires I /= 0
access check	Attempting to dereference a reference that could be null (CWE 476). For example in the following code: 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 (Inspector): check fails here
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: 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 (Inspector): 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: 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 (Inspector): check fails here; requires Attempt_Count /= Integer_32'Last
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: 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> (Inspector): precondition 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: 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> (Inspector): precondition failure on call to tag.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: 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 (Inspector): check fails here; requires not (Create (3, 2, 6.0).b /= True or else Create (3, 2, 6.0).l /= 3)
negative operand of exponentiation	The operand of integer exponentiation is negative. For example in the following code: function Neg_Operand return Integer is function Compute return Integer is begin return -2; end Compute; begin return 2 ** Compute; end Neg_Operand; the call to Create will generate the following message: neg_operand.adb:8:16: high: negative operand of exponentiation (Inspector): check fails here; requires (compute'Result) >= 0
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 Inspector 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.

11.6.3. User Checks

Inspector 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: 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; Inspector will detect that the pragma Assert will never be True: assert.adb:9:19: high: assertion (Inspector): check fails here; requires (and_or'Result) /= false
conditional check	An exception could be raised depending on the outcome of a conditional test in user code. For example in the following code: 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; Inspector will detect that Attempt_Count will always be greater than 3: overflow.adb:21:13: high: conditional raise (Inspector): exception is raised in a conditional branch 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: procedure Raise_Exc is X : Integer := (raise Program_Error); begin null; end Raise_Exc; will generate: raise_exc.adb:2:20: low: raise exception (Inspector): 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: 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> (Inspector): precondition failure on call to pre."**"; requires Left in ([IEEE_32_Float'First..0.0) | (0.0..IEEE_32_Float'Last])
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: 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; Inspector detects that the postcondition of Decrement will always be violated, given the precondition: post.adb:11:14: high: postcondition (Inspector): postcondition failure on call to post.decrement; requires not (stress_is_maximal'Result)

In addition, Inspector 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., GNAT SAS 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 Inspector'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 GNAT SAS 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.

11.6.4. Uninitialized and Invalid Variables

Inspector and Infer analyses attempt 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: procedure Uninit is A : Integer; B : Integer; begin A := B; -- we are reading B which is uninitialized! end Uninit; GNAT SAS will flag the read of B: uninit.adb:5:9: high: validity check (Inspector): B is uninitialized here When an OUT parameter is read without being initialized, it is flagged in the same way: procedure Uninit_Out (B : out Integer) is A : Integer; begin A := B; -- we are reading B which is uninitialized! end Uninit_Out; uninit.adb:11:9: high: validity check (Inspector): B is uninitialized here Infer also flags the read before initialization of the field of a record passed as an OUT parameter. While this can be valid code since the OUT parameter may be passed by reference, it is prone to errors. type Rec is record F1 : Integer; end record; procedure Uninit_Out_Rec (R : out Rec) is A : Integer; begin A := R.F1; -- R.F1 can be initialzed, but shouldn't be accessed end Uninit_Out_Rec; Infer will flag the read of R.F1 with a validity check message: uninit.adb:20:12: high: validity check (Infer): `_.F1` is read without initialization Note that for the same example, Inspector flags the problem with a message of a kind suspicious input. Finally, both Infer and Inspector flag with a validity check an OUT parameter of scalar type that isn't initialized at the end of a subprogram: procedure Out_Not_Set (O : out Integer) is begin null; end Out_Not_Set; GNAT SAS flags such subprogram with: uninit.adb:22:4: high: validity check (Inspector): out parameter O is uninitialized here

11.6.5. Warning Messages

In addition to run-time checks, Inspector 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.

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: 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; GNAT SAS will flag: dead_code.adb:5:9: medium warning: dead code (Inspector): dead code because I = 10 dead_code.adb:9:9: medium warning: dead code (Inspector): 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, GNAT SAS will also flag: dead_code.adb:4:9: low warning: test always false (Inspector): 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, GNAT SAS will also flag: dead_code.adb:6:4: medium warning: test always true (Inspector): 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: procedure Predetermined is I : Integer := 0; begin case I is when 0 => ... when 1 => ... when others => ... end case; end Predetermined; GNAT SAS will flag: predetermined.adb:4:4: low warning: test predetermined (Inspector): 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: 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; GNAT SAS will flag: condition.adb:6:27: medium warning: condition predetermined (Inspector): 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: 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; GNAT SAS will flag: loops.adb:8:10: medium warning: loop does not complete normally (Inspector)
unused assignment	Indicates redundant assignment. This may be an indication of unintentional loss of result or unexpected flow of control (CWE 563). Note that Inspector 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: procedure Unused_Assignment is C : Character := Get_Character; begin null; -- C is not used in this subprogram end Unused_Assignment; GNAT SAS will flag: unused_assignment.adb:2:4: medium warning: unused assignment (Inspector): 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: 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; GNAT SAS will flag: unused_global.adb:16:7: low warning: unused assignment to global (Inspector): 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: 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; GNAT SAS will flag: unused_out.adb:8:33: medium warning: unused out parameter (Inspector): unused out parameter Found unused_out.adb:8:33: medium warning: unused out parameter (Inspector): 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: procedure Self_Assign (A : in out Integer) is B : Integer; begin B := A; A := B; end Self_Assign; GNAT SAS will flag: self_assign.adb:5:6: medium warning: useless reassignment (Inspector): 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 GNAT SAS tutorial: 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; GNAT SAS will flag: stack.adb:3:4: medium warning: suspicious precondition (Inspector): precondition for S.Last does not have a contiguous range of values
suspicious input	Inputs mention a value reachable through an out-parameter of the subprogram 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: 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; GNAT SAS will flag: in_out.adb:13:7: medium warning: suspicious input (Inspector): 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: procedure Unread (X : in out Integer) is begin X := 0; -- X is assigned but never read end Unread; GNAT SAS will flag: unread.adb:1:1: medium warning: unread parameter (Inspector): parameter X could have mode out
unassigned parameter	Inspector emits a warning when 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: procedure Unassigned (X : in out Integer; Y : out Integer) is begin Y := X; -- X is read but never assigned end Unassigned; GNAT SAS will flag: unassigned.adb:1:1: medium warning: unassigned parameter (Inspector): parameter X could have mode in In addition, Infer emits the same warning when any component of a parameter of a composite type of mode in out or out is never assigned. For example in the following code: type Rec is record F1 : Integer; F2 : Integer; end record; procedure Unassigned_Composite (R1, R2 : out Rec) is begin R2.F1 := 10; end Unassigned_Composite; GNAT SAS will flag: unassigned_infer.adb:1:4: medium warning: unassigned parameter (Infer): out parameter R1 not written in a subprogram The warning is not emitted for primitives of tagged types and for null records.
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: 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; GNAT SAS will flag: constant_op.adb:6:16: medium warning: suspicious constant operation (Inspector): 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: procedure Infinite_Loop is X : Integer := 33; begin loop X := X + 1; end loop; end Infinite_Loop; GNAT SAS will flag: infinite_loop.adb:1:1: medium warning: subp never returns (Inspector): infinite_loop never returns infinite_loop.adb:5:9: medium warning: loop does not complete normally (Inspector)
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: procedure P is X : Integer := (raise Program_Error); begin null; end P; GNAT SAS will flag: p.adb:1:1: high warning: subp always fails (Inspector): p fails for all possible inputs p.adb:2:20: low: raise exception (Inspector): unconditional raise

11.6.6. Information Messages

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

Message	Description
call too complex	Indicates that Inspector skipped analyzing the subprogram call to avoid exhausting resources needed for analyzing the remainder of the system. Inspector 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 Inspector 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. Inspector will report any presumptions it makes about the results/effects of the otherwise unanalyzed call.
subp not analyzed	Indicates that Inspector 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 Inspector could not analyze any of the subprograms in this module. These subprograms need to be reviewed manually instead.
module analyzed	Indicates that Inspector completed analysis of this module
dead code continues	Indicates a block that is dead because its predecessor is dead.

11.6.7. Race Condition Messages

When GNAT SAS is run in deep analysis mode, Inspector's analysis produces three sorts of race condition messages. Note that when GNAT SAS 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 GNAT SAS.

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:

package Race is

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

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

end Race;

package body Race is

   Counter : Natural := 0;

   procedure Acquire;
   pragma Import (C, Acquire);

   procedure Release;
   pragma Import (C, Release);

   pragma Annotate (GNATSAS, 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;

GNAT SAS will generate the following messages:

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

If GNAT SAS 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 Inspector 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.

11.6.7.1. Identify Possible Race Conditions

Note

This section only applies when using GNAT SAS in deep analysis mode.

When GNAT SAS is run in deep analysis mode, Inspector detects common forms of race conditions. More precisely, Inspector focuses on the data race subset of race conditions: Race conditions that 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. Inspector identifies race conditions where synchronization is not used or is used incorrectly. Since Inspector focuses on data races, concurrent references to atomic objects are presumed to be free of race conditions. (Note that the current release of GNAT SAS 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, GNAT SAS 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. Inspector ignores locks on objects that are not visible to multiple tasks since they have no synchronizing effect. This means GNAT SAS 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.

Inspector 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 GNAT SAS as needed. In addition, you can manually identify reentrant entry points (aka task types) with the -reentrant "package.subp" switch on the GNAT SAS command line. Use the -daemon "package.subp" to identify daemon entry points (aka tasks). See GNAT SAS CLI Reference for the syntax for these switches.

You may also identify tasks and task types for GNAT SAS 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 Inspector's race condition analysis. In this example:

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

Inspector will assume that Pkg.Single is a single thread entry point (or "daemon", or "task") procedure and that Pkg.Multiple is a multiple thread entry point (or "reentrant", or "task type") procedure. An Annotate pragma used in this way must have exactly three operands: the identifier GNATSAS, 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 switches. In this example:

package Foo_Procs is
   procedure Foo_123;
   procedure Foo_456;
   pragma Annotate (GNATSAS, 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 gnatsas.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 Inspector.

Inspector performs race condition analysis only with the deep analysis mode. 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 add the --no-race-conditions switch to your project file's "inspector" switches to suppress race condition analysis.

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 GNAT SAS. This pragma has no effect on the code generated for the execution of a program; the pragma only affects Inspector's race condition analysis. Given this example:

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

Inspector 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;

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

Inspector 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 GNATSAS, 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 in GNATstudio provides details about the shared objects in your program that might be subject to unsafe access. In GNAT Studio, there is one global report accessible from the main GNAT SAS report. Clicking on each shared object displays information about entry points associated with possible race conditions, including the information whether it is a read or a write access. As mentioned above, GNAT SAS only concerns itself with locks that are visible to multiple tasks, so an empty column Locks 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.

11.6.8. Understanding the Differences between Preconditions and Run-time Errors

One possibly surprising behavior of Inspector 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, Inspector 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 Inspector flags a precondition violation here. This precondition violation is due to a potential run-time error, which is indicated in angle brackets as part of the message generated by GNAT SAS:

bug.adb:13:12: high: precondition <array index check> (Inspector):  precondition 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 GNAT SAS 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 Inspector 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 adding the --no-preconditions switch to your project file's list of inspector switches. This will disable the generation and propagation of preconditions and will generate messages instead at the point of the potential failure.

11.7. Inspector Annotations

In addition to messages, GNAT SAS' Inspector analysis 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 Inspector.

11.7.1. Annotations

The Inspector engine 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 Inspector 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 Inspector 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 add the --dbg-off inout_limit switch to the list of Inspector switches in your project file..

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

11.7.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 Inspector specific notations:

X'Initialized	Means that X is expected to be initialized, but no further requirement or knowledge is imposed on its value. Inspector 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. Inspector 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. Inspector 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.
//	This operator is used to represent the division operator used for converting (with rounding) a fixed point value to an integer value, with the semantics described in Ada RM 4.6(33). Here is an example precondition: requires (if Arg >= 1_415_577_600 then 0 else (Arg//16_384)/3_600) in 0..23. Note that, in the precondition above, 1_415_577_600 is not a value of the type of Arg, but of the underlying integer type GNAT uses to represent its (fixed-point) value. Likewise, Arg//16_384 is actually an integer division, but with special rounding properties. Reading such annotations may be confusing at first, and special care should be exercised.

11.7.3. Use Annotations generated by Inspector for Code Reviews

Note

This section only applies in deep mode.

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. Inspector 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, Inspector 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. GNAT SAS displays preconditions, presumptions, and postconditions within the GNAT Studio source editor as an Ada comment block immediately preceding the first executable line of the subprogram.

The preconditions displayed by GNAT SAS 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 Inspector 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 Inspector 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, Inspector's generated preconditions can be used to verify both the written and unwritten assumptions made by the codewriters.

Presumptions represent assumptions made by Inspector 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.