Astrée comes with comprehensive documentation and a variety of real-world examples.
When creating a new project, Astrée guides you through the analysis settings and offers interactive help for each of the configured options.
It is possible to specify a list of original source files and preprocessor settings (include paths and defines). The specified files can be automatically preprocessed and analyzed by Astrée using a built-in preprocessor.
Sample analysis results. Several runtime errors have been found and can be interactively explored, commented on, or fixed right away in the built-in editor.
The errors are classified by severity, and the overall result is summed up by a traffic-lights symbol.
The results can be exported, for example as customizable HTML reports, for documentation and certification purposes. The entire project can be saved as well, including all files, settings, annotations and comments.
Code parts that cause the runtime errors are highlighted in the built-in text editor and can be fixed right there.
The call graph browser provides an overview of the alarm distribution in the analyzed software.