Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • stable/zinc
  • 2699-wp-region-plugin-division-by-0-with-empty-region-node
  • stable/copper
  • stable/nickel
  • stable/cobalt
  • stable/iron
  • stable/manganese
  • stable/chromium
  • stable/vanadium
  • stable/titanium-backport
  • stable/titanium
  • stable/scandium
  • 30.0 protected
  • 30.0-beta protected
  • MIEL-2024-10 protected
  • 29.0 protected
  • 29.0-beta protected
  • 28.1 protected
  • 28.0 protected
  • MIEL-2023-10 protected
  • 28.0-beta protected
  • 27.1 protected
  • 27.0 protected
  • 27.0-beta protected
  • 26.1 protected
  • 26.0 protected
  • 26.0-beta protected
  • 25.0-r1 protected
  • pre-dune protected
  • 25.0 protected
  • 25.0-beta protected
  • 2022-03-23 protected
33 results
Blame Permalink
INSTALL.md 15.90 KiB

Installing 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.

Installing opam

Several Linux distributions already include an opam package.

Note: make sure your opam version is >= 2.0.0.

macOS has opam through Homebrew.

Windows users can install opam via WSL (Windows Subsystem for Linux).

If your system does not have an opam package >= 2.0.0 you can compile it from source, or use the provided opam binaries available at:

http://opam.ocaml.org/doc/Install.html

Installing Frama-C from opam repository

The Frama-C package in opam is called frama-c, which includes both the command-line frama-c executable and the graphical interface frama-c-gui.

frama-c has some 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

# install Frama-C's dependencies
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 depext package.

# install Frama-C
opam install frama-c

Configuring provers for Frama-C/WP

Frama-C/WP uses the Why3 platform to run external provers for proving ACSL annotations. The Why3 platform and the Alt-Ergo prover are automatically installed via opam when installing Frama-C.

Other recommended, efficient provers are CVC4 and Z3. They can be used as replacement or combined with Alt-Ergo. Actually, you can use any prover supported by Why3 in combination with Frama-C/WP.

Most provers are available on all platforms. After their installation, Why3 must be configured to make them available for Frama-C/WP:

```shell
why3 config --detect
```

Known working configuration

The following set of packages is known to be a working configuration for Frama-C 20 (Calcium):

  • OCaml 4.05.0
  • ocamlfind.1.8.0
  • apron.20160125 (optional)
  • lablgtk.2.18.8 | lablgtk3.3.0.beta6 + lablgtk3-sourceview3.3.0.beta6
  • mlgmpidl.1.2.11 (optional)
  • ocamlgraph.1.8.8
  • why3.1.2.0
  • alt-ergo.2.0.0 (for wp, optional)
  • yojson.1.7.0
  • zarith.1.9.1

Installing Custom Versions of Frama-C

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

# 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>

where <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 WSL

Frama-C is developed on Linux, but it can be installed on Windows using the following tools:

  • Windows Subsystem for Linux
  • VcXsrv (X server for Windows)

Prerequisites: WSL + a Linux distribution

For enabling WSL on Windows, you may follow these instructions (we tested with Ubuntu 18.04 LTS; other distributions/versions should also work, but the instructions below may require some modifications).

https://docs.microsoft.com/en-us/windows/wsl/install-win10

Note: older builds of Windows 10 and systems without access to the Microsoft Store may have no compatible Linux packages.

PowerShell-based quick guide

This is a quick guide based on running a PowerShell with administrator rights. Note that, depending on your build version of Windows 10, the Ubuntu package selected below may not work. If you are unsure, follow the above instructions from the Microsoft website.

Inside PowerShell, run the following command to activate Windows Subsystem for Linux:

Enable-WindowsOptionalFeature -Online -FeatureName Microsoft-Windows-Subsystem-Linux

Then, reboot the operating system.

After rebooting, run again the PowerShell terminal with administrator rights. Move to your user directory, download the distribution and install it:

cd C:\Users\<Your User Directory>
Invoke-WebRequest -Uri https://aka.ms/wsl-ubuntu-1804 -OutFile Ubuntu.appx -UseBasicParsing
Add-AppxPackage .\Ubuntu.appx

