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

Installation instructions for Frama-C Hydrogen (released on 2008-05-02)

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-Hydrogen-20080502.tar.gz
  cd frama-c-Hydrogen-20080502
  ./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.

Requirements

The following environments have been verified to compile Frama-C:

  • Ubuntu Linux 7.10 and 8.04 (x86 and AMD64)
  • Windows XP x86 with the Mingw version of ocaml
  • MacOS X 5.2 on Intel and PowerPC. (installation of the Why platform is not yet possible)

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

  • GNU make version 3.81
  • Objective Caml 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).

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. The current distributed version of Why is not compatible with Frama-C.

Configuration

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

The configure file is generated by autoconf, so that the standard options for setting installation directories are available, in particular --prefix=/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).

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.