AbsInt Astrée

Astrée primarily targets embedded applications as found in aero­nautics, earth trans­por­tation, medical instrumen­tation, nuclear energy, and space flight. Never­theless, it can just as well be used to analyze any structured C/C++ programs, handwritten or generated, with complex memory usages, dynamic memory allocation, and recursion.

Astrée is sound — that is, if no errors are signaled, the absence of errors has been proved.

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 corresponding 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),
• other critical data and control-flow errors,
• all violations of optional user-defined assertions to prove additional runtime properties (similar to assert diagnostics),
• code it can prove to be unreachable under any circumstances.

Astrée is also 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.

In 2020, the US National Institute of Standards and Technology determined that Astrée satisfies their criteria for sound static code analysis.

Since 2020, runtime error analysis can also be applied to C++ and mixed C/C++ code bases. The new analysis mode supports all modern C++ versions up to C++17 and many of the features known from the classic C code analysis.

Astrée’s C++ analysis uses the same technology as its C code analysis. It is designed to meet the characteristics of safety-critical embedded software, and is subject to the same restrictions as Astrée for C.

The high-level abstraction features and template library of C++ facilitate the design of very complex and dynamic software. Extensive use of these features may violate the established principles of safety-critical embedded software development and lead to unsatisfactory analysis times and results. The Astrée manual gives recommendations on the use of C++ features to ensure that the code can be well analyzed. For less constrained (less critical) C++ code, we recommend using the standalone RuleChecker.

The seamlessly integrated RuleChecker lets you check your code for compliance with various coding standards, including MISRA, CWE, ISO/IEC, SEI CERT, and AUTOSAR. You can easily toggle individual rules and even specific aspects of certain rules. The tool can also check for various code metrics such as com­ment den­sity or cyclomatic complexity. Custom extensions for your own in-house coding guidelines are available on request.

RuleChecker can be envoked separately, to allow for even faster checks of your code, or in conjunction with the sound semantic analyses offered by Astrée, to additionally guarantee zero false negatives and minimize false positives on semantical rules. No competing standalone MISRA checker can offer this, and no testing environment can match the full data and path coverage provided by the static analysis.

Astrée offers powerful annotation mechanisms for supplying external knowledge and fine-tuning the ana­lysis precision for individual loops or data structures. Detailed messages and an intui­tive GUI guide you to the exact cause of each potential runtime error. Actual errors can then be fixed, and in case of a false alarm the analyzer can be tuned to avoid it. This allows for analyses with very few or even zero false alarms.

The analyzer can also run in batch mode for easy integration into established tool-chains.

Plugins for TargetLink, Jenkins, and Eclipse are available and actively supported.

Your usage of Astrée can be qualified according to DO-178B/C, ISO 26262, IEC 61508, EN-50128, the FDA Principles of Software Validation, and other safety standards. We offer special Qualification Support Kits that simplify and automate the qualification process.

Astrée Flyer

Astrée Datasheet

Cancellation: You can cancel your subscription at any time. Please note that we do not provide credit, refunds or prorated billing for any licenses that are cancelled once purchased.

No Return/Refund: All sales are final, there are no refunds.