6. Reviewing Results and Improving Code

A message generated by GNAT SAS may be a false positive (i.e. the error situation GNAT SAS is warning about cannot actually occur) or point out an intended behavior (e.g., numeric overflow might be intentionally raised in some situations). In either case, such a message does not indicate a potential error in the code that requires further investigation. It is often useful to preserve the results of such review. The following sections describe two ways to deal with such a message once identified, namely:

tell GNAT SAS about the status of this message with the review mechanism described in Reviewing Messages. This way, GNAT SAS knows to either hide and/or attach information to said message for the current and future runs. Or,
improve the code specification in order to clarify the intent of the code, and at the same time eliminate false alarms, as seen in Improve Your Code Specification.

6.1. Reviewing Messages

GNAT SAS provides two different mechanisms for capturing review information and associating it with the corresponding messages.

The first mechanism allows interactively reviewing messages via either:

The GNAT Studio IDE (see Reviewing messages through GNAT Studio)
The CSV output (see Through a CSV File)

The second mechanism consists of adding annotations in the form of pragmas to the Ada source code being analyzed as described in Through Pragma Annotate / Justification in Source Code.

Each approach has its pros and cons.

Advantages of interactive review include:

No source code modifications are required; frozen source code can be reviewed.
Review does not perturb line numbering of sources, which in turn can affect the text of other messages.
Review can be performed by people not familiar with modifying Ada source code.
Review status values other than False_Positive and Intentional are available (e.g., Pending as well as Custom Review Status).
Review affects the messages of the current run.

Advantages of adding pragmas to the source include:

Review is integrated with the sources and easier to relate to the sources.
Review is less likely to be invalidated by other source changes; the mapping from the review to the message being reviewed is more straightforward.
Existing editing and version control tools can be used to create and manage reviews.

The different techniques can be mixed, even within a single Ada unit.

In addition, it is also possible and sometimes desirable to improve the code specification to clarify the intent of the code and at the same time eliminate false alarms, as explained in Improve Your Code Specification.

When reanalyzing a source code, GNAT SAS classifies messages as unchanged, added, or removed with respect to the baseline run and it will preserve the existing reviews for unchanged messages. See Classifying Messages as Unchanged, Added, and Removed for more details.

6.1.1. Through GNAT Studio

See Reviewing messages through GNAT Studio for a detailed guide.

6.1.2. Through a CSV File

Note

This section assumes that the analysis has already been run on the project and that it found messages.

Another possibility for users to review messages is to export the messages via the CSV Output and then edit in e.g. a spreadsheet the CSV file to add manual reviews.

In order to input a review from a CSV file, you need to fill the review_status column (field) for the row corresponding to the message that you want to review. The value should be either pending, false_positive, not_a_bug, intentional, bug, or any Custom Review Status. Note that the review_kind field is automatically computed from the review_status field and should not be modified.

Additionally, you can fill the review_author field, and the review_text field, or leave them empty. The review_date field can be left empty, in which case it will be set to the time of the import by csv-review. If review_author is left empty, the tool will automatically add one using your login: <login> (from csv).

Any other field should be left as set by the CSV export.

6.1.3. Through Pragma Annotate / Justification in Source Code

To mark a message as reviewed in GNATSAS reports with a source annotation, insert an Annotate pragma directly below the line that triggers the message. (Refer to the section below for details on correct pragma placement.) The Annotate pragma uses the following format:

pragma Annotate (GNATSAS, False_Positive|Intentional, "<check name>", "<review message>");

Reports of analysis made with this annotation no longer contain the corresponding message by default and, instead, list a manual review in the SAM file.

Warning

Since annotations are part of the code, they need to be written prior to an analysis to have an effect on the analysis' report: When writing a new annotation to review a message from the current analysis, you need to make a second analysis for the annotation to have an effect on the report.

Note that this pragma is ignored by the compiler when generating code, it only affects GNAT SAS' handling of generated messages, so you can safely add it to your source code without impacting compilation or run-time behavior. If for some reason pragma Annotate would be both recognized and not handled the same way by your Ada compiler, then you can safely replace pragma Annotate by pragma Gnat_Annotate.

When used in this way, an Annotate pragma takes exactly four arguments:

