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.
Each analysis process may also briefly spawn a filter process for stripping incompatible expressions (e.g. inline assembly) from the C source code.
Astrée works on preprocessed C code. If desired, a built-in preprocessor saves you that step. The code is then parsed and translated into an intermediate representation on which the runtime error analysis is performed.
For each analysis, you specify an entry point of your choosing —
typically a function of particular interest, or simply
Astrée will then analyze all portions of the code that can be
reached by non-interrupted sequential program execution starting from that
You can provide an analysis wrapper — e.g. to model reactive system behavior — in a dedicated C file associated with the analysis.
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), so that your 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 type 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 Type A|
|green and yellow||no errors and no Type A alarms, but at least one alarm of Type C|
|green||no errors and no alarms|
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 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 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 or increase analysis precision for select 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: