CodePeer 21 Release Notes¶
We present here a few highlights of the new features in CodePeer 21. You can access the complete list here.
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
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.
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.