.. _Messages_and_Annotations: *************************** 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 :ref:`How_To_View_GNAT_SAS_Output`. 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 :ref:`CWE_Messages` for a complete table of all CWE ids supported by GNAT SAS. .. _Categorization_of_Messages: 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 :file:`MessagePatterns.xml` file. .. table:: :class: longtable :widths: 20 80 =============== ============================================================== 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. =============== ============================================================== .. _CWE_Support: 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 `_). .. _CWE_Messages: CWE to GNAT SAS Message Mapping ------------------------------- GNAT SAS will look for the following CWE weaknesses: .. csv-table:: :header: CWE weakness, Description, GNAT SAS Message :delim: & "`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 :ref:`Inspector_Messages` and :ref:`Infer_Messages` for more details on the meaning of each GNAT SAS message. .. _Use_of_Potentially_Dangerous_Functions: 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: .. code-block:: ada pragma Restrictions (No_Unchecked_Conversion, No_Unchecked_Deallocation); that you can put in a :file:`gnatsas.adc` file and reference this file in your project file via the ``Global_Configuration_Pragmas`` project attribute, as described in :ref:`Configuration_of_System`. 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: .. csv-table:: :header: Rank, ID, GNAT SAS Message :delim: & 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 .. _GNATcheck_Messages: 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: .. table:: :class: longtable :widths: 20 80 ======================= ========================================================== 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 :ref:`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`__. __ https://docs.adacore.com/live/wave/lkql/html/gnatcheck_rm/gnatcheck_rm/predefined_rules.html .. _Infer_messages: Infer Messages ============== By default, GNAT SAS reports messages issued by Infer (unless Infer is explicitly disabled). See :ref:`Configuring_Infer` for more details. First, some messages correspond exactly to messages emitted by Inspector, and won't be described further: ``validity check`` (see :ref:`Validity_Check`). Second, the following checkers are specific to Infer: .. table:: :class: longtable :widths: 20 80 ========================================== ==================================================================================== 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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`. .. code-block:: ada :linenos: procedure P is X : access Integer := new Integer; begin null; end P; Infer will flag: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none p.adb:16:13: high: use after free (Infer): accessing memory that was invalidated by call to `p.free` on line 14 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none p.adb:15:24: medium warning: function with side effects in conditional (Infer): Impure function reprod.side_effects in conditional ========================================== ==================================================================================== .. _GNAT_Warnings_Messages: 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 :ref:`Configuring_GNAT_Warnings`. __ https://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ugn/building_executable_programs_with_gnat.html#warning-message-control .. _GNAT_Warnings_table: .. table:: :class: longtable :widths: 20 20 40 +----------------------------+-------------+------------------------------+ | 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. | +----------------------------+-------------+------------------------------+ .. _Inspector_Messages: Inspector Messages ================== GNAT SAS reports messages issued by Inspector (unless Inspector is disabled). See :ref:`Configuring_Inspector` for more details. .. _Run-Time_checks: Run-Time Checks --------------- These are language defined run-time checks that are searched by Inspector: .. table:: :class: longtable :widths: 20 80 =================================== ======================================================================================================= 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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``): .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none alias.adb:18:4: high: precondition (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: .. code-block:: ada :linenos: 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: .. code-block:: none tag.adb:21:4: high: precondition (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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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 :ref:`Description_of_Annotations` and :ref:`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. =================================== ======================================================================================================= .. _User_Checks: User Checks ----------- Inspector will analyze checks inserted manually by the programmer either as an explicit Assert or via Ada 2012 aspects. .. table:: :class: longtable :widths: 20 80 ================== ======================================================================================================== Message Description ================== ======================================================================================================== assertion A user assertion (using e.g. pragma Assert) could fail. For example in the following code: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: procedure Raise_Exc is X : Integer := (raise Program_Error); begin null; end Raise_Exc; will generate: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none pre.adb:7:19: high: 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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 :ref:`Improve_Your_Code_Specification` for more details on pragma Assert and Assume. .. _Validity_Check: 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). .. table:: :widths: 20 80 ================== ====================================================================== 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: procedure Uninit_Out (B : out Integer) is A : Integer; begin A := B; -- we are reading B which is uninitialized! end Uninit_Out; .. code-block:: none 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. .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: procedure Out_Not_Set (O : out Integer) is begin null; end Out_Not_Set; GNAT SAS flags such subprogram with: .. code-block:: none uninit.adb:22:4: high: validity check (Inspector): out parameter O is uninitialized here ================== ====================================================================== .. _Warning_Messages: 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. .. table:: :class: longtable :widths: 20 80 ================================ ========================================================================================== 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: none 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: .. code-block:: none 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: .. code-block:: ada :linenos: procedure Predetermined is I : Integer := 0; begin case I is when 0 => ... when 1 => ... when others => ... end case; end Predetermined; GNAT SAS will flag: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: procedure Unused_Assignment is C : Character := Get_Character; begin null; -- C is not used in this subprogram end Unused_Assignment; GNAT SAS will flag: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: procedure Self_Assign (A : in out Integer) is B : Integer; begin B := A; A := B; end Self_Assign; GNAT SAS will flag: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: procedure Unread (X : in out Integer) is begin X := 0; -- X is assigned but never read end Unread; GNAT SAS will flag: .. code-block:: none unread.adb:1:1: medium warning: unread parameter (Inspector): parameter X could have mode out unassigned parameter A parameter of a scalar type of mode in out is never assigned, and so could be declared with mode in. For example in the following code: .. code-block:: ada :linenos: 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: .. code-block:: none unassigned.adb:1:1: medium warning: unassigned parameter (Inspector): parameter X could have mode in suspicious constant operation An operation computes a constant value from non-constant operands. This is characteristic of a typographical mistake, where a variable is used instead of another one, or a missing part in the operation, like the lack of conversion to a floating-point or fixed-point type before division. For example in the following code: .. code-block:: ada :linenos: 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: .. code-block:: none 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: .. code-block:: ada :linenos: procedure Infinite_Loop is X : Integer := 33; begin loop X := X + 1; end loop; end Infinite_Loop; GNAT SAS will flag: .. code-block:: none 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: .. code-block:: ada :linenos: procedure P is X : Integer := (raise Program_Error); begin null; end P; GNAT SAS will flag: .. code-block:: none 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 ================================ ========================================================================================== .. _Information_Messages: Information Messages -------------------- These are extra information messages generated by Inspector during analysis to complement existing warnings or check messages. .. table:: :class: longtable :widths: 20 80 +----------------+-----------------------------------------------------------+ | Message | Description | +================+===========================================================+ | call too | Indicates that Inspector skipped analyzing the subprogram | | complex | 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 | | | :ref:`Call_Too_Complex` for more information on the | | | possible causes of this message. | +----------------+-----------------------------------------------------------+ | subp not | Indicates that Inspector cannot analyze the call because | | available | 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 | Indicates that Inspector encountered a problem while | | analyzed | analyzing this subprogram and skipped its analysis as well| | | as its nested subprograms. These subprograms need to be | | | reviewed manually instead. | +----------------+-----------------------------------------------------------+ | module not | Indicates that Inspector could not analyze any of the | | analyzed | subprograms in this module. These subprograms need to be | | | reviewed manually instead. | +----------------+-----------------------------------------------------------+ | module | Indicates that Inspector completed analysis of this module| | analyzed | | +----------------+-----------------------------------------------------------+ | dead code | Indicates a block that is dead because its predecessor | | continues | is dead. | +----------------+-----------------------------------------------------------+ .. _Race_Condition_Messages: Race Condition Messages ----------------------- When GNAT SAS is run in :ref:`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. .. table:: :widths: 20 80 ============================ ========================================================================================== 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: .. code-block:: ada :linenos: 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; .. code-block:: ada :linenos: 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: .. code-block:: none 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. .. _Identify_Possible_Race_Conditions: Identify Possible Race Conditions ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ .. note:: This section only applies when using GNAT SAS in :ref:`deep analysis mode`. When GNAT SAS is run in :ref:`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 :ref:`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: .. code-block:: ada 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: .. code-block:: ada 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 :file:`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: .. code-block:: ada 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: .. code-block:: ada 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 :ref:`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. .. _Preconditions_And_Run-Time_Errors: 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: .. code-block:: ada 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: .. code-block:: ada return Arr (X + 10); However, Inspector does not flag the potential problem here. Instead, it "protects" the calls to Get1 with a deduced precondition: .. code-block:: ada X in -9..0 This precondition has to be respected by callers. This is clearly not the case in the call: .. code-block:: ada 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: .. code-block:: none bug.adb:13:12: high: precondition (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: .. code-block:: ada 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. .. _Description_of_Annotations: 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. .. _Annotations: Annotations ----------- The Inspector engine generates the following kinds of annotations on each Ada subprogram: .. table:: :class: longtable :widths: 20 80 ================ ============================================================== 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 `@` 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 :ref:`Use_Annotations_for_Code_Reviews` for more details on how annotations can be used to aid in source code review. .. _Annotation_Syntax: 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: .. table:: :class: longtable :widths: 20 80 ========================== ==================================================== `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.` 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. ========================== ==================================================== .. _Use_Annotations_for_Code_Reviews: Use Annotations generated by Inspector for Code Reviews ------------------------------------------------------- .. note:: This section only applies in :ref:`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 `@` 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.