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.

Each analysis process may also briefly spawn a filter process for stripping incompatible expressions (e.g. inline assembly) from the C source code.

Input

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

  2. For each analysis, you specify an entry point of your choosing — typically a function of particular interest, or simply main. Astrée will then analyze all portions of the code that can be reached by non-interrupted sequential program exe­cution starting from that entry point.

  3. You can provide an analysis wrapper — e.g. to model reactive system behavior — in a dedicated C file associated with the analysis.

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

  5. 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), so that your 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.

Output

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 type 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 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
  • Type A alarm: a potential runtime error with an unpredictable result
  • Type C alarm: a potential runtime error with a predictable result
  • Error: either a Type 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, and SEI CERT C.

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

Take it to the next level

Once your C code is error-free, compiling it may introduce all-new errors of its own. To prevent that from happening, use our formally verified optimizing C compiler CompCert. It is the only compiler worldwide that is mathematically proven to be free of mis­compilation issues.

Configuration

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