Notes de publication
aiT, StackAnalyzer, TimingProfiler, ValueAnalyzer, TimeWeaver
- Improved performance
- Support for DWARFv5
- New AIS2 functors
- WCET analysis for ARM Cortex-M0
- Support for LLVM/Clang
- Additional QSK test cases
- Improved stack and value analysis
- Value partitioning
- Support for S12Z and 64-bit ARM
Astrée
- New Eclipse plugin
- Faster analyses and reduced memory consumption
- Improved commenting and categorization of rule violation alarms
- Improved interpolation domain
- 100+ other improvements and new features
- Support for C11
- CompCert configurations
- Floating licenses
- New comment mode
- Much faster analyses
- Support for GCC-extended assembler
- Standalone RuleChecker
- Improved performance and
reduced memory consumption
RuleChecker
- New Eclipse plugin
- Improved commenting and categorization of rule violation alarms
- Support for 30+ more MISRA C++ rules
- Improved support for MITRE CWE and SEI CERT
- 20+ new QSK test cases
- Analysis of C++ code
- Support for macOS
- Floating licenses
- Support for CWE guidelines
- Re-categorizations of MISRA rules
- Style rules for naming identifiers
- First standalone version
- Support for SEI CERT C rules
- Improved support for 50+ MISRA rules
CompCert
- Improved handling of
_Alignof and _Alignas
- New configurable check for correct placement of symbols in sections in Valex
- New diagnostics for non-robust language features
- New builtin for integration with a³
- JSON export of ARM assembly
- Valex for ARM
- New backend for hybrid 64-bit/32-bit PowerPC code
- New generic compiler optimizations
- QSK for Valex
- Full support for C11 anonymous compound types
- Checks for unused variables and parameters
