Table of Contents
- Installing Frama-C
- Table of Contents
- Installing Frama-C via opam
- Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)
- Compiling from source
- Available resources
- Installing Additional Plugins
- HAVE FUN WITH FRAMA-C!
Installing Frama-C via opam
opam is the OCaml package manager. Every Frama-C release is made available via an opam package.
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.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
OSX has opam through Homebrew.
A Cygwin-based opam is available on Windows. It is less stable than it is for the other OSes, but should work.
If your system does not have an opam package >= 1.2.2 you can compile it from source, or use the provided opam binaries available at:
Installing Frama-C from opam
The Frama-C package in opam is called
frama-c, which includes both the command-line
frama-c executable and the graphical interface
(Note: before version 16 Sulfur, there were two packages,
frama-c, which were merged together.)
frama-c includes non-OCaml dependencies, such as Gtk and GMP. In most 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 administrator rights on the system).
If your system is not supported by
depext, you will need to install Gtk, GtkSourceView, GnomeCanvas and GMP, including development libraries, separately. If you do so, please consider providing the system name and list of packages (e.g. via a Github issue) so that we can add it to the Frama-C
Installing Custom Versions of Frama-C via opam
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 --kind=path frama-c <dir>
<dir> is the root of your unpacked Frama-C archive. See
opam pin for more details.
If your extensions require other libraries than the ones already used by Frama-C, they must of course be installed as well.
Installing Frama-C on Windows (via Cygwin + opam)
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 successfully compiled in Windows with the following tools:
- Cygwin (for shell and installation support only; the compiled binaries do not depend on Cygwin)
- opam for Windows (currently experimental)
- OCaml MinGW-based compiler
You may follow these instructions for installing OCaml for Windows:
lablgtk (used by Frama-C) requires installing
depext-cygwinports, as indicated in the page.
Once the Windows-based opam repository is configured, simply run:
opam install frama-c
Some (now obsoleted) compilation instructions for older versions of Frama-C on Windows are available on the Frama-C wiki:
Installing Frama-C on macOS
Install required general macOS tools for OCaml:
brew install autoconf pkg-config opam
Do not forget to
eval `opam config env`for a proper opam installation (if not already done before on your machine).
Install required dependencies for Frama-C:
brew install gmp gtk+ gtksourceview libgnomecanvas
Install recommended dependencies for Frama-C:
brew install graphviz opam install altgr-ergo why3
Install optional dependencies for Frama-C/WP:
opam install coq coqide
opam install frama-c
Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)
NOTE: Distribution packages are updated later than opam packages, so if you want access to the most recent versions of Frama-C, opam is currently the recommended approach.
Also note that it is not recommended to mix OCaml packages installed by your distribution with packages installed via opam. When using opam, we recommend uninstalling all
ocaml-* packages from your distribution, and then installing, exclusively via opam, an OCaml compiler and all the OCaml packages you need. This ensures that only those versions will be in the PATH.
The advantage of using distribution packages is that dependencies are almost always handled by the distribution's package manager. The disadvantage is that, if you need some optional OCaml package that has not been packaged in your distribution (e.g.
landmarks, which is distributed via opam), it may be very hard to install it, since mixing opam and non-opam packages often fails (and is strongly discouraged).
apt-get install frama-c
dnf install frama-c
yaourt -S frama-c
Compiling from source
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.
./configure --prefix="$(cygpath -a -m <installation path>)" && make && make install
frama-c-guiif 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
Full Compilation Guide
- GNU make version >= 3.81
- OCaml >= 4.02.3
- a C compiler with standard C and POSIX headers and libraries
- OCamlGraph >= 1.8.8
- findlib >= 1.6.1
The Frama-C GUI also requires:
- Gtk (>= 2.4)
- GtkSourceView 2.x
- GnomeCanvas 2.x
- LablGtk >= 2.18.5
Plugins may have their own requirements. Consult their specific documentations for details.
Frama-C is configured by
configure is generated by
autoconf, so that the standard options for setting installation directories are available, in particular
A plugin can be enabled by
--enable-plugin and disabled by
--disable-plugin. By default, all distributed plugins are enabled. Those who default to 'no' are not part of the Frama-C distribution (usually because they are too experimental to be released as is).
./configure --help for the current list of plugins, and available options.
./configure --prefix="$(cygpath -a -m <installation path>)".
(using Unix-style paths without the drive letter will probably not work)
Some Makefile targets of interest are:
docgenerates the API documentation.
topgenerates an OCaml toplevel embedding Frama-C as a library.
oraclessets up the Frama-C test suite oracles for your own configuration.
testsperforms Frama-C's own tests.
make install (depending on the installation directory, this may require superuser privileges. The installation directory is chosen through
Testing the Installation
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 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:
frama-c-configdisplays Frama-C configuration paths
frama-c.bytebytecode version of frama-c
frama-c-gui.bytebytecode version of frama-c-gui, if available
ptests.opttesting tool for Frama-c
frama-c.toplevelif 'make top' previously done
Shared files: (in
/INSTALL_DIR/share/frama-c and subdirectories)
.cfiles used as preludes by Frama-C
Makefilesused to compile dynamic plugins
.rcfiles used to configure Frama-C
- some image files used by the Frama-C GUI
- some files for Frama-C/plug-in development (autocomplete scripts, Emacs settings, scripts for running Eva, ...)
Documentation files: (in
- files used to generate dynamic plugin documentation
Object files: (in
- object files used to compile dynamic plugins
Plugin files: (in
- object files of available dynamic plugins
Man files: (in
Installing Additional Plugins
Plugins may be released independently of Frama-C.
The standard way for installing them should be:
./configure && make && make install
Plugins may have their own custom installation procedures. Consult their specific documentation for details.