13. FAQ

13.1. Migrating Away from the Historical CodePeer Database

Starting with GNAT SAS 24.0w (20230404), GNAT SAS's historical database is replaced by a set of files, the most important ones being the SAM and SAR files, that store GNAT SAS's messages and reviews, respectively (see Message Files).

After updating and when running GNAT SAS, a user with a historical database will be prompted to import its database before doing any new analysis. This is done with the sam-from-db tool. To remove the migration message, simply move (or remove) the database codepeer/<prj>.db/Sqlite.db. Similarly, if the project file contains a CodePeer package, the user is prompted to migrate it to the new Analyzer package (see Ensuring compatibility with GNAT SAS) before doing any new analysis.

This move away from the database implies the following changes:

  • GNAT SAS does not maintain a full history of analysis anymore.

    • However, it is now easy to save the results of a particular run, by simply saving the associated SAM file (see GNAT SAS Files Reference).

    • We encourage users to version the SAM files along with their sources, this way the analysis results can be kept in sync with a given revision of the corresponding sources.

  • The IDE server is discontinued.

    Users should do reviews locally (from scratch or from a copied SAR, see Reviewing Messages), and update their changes. Concurrent reviewing can be handled with the merge-reviews tool, see Importing and Sharing GNAT SAS User Reviews.

  • The run id notion is now replaced by SAM files themselves. The --current switch that took a run id as an argument is replaced by the capability to display an arbitrary SAM file with gnatsas report <sam-file>. Similarly, --set-baseline-id is replaced by gnatsas baseline --set-baseline <sam-file>.

Switching to SAM/SAR files introduces a lot of flexibility with regard to result and review sharing, run comparison, backups, as well as advanced workflows setup. All that while keeping the gist of the historical database: baselines, run comparison, and reviews.

In addition, this complete re-implementation of the GNAT SAS pipeline results in sizable speed up in particular when storing results or generating reports of any format.

13.1.1. GNAT SAS Switches Changes

GNAT SAS 24.0 implements a new command line interface. It is possible to convert your old codepeer commands to the new gnatsas commands by just running your old codepeer command and following the instructions that are printed.

You can learn more about GNAT SAS' command line switches by passing the --help switch to gnatsas and its various subcommands, e.g. gnatsas analyze --help will print the analyze's command help, while gnatsas report --help will print the report's command help.

See also

See GNAT SAS CLI Reference for more information about available command-line switches.

Additionally, you should make sure that the Switches listed in the CodePeer package of your project files are adapted to the new Switches syntax of the new Analyzer package, check Ensuring compatibility with GNAT SAS for more information.

13.1.2. sam-from-db

The sam-from-db tool is a tool to extract data from a CodePeer historical database and generate SAM and SAR files from it.

The default invocation is:

$ sam-from-db -P <prj>.gpr

You should add any -X or --subdirs switch that you use with CodePeer to this command line.

This extracts, for each analysis level in the database, a pair of SAM files for the baseline run and the last run, as well as a SAR file containing all reviews associated to the exported messages. Once extracted, the tool puts the files in the output directory of your project, and writes the prj.runs_info.json file that contains the levels information.

See also

See also GNAT SAS Files Reference.

Warning

GNAT SAS does not have analysis levels, instead it has two analysis modes, namely fast analysis mode and deep analysis mode (see Analysis modes). Data from each legacy CodePeer analysis level is exported in a timeline with the level number as name (see Timelines). As a result, the imported results are not directly available through the GNAT SAS analysis modes. In order to get the imported results with an analysis mode, you can either:

  • use the --set-baseline and --set-current switches with, e.g.:

    gnatsas baseline -P<prj> --set-baseline <output_dir>/<prj>.1.baseline.sam --set-current <output_dir>/<prj>.1.sam

    (see Comparing GNAT SAS Runs and Importing GNAT SAS Results),

  • or directly use the imported timeline, e.g., use:

    gnatsas report -P<prj> --timeline 1

    or

    gnatsas analyze -P<prj> --mode fast --timeline 1

    Adding --timeline 1 to a gnatsas command puts this command in the context of the imported CodePeer level 1 analysis.

If sam-from-db is not able to locate your database, or if you want to specify a custom path, use the --db-path switch to manually set it.

Warning

sam-from-db does not extract all the information stored in the database. By default, it only extracts the baseline and last run of each analysis level.

