AbsInt Astree is a static program analyzer that proves the absence of run-time errors (RTE) in safety-critical embedded applications written or automatically generated in C. Email firstname.lastname@example.org for Price Quote.
Features: Astrée is a static program analyzer that proves the absence of run-time errors (RTE) in safety-critical embedded applications written or automatically generated in C. Astrée analyzes 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. Which run-time properties are analyzed by Astrée? Astrée analyzes 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), code it can prove to be unreachable under any circumstances (note that this is not necessarily all unreachable code), read access to unintialized variables. Astrée is sound for floating-point computations and handles them precisely and safely. It takes all possible rounding errors into account. Tailor it to your own requirements: 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 analyzer can be tuned to avoid it. These mechanisms allow to perform analyses with very few or even zero false alarms. Astrée can also be customized and integrated into established tool-chains. MISRA rule checker: Astrée is now also able to check coding rules (MISRA), compute code metrics such as comment density, cyclomatic complexity, etc., and check metric thresholds. The rule checker is highly configurable, allowing you to toggle checks for individual rules or aspects of certain rules. Technical Specs: Astrée: www.absint.com/astree/index.htm