Installation instructions:

if you have ocaml installed,

  ./configure && make && sudo make install

will install frama-c (and frama-c-gui if you have lablgtk2) in /usr/local/bin.
See below for more detailed instructions.

1) Requirements

- GNU make version 3.81
- Objective Caml 3.10.2 ;
  Caml 3.11 is required for compiling dynamic plugins with ocamlopt
- Gtk (>= 2.4) and GtkSourceView 1.x
- lablgtk >= 2.12.0

Note that by default the Why platform is installed together with Frama-C
(if the Jessie plugin is enabled), and might overwrite an existing why
installation. Notice that Why version 2.19 is actually required.

The Jessie plug-in optionally can make use of the APRON library
for its automatic generation of loop invariants. APRON can be found at

2) Configuration

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

configure 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 too experimental to be
released as is).

If you are under Cygwin, use
   "./configure --prefix C:/windows/path/with/direct/slash".

If you have a compatible Why platform version (>= 2.19) installed, using
      "./configure --with-whydir=no"
will not overwrite your Why platform installation.

3) Compilation


Makefile targets that can be interesting 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
tests: performs Frama-C's own tests (use it after oracles)

4) Installation

"make install" (depending on the installation directory, may require superuser

It is possible to perform the installation in a given directory by setting
the DESTDIR variable: "make install DESTDIR=/tmp" installs Frama-C in
sub-directories of /tmp.

The following files are installed:

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

shared files: a directory share/frama-c contains some .h files used as
preludes by Frama-C.

Moreover, as stated above, the Why platform itself is installed if you have
enabled the jessie plugin.