CodePeer 22 Release Notes¶

We present here a few highlights of the new features in CodePeer 22. You can access the complete list here.

Full re-implementation of level 0 ¶

The CodePeer team has entirely rewritten the implementation of level 0 analyses on top of an existing platform, paving the way for future exciting extensions. The new level 0 analysis is based on the Infer technology, developed by Facebook, and enriched with an Ada front end written by AdaCore.

This new level 0 already brings some improvements. Among them:

Analysis time should be significantly improved, thanks to the use of a compiled language.
Both the Linux and Windows versions take advantage of CPU-level parallelism. This was only available in the Linux version of CodePeer 20.2.
The analysis engine is now able to emit diagnostics on array index checks, as well as on length checks.
The new analysis is interprocedural: some preconditions or postconditions are internally generated for callees, and used inside callers. This usually results in more precise results.
Infer is able to generate backtraces for messages resulting from a failed precondition. Support has been added to display those Infer backtraces within GNAT Studio.
A new option –infer-messages has been added to prevent Infer from emitting some families of checks. (Similarly to the existing –be-messages switch.)

Unlike the previous level 0, Infer’s analysis is performed at all levels by default. Messages common to Infer and the original CodePeer engine are automatically filtered to remove duplicates. If needed, Infer’s analysis can be inhibited using option –no-infer.

Incremental level 1 analysis ¶

CodePeer’s level 1 analysis is now incremental. Files that have not changed are no longer re-analyzed; instead, the results of the previous run are re-emitted. Since (at this level) files are analyzed in isolation, this allows providing the same level of precision in the results, while tremendously improving the speed of the analysis.

Note that analysis artefacts must be preserved accross successive runs for this feature to work.

Improvements to the support of pragma Annotate ¶

Pragma Annotate can be used to review the diagnostics emitted by CodePeer with relevant triaging information. CodePeer 22.x offers two enhancements to this functionality.

Flagging of unnecessary pragma ¶

CodePeer will now emit a warning when a pragma Annotate no longer matches a message emitted by CodePeer. This might mean that the pragma is no longer relevant, and should be removed.

Unused CodePeer annotate pragma in float_utils.adb at line 21.

Support of external tools ¶

Pragma Annotate are now understood by all the Ada analysis backends supported by CodePeer: the main analysis, Infer, GNATcheck and GNAT Warnings. Thus, it is now possible to annotate the messages emitted by any of those tools.

Improved user experience regarding analysis progress ¶

Reporting of incompatible options ¶

CodePeer will now warn when incompatible options are specified on the command-line for a single run. The analysis will then abort, and suggestions on how to fix the incompatibility will be provided (when possible).

Early failure detection ¶

CodePeer now stops at the first failed analysis phase. Previously, CodePeer would report the error, and either register an incomplete run without further complaints, or fail at a later phase; in both cases, the initial error was easy to miss. The new behavior makes such errors much more apparent.

Improved error reporting in case of crash ¶

CodePeer will now display additional contextual information if it encounters an unrecoverable error. In particular, a backtrace is now emitted, to help identify the context in which the problem occurred.

New analysis and reporting options ¶

Analyzing a set of files ¶

Using the new option -files-from, it is now possible to specify a file containing a list of source files to be analyzed by CodePeer. This new option is similar to -file but can be used to analyze multiple sources. It is meant to facilitate integration in dev-ops pipelines, in which it is not always easy to customize the command-line being ran.

Allow -level with -current ¶

It is now possible to use the switch -level in conjunction with the switch -current, in order to look at the results of a specific run at a specific analysis level in the history. Previously, -current picked the nth run of the last analysis level, and it was not possible to override this level information.

Reducing the database size ¶

A CodePeer run generates significantly more annotations than messages, which may furthermore fluctuate between runs. As a result, the database can grow in size very quickly just because of old annotations. CodePeer 22 no longer stores old annotations in the database, and only keeps the annotations of each analysis level’s current run.

Improved integrated Ada preprocessor in CodePeer ¶

The integrated Ada preprocessor (enabled via e.g. -gnateD) has been enhanced to support syntax from other legacy Ada preprocessors, and in particular:

now accepts endif instead of end if
no longer requires a closing semicolon.

File exclusion support for aggregate projects ¶

Excluding files from an analysis is sometimes useful, for example when the analysis time is too high. Users can now exclude files from the analysis of an aggregate project, making this feature more universally available.

Better CWE information for precondition checks ¶

For precondition checks, CodePeer 22 now displays more fine-grained information in the CWE column of CSV reports. The CWEs are derived from the check that led to the precondition being emitted – which is more precise than the generic list of CWE previously used.