CodePeer 21 Release Notes

We present here a few highlights of the new features in CodePeer 21. 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 GNATStudio

Improvements to the support of pragma Annotate

Pragma Annotate can be used to review the diagnostics emitted by CodePeer with relevant triaging information. CodePeer 21.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.

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.