Static runtime error analysis with Astrée

Astrée workflow

Tool architecture

Astrée consists of two parts:

  1. The Astrée client, which you use to set up an analysis and view the results. The client offers both a GUI and a batch mode for easy auto­mation and integration.
  2. The analysis server, which carries out the actual analysis (or several analyses as separate processes).

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 indi­vidual developers and managers on their PCs or other devices.

Your license file determines how many clients may connect to the ser­ver at the same time, and how many ana­lysis processes can run there in parallel.


  1. 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.

  2. For each analysis, you specify an entry point of your choosing — typically a function of particular interest, or simply main.
    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 specifi­cations.

  3. Astrée can also be configured with different ABI (appli­cation binary interface) settings.

  4. Lastly, you can supply formal analysis directives to provide external information to the analyzer, e.g. about the environ­ment, or to steer the analysis precision. The directives are specified in the dedi­cated, human-readable Astrée Anno­tation 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 speci­fied 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 potenti­al run­time errors. Each error is reported to­gether with its class and the source code lo­ca­tion where it occurs. If Astrée can prove that an alarm will always occur in a speci­fic context, it is classified as a defi­nite run­time 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
  • Class A alarm: a potential runtime error with an unpredictable result
  • Class B alarm: a potential data race
  • Class C alarm: a potential runtime error with a predictable result
  • Error: either a class A alarm that definitely occurs in some context, or a fatal error in the analysis (e.g., a parse error due to incorrect input)
Analysis results

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 ab­sence of definite run­time errors, code reported as unanalyzed is defi­nitely un­reachable.

You can also use the integrated RuleChecker to check your code for adherence to standards such as MISRA, CWE, ISO/IEC, AUTOSAR, and SEI CERT.

Lastly, you can use Astrée to check for functional program pro­perties by a static assertion mecha­nism. If Astrée does not report the assertion to be violated, the asserted C/C++ ex­pression 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.

Fixing the errors

Fixing the errors

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.

Take it to the next level

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 mis­compilation issues.


Each Astrée runtime error analysis can be configured by the following means:

  1. Options
    • abstract domains and precision settings
    • aspects of the considered semantics
    • output and verbosity
  2. Directives
    • semantic information such as value ranges and invariants
    • parameters for local fine-tuning of the analysis precision
  3. ABI settings
    • sizes of atomic types
    • alignment settings
    • endianess
    • sign of char and bitfield
    • etc.
  4. Filters
    e.g. for ignoring non-standard keywords or inline assembly
  5. Wrapper and stub code