The identifier GNATSAS (for backward compatibility, CodePeer is also accepted).
One of two identifiers: False_Positive or Intentional.
- False_Positive indicates a situation where the condition in question cannot occur but GNAT SAS was unable to deduce this
- Intentional indicates that the condition can occur but is not considered to be a bug.
A string literal matching one of the message kinds listed in the tables presented in GNAT SAS Messages Reference.
A string literal which is used as the comment associated with the review of this message in the database.

The placement of the pragma in the source determines the messages (of the kind specified by the third argument) that it applies to. The pragma applies to messages associated with the preceding item in a statement or declaration list (ignoring other Annotate pragmas); if no such preceding item exists, then the pragma applies to messages associated with the immediately enclosing construct (excluding any portion of that construct which occurs after the pragma).

For a message saying that a subprogram always fails, the pragma can be placed either after the definition of the subprogram or at the start of the declaration part of the subprogram.

If unsure, you can use GNAT Studio to place the pragma at the correct place for you, see Annotating the source.

For the following example:

procedure Throw_Exception (Progr_Error : Boolean) is
begin
   if Progr_Error then
      raise Program_Error;
   else
      raise Constraint_Error;
   end if;
end Throw_Exception;

GNAT SAS generates the following message:

throw_exception.adb:1:1: high warning: subp always fails (Inspector): throw_exception always ends with an exception or a non-returning call

One way to handle this situation is to justify the message by adding an Annotate pragma as follows:

procedure Throw_Exception (Progr_Error : Boolean) is
   pragma Annotate (GNATSAS, Intentional, "subp always fails", "reviewed by John Smith");
begin
   if Progr_Error then
      raise Program_Error;
   else
      raise Constraint_Error;
   end if;
end Throw_Exception;

A better solution to this problem would be to use the pragma No_Return. Applying this pragma to the procedure Throw_Exception will prevent the display of the "subprogram always fails" message and in addition to this, it will provide a compiler check that there is no control-flow path that can reach the "end" of the procedure.

The message saying that a subprogram always fails may be emitted because of one or more messages saying that some errors always happen in the subprogram. Note that in this case, the "subprogram always fails" message must be explicitly justified by a dedicated pragma Annotate. The following example shows that to justify the message that a subprogram always fails, it is not enough to just justify the message about error(s) in the subprogram:

procedure Justified_Error_Inside (Progr_Error : Boolean) is
begin
   if Progr_Error then
      raise Program_Error;
   end if;
   pragma Assert (Progr_Error);  --  Justified error inside subprogram
   pragma Annotate (GNATSAS, Intentional, "assertion", "reviewed by John Smith");
end Justified_Error_Inside;

GNAT SAS still generates the message indicating the subprogram always fails:

justified_error_inside.adb:1:1: high warning: subp always fails (Inspector): justified_error_inside fails for all possible inputs

Similarly, for the following example:

function Func return Integer is
   X, Y : Integer range 1 .. 10000 := 1;
begin
   for I in 1 .. 123 loop
      X := X + ((3 * I) mod 7);
      Y := Y + ((4 * I) mod 11);
   end loop;
   return (X + Y) / (X - Y);
end Func;

GNAT SAS generates the following message:

func.adb:8:19: medium: divide by zero (Inspector): requires X /= Y

As it happens, this message is a false positive; the function will always safely return -4, but GNAT SAS is unable to deduce this fact.

One way to handle this situation is to justify the message by adding an Annotate pragma.

Consider adding a pragma as follows:

function Func return Integer is
   X, Y : Integer range 1 .. 10000 := 1;
begin
   for I in 1 .. 123 loop
      X := X + ((3 * I) mod 7);
      Y := Y + ((4 * I) mod 11);
   end loop;
   return (X + Y) / (X - Y);
   pragma Annotate (GNATSAS, False_Positive,
                    "Divide By Zero", "reviewed by John Smith");
end Func;

With this modification, GNAT SAS displays no message for this example.

In addition, if manual reviews are displayed (for example, if GNAT SAS is invoked with the --show review_kind+not_a_bug --show-reviews switches), the following is displayed:

func.adb:8:19: medium: divide by zero (Inspector): requires X /= Y. review: False Positive,
Not A Bug, approved by Annotate pragma at 9:4: reviewed by John Smith

Note

During analysis, GNAT SAS emits a warning when an Annotate pragma does not have any effect. It is possible to hide these warnings with the switch --no-unused-annotate-warning.

6.1.4. Viewing Reviews in the HTML Interface

Starting from CodePeer 23, the HTML interface allows you to browse the reviews, but no longer offers the possibility of adding reviews. The review status is shown in a dedicated column of the Messages panels, and the review history can be displayed by clicking on the icon in the rightmost column of the message line.

