Astreè

Astrée is a static analyzer for safety-critical software written or gen­er­ated in C or C++.

Finding all Runtime Errors and Data Races in C/C++ Programs

Astrée is a static analyzer which signals all potential runtime errors, data races, and further critical program defects in safety-critical C/C++ programs adhering to the C90, C99, C11, C18, and C++98, C++11, C++14, C++17 language norms. Astrée is sound, i.e., if no errors are signaled, this means there are no errors from the class of errors under investigation – the absence of errors has been proven. It reports program defects caused by unspecified and undefined behaviors according to the C and C++ language standards, program defects caused by invalid concurrent behavior, and computes program properties relevant for functional safety.

Features

  • Exceptionally fast and precise analyses, including:
  • Runtime error analysis
  • Non-interference analysis
  • Advanced taint analysis
  • Detection of Spectre vulnerabilities
  • Signal-flow, data-flow, and control-flow analysis
  • Control-coupling and component-interference analysis
  • User-defined cybersecurity analyses
  • Analysis of functional program properties
  • Rule checks for MISRA, CERT, CWE, AUTOSAR, and other guidelines
  • Analysis of numerous code metrics
  • Detection of dead code
  • Support for C, C++, and mixed code bases
  • Automatically generated report files for documentation and certification purposes
  • Qualification Support Kits for DO-178B/C, ISO 26262, EN-50128, and other standards
  • Feature-rich GUI with graphical and textual views for analysis results, source code, control flow, and user comments
  • Batch mode for seamless integration into established tool chains
  • Plugins for TargetLink, Jenkins, μVision, JSON, and Eclipse
  • Support for node-locked, floating, and cloud setups
  • Regular updates

Static analysis of runtime properties

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 selected 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),
  • Spectre vulnerabilities,
  • other critical data and control-flow errors,
  • violations of optional user-defined assertions to prove additional runtime properties (similar to assert diagnostics), dead code.

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

Request Info