Frama-C

Frama-C has been developed by the French Commissariat à l'Énergie Atomique et aux Énergies Alternatives (CEA-List)[2] and Inria.

Frama-C has a modular plugin architecture[3] 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.