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! ===============================================================================