You can use this tool to do selective exportation with either:

  • --level <level> to only export one level,

  • --run-id <id> to only export one run-id (requires --level),

  • --reviews-only to only export reviews.

If one of those switches is set, sam-from-db generates the specified files in the current directory, or --out-dir if set, and exits.

13.1.2.1. Tool Limitation with GNATcheck's Messages

Due to a change in the way GNATcheck messages are stored, GNAT SAS is not able to properly identify a GNATcheck message from a database import with one from a new run. As a result, when you use a SAM file generated from the database as a baseline, all GNATcheck messages from the database are marked as Removed, and all the ones from the current run are marked as Added. The problem disappears once the baseline is updated.

13.2. What is the Difference between GNAT SAS and SPARK?

Static analyzers fall into two broad categories: bug finders and verifiers. Bug finders detect violations of properties. Verifiers guarantee the absence of violations of properties. Because they target opposite goals, bug finders and verifiers usually have different architectures, are based on different technologies, and require different methodologies.

Typically, bug finders require little upfront work, but may generate many false alarms which need to be manually triaged and addressed, while verifiers require some upfront work, but generate fewer false alarms.

GNAT SAS belongs to the bug finder category, while SPARK belongs to the verifier category.

In other words, if you want to assess the quality of your code and detect potential run-time or security errors for manual review in Ada code then GNAT SAS is the right tool.

If you want instead to guarantee absence of run-time or security errors automatically and demonstrate useful properties of your application then SPARK is the right tool.

13.3. What is the difference between GNAT SAS Messages and Compiler Warnings?

A question asked by some users is: Why not just use the compiler? The Ada compiler generates warnings, so what added value does GNAT SAS bring?.

It is true that Ada compilers (and in particular GNAT) generate warnings, and these warnings are useful, but they are definitely not comparable to what GNAT SAS' Inspector and Infer engines can achieve for several fundamental reasons:

  • Most messages generated by Inspector and Infer are not considered at all by Ada compilers beyond really obvious cases (e.g. all potential cases of run-time errors are not flagged by Ada compilers, detection of race conditions, etc...)

  • Compilers in general will do no or little data and control flow tracing to emit warnings. GNAT SAS, and in particular Inspector, performs full data and control flow tracing as explained in How Does Inspector Work?.

  • Compiler warnings operate only on a single subprogram (or in the best cases, single unit), while Inspector and Infer do interunit analysis and propagate information from one unit to the other.

  • Inspector and Infer will keep much more precise track of values of e.g. individual fields or array elements and generate more precise messages as a result.

GNAT SAS also comes with many additional capabilities not available in compilers such as baselines, the ability to generate contracts for subprograms, etc...

Finally, when using GNAT SAS you can decide to take advantage of GNAT Warnings via the --gnat switch, see Configuring GNAT Warnings for more details.

13.4. Common Issues

13.4.1. Compilation Errors

Note

This section only applies to GNAT-based engines (i.e. Inspector and GNAT Warnings).

GNAT-based engines may issue compilation errors during the GNAT SAS analysis, but that does not always prevent completing the analysis since both Inspector and GNAT warnings are able to partially analyze projects with these errors. Inspector needs a file to be compilable to analyze it, but analyzes the rest of the files treating the calls to subprograms defined in the files with compilation errors as Calls to Unknown Subprograms. GNAT Warnings can in some cases partially analyze even files with compilation errors.

A compilation error can be caused either by the fact that the code is not valid Ada code and cannot be compiled by GNAT compiler or by the fact that that project is not properly set up.

To resolve compilation errors due to improper setup, see the instructions in the section Ensuring compatibility with GNAT SAS.

In the case of invalid Ada code, you can resolve the compilation error either by fixing the code or by excluding the file from the compilation using the Excluded_Source_Files attribute in the top-level of the project:

project Work  is
  ...
  for Excluded_Source_Files use ("pack.adb");
  ...
end Work;

Note

Using this attribute at the project level is different from using it in the Analyzer package as described in the section Partial Analysis. When the attribute is used in the Analyzer package, the file is still compiled.

Warning

There are limitations to this exclusion mechanism. In particular, as mentioned in Inspector-specific handling:

  • It is problematic to do this for specification files since excluding them may cause compilation errors in all the files depending on them.

  • Excluding a file at the project level has an impact on Inspector's incremententality.