Note: these instructions refer to an older release of Frama-C; for the latest stable release, click here

Installation instructions for Frama-C Lithium (released on 2008-12-01)

Assuming OCaml (and the LablGtk2 bindings for the GUI) are installed, the following commands should be enough to compile Frama-C: 

  tar zxvf frama-c-Lithium-20081201.tar.gz
  cd frama-c-Lithium-20081201
  ./configure
  make
  make install

The binaries frama-c (and frama-c-gui if you have LablGtk2) are installed in /usr/local/bin. See below for more detailed instructions. You may also consult the INSTALL file within the source distribution.

Requirements

The following environments have been verified to compile Frama-C provided that the proper OCaml and LablGTK version were installed:

  • Ubuntu Linux 7.10 and 8.04 (x86 and AMD64)
  • Windows XP x86 with the MinGW version of OCaml
  • Mac OS X 10.5.5 on Intel and PowerPC

Other distributions may also be able to compile Frama-C provided they have the following tools:

  • GNU make version 3.81
  • OCaml 3.10.2 (other versions of OCaml are not supported)
  • LablGtk2 2.10.1 (gtksourceview must be installed and have been detected by lablgtk's configure).

You may use Godi to install Frama-C and the appropriate OCaml and LablGtk versions.

Ocamlgraph and the Why platform are included in this distribution. Note that the Why platform is installed together with Frama-C (if the jessie plug-in is enabled), and might overwrite an existing why installation. Why version 2.17 is required, and versions 2.16 and below are not compatible with Frama-C.

Configuration

Frama-C is configured by ./configure [options]

The configure script is generated by autoconf, so that the standard options for setting installation directories are available. In particular --prefix=/path sets the installation path. A plugin can be enabled by --enable-plugin and disabled by --disable-plugin. By default, all distributed plugins are enabled. See ./configure --help for the current list of plugins. Those who defaults to 'no' are not part of the Frama-C distribution (usually because they are currently too experimental to be released).

If you have a compatible Why platform version (2.16 or higher) installed, using ./configure --with-why-dir=no will not overwrite your Why platform installation.

Compilation

make

Interesting Makefile targets are:

  • doc: generates the API documentation
  • ptests: generates the executable that takes care of running Frama-C's tests
  • oracles: set up the tests oracle of Frama-C test suite for your own configuration.
  • tests: performs Frama-C's tests (use it after oracles)

Installation

make install

Depending on the installation directory, this may require superuser privileges. This installs the following binary files:

  • frama-c
  • frama-c-gui if available
  • frama-c.byte (bytecode version of frama-c)

Shared files are installed into the directory share/frama-c. It contains some .h files used as prelude by Frama-C. As stated above, the Why platform is installed if you have enabled the jessie plug-in.