The tool analyses structured C programs with complex memory usages, but without recursion or dynamic memory allocation. This targets embedded applications as found in earth transportation, nuclear energy, medical instrumentation, aeronautics and space flight, in particular synchronous control/command such as electric flight control.
Astrée analyses whether the C 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 that has undefined behaviour as defined by the C99 standard, or that violates hardware-specific aspects as defined by the C99 standard.
Astrée reports 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,
- violation of optional user-defined assertions to prove additional run-time properties (similar to assert diagnostics),
- read access to uninitialized variables.
Astrée reports code it can prove to be unreachable under any circumstances (although this is not necessarily all unreachable code) and is sound for floating-point computations and handles them precisely and safely. It takes all possible rounding errors into account.
Astrée offers powerful annotation mechanisms, which enable you to make external knowledge available to it, or to selectively influence the analysis precision for individual loops or data structures. Detailed messages and an intuitive GUI help you understand alarms about potential errors. Actual errors can then be fixed, and in case of a false alarm, the analyser can be tuned to avoid it. These mechanisms allow to perform analyses with very few or even zero false alarms.
General-purpose static analysers aim at analysing any application written in a given programming language. They can rely on language related properties to find potential run-time errors. Specialised static analysers put additional restrictions on the applications so as to be able to take specific program structures into account.
In contrast, Astrée is domain-aware. It nows facts about application domains that are indispensable to make sophisticated proofs. For