2. Getting Started

This chapter provides a quick introduction to GNAT SAS by illustrating the main concepts: analysis, report and review. The user is guided through a simple command-line example which does not require any particular configuration.

Note

This chapter assumes that:

• the user environment is a bash terminal;

• GNAT SAS has been installed according to Installation.

It also provides links to more advanced resources in More Resources.

The chapter does not try to cover all features or more advanced use cases. Refer to other chapters for more comprehensive documentation.

2.1. Quick Start example

This section will illustrate how to run an analysis with GNAT SAS and view the analysis results, before showing how results can be reviewed and the code fixed.

Let's first change the directory to the directory containing our example project <INSTALL_DIR>/share/examples/gnatsas/uninitialized/:

$ cd <INSTALL_DIR>/share/examples/gnatsas/uninitialized/

This example namely contains:

• a README file

• a GPR project file uninitialized.gpr (if that is new to you, refer to Creating a Project File).

• Ada source code (*.adb/*.ads files).

The project file is configured to use uninit.adb as the main unit, and to use GNAT SAS in deep mode.

See also

Refer to Analysis modes for a description of the fast and deep modes provided by GNAT SAS.

2.1.1. Analyzing the project

To analyze the project, run the gnatsas analyze command by specifying the name of the project file (the extension is optional):

$ gnatsas analyze -P uninitialized

[gnatsas]: launching GNATcheck
[gnatsas]: launching Infer
[gnatsas]: launching Inspector
Compile
   [Ada]          uninit.adb
   [Ada]          adt.adb
Bind
   [gprbind]      uninit.bexch
   [Ada]          uninit.ali
no partitioning needed.
starting the analysis of adt.scil
analyzed adt.scil in 0.00 seconds
starting the analysis of adt__body.scil
analyzed adt__body.scil in 0.00 seconds
re-starting the analysis of adt.scil
re-analyzed adt.scil in 0.00 seconds
starting the analysis of uninit__body.scil
analyzed uninit__body.scil in 0.00 seconds
starting the analysis of uninit.scil
analyzed uninit.scil in 0.00 seconds
starting the analysis of b__uninit.scil
analyzed b__uninit.scil in 0.00 seconds
starting the analysis of b__uninit__body.scil
analyzed b__uninit__body.scil in 0.00 seconds
re-starting the analysis of b__uninit.scil
re-analyzed b__uninit.scil in 0.00 seconds
analysis complete.
6 .scil files processed; 14 subprograms analyzed.

In the above output, we can see that GNAT SAS launched the following integrated engines and returned successfully (with exit code 0):

• GNATcheck

• Infer

• Inspector

There is some verbose output, in particular about the Inspector analysis, telling us that some files were compiled, and 14 subprograms were analyzed in total.

Upon analysis GNAT SAS analysis artifacts were generated and stored under a directory gnatsas, which in particular contains the output directory gnatsas/uninitialized.outputs (hereafter referred to as <output_dir>). That directory contains important files among others:

• a Message file containing messages found during the current analysis run: uninitialized.deep.sam

• the baseline for this run: uninitialized.deep.baseline.sam.

However, gnatsas analyze does not directly display the results. That is done by the gnatsas report command as we will see next.

Note

The version of engines in the output (e.g. gnatcheck 25.0w (20231112) may vary depending on the GNAT SAS version).

See also

• Refer to Analyzing Code for a comprehensive description of GNAT SAS analysis.

• Refer to GNAT SAS Files Reference for a description of GNAT SAS artifacts.

2.1.2. Viewing the results

2.1.2.1. Printing the text report

The resuts from the Message file <output_dir>/uninitialized.deep.sam can be displayed with the gnatsas report command that is run similarly by specifying the project file name:

$ gnatsas report -P uninitialized

which outputs the following list of messages in text format on standard output:

uninit.adb:7:4: high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update`
uninit.adb:7:4: medium: precondition <overflow check> [CWE 190] (Inspector): precondition might fail on call to adt.update; requires not X.B1 or X.DZ /= Integer_32'Last

The messages are formatted such as:

filename:line:column: rank: kind (analysis engine name): message contents

Here, for instance, the first message is emitted by Infer, has a high ranking, and is reported on uninit.adb at line 7, column 4:

with ADT; use ADT;

procedure Uninit is
   T : ADT_Type;
begin
   Initialise (T);
   Update (T); -- high validity check reported here
end Uninit;

The kind of the message is validity check [CWE 457], which means that GNAT SAS reports a potential error due to accessing an uninitialized variable. The [CWE 457] part indicates that this kind of message has the identifier 457 in the Common Weakness Enumeration (CWE); it is optional, not all messages can be linked to a CWE weakness.

The description of the specific potential violation corresponding to this kind is detailed in the message contents that lets us know that X.B1 is read without initialization when calling adt.update. Note that this is an example of performing analysis across multiple units.

Note

Such check requiring cross-unit analysis can only be done in deep mode with the Inspector engine (the analysis mode only influences the results of Inspector and the result of Infer is not impacted). If you want to compare to the results in fast mode, you can quickly run:

$ gnatsas analyze -P uninitialized --mode=fast
$ gnatsas report -P uninitialized

That will only report the Infer message.

Indeed, if we look at how the body of adt.adb, we can see that X.B1 is never initialized:

package body ADT is

   ----------------
   -- Initialise --
   ----------------

   procedure Initialise (X :  out ADT_Type) is
   begin
      X.V1 := 1;  --  we didn't initialize X.B1 nor X.DZ
   end Initialise;

   ------------
   -- Update --
   ------------

   procedure Update (X : in out ADT_Type) is
   begin
      if X.B1 then          --  read uninitialized field X.B1
         X.V1 := X.V1 +2;
         X.DZ := X.DZ +1;   --  read uninitialized field X.DZ
      end if;
   end Update;

end ADT;

See also

• We will not describe other messages here; refer to GNAT SAS Messages Reference for more information about all supported checks and related message kinds.

• For more information about the CWEs supported by GNAT SAS, refer to CWE Categorization of Messages.

• In this example the results are reported as text, but GNAT SAS supports various other formats (e.g. CSV, SARIF...). Refer to Viewing Results for a comprehensive description of GNAT SAS reporting capabilities.

2.1.2.2. Looking at backtraces

Messages reported by GNAT SAS may contain even more details, by showing us the backtraces associated to the potential issues. To enable displaying backtraces, simply run with --show-backtraces:

$ gnatsas report -P uninitialized --show-backtraces

The first message is now reported as:

uninit.adb:7:4: high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update`
   struct field address `B1` created at uninit.adb:4:4
   when calling `adt.update` here at uninit.adb:7:4
      parameter `X` of adt.update at adt.adb:16:4
      read to uninitialized value occurs here at adt.adb:18:10

The backtrace provides more information:

• first, X.B1 is created as a record field when declaring the variable T with type ADT_Type in uninit.adb:4:4

• then T is passed as argument to ADT.Update where the corresponding formal parameter X has its field X.B1 read without initialization in adt.adb:18:10.

See also

Refer to GNAT SAS CLI Reference for more information about command-line switches.

2.1.2.3. Filtering messages

The gnatsas report command also supports advanced filtering of messages. For example, say that as a first step, we are only interested in seeing messages of high ranking. This is specified with --show rank=high:

$ gnatsas report -P uninitialized --show rank=high

Only high ranked messages are reported (one in this case):

uninit.adb:7:4: high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update`

See also

• The --show switch provides much flexibility. See Filtering Messages for a full description.

• The ranking described above corresponds to a message categorization done by GNAT SAS, depending on how interesting and likely to happen they are. See Categorization of Messages.

2.1.3. Reviewing the results

2.1.3.1. Triaging

The first step of a review is to "triage" the message depending on its nature: false positive, intentional violation, or actual bug. Then, depending on the use cases, the review information may be shared with other developers, validated, before the code is fixed if needed. Or you may want to fix the code directly if the error is introduced in your development branch.

See also

Refer to Workflows for example use cases and recommended workflows.

In this example, we'll consider the case where we want to store the review information. We will use the review through CSV file method to review the first message described above, which we already identified as being a bug. Following this method we will:

• output messages in CSV format

• add the review information to the CSV file

• tell GNAT SAS to import the review information.

First, let's output only the Infer messages with high ranking, this time in a CSV format using gnatsas report csv, and store them in a file messages.csv with the -o switch:

$ gnatsas report csv -P uninitialized --show rank=high,tool=infer -o messages.csv

messages.csv contents is as below, containing exactly one message in this example:

project,basename,path,subp,line,column,category,history,ranking,tool,message,cwe,kind,related_checks,key,key_seq,review_from_source,review_kind,review_date,review_status,review_author,review_text
uninitialized.gpr,uninit.adb,uninit.adb,uninit,7,4,check,unchanged,high,Infer,`X.B1` is read without initialization during the call to `adt.update`,457,validity check,,6c2d263aed531f7fcb81e1f2c3a864c6,1,false,uncategorized,,,,

Now, let's modify the fields, then save the modified file as reviews.csv:

• review_status with bug

• review_author with your name (e.g. Jules Verne)

• review_text with a comment (e.g. Missing initialization of ADT_Type.B1 field).

which now contains:

project,basename,path,subp,line,column,category,history,ranking,tool,message,cwe,kind,related_checks,key,key_seq,review_from_source,review_kind,review_date,review_status,review_author,review_text
uninitialized.gpr,uninit.adb,uninit.adb,uninit,7,4,check,unchanged,high,Infer,`X.B1` is read without initialization during the call to `adt.update`,457,validity check,,6c2d263aed531f7fcb81e1f2c3a864c6,1,false,uncategorized,,bug,Jules Verne,Missing initialization of ADT_Type.B1 field

Finally, let's inform GNAT SAS about this new review information with the gnatsas review command:

$ gnatsas review -P uninitialized --from-csv reviews.csv

[gnatsas | review]: reviews imported

The output directory should now contain a Review File named <output_dir>/uninitialized.sar containing the review information in a GNAT SAS format.

Let's display again the messages (e.g. as text with --show-reviews) to confirm that the review has been associated to the corresponding message:

$ gnatsas report -P uninitialized --show-reviews

uninit.adb:7:4: high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update`. review: 2023-11-30 13:05:42: Bug, Bug, approved by Jules Verne: Missing initialization of ADT_Type.B1 field
uninit.adb:7:4: medium: precondition <overflow check> [CWE 190] (Inspector): precondition might fail on call to adt.update; requires not X.B1 or X.DZ /= Integer_32'Last

As you can see above, the first message now has review information available.

See also

Refer to Reviewing Results and Improving Code for a comprehensive description of the reviewing capabilities in GNAT SAS.

2.1.3.2. Fixing the code

Now that we have examined the first message reported and triaged it as a bug with relevant review information, let's fix it by editing the Initialize procedure in adt.adb to initialize X.B1:

package body ADT is

   ----------------
   -- Initialise --
   ----------------

   procedure Initialise (X :  out ADT_Type) is
   begin
      X.V1 := 1;
      X.B1 := True;  -- fixed
   end Initialise;

Let's run the analysis again and display the results (filtering Infer messages only for the example) to confirm that the issue has been fixed:

$ gnatsas analyze -P uninitialized
$ gnatsas report -P uninitialized --show tool=infer

uninit.adb:7:4: [added] high: validity check [CWE 457] (Infer): `X.DZ` is read without initialization during the call to `adt.update`

The first message related to the missing initialization of X.B1 has disappeared from the output and we now have another message related to a similar issue with X.DZ, showing as [added].

2.1.3.3. Comparing runs

Another useful GNAT SAS feature is the capability to compare analysis runs. By default, gnatsas report will automatically compare the results of the analysis with the results of the previous run (of the same timeline, see Timelines for more details). This is why the new message was tagged as [added].

We can also force the display of removed messages with --show age+removed:

$ gnatsas report -P uninitialized --show tool=infer,age+removed --show-reviews

The list of messages now shows the previously fixed message as [removed]:

uninit.adb:7:4: [removed] high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update`. review: 2023-11-30 13:05:42: Bug, Bug, approved by Jules Verne: Missing initialization of ADT_Type.B1 field
uninit.adb:7:4: [added] high: validity check [CWE 457] (Infer): `X.DZ` is read without initialization during the call to `adt.update`

See also

• See Filtering Messages for a full description of the --show switch.

• You may also compare arbitrary runs; refer to Comparing GNAT SAS Runs for more details.

2.2. More Resources

• Several other example projects are available:

  • under <GNAT_SAS_INSTALL_DIR>/share/examples/gnatsas

  • or via the Help ‣ GNATSAS ‣ Examples menu in GNAT Studio.

• For an advanced tutorial focusing particularly on the use of GNAT SAS in GNAT Studio and on the Inspector analysis engine, refer to the GNAT SAS tutorial available:

  • under <GNAT_SAS_INSTALL_DIR>/share/doc/gnatsas/tutorial

  • or via the Help ‣ GNATSAS ‣ GNATSAS Tutorial menu in GNAT Studio.