product

ABSINT

AbsInt provides advanced development tools for embedded sys­tems, and tools for validation, veri­fication 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.

product

Astrée

Astrée is a static code analyzer that proves the absence of run­time errors and invalid con­current behavior in safety-critical software written or generated in C.

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 programs, handwritten or generated, with complex memory usages, dynamic memory allocation, and recursion.

StackAnalyzer

product

StackAnalyzer automatically determines the worst-case stack usage of the tasks in your appli­cation. 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

product

RuleChecker is a static program analyzer that automatically checks your C or C++ code for compliance with MISRA rules, CERT recom­mendations, 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 com­ment den­sity 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 ac­cepts 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 math­ematical proofs, to be exempt from miscompilation issues. The code it pro­duces 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 con­tributes to meeting the highest levels of software assurance.

CompCert
The formal proof covers all transformations from the abstract syntax tree to the generated assem­bly code. To preprocess and produce object and executable files, an external C pre­processor, assemblers, linkers, and C libraries have to be used. However, these unverified stages are well-understood and robust from an implementation perspective. This was demon­strated on a devel­op­ment version of CompCert in a 2011 study by Regehr, Yang et al.: