1. Introduction

1.1. About GNAT SAS

GNAT SAS is the GNAT Static Analysis Suite. It is a set of analysis engines with complementary capabilities, that are able to detect a range of issues spanning from breaking coding style standards to deep logic errors.

GNAT SAS is designed to support large systems and to detect a wide range of programming errors such as misuse of pointers, indexing out of arrays, buffer overflows (a prevalent source of security storage leaks), numeric overflows, numeric wraparounds, and improper use of Application Programming Interfaces (APIs). It pinpoints the root cause of each error down to the source line of code.

GNAT SAS enables finding defects early in the development process in conjunction with compilation when they are least costly to repair. In addition, it should be run on existing code to find latent defects before they become a problem in the field.

One of the strengths of GNAT SAS is its ability to analyze partial systems (e.g. libraries, incomplete set of sources, etc.) and make reasonable assumptions about functions that are not visible.

Another strength is GNAT SAS' capability to compare each new run to a selected baseline run. This allows users to ignore initial messages on an existing code base, and concentrate on new messages only detected as part of code changes. GNAT SAS also provides advanced capabilities to filter and review generated messages.

In addition, GNAT SAS supports analysis of Ada code written for many different Ada compilers via the configuration of a project file, see Ensuring compatibility with GNAT SAS.

An analysis may be launched from the command line for easy scripting and automation, or interactively using the GNAT SAS integration in GNAT Studio. The analysis results can be output in various formats (e.g. text, CSV, Code Climate, SARIF, HTML).

GNAT SAS stores its analysis results in Message files with a .sam extension, and user reviews in a Review file with a .sar extension, as explained in GNAT SAS Files Reference.

1.2. Features Overview

Integration of multiple analysis engines

GNAT SAS currently integrates four analysis engines, providing a rich set of complementary checks, and lets the user baseline and review their messages in a uniform way. Each engine can be individually configured for more precise analysis.
Analysis modes

GNAT SAS provides two analysis modes, fast and deep. Fast mode offers the best precision/performance trade-off, with fewer messages but less false positives. It is suitable for quick development workflows. Deep mode will output more precise messages but at the expense of reporting more false positives and taking more execution time.
Incrementality

The GNAT SAS analysis is fully incremental when run in fast mode. This means that during the first run all files will be analyzed, while only modified source files will be analyzed during subsequent runs. In deep mode, the Inspector engine will lose incrementality, but other engines will still run incrementally.
Configurable analysis scope

The GNAT SAS analysis can be easily configured to target various scopes, such as the full closure of a project, all sources in a project tree, or individual files. See Partial Analysis for more details.
Advanced reporting capabilities

GNAT SAS provides multiple report formats, from simple text or Comma-Separated Values (CSV) to standard formats such as CodeClimate or SARIF, enabling advanced CI integration workflows. GNAT SAS also provides comparison between subsequent runs or arbitrary ones. All this is also available within GNAT Studio. See Viewing Results for more details.
Review capabilities

GNAT SAS provides several ways to review the messages, graphically in GNAT Studio, using CSV files or using source code annotations. Those reviews can then be easily versioned and shared between multiple users when necessary. See Reviewing Messages for more details.
Full integration with GNAT Studio

GNAT SAS has full integration support within the GNAT Studio IDE, to run analyses, display reports, compare runs and review results. This is documented in Using GNAT SAS in GNAT Studio.

1.3. Integrated Analysis Engines

GNAT SAS includes several analysis engines providing together a rich set of checks. This section describes each engine at a high-level.

1.3.1. Inspector

Inspector is designed to follow numerical computations in a very precise way and thus excels in detecting possibly failing run-time checks as well as wide range of logical errors. Inspector guarantees full path coverage.

Even in the absence of explicit errors, Inspector provides a thorough characterization of every component of the system in terms of the preconditions on the inputs necessary to preclude run-time failures, the presumptions about return values of external subprograms, the postconditions that characterize the range of outputs, and heap object creations.

Inspector uses partitioning in its analysis. It usually gains in precision when using bigger partitions, including when switching from fast to deep mode. The downside of bigger partitions is an increase in Inspector's analysis time. Furthermore, messages are aggressively filtered in fast mode. This means that deep mode will display more messages, but they may contain more false positives.

