Static analysis with Astrée

Astrée screenshot

Astrée comes with comprehensive documentation, a variety of real-world examples, and free interactive Web-based training.

If you are unfamiliar with the tool but have to take over an analysis project previously managed by a colleague, we are happy to provide you with the same training that they received and to additionally help you with the specific project in question if you so wish. Simply get in touch by writing to support@absint.com.


Astrée screenshot

When creating a new analysis project, the software guides you through the analysis settings and offers interactive help for each of the configured options.


Astrée screenshot

It is possible to specify a list of original source files and preprocessor settings (include paths and defines). The specified files are then automatically preprocessed and analyzed using a built-in preprocessor.


Astrée screenshot

Sample analysis results, showing a variety of different errors. A quick overview is offered in tabular and chart form, the errors are classified by severity, and the overall result is summed up by a traffic-lights symbol.

From here, each individual error can be interactively explored, commented on, or fixed right away in the built-in editor.

The analysis results can also be exported in a variety of formats — for example, as customizable HTML reports for documentation and certification purposes, or as an XML file for further processing by your toolchain as part of your nightly build process.

The entire project can be saved as well, including all files, settings, annotations and comments.


Astrée screenshot

Code parts that cause the errors are highlighted in the built-in text editor and can be fixed right there.

In case of a false alarm, it can be annotated as such, to ensure that it no longer occurs on subsequent analysis runs. Alternatively, you can tweak the analysis settings for the whole project or increase the analysis precision for specific code parts.

Lastly, each alarm can be classified or commented on according to your own in-house criteria. Collaborative reviews of the analysis results are supported. All communication is TLS-encrypted with OpenID support.


Astrée screenshot

The call graph browser provides an overview of the alarm distribution in the analyzed code. The visual representation helps you discover unexpected behavior of your software, and enables a faster and deeper understanding of third-party or legacy modules.


RuleChecker screenshot

With the seamlessly integrated RuleChecker, you can check your code for adherence to various coding standards, including MISRA, CWE, ISO/IEC, SEI CERT C, and AUTOSAR. The configuration screen allows you to select the desired rule sets, individual rules, and even specific aspects of certain rules.

On request, the tool can also be extended to check for custom coding rules of your own.


RuleChecker screenshot

RuleChecker can also check for various code metrics, such as com­ment den­sity, cyclomatic complexity, or number of instructions per function.


RuleChecker screenshot

Interactive statistics let you see at a glance which parts of your code are most prone to which kinds of problems. This is especially helpful for large projects with dozens or even hundreds of individual files.

You can try Astrée and RuleChecker for free, on your own code, for a period of 30 days.