Astreè

Astrée statically analyzes whether the programming language is used correctly and whether there can be any run­time 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 detects any:
• division by zero,
• out-of-bounds array indexing,
• erroneous pointer manipulation and dereferencing (NULL, uninitialized and dangling pointers),
• integer and floating-point arithmetic overflow,
• read access to uninitialized variables,
• data races (read/write or write/write concurrent accesses by two threads to the same memory location without proper mutex locking),
• inconsistent locking (lock/unlock problems),
• invalid calls to operating system services (e.g. OSEK calls to TerminateTask on a task with unreleased resources),
• Spectre vulnerabilities,
• other critical data and control-flow errors,
• violations of optional user-defined assertions to prove additional runtime properties (similar to assert diagnostics), dead code.

Astrée is sound for floating-point computations and handles them precisely and safely. All possible rounding errors, and their cumu­lative effects, are taken into account. The same is true for −∞, +∞ and NaN values and their effects through arithmetic calculations and comparisons.