6.1.5. Custom Review Status

It is possible to define your own review statuses for special needs. In order to define one you first need to select a review status kind. There are three kinds: Pending, Not_A_Bug and Bug. The review status kind impacts the behavior of the user interface: by default, GNAT SAS hides (in textual and HTML output as well as in GNAT Studio) any messages that have a review with a review status of kind Not_A_Bug. In addition, in the Locations View GNAT Studio highlights the messages with a review, using one particular color per review status kind.

Once you have selected a kind, you can define your custom review status in your project file with the project attribute corresponding to the selected kind among: Pending_Status, Not_A_Bug_Status and Bug_Status, e.g.:

project Proj is
   package Analyzer is
      for Pending_Status use ("To Do", "Don't know");
      for Not_A_Bug_Status use ("To Be Dealt With Later", "Don't care");
      for Bug_Status use ("To be fixed ASAP", "Problem");
   end Analyzer;
end Proj;

Default review statuses map to the following review status kinds (status -> kind):

pending -> pending
bug -> bug
not_a_bug, false_positive, intentional -> not_a_bug

Note that custom statuses can be set from the GNAT Studio interface with the project editor menu Edit ‣ Project Properties....

6.2. Improve Your Code Specification

In some cases, it may be better to annotate the Ada code directly, providing additional information to help going further in the analysis and help also clarify the intent of the code.

Ada provides various ways to improve the specification of the code and thus allowing static-analysis tools to reason on additional information. For example:

explicit range given on types, subtypes and variables
explicit assertions written in the code via pragma Assert or pragma Assume
explicit annotations written in the code via pragma Annotate
pre and post conditions
predicates and invariants

Note

Note that pragma Annotate is ignored by the compiler when generating code, so is only taken into account by GNAT SAS.

6.2.1. Using Pragmas Assert and Assume

Note

pragma Assert is supported by both Inspector and Infer, and has no effect on the analysis of other engines.
pragma Assume is only supported by Inspector.

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

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

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

6.2.2. Pragma Annotate / Modified in Source Code

Note

The approach described in this section is only supported in the Inspector and Infer engines and will only affect messages reported by those.

Pragma Annotate can also be used in another way to help cope with the problem of incorrect message generation. Suppose, for example, that the analysis engine somehow becomes confused about the value of a variable at some point in a program and consequently generates incorrect messages. Pragma Annotate / Modified can be used to tell the engine to assume that (at the point where the pragma is placed) a given object is fully initialized and that nothing else should be assumed about the value of that object; any previous deductions that have been made about the value of the object at the point of the pragma should be discarded. Note that this means that Inspector and Infer can issue false positive messages stemming from the fact that they assume that the object can have any value after the location of the pragma.

This is illustrated by the following examples:

procedure Proc1 is
begin
   -- Before the call to Initialize_Global_Variable_1,
   -- Global_Variable_1 is correctly known to be uninitialized.
   Initialize_Global_Variable_1;
   -- Suppose that Global_Variable_1 is initialized by the preceding
   -- call, but for some reason Inspector fails to realize that and
   -- therefore incorrectly assumes that Global_Variable_1 remains
   -- uninitialized after the call. The pragma corrects this mistaken
   -- assumption.
   pragma Annotate (GNATSAS, Modified, Global_Variable_1);
   -- Because of the pragma, no false positive message about reading
   -- an invalid value will be generated when Global_Variable_1 is
   -- passed as a parameter in the following call.
   Some_Procedure (In_Mode_Parameter => Global_Variable_1);
end Proc1;

procedure Proc2 (Count : in out Natural) is
begin
   Global_Variable_2 := 0;
   Update_Global_Variable_2;
   -- Suppose that Global_Variable_2 is updated by the preceding call,
   -- but for some reason Inspector fails to realize that and
   -- therefore incorrectly assumes that Global_Variable_2 still has the
   -- value zero after the call.
   pragma Annotate (GNATSAS, Modified, Global_Variable_2);
   -- Because of the pragma, the assignment to Count will not be
   -- incorrectly identified as dead code.
   if Global_Variable_2 /= 0 then
      Count := Count + 1;
   end if;
end Proc2;

When used in this way, an Annotate pragma takes exactly three arguments:

The identifier GNATSAS (for backward compatibility, CodePeer is also accepted).
The identifier Modified.
A name denoting a stand-alone object or a parameter.

