Release snapshots of the Frama-C platform for source code analysis
OCaml C Coq Makefile Shell M4 Other
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
bin release Silicon-20161101 Dec 7, 2016
doc
licenses
man
opam
ptests release Silicon-20161101 Dec 7, 2016
share
src release Silicon-20161101 Dec 7, 2016
tests
.force-reconfigure
.make-clean
.make-clean-stamp release Nitrogen-20111001 Apr 15, 2016
Changelog
INSTALL.md
Makefile release Silicon-20161101 Dec 7, 2016
Makefile.generating
README.md release Silicon-20161101 Dec 7, 2016
VERSION
config.h.in
configure
configure.in release Silicon-20161101 Dec 7, 2016

README.md

Frama-C

Frama-C is a platform dedicated to the analysis of source code written in C.

A Collaborative Platform

Frama-C gathers several analysis techniques in a single collaborative platform, consisting of a kernel providing a core set of features (e.g., a normalized AST for C programs) plus a set of analyzers, called plug-ins. Plug-ins can build upon results computed by other plug-ins in the platform.

Thanks to this approach, Frama-C provides sophisticated tools, including:

  • an analyzer based on abstract interpretation, aimed at verifying the absence of run-time errors (Value);
  • a program proof framework based on weakest precondition calculus (WP);
  • a program slicer (Slicing);
  • a tool for verification of temporal (LTL) properties (Aoraï);
  • several tools for code base exploration and dependency analysis (From, Impact, Metrics, Occurrence, Scope, etc.).

These plug-ins share a common language and can exchange information via ACSL (ANSI/ISO C Specification Language) properties. Plug-ins can also collaborate via their APIs.

Installation

For more detailed information about installing OPAM/Frama-C, see INSTALL.md.

Frama-C is available through OPAM, the OCaml Package Manager. This is the preferred installation method. Be sure to install opam v1.2 or higher. Then the following sequence of commands should install frama-c and its gui:

opam init
opam install depext
opam depext frama-c
opam install frama-c

Frama-C is developed mainly in Linux, often tested in Mac OSX (via Homebrew), and occasionally tested on Windows (with Cygwin + MinGW).

Usage

Frama-C can be run from the command-line, or via its graphical interface.

Simple usage

The recommended usage for simple files is one of the following lines:

frama-c file.c -<plugin> [options]
frama-c-gui file.c

Where -<plugin> is one of the several Frama-C plug-ins, e.g. -val, or -wp, or -metrics, etc. Plug-ins can also be run directly from the GUI.

To list all plug-ins, run:

frama-c -plugins

Each plug-in has a help command (-<plugin>-help or -<plugin>-h) that describes its several options.

Complex scenarios

For more complex usage scenarios (lots of files and directories, with several preprocessing directives), we recommend splitting Frama-C's usage in two parts:

  1. Parsing the input files and saving the result to a file;
  2. Loading the parsing results and then running the analyses or the GUI.

Parsing typically involves giving extra arguments to the C preprocessor, so the -cpp-extra-args option is often useful, as in the example below:

frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

The results are then loaded into Frama-C for further analyses or for inspection via the GUI:

frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

Further reference

  • Links to user and developer manuals, Frama-C archives, and plug-in manuals are available at
    http://frama-c.com/download.html

  • StackOverflow has several questions with the frama-c tag, which is monitored by several members of the Frama-C community.

  • The Frama-c-discuss mailing list is used for announcements and general discussions.

  • The official bug tracking system can be used for bug reports.

  • The Frama-C wiki has some useful information, although it is not entirely up-to-date.

  • The Frama-C blog has several posts about new developments of Frama-C, as well as general discussions about the C language, undefined behavior, floating-point computations, etc.

  • The Github snapshot repository contains the .tar.gz archives of stable Frama-C releases, ready to be cloned.