Installation instructions:
Summary:
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
http://apron.cri.ensmp.fr/library/
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
"make"
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
configuration.
tests: performs Frama-C's own tests (use it after oracles)
4) Installation
"make install" (depending on the installation directory, may require superuser
privileges)
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:
executables:
frama-c
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.