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 The National Institute for Research in Digital Science and Technology (Inria) () is a French national research institution focusing on computer science and applied mathematics. It was created under the name ''Institut de recherche en informatiq ...

. It has also received funding from the

Core Infrastructure Initiative The Core Infrastructure Initiative (CII) was a project of the Linux Foundation to fund and support free and open-source software projects that are critical to the functioning of the Internet and other major information systems. The project was a ...

. Frama-C, as a

static analyzer In computer science, static program analysis (or static analysis) is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution. The term ...

, inspects programs without executing them. Despite its name, the software is not related to the French project

Framasoft Framasoft is a popular education social network created in November 2001 by , Paul Lunetta, and Georges Silva. Since 2014, it is supported by a nonprofit organization of the same name based in Lyon, France. Mainly focused on free software valori ...

Architecture

Frama-C has a modular plugin architecture comparable to that of

Eclipse (software) Eclipse is an integrated development environment (IDE) used in computer programming. It contains a base workspace and an extensible plug-in system for customizing the environment. It is the second-most-popular IDE for Java development, and, u ...

or GIMP. Frama-C relies on CIL ( C Intermediate Language) to generate an

abstract syntax tree In computer science, an abstract syntax tree (AST), or just syntax tree, is a tree representation of the abstract syntactic structure of text (often source code) written in a formal language. Each node of the tree denotes a construct occurr ...

. The

supports annotations written in

ANSI/ISO C Specification Language The ANSI/ISO C Specification Language (ACSL) is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as C annotation commen ...

(ACSL). Several modules can manipulate the

to add

(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 of its results. * ''Jessie'' verifies properties in a deductive manner. Jessie relies on the Why or Why3 back-end to enable proof obligations to be sent to automatic theorem provers like Z3, Simplify, Alt-Ergo or interactive theorem provers like

Coq Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...

or Why. Using Jessie
an implementation of bubble-sort
o
a toy e-voting system
can be proved to satisfy their respective specifications. It uses a separation memory model inspired by separation logic. * ''WP (Weakest Precondition)'' similar to ''Jessie'', verifies properties in a deductive manner. Unlike Jessie, it focuses on parameterization with regards to the memory model. WP is designed to cooperate with other Frama-C plugins such as the value analysis plug-in, unlike Jessie that compiles the C program directly into the Why language. WP can optionally use the Why3 platform to invoke many other automated and interactive provers. * ''Impact analysis'' highlights the impacts of a modification in the C source code. * ''Slicing'' enables slicing of a program. It enables generation of a smaller new C program that preserves some given properties. * ''Spare code'' removes useless code from a C program. Other plugins are: * ''Dominators'' computes dominators and postdominators of statements. * ''From analysis'' computes functional dependencies.

Features

Frama-C can be used for the following purposes: * To understand C code which you have not written. In particular, Frama-C enables one to observe a set of values, slice the program into shorter programs, and navigate in the program. * To prove formal properties on the code. Using specifications written in

enables it to ensure properties of the code for any possible behavior. Frama-C handles floating point numbers. * To enforce coding standards or

code conventions Coding conventions are a set of guidelines for a specific programming language that recommend programming style, practices, and methods for each aspect of a program written in that language. These conventions usually cover file organization, ind ...

on C source code, by means of custom plugin(s) * To instrument C code against some security flaws

References

External links

*{{Official website, frama-c.com
Frama-C discussion listFrama-C Bug Tracking System
C programming language family Formal methods tools Linux software OCaml software Science software that uses GTK Software testing tools Software that uses Cairo (graphics) Software using the LGPL license Static program analysis tools

Architecture

Features

See also

References

External links