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

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

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

You can also supply formal analysis directives to provide external information to the analyzer, e.g., about the environ­ment, or to steer the analysis precision.

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.

The errors can then be investigated and fixed right within Astrée using the built-in text editor. In case of a false alarm, the analyzer can be tuned to avoid it.

This process can then be repeated until no errors are reported, at which point the absence of any errors has been formally proven.

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.

Astrée can also check your code for compliance with MISRA, CWE, SEI, and ISO coding rules.

Lastly, the analyzer computes code metrics (com­ment den­sity, cyclomatic complexity, etc.) and detects code that is not executed under any circumstances (“dead code”).