--- layout: doc_page title: Installation instructions for Phosphorus ---
The preferred method of installation for Frama-C is using OPAM (v1.2 or newer).
First you need to install OPAM, then you may install Frama-C using OPAM:
opam install frama-c
Note: make sure your OPAM version is >= 1.2.
Also, it is highly recommended that you install an external solver
for OPAM, such as aspcud
, otherwise unexpected
dependency errors may occur during installation.
Several Linux distributions already include an opam
package.
OSX has OPAM through Homebrew.
A Windows OPAM is currently being developed, but it is not yet stable.
Note: Some distributions include an old version of OPAM (<= 1.1). It cannot be used to reliably install Frama-C due to conflicts between dependencies.
If your system does not have an OPAM package, you can compile it from source, or use the provided OPAM binaries available at:
http://opam.ocaml.org/doc/Install.html
There are two Frama-C packages in OPAM:
frama-c-base
: minimal Frama-C installation,
without GUI; few dependenciesframa-c
: includes all GUI-related dependencies,
plus other recommended packages.The frama-c
package recommends the installation of
optional packages, e.g. external provers for WP, such as
why3
and coq
.
To install frama-c
, you may need to install Gtk,
GtkSourceView and GnomeCanvas separately. These are C libraries
with OCaml bindings used by the GUI. On many systems, OPAM can take
care of these external dependencies through its depext
plug-in: issuing the two commands
opam install depext
opam depext frama-c
will install the appropriate system packages (this of course requires to have administrator rights on the system).
If you have a non-standard version of Frama-C available (with proprietary extensions, custom plugins, etc.), you can use OPAM to install Frama-C's dependencies and compile your own sources directly:
# optional: remove the standard frama-c package if it was installed
opam remove --force frama-c frama-c-base
# install Frama-C's dependencies
opam install depext
opam depext frama-c
opam install --deps-only frama-c
# install custom version of frama-c
opam pin add frama-c-base <dir>
where <dir>
is the root of your unpacked
Frama-C archive.
If your extensions require other libraries than the ones already used by Frama-C, they must of course be installed as well.
Windows is not officially supported by the Frama-C team (as in, we may not have the time to fix all issues), but Frama-C has been succesfully compiled in Windows with the following tools:
Installation instructions are described (and updated continuously) on the Frama-C wiki:
https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:compiling_from_source
Frama-C Windows releases are periodically made available on the non-official OPAM MinGW repository:
https://github.com/fdopen/opam-repository-mingw
OPAM works perfectly on Mac OS via Homebrew.
Recommended installation:
General Mac OS tools for OCaml:
xcode-select --install
open http://brew.sh
brew install git autoconf opam gmp
brew cask install meld
Graphical User Interface:
brew install gtk+ --with-jasper
brew install gtksourceview libgnomecanvas graphviz
opam install lablgtk ocamlgraph
Required for Frama-C:
opam install zarith
Necessary for Frama-C/WP:
opam install alt-ergo
Also recommended for Frama-C/WP:
opam install altgr-ergo coq coqide why3
NOTE: Distribution packages are not as up-to-date as OPAM packages. We recommend using OPAM if possible.
If you are using Debian >= Squeeze 6.0 or Ubuntu >= Lucid Lynx 10.04 then a Frama-C package is provided:
sudo apt-get install frama-c
or, if you don't want the Gtk-based GUI:
sudo apt-get install frama-c-base
If you are using Fedora >= 13 then a Frama-C package is provided:
yum install frama-c
Note: These instructions are no longer required in the vast majority of cases. They are kept here mostly for historical reference.
Install OCaml, OCamlfind, OCamlGraph and Zarith if not already installed. Note that OCaml >= 4.02.3 is needed in order to compile Frama-C.
(Optional) For the GUI, also install Gtk, GtkSourceView, GnomeCanvas and Lablgtk2 if not already installed. See section 'REQUIREMENTS' below for indications on the names of the packages to install, or use 'opam depext' as explained in section 'Opam' above.
On Linux-like distributions:
./configure && make && sudo make install
See section Configuration below for options.
On Windows+Cygwin or Windows+MinGW+msys:
./configure --prefix C:/windows/path/with/direct/slash/no/space && make && make install
The binary frama-c
(and frama-c-gui
if
you have lablgtk2) is now installed.
Optionally, test your installation by running:
frama-c -val tests/misc/CruiseControl*.c
frama-c-gui -val tests/misc/CruiseControl*.c # if frama-c-gui is available
The Frama-C GUI also requires:
Plugins may have their own requirements. Consult their specific documentations for details.
If you are using Ubuntu >= Precise Pangolin 12.04 then an optimal list of packages is installed by:
sudo apt-get install ocaml ocaml-native-compilers graphviz \
libzarith-ocaml-dev libfindlib-ocaml-dev \
liblablgtksourceview2-ocaml-dev liblablgtk2-gnome-ocaml-dev
If you are using a recent Fedora, an optimal list of packages
can be installed through (replace dnf
by
yum
in older versions of Fedora):
sudo dnf install ocaml graphviz \
ocaml-zarith-devel ocaml-findlib ocaml \
ocaml-lablgtk-devel gtksourceview2-devel libgnomecanvas-devel
Some other Linux systems provide packages for the required tools and libraries. Please send us patches to update this section for your favorite distro.
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. Those who defaults to 'no' are not
part of the Frama-C distribution (usually because they are too
experimental to be released as is).
See ./configure --help
for the current list of
plugins, and available options.
Use ./configure --prefix
C:/windows/path/with/direct/slash
.
Type make
.
Some Makefile targets of interest are:
doc
generates the API documentationtop
generates an OCaml toplevel embedding Frama-C
as a library.oracles
sets up the Frama-C test suite oracles for
your own configuration.tests
performs Frama-C's own testsUse: make FRAMAC_ROOT_SRCDIR="$(cygpath -a -m
$PWD)"
Type make install
(depending on the installation
directory, this may require superuser privileges. The installation
directory is chosen through --prefix
).
This step is optional.
Test your installation by running:
frama-c -val tests/misc/CruiseControl*.c
frama-c-gui -val tests/misc/CruiseControl*.c (if frama-c-gui is available)
For plugin developers, the API documentation of the Frama-C
kernel and distributed plugins is available in the file
frama-c-api.tar.gz
, after running make
doc-distrib
.
Type make uninstall
to remove Frama-C and all the
installed plugins. (Depending on the installation directory, this
may require superuser privileges.)
Once Frama-C is installed, the following resources should be installed and available:
/INSTALL_DIR/bin
)frama-c
frama-c-gui
if availableframa-c-config
displays Frama-C configuration
pathsframa-c.byte
bytecode version of frama-cframa-c-gui.byte
bytecode version of frama-c-gui,
if availableptests.opt
testing tool for Frama-cframa-c.toplevel
if 'make top' previously
done/INSTALL_DIR/share/frama-c
and
subdirectories).h
and .c
files used as preludes
by Frama-CMakefiles
used to compile dynamic
plugins.rc
files used to configure Frama-C/INSTALL_DIR/share/frama-c/doc
)/INSTALL_DIR/lib/frama-c
)/INSTALL_DIR/lib/frama-c/plugins
)/INSTALL_DIR/man/man1
)man
files for frama-c
(and
frama-c-gui
if available)Plugins may be released independently of Frama-C.
The standard way for installing them should be:
./configure && make && sudo make install
Plugins may have their own custom installation procedures. Consult their specific documentations for details.