Static analysis with Astrée

Tool architecture

The static analyzer consists of two parts:

1. The analysis client, which you use to set up an analysis and view the results. It 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.

How many clients may connect to the ser­ver at once, and how many ana­lysis processes can run there in parallel, is controlled by your license file. Node-locked, floating, and cloud licenses are supported.

Input

1. Both Astrée and RuleChecker can analyze C code, C++ code, and 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.
   The analysis will then consider all portions of the code that can be reached during any execution scenario covered by your specifi­cations.

3. The analyzer 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 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 placement of the directives is speci­fied over the program structure and so 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 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)

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, SEI CERT, and AUTOSAR.

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

Every error can be interactively explored, commented on, or fixed right away in the built-in C/C++ source code editor.

In case of a false alarm, it can be marked as such using AAL annotations, so it no longer occurs 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.

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