Frama-C Note: these instructions refer to an older release of Frama-C; for the latest stable release, click here
--------------------------------------------
INSTALLATION INSTRUCTIONS FOR FRAMA-C SODIUM
--------------------------------------------
(released on 2015-02-01)
===============================================================================
SUMMARY
===============================================================================
0) Summary
1) Automatic Installation
2) Quick Start
3) Requirements
4) Configuration
5) Compilation
6) Installation
7) Custom Installation
8) Testing the Installation
9) Installation of additional plug-ins
10) API Documentation
11) Uninstallation
12) Have Fun with Frama-C!
===============================================================================
AUTOMATIC INSTALLATION
===============================================================================
----------------------------------------------------
Debian >= Squeeze 6.0 and Ubuntu >= Lucid Lynx 10.04
----------------------------------------------------
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
It might be **not** up-to-date with the latest Frama-C release.
------------
Fedora >= 13
------------
If you are using Fedora >= 13 then a Frama-C package is provided:
yum install frama-c
It might be **not** up-to-date with the latest Frama-C release.
----
Opam
----
Opam (http://opam.ocamlpro.com) is a package manager for OCaml libraries and
applications, that runs under Linux and Mac OS X. There is a package for
Frama-C, so that if you have opam installed, you just have to type
opam install frama-c
Note however that you may need to install Gtk, GtkSourceView and GnomeCanvas
separately. These are C libraries with OCaml bindings that are used by the
GUI. Opam manages the binding but not the external libraries yet.
-----------------
Wodi (Windows OS)
-----------------
Wodi (http://wodi.forge.ocamlcore.org/) is a package manager for OCaml libraries
and applications that specifically target the Windows platform. It features
a GUI, so that you just have to select the Frama-C package from there.
--------
Mac OS X
--------
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 meld opam
# Graphical User Interface:
> brew install gtk+ --with-jasper
> brew install gtksourceview libgnomecanvas graphviz
> opam install lablgtk ocamlgraph
# Recommended for Frama-C:
> brew install gmp
> 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
===============================================================================
The remainder of these installation instructions is for building Frama-C from
source.
QUICK START
===============================================================================
1) Install OCaml if not already installed.
1b) Optionally, for the GUI, also install Gtk, GtkSourceView, GnomeCanvas and
Lablgtk2 if not already installed.
2a) On Linux-like distribution:
./configure && make && sudo make install
2b) On Windows+Cygwin or Windows+MinGW+msys:
./configure --prefix C:/windows/path/with/direct/slash && make && make install
3) The binary frama-c (and frama-c-gui if you have lablgtk2) is now installed.
4) 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)
See below for more detailed and specific instructions.
===============================================================================
REQUIREMENTS
===============================================================================
- GNU make version >= 3.81
- Objective Caml >= 3.12.1 (except 4.02.0);
- a C compiler with standard C and POSIX headers and libraries
The Frama-C GUI also requires:
- Gtk (>= 2.4)
- GtkSourceView 2.x
- GnomeCanvas 2.x
- LablGtk >= 2.14.0 (and >= 2.18.2 if you use OCaml >= 4.02.1)
If OcamlGraph 1.8.5 or 1.8.6 [1] is already installed, then it will be used by
Frama-C. Otherwise the distributed local copy (file ocamlgraph.tar.gz) will be
used.
If Zarith [2] is installed, it will be used by Frama-C. Otherwise another
equivalent less efficient library will be use.
Plug-ins may have their own requirements.
Consult their specific documentations for details.
[1] OcamlGraph: http://ocamlgraph.lri.fr
[2] Zarith: http://forge.ocamlcore.org/projects/zarith
--------------------------
Ubuntu >= Lucid Lynx 10.04
--------------------------
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 \
liblablgtksourceview2-ocaml-dev liblablgtk2-gnome-ocaml-dev
-------------------
Other Linux systems
-------------------
Some other Linux systems (e.g. Fedora) provide packages for the required tools
and libraries. Please look at your favorite one.
Anyway, on any Linux systems, you may use Godi
(http://godi.camlcity.org/godi/index.html) for installing Frama-C with all the
OCaml requirements (but you must install C libraries and tools before).
===============================================================================
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 plug-in can be enabled by --enable-plugin and disabled by --disable-plugin.
By default, all distributed plug-ins 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 plug-ins, and available options.
Under Cygwin or MinGW:
----------------------
Use "./configure --prefix C:/windows/path/with/direct/slash".
===============================================================================
COMPILATION
===============================================================================
Type "make".
Some Makefile targets of interest are:
- doc generates the API documentation
- top generates an OCaml toplevel embedding Frama-C as a library.
- 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)
===============================================================================
INSTALLATION
===============================================================================
Type "make install"
(depending on the installation directory, may require superuser privileges).
It is possible to install 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: (usually in /usr/local/bin)
------------
- frama-c
- frama-c-gui if available
- frama-c.byte bytecode version of frama-c
- frama-c-gui.byte bytecode version of frama-c-gui, if available
- ptests.opt testing tools for Frama-c
- frama-c.toplevel if 'make top' previously done
Shared files: (usually in /usr/local/share/frama-c and subdirectories)
-------------
- some .h and .c files used as preludes by Frama-C;
- some Makefiles used to compile dynamic plug-ins
- some .rc files used to configure Frama-C
- some image files used by the Frama-C GUI
Manuals: (usually in /usr/local/share/frama-c/manuals)
--------
- the Frama-C manuals as .pdf files
Documentation files: (usually in /usr/local/share/frama-c/doc)
--------------------
- files used to generate dynamic plug-in documentation
Object files: (usually in /usr/local/lib/frama-c)
-------------
- object files used to compile dynamic plug-ins
Plug-in files: (usually in /usr/local/lib/frama-c/plugins)
--------------
- object files of available dynamic plug-ins
Man files: (usually in /usr/local/man/man1)
----------
- man files for frama-c (and frama-c-gui if available)
===============================================================================
CUSTOM INSTALLATION
===============================================================================
You can manually move any installed files. However, in such a case, you have to
set specific environment variables in order that Frama-C found the appropriate
objects when required.
The environment variables are:
------------------------------
FRAMAC_SHARE: absolute path to the Frama-C share subdirectory
FRAMAC_LIB: absolute path of the Frama-C lib subdirectory
FRAMAC_PLUGIN: absolute path of the Frama-C plug-in directory.
===============================================================================
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)
===============================================================================
INSTALLATION OF ADDITIONAL PLUG-INS
===============================================================================
Plug-ins may be released independently of Frama-C.
The standard way for installing them should be:
./configure && make && sudo make install
Plug-ins may have their own custom installation procedures.
Consult their specific documentations for details.
===============================================================================
API DOCUMENTATION
===============================================================================
For plug-in developers, the API documentation of the Frama-C kernel and
distributed plug-ins is available in the file frama-c-api.tar.gz, after running
"make doc-distrib".
===============================================================================
UNINSTALLATION
===============================================================================
Type "make uninstall" to remove Frama-C and all the installed plug-ins
(depending on the installation directory, may require superuser privileges).
That works only if you have not manually moved the installed files (see Section
"Custom Installation").
===============================================================================
HAVE FUN WITH FRAMA-C!
===============================================================================