Ubuntu should now be available in the Windows menu. Run it and follow the instructions to create a user.

Installing opam and Frama-C on WSL

For installing opam, some packages are required. The following commands can be run to update the system and install those packages:

sudo add-apt-repository -y ppa:avsm/ppa
sudo apt update
sudo apt upgrade
sudo apt install make m4 gcc opam

Then opam can be set up using these commands:

opam init --disable-sandboxing -c 4.05.0 --shell-setup
eval $(opam env)
opam install -y depext

Now, for installing Frama-C, run the following commands that will use apt to install the dependencies of the opam packages and then install them:

opam depext --install -y lablgtk3 lablgtk3-sourceview3
opam depext --install -y frama-c

Running the Frama-C GUI on WSL

Microsoft WSL does not support graphical user interfaces directly. If you want to run Frama-C's GUI, you need to install an X server, such as VcXsrv or Cygwin/X. We present below how to install VcXsrv.

First, install VcXsrv from:

https://sourceforge.net/projects/vcxsrv/

The default installation settings should work. Now run it from the Windows menu (it is named XLaunch). On the first configuration screen, select "Multiple Windows". On the second, keep "Start no client" selected. On the third configuration step, add an additional parameter -nocursor in the field "Additional parameters for VcXsrv". You can save this configuration at the last step if you want, before clicking "Finish".

Once it is done, the Xserver is ready. From WSL, run:

export DISPLAY=:0
frama-c-gui

Installing Frama-C on macOS

opam works perfectly on macOS via Homebrew. We highly recommend to rely on it for the installation of Frama-C.

  1. Install required general macOS tools for OCaml:

    brew install autoconf pkg-config opam

    Do not forget to opam init and eval `opam config env` for a proper opam installation (if not already done before).

  2. Set up a compatible OCaml version (replace <version> with the version indicated in the 'recommended working configuration' section):

    opam switch create <version>

  3. Install required dependencies for Frama-C:

    brew install gmp gtk+ gtksourceview libgnomecanvas

    The graphical libraries require additional manual configuration of your bash profile. Consult this issue on opam for details. A known working configuration is:

    export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/usr/local/lib/pkgconfig

  4. Install recommended dependencies for Frama-C:

    brew install graphviz

  5. Install Frama-C:

    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).

Debian/Ubuntu: apt-get install frama-c

Fedora: dnf install frama-c

Arch Linux: pikaur -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.

Quick Start

  1. Install OCaml, OCamlfind, OCamlGraph and Zarith if not already installed. Note that OCaml >= 4.05.0 is needed in order to compile Frama-C.

  2. (Optional) For the GUI, also install Gtk, GtkSourceView, GnomeCanvas and Lablgtk2 or Lablgtk3 + Lablgtksourceview3 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.

  3. On Linux-like distributions:

     ./configure && make && sudo make install

    See section Configuration below for options.

  4. On Windows+Cygwin:

     ./configure --prefix="$(cygpath -a -m <installation path>)" && make && make install

  5. The binary frama-c (and frama-c-gui if you have lablgtk2) is now installed.

Full Compilation Guide

Frama-C Requirements

  • GNU make version >= 3.81
  • OCaml >= 4.05.0
  • a C compiler with standard C and POSIX headers and libraries
  • OCamlGraph >= 1.8.8
  • findlib >= 1.6.1
  • Zarith

The Frama-C GUI also requires:

  • Gtk (>= 2.4)
  • GtkSourceView 2.x or 3.x (compatible with your Gtk version)
  • GnomeCanvas 2.x (only for Gtk 2.x)
  • LablGtk >= 2.18.5 or Lablgtk3 >= beta5 + corresponding Lablgtksourceview3

Plugins may have their own requirements. Consult their specific documentations for details.

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 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).

See ./configure --help for the current list of plugins, and available options.

Under Cygwin

Use ./configure --prefix="$(cygpath -a -m <installation path>)".

(using Unix-style paths without the drive letter will probably not work)

Compilation