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 MAGNESIUM
-----------------------------------------------
(released on 2015-10-02)
===============================================================================
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. To get the exact list of packages that are needed, use
opam install depext
opam depext frama-c
and install the packages listed as missing.
------------------------
Opam from custom sources
------------------------
If you have a non-standard version of Frama-C available (containing proprietary
extensions, custom plugins, etc.), you can install it through
Opam using the commands:
#remove the previous version of frama-c
opam remove --force frama-c frama-c-base
# All these packages are optional. However, zarith is strongly recommended,
# and the other packages are required for the GUI
opam install depext
opam depext zarith lablgtk conf-gtksourceview conf-gnomecanvas
opam install zarith lablgtk conf-gtksourceview conf-gnomecanvas
# Install the custom version of frama-c
opam pin add frama-c-base <dir>
where <dir> is the root of the unpacked Frama-C distribution
-----------------
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. If possible, also install Zarith.
See section 'REQUIREMENTS' below for indications on the names of the
packages to install, or use 'opam depext' as explained in section 'Opam'
above.
2a) On Linux-like distribution:
./configure && make && sudo make install
See section CONFIGURATION below for options
2b) On Windows+Cygwin or Windows+MinGW+msys:
./configure --prefix C:/windows/path/with/direct/slash/no/space && 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 4.x (except 4.02.2, 4.02.0 and 4.00.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 libfindlib-ocaml-dev \
liblablgtksourceview2-ocaml-dev liblablgtk2-gnome-ocaml-dev
------
Fedora
------
If you are using a recent Fedora, an optimal list of packages can be installed
through (replace dnf by yum in older version of Fedora):
sudo dnf install ocaml graphviz \
ocaml-zarith-devel ocaml-findlib ocaml \
ocaml-lablgtk-devel gtksourceview2-devel libgnomecanvas-devel
-------------------
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!
===============================================================================