Astrée workflow

The figure to the right shows the tool chain of the Astrée run­time error analyzer.

The analysis is controlled via the Astrée client GUI that com­mu­nicates with the Astrée server process. The Astrée server pro­cess may run on the same machine as the GUI or on a remote host. It starts an Astrée Analyzer process to which it passes the analysis configuration. The analyzer may start an additional Astrée filter process for removing incompatible expressions (e.g., inline assembly) from the C source code. The filtered source code is passed to the analyzer which sends its results to the server process. The server sends the results back to the client for graphical display.

Astrée works on preprocessed C code. It parses the source files and translates the code into an intermediate representation on which the runtime error analysis is then performed. Astrée will analyze all portions of the code that can be reached by non-interrupted sequential program execution starting from a user-specified entry point.

The user can provide an analysis wrapper — e.g. to model reactive system behavior — in a dedicated C file associated with the analysis project. Astrée can be configured with different ABI (appli­cation binary interface) settings.

The result of the analysis is a list of alarms, i.e. of potential runtime errors. Each potential run­time error is reported together with information about the type of error and the source code lo­ca­tion 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.

The overall analysis result is visualized by a traffic lights symbol in the GUI as follows:

red at least one error
yellow no errors, but at least one alarm of Type A
yellow and green no errors and no Type A alarms,
but at least one alarm of Type C
green no errors and no alarms
  • Alarm: a potential runtime error with either an unpredictable result (Type A),
    or a predictable result (Type C)
  • 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)

The analyzer also provides coverage information showing unanalyzed code statements. In ab­sence of definite runtime errors code reported as unanalyzed is definitely unreachable. Astrée also allows 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 stops with an error if indispensable data is missing or if source files cannot be correctly parsed and translated.

Astrée features formal analysis directives to provide external information to the analyzer, e.g., about the environment, and to steer the analysis precision. The directives can be specified in a dedicated language denoted AAL (Astrée Annotation Language) so that the 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 tool can be configured by the following means:

Finally, the tool supports two modes: a batch mode for automatic runtime error analysis and an interactive mode with a graphical user interface.

Top