AbsInt
AbsInt provides advanced development tools for embedded systems, and tools for validation, verification and certification of safety-critical software. Absint tools are based on a generic and generative framework which allows an extremely quick, sound and flexible response to customer needs.
Astrée
Astrée is a static code analyzer that proves the absence of runtime errors and invalid concurrent behavior in safety-critical software written or generated in C.
Astrée primarily targets embedded applications as found in aeronautics, earth transportation, medical instrumentation, nuclear energy, and space flight. Nevertheless, it can just as well be used to analyze any structured C programs, handwritten or generated, with complex memory usages, dynamic memory allocation, and recursion.
StackAnalyzer
StackAnalyzer automatically determines the worst-case stack usage of the tasks in your application. It lets you find any stack overflows, or formally prove the absence thereof.
Features
- Detailed and precise information on user-stack usage and system-stack usage by application tasks.
- Freely selectable entry points for the analysis. You can easily focus on any code parts of particular interest to you.
- Control-flow reconstruction directly from binary code. Potential flaws in the debug information will not confuse StackAnalyzer.
- Fully integrated, feature-rich graphical and textual viewers for control flow, analysis results, source code, assembly code, and configuration files.
- Customizable XML reports for documentation and certification.
- Optional ValueAnalyzer add-on for static analysis of register and memory cells, memory accesses and function calls.
- Seamless integration with other analysis tools from AbsInt (e.g. aiT for worst-case execution time analysis).
- Batch mode for easy integration with other tools, or into automated build processes.
RuleChecker
RuleChecker is a static program analyzer that automatically checks your C or C++ code for compliance with MISRA rules, CERT recommendations, and other coding guidelines.
RuleChecker primarily targets safety-critical embedded applications, but can also be used to analyze any structured C programs, handwritten or generated, with complex memory usages, dynamic memory allocation, and recursion.
Supported standards
- MISRA 2004
- MISRA 2012
- MISRA 2012 Amendment 1
- MISRA AC AGC
- MISRA C++:2008
- SEI CERT Secure C
- MITRE CWE (Common Weakness Enumeration)
- ISO/IEC TS 17961:2013 (C Secure Coding Rules)
- ISO/IEC 9899:1999 diagnostics
- Adaptive AUTOSAR C++14
- HIS metrics
- Customizable style rules for all C identifiers
- Your very own in-house coding guidelines (on request)
Features
- Easy configuration, allowing you to toggle individual rules and even specific aspects of certain rules.
- Exceptionally fast analyses for complex real-world programs with hundreds of thousands lines of code.
- Various statistics and code metrics, such as comment density or cyclomatic complexity. Optional checks for metric thresholds.
- Interactive graphs, charts, and tables for efficient exploration of the analysis results.
- Customizable reports for documentation and certification purposes.
- Batch mode for use in continuous integration frameworks. Plugins for TargetLink, Jenkins, and Eclipse.
- Optional integration with the runtime error analyzer Astrée to guarantee zero false negatives and minimize false positives on semantical rules.
CompCert
CompCert is a formally verified optimizing C compiler. Its intended use is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It accepts most of the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for ARM, PowerPC, x86, and RISC-V architectures.
What sets CompCert apart?
CompCert is the only production compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. The code it produces is proved to behave exactly as specified by the semantics of the source C program.
This level of confidence in the correctness of the compilation process is unprecedented and contributes to meeting the highest levels of software assurance.
