Frama-C

From Infogalactic: the planetary knowledge core
Jump to: navigation, search


Frama-C
Frama-C logo.
Developer(s) Commissariat à l'Énergie Atomique and Inria
Written in OCaml
Operating system Microsoft Windows, FreeBSD, Linux, Mac OS X
Available in English
Type Formal verification, Static code analysis
License mostly LGPL, some parts under BSD licenses
Website frama-c.com

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 and Inria. Frama-C, as a static analyzer, inspects programs without executing them.

Architecture

Frama-C has a modular plugin architecture[1] 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[vague] 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[2] 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 or Why. Using Jessie, an implementation of bubble-sort or a toy e-voting system can be proved to satisfy their respective specifications. It uses a separation memory model inspired by separation logic.
  • WP – 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.[3]
  • 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 ANSI/ISO C Specification Language enables it to ensure properties of the code for any possible behavior. Frama-C handles floating point numbers.[4]
  • To enforce coding standards or code conventions on C source code, by means of custom plugin(s)[5]
  • To instrument C code against some security flaws[6]

See also

References

  1. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  2. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  3. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  4. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  5. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  6. ↑ Lua error in package.lua at line 80: module 'strict' not found.

External links

Retrieved from "https://infogalactic.com/w/index.php?title=Frama-C&oldid=722923876"