You may have noticed that over the past two years, we have made significant updates to our CodePeer product - the most visible change being the renaming of the product itself, now branded as “GNAT Static Analysis Suite”. For those who are already using the product and are looking to use the new version, it may be a good time to step back and share our vision, at AdaCore, for static analysis.

Our objective for the suite is to allow users to find as much valuable information as possible from the static analysis of source code. Some of this information will be exhaustive, meaning the analysis is sound. For example, when asking the suite to verify a coding standard rule, we don’t want to miss any violations. Some of this information will be as precise as possible. For example, it is challenging to identify all possible buffer overflows without also flagging constructs that in fact will execute safely; performing a conservative analysis designed to detect every possible instance can end up with thousands of messages with very little added value. This is not specific to the suite, but rather an inherent property of the kind of analysis performed. Consequently, the suite’s job is to filter the reporting to only show messages that are likely to be real problems or that provide the best value for you.

As a side note, there is a way to develop code such that this kind of analysis is possible and sound. This development and verification methodology is known as formal methods, and can be achieved with our SPARK Pro technology. However, GNAT SAS has a different goal; unlike formal methods, the analysis is applied to full Ada programs, from any version of the language standard.

CodePeer historically incorporated a single analysis engine. We now call that engine “Inspector”, which was also the tool's name before it was branded as CodePeer. Over the years, we’ve integrated a number of information sources, including compiler warnings, GNATcheck diagnostics and more recently Meta’s Infer engine as well as custom analysis developed with the LangKit Query Language (LKQL). So we’re moving to a collection of analyses, some very local, some using data and control flow, some more global. GNAT SAS is the collective name for these advanced capabilities that work together to identify vulnerabilities, bugs and other defects in your code.

You may have noticed in GNAT SAS 24 that the name of the driver has changed. You won’t call “codepeer” directly anymore, but rather “gnatsas”. Switches and project attributes have changed; the new codepeer executable will assist with the migration (see also the documentation).

Another significant change is in the description of levels of analysis. We used to have levels from 0 to 4, which were intended to grade the amount of effort put forth by the underlying analyzer. In practice, however, it was difficult to know what these levels actually meant and which one was best for a particular project. GNAT SAS now offers two levels: --mode=fast, which is intended to be used locally during development and --mode=deep, designed to be used by offline analysis, for example, CI/CD (Continuous Integration / Continuous Deployment) pipelines.

The last significant change concerns the database that stores results and messages. We previously used a SQLite database but have now moved to a text file format. The key benefit of a text file is that it can then live together with source code, and in particular it can be checked into the version control system alongside the corresponding source, thus keeping the artifacts in sync.

The gnatsas driver is intended as the main point of entry for static analysis. Even though we still have separate gnatcheck and gnatsas executables for now, we plan to harmonize the selection of coding standard rules in both, regardless of which tool implements them. We’re also planning to integrate compiler warnings by default. We have more work to do there, alongside developing new analysis and checks. As usual, if you’re a GNAT Tracker user, feel free to open a ticket for comments, feedback and questions!