Frama-C stands for Framework for Modular Analysis of C programs. Frama-C is a set of interoperable program analyzers for C programs. Frama-C has been developed by the French Commissariat à l'Énergie Atomique et aux Énergies Alternatives (CEA-List) and Inria. It has also received funding from the Core Infrastructure Initiative. Frama-C, as a static analyzer, inspects programs without executing them. Despite its name, the software is not related to the French project Framasoft.
Architecture
Frama-C has a modular plugin architecture comparable to that of Eclipse (software) or GIMP.
Frama-C relies on CIL (C Intermediate Language) to generate an abstract syntax tree.
The abstract syntax tree supports annotations written in ANSI/ISO C Specification Language (ACSL).
Several modules can manipulate the abstract syntax tree to add ANSI/ISO C Specification Language (ACSL) annotations. Among frequently used plugins are:
Value analysis – computes a value or a set of possible values for each variable in a program. This plugin uses abstract interpretation techniques and many other plugins make use...
Haelwenn /элвэн/ :triskell:
All GNU social JP content and data are available under the