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 Commissariat à l'Énergie Atomique et aux Énergies Alternatives

Commissariat à l'Énergie Atomique

The Commissariat à l'énergie atomique et aux énergies alternatives or CEA, is a French “public establishment related to industrial and commercial activities” whose mission is to develop all applications of nuclear power, both civilian and military...

 and Inria. Frama-C enables the analysis of C programs without executing them.

Architecture

Frama-C has a modular plugin architecture comparable to that of Eclipse (software)

Eclipse (software)

Eclipse is a multi-language software development environment comprising an integrated development environment and an extensible plug-in system...

 or GIMP

GIMP

GIMP is a free software raster graphics editor. It is primarily employed as an image retouching and editing tool and is freely available in versions tailored for most popular operating systems including Microsoft Windows, Apple Mac OS X, and Linux.In addition to detailed image retouching and...

.

Frama-C relies on CIL (C Intermediate Language

C Intermediate Language

CIL is a simplified subset of the C programming language, as well as a set of tools for transforming C programs into that language.Several other tools use CIL as a way to have access to a C abstract syntax tree...

) to generate an abstract syntax tree

Abstract syntax tree

In computer science, an abstract syntax tree , or just syntax tree, is a tree representation of the abstract syntactic structure of source code written in a programming language. Each node of the tree denotes a construct occurring in the source code. The syntax is 'abstract' in the sense that it...

.
The abstract syntax tree

Abstract syntax tree

In computer science, an abstract syntax tree , or just syntax tree, is a tree representation of the abstract syntactic structure of source code written in a programming language. Each node of the tree denotes a construct occurring in the source code. The syntax is 'abstract' in the sense that it...

 supports annotations written in ANSI/ISO C Specification Language

ANSI/ISO C Specification Language

The ANSI/ISO C Specification Language is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm...

 (ACSL).

Several modules can manipulate the abstract syntax tree

Abstract syntax tree

In computer science, an abstract syntax tree , or just syntax tree, is a tree representation of the abstract syntactic structure of source code written in a programming language. Each node of the tree denotes a construct occurring in the source code. The syntax is 'abstract' in the sense that it...

 to add ANSI/ISO C Specification Language

ANSI/ISO C Specification Language

The ANSI/ISO C Specification Language is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm...

 (ACSL) annotations. Among frequently used plugins are:

• value analysis: which computes a value or a set of possible values for each variable in a program. This plugin uses abstract interpretation
  Abstract interpretation
  In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...
  
   techniques and many other plugins make use of its results.
• jessie: to verify properties in a deductive manner. Jessie relies on the Why back-end to enable proof obligations to be sent to automatic theorem provers like Z3, Simplify, Alt-Ergo or interactive theorem provers
  Interactive theorem proving
  In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...
  
   like Coq
  Coq
  In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
  
  . Using Jessie, an implementation of bubble-sort or a toy e-voting system can be proved to satisfy their respective specifications.
• impact analysis: to highlight in the C source code the impacts of a modification.
• slicing: this plugin enables to slice a program (program slicing). It enables to generate a smaller new C program which preserves some given properties.
• spare code: this plugin removes useless code from a C program.

Features

Frama-C can be used for the following purposes:

• to understand C code which you have not written. In particular Frama-C enables to: observe a set of values, slice the program into shorter programs, navigate in the program.

• to prove formal properties on the code. Using specifications written in ANSI/ISO C Specification Language
  ANSI/ISO C Specification Language
  The ANSI/ISO C Specification Language is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm...
  
   enables to ensure properties of the code for any possible behavior. Frama-C handles floating point numbers .

• to enforce coding standards or code conventions on C source code, by means of custom plugin(s).

• to instrument C code against some security flaws

See also

• comparison with SPARK (programming language)

External links

• Frama-C website
• Frama-C discussion list
• Frama-C Bug Tracking System