Such an Annotate pragma is subject to the same placement restrictions as an Assert pragma (roughly speaking, such a pragma shall only occur within a statement list or a declaration list).

6.2.3. Pragma Annotate / Identifying Race conditions

Note

The option described in this section is only supported in the Inspector engine and will only affect its messages.

In deep analysis mode, the pragma Annotate can also be used to aid Inspector in identifying tasks and race conditions with one of the following pragmas:

pragma Annotate (GNATSAS, Single_Thread_Entry_Point|Multiple_Thread_Entry_Point, "entry point");

pragma Annotate (GNATSAS, Mutex, "lock subprogram", "unlock subprogram");

6.2.4. Using Pre and Post conditions

Note

Using pre/post conditions as described in this section will only impact Inspector's analysis. Other engines will ignore them.

Taking the GNAT Studio demo located under <GNAT Studio install>/share/examples/gnatstudio/demo as an example, and running it under GNAT SAS via:

$ gnatsas analyze -P demo --mode deep
$ gnatsas report text -P demo --show-backtraces

will generate in particular a potential array index check failure.

input.adb:258:31: low: precondition <array index check> [CWE 120] (Inspector): precondition might fail on call to input.get_char; requires (if First_Char <= Last_Char then First_Char else 1) <= 1_024
   array index check at input.adb:110:12

Instead of hiding the error, we're going to extend the contract of the subprogram Get_Char so that we can make sure the callers are correct.

First, let's look more closely at the subprogram itself:

function Get_Char return Character is
   C : Character;

begin
   --  First check if the line is empty or has been all read.

   if End_Line then
      Read_New_Line;
   end if;

   C := Line (First_Char);
   First_Char := First_Char + 1;

   return C;
end Get_Char;

The potential error occurs on the access to the element of Line at line 110, where First_Char might not be smaller or equal to 1024. So instead of removing this error, we're going to provide as a precondition of Get_Char the fact that the value has to be within expected range:

function Get_Char return Character;
pragma Precondition (First_Char <= 1_024);

Note

Note that the above is using a pragma so that this syntax can be used with any Ada compiler (the pragma will basically be ignored by non-GNAT compilers).

If you are using an Ada 2012 compiler then the following syntax is preferred:

function Get_Char return Character
  when Pre => First_Char <= 1_024;

Re-running GNAT SAS will remove the error. Now First_Char is assumed to be below 1024 and thus there is no potential error.

Note

Note that with GNAT, this pragma does not have any effect on the executable code by default - it is just here for documentation purposes and used by the additional tools. However, when using the GNAT compiler, a corresponding dynamic check can be added when e.g. compiling with the -gnata switch.

Warning

Although the capability of writing assertions or pre/post conditions may generally sound promising to users, please be aware that there are tool limitations and such complex conditions may not always help the analysis. For example, the use of quantified expressions such as for all I in F'Range => F(I) in 1..100 might not be understood by Inspector in all cases, but simple preconditions about some elementary-type global variable or parameter being in a certain range, or being non-null, would be fully understood. Combining such simple preconditions with and would also be fully understood.

The way pre/post conditions are being used by Inspector can be viewed by displaying annotations in the GNAT SAS report:

$ gnatsas report text -P demo --show kind+annotation

input.adb:101: (pre)- input.get_char:(user precondition, overflow check) First_Char <= 1_024

or in context within the source file, using GNAT Studio:

--
--  Subprogram: input.get_char
--
--  Global_outputs:
--    First_Char, Last_Char, Line(1..1_024), Line_Num
--
--  Pre:
--    First_Char <= Last_Char or Line_Num /= 2_147_483_647
--    First_Char <= 1_024
--
--  Post:
--    possibly_updated(Line(1..1_024))
--    input.get_char'Result'Initialized
--    Line_Num'Initialized
--    Line_Num = One-of{Line_Num'Old, Line_Num'Old + 1}
--    Last_Char /= 0
--    First_Char in 2..1_025
--    First_Char = One-of{First_Char'Old, 1} + 1
--
--  Global_inputs:
--    First_Char, Last_Char, Line, Line_Num
--
function Get_Char return Character is
   C : Character;

begin
   --  First check if the line is empty or has been all read.

   if End_Line then
      Read_New_Line;
   end if;

   C := Line (First_Char);
   First_Char := First_Char + 1;

   return C;
end Get_Char;