INSTALL.md

Installing Frama-C

• Installing Frama-C
  • Table of Contents
  • Installing Frama-C via opam
    • Installing opam
    • Installing Frama-C from opam repository
    • Installing Custom Versions of Frama-C
    • Installing Frama-C on Windows via WSL
    • Installing Frama-C on macOS
  • Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)
  • Compiling from source
    • Quick Start
    • Full Compilation Guide
• Testing the Installation
  • Available resources
    • Executables: (in /INSTALL_DIR/bin)
    • Shared files: (in /INSTALL_DIR/share/frama-c and subdirectories)
    • Documentation files: (in /INSTALL_DIR/share/frama-c/doc)
    • Object files: (in /INSTALL_DIR/lib/frama-c)
    • Plugin files: (in /INSTALL_DIR/lib/frama-c/plugins)
    • Man files: (in /INSTALL_DIR/share/man/man1)
• Installing Additional Frama-C 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.

Installing opam

Several Linux distributions already include an opam package.

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, you can 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. On most systems, opam's depext mechanism can take care of installing these external dependencies. As of version 2.1.0, depext is directly included in opam, so that the following command should install everything, at least if your OS is supported by depext (and you have administrative rights):

opam install frama-c

For older opam versions, you have to install it separately and call it explicitely with the following commands, before installing Frama-C as above. Again, installing the external dependencies requires administrative rights.

# install Frama-C's dependencies with pre-2.1.0 opam
opam install depext
opam depext frama-c

If there are errors due to missing external dependencies, opam may emit a message indicating which packages to install. If this is not sufficient, there may be missing dependencies in opam's depext tool. In this case, you may create a Gitlab issue indicating your distribution and error message.

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:

why3 config detect

Reference configuration

See file reference-configuration.md for a set of packages that is known to work with Frama-C 24 (Chromium).

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 # only for opam < 2.1.0
opam depext frama-c # only for opam < 2.1.0
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.