On the recordRead 30 Sep 202627 facts
Astrée
Saarbrücken, Germany
On the record
- Analysis features
- Additional features include finding unreachable code and non-terminating loops, user-configurable taint analysis, and proving functional properties with static assertions.absint.com · read 30 Sep 2026
- Analysis input
- Astrée analyzes preprocessed C code and includes a preprocessor to handle that step if desired.absint.com · read 30 Sep 2026
- Analysis setup
- Users can choose an analysis entry point, such as main, and Astrée analyzes code reachable from it.absint.com · read 30 Sep 2026
- Automation
- The client provides a graphical interface and batch mode for automation and integration.absint.com · read 30 Sep 2026
- C++ analysis
- Release 24.10 says Astrée can report data races and deadlocks in C++ and mixed C/C++ analysis mode.absint.com · read 30 Sep 2026
- Client and server
- Astrée has a client for setting up analyses and reviewing results, and a server where analyses run.absint.com · read 30 Sep 2026
- Code support
- Astrée can analyze handwritten or automatically generated code without requiring the program to be instrumented, executed, or stimulated by test cases.absint.com · read 30 Sep 2026
- Configuration
- Users can supply wrapper code and separate Astrée Annotation Language information to describe the execution environment or control analysis precision.absint.com · read 30 Sep 2026
- Coverage and precision
- The maker says Astrée considers all possible data and function pointer targets and thread interleavings, provides 100% control and data coverage, and can be tuned to eliminate false alarms.absint.com · read 30 Sep 2026
- Defects detected
- It detects issues including out-of-bounds array accesses, pointer errors, division by zero, arithmetic overflows, memory leaks, data races, inconsistent locking, and deadlocks.absint.com · read 30 Sep 2026
- Developer and distributor
- The release notes state that Astrée is developed and distributed by AbsInt under license from CNRS and ENS.absint.com · read 30 Sep 2026
- Integration
- Release 24.10 notes that the Astrée Jenkins plugin was updated.absint.com · read 30 Sep 2026
- Integrations
- The maker describes CI/CD and DevOps integration, automatic AUTOSAR integration analysis from ARXML files, and a TargetLink coupling; release notes also mention an Astrée Jenkins plugin.absint.com · read 30 Sep 2026
- Language standards
- The product factsheet lists support for C90, C99, C11, C18, C++98, C++11, C++14, and C++17.absint.com · read 30 Sep 2026
- License
- Astrée is developed and distributed by AbsInt under license from CNRS/ENS.absint.com · read 30 Sep 2026
- License limits
- The Astrée workflow page says the license file determines how many clients may access the server concurrently and how many analyses may run in parallel.absint.com · read 30 Sep 2026
- Purpose
- Astrée is a sound static analyzer designed to prove the absence of runtime errors and data races in C/C++ programs.absint.com · read 30 Sep 2026
- Results
- Astrée reports possible run-time errors with their type and source-code location, and can classify an alarm as a definite run-time error when it proves it must occur in a given context.absint.com · read 30 Sep 2026
