Astrée consists of two parts:
Both parts may run on the same machine at once. In production, however, the server typically runs on a powerful remote host, while clients are run by the individual developers and managers on their PCs or other devices.
Your license file determines how many clients may connect to the server at the same time, and how many analysis processes can run there in parallel.
Astrée analyzes C code, C++ code, or mixed C/C++ code bases. A built-in preprocessor replicates the preprocessing step of your build process.
For each analysis, you specify an entry point of your choosing —
typically a function of particular interest, or simply
You can provide an analysis wrapper — e.g. to model reactive system behavior — in a dedicated C/C++ file associated with the analysis.
For asynchronous applications, you may specify task and ISR entry points, as well as priorities of tasks and ISRs.
Astrée will then analyze all portions of the code that can be reached during any execution scenario covered by your specifications.
Astrée can also be configured with different ABI (application binary interface) settings.
Lastly, you can supply formal analysis directives to provide external information to the analyzer, e.g. about the environment, or to steer the analysis precision. The directives are specified in the dedicated, human-readable Astrée Annotation Language (AAL) and can be inserted into your code during analysis so that your actual source code does not have to be modified. The location of the directives is specified over the program structure and is robust with respect to line numbers.
The most important result of the analysis is a list of alarms, i.e. of potential runtime errors. Each error is reported together with its class and the source code location where it occurs. If Astrée can prove that an alarm will always occur in a specific context, it is classified as a definite runtime error.
In the GUI, the alarms are additionally summarized by a traffic lights symbol as follows:
|red||at least one error|
|yellow||no errors, but at least one alarm of class A or B|
|green and yellow||no errors and no alarms of class A or B, but at least one alarm of class C|
|green||no errors and no alarms of class A, B, or C|
Various statistics are compiled. Interactive tables, graphs and charts let you quickly see which code areas are most prone to which kinds of errors.
Report files can be generated for documentation and certification purposes. The entire analysis project can be saved as well, including all files, settings, annotations and comments.
The analyzer also provides coverage information showing unanalyzed code statements. In absence of definite runtime errors, code reported as unanalyzed is definitely unreachable.
Lastly, you can use Astrée to check for functional program properties by a static assertion mechanism. If Astrée does not report the assertion to be violated, the asserted C/C++ expression has been proven correct.
Astrée will always stop with an error if indispensable data is missing or if source files cannot be correctly parsed and translated.
Every error can be interactively explored, commented on, or fixed right away in the built-in C/C++ source code editor.
Possible false alarms can be marked as such using AAL annotations, so they no longer occur on subsequent analysis runs. Alternatively, you can tweak the analysis settings for the whole project or increase analysis precision for specific code parts.
After that, you can run the analysis once again and examine the improved results.
These steps are repeated as needed, until all alarms have been dealt with and no errors are reported anymore. At that point, the absence of errors in your code has been formally proven.
Once your C code is error-free, you can use our formally verified optimizing C compiler CompCert to guarantee that all safety properties verified on the source code also hold for the generated executable. CompCert is the only compiler worldwide that is mathematically proven to be free of miscompilation issues.
Each Astrée runtime error analysis can be configured by the following means: