Frama-C
Frama-C — Framework for Static Analysis of the C language
Core
-
C source code → Abstract Syntax Tree
-
ACSL — ANSI/ISO C Specification Language
/*@ ... */
Plugins
Annotate syntax trees with static analysis.
- WP — Weakest Precondition
- Value analysis, Jessie, InOut, Metrics, Aorai, PathCrawler, Spare code, ...
- several in-house plugins at Atos, Airbus, Dassault, CEA, ...