Importantly, the same kinds of errors are searched in both modes.

Fast mode

Inspector analyzes each library unit separately. This allows Inspector's analysis to be incremental: when re-analyzing a project, only the units that have changed will need to be re-inspected.

Inspector is able to precisely follow function calls when the caller and the callee are in the same file. For other function calls, the effects of the call are approximated.

Deep mode

Inspector performs the analysis by group of units, whose size depend on factors depending on Partitioning of Analysis. The analysis will start from scratch each time, losing incrementality, but it will be more thorough overall.

In deep mode, Inspector is able to precisely follow all function calls in the same partitions.

In addition, Inspector also provides detection of race conditions.

For information about how Inspector works internally, see How Does Inspector Work?.

1.3.2. Infer

The Infer framework, specialized to Ada by AdaCore, is designed to provide fast analyses with a very low false positive rate. Infer analyses can precisely follow different paths in the program even across function calls including calls to functions in different files. Infer is thus especially good in detecting problems occurring on certain program paths, such as null-pointer dereferences or memory leaks, and providing precise and comprehensible explanations of these problems.

Infer analysis is fully incremental with respect to previous runs.

1.3.3. GNAT Warnings

GNAT Warnings provides warnings issued by the GNAT compiler frontend. This includes warnings about suspicious constructs and warnings about situations when the compiler is sure an exception will be raised at run-time. This can be especially useful if you are using a different compiler for compilation of your code. Even if you are using GNAT, you can activate more warnings when running GNAT SAS and then use GNAT SAS' filtering and reviewing capabilities to select interesting messages.

1.3.4. GNATcheck

GNATcheck provides automated checking for suspicious code constructs and compliance with organizational and project-specific coding standard rules. This includes coding style rules, feature restriction rules, and metric compliance rules. GNATcheck provides a wide range of predefined rules and also makes it possible to define new rules.

1.4. Installation

1.4.1. Prerequisites

1.4.1.1. System Requirements

Static error detection is complex and time consuming, so GNAT SAS will benefit from all the speed (CPU) and memory (RAM) that can be made available.

Even though any machine can run GNAT SAS these days, in order to get the most out of GNAT SAS, you will need to use a powerful machine with many cores and memory. A comfortable setup for a GNAT SAS server is a machine with 16 physical cores or more, with at least 64GB of memory (4GB per core) running a 64bits GNAT SAS.

For a desktop machine a minimum of 4 cores is recommended (8 preferred) with at least 4GB per core (so 16 to 32GB).

Note that using local and fast drives will also make a difference in terms of analysis and storing results. Network drives such as NFS, SMB or worse, configuration management filesystems (such as ClearCase dynamic views) should be avoided as much as possible and will produce very degraded performance (typically 2 to 3 times slower than on local fast drives). If such slow drives cannot be avoided for accessing the source code, you can still configure your project file so that the object directory for GNAT SAS' analysis is stored on a drive local to the machine performing the run. This can be achieved by setting the Object_Dir project attribute, see Analyzer package attributes for more details.

1.4.1.2. Installing GNAT Studio (optional)

The GNAT Studio IDE provides great integration of the GNAT SAS tool, allowing users to easily analyze their projects, display reports and review the results as described in Using GNAT SAS in GNAT Studio. Please refer to the GNAT Studio documentation for installation and use instructions.

Note that using GNAT Studio is optional as GNAT SAS is fully usable through the Command-Line Interface and provides various means and formats to output the results and review them.

1.4.2. Installation under Windows

Run the GNAT SAS installer, e.g. by double clicking on gnatsas-VERSION-x86_64-windows-bin.exe.

You should have sufficient rights for installing the package (administrator or normal rights depending on whether it is installed for all users or a single user).

The GNAT SAS installer can also be run from the Windows command line with the switches /D, to select the installation directory, and /S, to perform unattended installation.

1.4.3. Installation under GNU/Linux

Extract the GNAT SAS installer package and run the .doinstall script as below:

$ tar -xvf gnatsas-{VERSION}-x86_64-linux-bin.tar.gz $ cd
gnatsas-{VERSION}-x86_64-linux-bin $ ./doinstall

Note that you need to have sufficient rights for installing the package at the chosen location (e.g. root rights for installing under /opt/gnatsas).