Astrée is a static analyzer for safety-critical software written or generated in C or C++.
Astrée is a static analyzer which signals all potential runtime errors, data races, and further critical program defects in safety-critical C/C++ programs adhering to the C90, C99, C11, C18, and C++98, C++11, C++14, C++17 language norms. Astrée is sound, i.e., if no errors are signaled, this means there are no errors from the class of errors under investigation – the absence of errors has been proven. It reports program defects caused by unspecified and undefined behaviors according to the C and C++ language standards, program defects caused by invalid concurrent behavior, and computes program properties relevant for functional safety.
Astrée statically analyzes whether the programming language is used correctly and whether there can be any runtime errors during any execution in any environment. This covers any use of C or C++ that, according to the selected language standard, has undefined behavior or violates hardware-specific aspects.
Additionally, Astrée reports invalid concurrent behavior, violations of user-specified programming guidelines, and various program properties relevant for functional safety.
Astrée is sound for floating-point computations and handles them precisely and safely. All possible rounding errors, and their cumulative effects, are taken into account. The same is true for −∞, +∞ and NaN values and their effects through arithmetic calculations and comparisons.
