Astrée can now track taint information for memory locations.
This new feature can be used for analyzing security properties.
It is disabled by default and can be enabled by setting the option
track-taint-hues. Additionally, the new directives
can be inserted into the code for expressing where variables
are tainted and which memory locations must not be reached by taints.
Astrée now detects and reports Spectre v1, Spectre v1.1,
and SplitSpectre vulnerabilities.
The detection is disabled by default and can be enabled via the new option
This is the first Astrée release to offer static run-time error analysis of C++ code. Evaluation licenses can now be issued on request.
RuleChecker can now check C++ code for compliance with AUTOSAR C++ coding rules as defined in the AUTOSAR document “Guidelines for the use of the C++14 language in critical and safety-related systems”.
Astrée now supports AUTOSAR multi-core systems using a multi-core aware OS model with support for spinlocks. The OS setup can be automatically derived from ARXML.
This release introduces a new relational domain for a more precise analysis of finite-state machines. The above screenshot showcases one tricky example that Astrée is now able to analyse with no false alarms.
The new domain is activated with the option
and reacts to the new directive
which indicates that
x is used to encode
the state of a state machine.
Special treatment stops upon encountering either
The new option
automatic detection of code patterns used in state machine
implementations, for which Astrée can then insert