-
Andre Maroneze authoredAndre Maroneze authored
- Installing Frama-C
- Installing Frama-C via opam
- Installing opam
- Installing Frama-C from opam repository
- Configuring provers for Frama-C/WP
- Reference configuration
- Installing Custom Versions of Frama-C
- Installing Frama-C on Windows via WSL
- Prerequisites: WSL + a Linux distribution
- Installing opam and Frama-C on WSL
- Running the Frama-C GUI on WSL
- WSL 1
- WSL 2
- Installing Frama-C on macOS
- Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)
- Compiling from source
- Quick Start
- Full Compilation Guide
- Frama-C Requirements
- Compilation
- Testing
- Installation
- API Documentation
- Uninstallation
- Testing the Installation
- Available resources
- Executables: (in /INSTALL_DIR/bin)
- Shared files: (in /INSTALL_DIR/share/frama-c and subdirectories)
- 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
- Frama-C additional tools
- HAVE FUN WITH FRAMA-C!
Installing Frama-C
- Installing Frama-C
- Testing the Installation
- Installing Additional Frama-C Plugins
- Frama-C additional tools
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 explicitly 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 this version of Frama-C.
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 [--with-test]
# 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. The option --with-test
is optional and
is necessary only if you want to be able to execute the tests available in
the frama-c repository.
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 Windows Subsystem for Linux (WSL).
Note: if you have WSL2 (Windows 11), you can run the graphical interface directly, thanks to WSLg. If you are using WSL 1, you need to install an X server for Windows, such as VcXsrv (see section "Running the Frama-C GUI on WSL").
Prerequisites: WSL + a Linux distribution
To enable WSL on Windows, you may follow these instructions (we tested with Ubuntu 20.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
Notes:
- older builds of Windows 10 and systems without access to the Microsoft Store may have no compatible Linux packages.
- in WSL 1, Frama-C/WP cannot use Why3 because of some missing features in WSL support, thus using WSL 2 is highly recommended.
Installing opam and Frama-C on WSL
To install opam, some packages are required. The following commands can be run to update the system and install those packages:
sudo apt update
sudo apt upgrade
sudo apt install make m4 gcc opam gnome-icon-theme
Then opam can be set up using these commands:
opam init --disable-sandboxing --shell-setup
eval $(opam env)
opam install -y depext
You can force a particular Ocaml version during opam init
by using the option
-c <version>
if needed. For instance, you can try installing the OCaml version
mentioned in the reference configuration.
Now, to install Frama-C, run the following commands, which 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
If you have WSL2: a known issue with some versions of Frama-C, lablgtk3 and
Wayland requires prefixing the command running the Frama-C GUI with
GDK_BACKEND=x11
, as in:
GDK_BACKEND=x11 frama-c-gui <options>
If you have WSL 1: WSL 1 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 VcXsrv from the Windows menu (it is named XLaunch), the firewall must authorize both "Public" and "Private" domains. On the first configuration screen, select "Multiple Windows". On the second:
- keep "Start no client" selected,
- keep "Native opengl" selected,
- select "Disable access control".
Now specific settings must be provided in WSL. you can put the export commands
in your ~/.bashrc
file, so this is done automatically when starting WSL.
WSL 1
The Xserver is ready. From WSL, run:
export LIBGL_ALWAYS_INDIRECT=1
export DISPLAY=:0
frama-c-gui
WSL 2
export LIBGL_ALWAYS_INDIRECT=1
export DISPLAY=$(cat /etc/resolv.conf | grep nameserver | awk '{print $2; exit;}'):0.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.
-
Install required general macOS tools for OCaml:
brew install opam
Do not forget to
opam init
andeval $(opam env)
for a proper opam installation (if not already done before). -
Set up a compatible OCaml version (replace
<version>
with the version indicated in the reference configuration):opam switch create <version>
-
Install Frama-C:
opam install frama-c
Opam may ask for the administrator password to handle required system dependencies.
It is likely that, at this point, opam will fail due to some Homebrew packages and pkg-config. The error messages should indicate what you need to do, e.g.:
For pkg-config to find zlib you may need to set: export PKG_CONFIG_PATH="/usr/local/opt/zlib/lib/pkgconfig"
After setting such environment variables, re-running
opam install frama-c
should work. If you still have issues, try manually installing the required packages (viabrew install <package>
) and then re-installing Frama-C. Note: opam packages prefixed withconf-
only check if the corresponding system package is findable. If you cannot install someconf-
package, the solution will likely involve Homebrew and/or setting environment variables, not opam. -
Install the new Frama-C graphical interface (Ivette).
The traditional GTK-based Frama-C GUI no longer works on macOS!
You need to use Ivette, the new Frama-C graphical interface. Instructions on installing and running it are presented by opam when the
frama-c
package is installed. Follow them to get Ivette running.
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
-
Install opam and use it to get all of Frama-C's dependencies (including some external ones):
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
If not using opam, you will need to install the Frama-C dependencies by yourself. The
opam
file in the Frama-C .tar.gz lists the required dependencies (e.g.ocamlfind
,ocamlgraph
,zarith
, etc.). A few of these dependencies are optional, only required for the graphical interface:lablgtk
,conf-gnomecanvas
andconf-gtksourceview
(or the equivalent Gtk+3 packages). -
On Linux-like distributions:
make RELEASE=yes && make install
See section Installation below for options.
-
On Windows+Cygwin:
make RELEASE=yes && make install
-
The binary
frama-c
(andframa-c-gui
if you have lablgtk2) is now installed.
Full Compilation Guide
Frama-C Requirements
See the opam
file, section depends
, for compatible OCaml versions and
required dependencies (except for those related to lablgtk
, which are
required for the GUI but otherwise optional).
To install the required dependencies, you can use opam v2.1 or higher to do the following (assuming you are in frama-c root source folder):
-
opam switch create frama-c ocaml-base-compiler.4.13.1
to create a compatible opam switch -
opam pin . -n
to pin to the latest development version -
opam install --deps-only .
will fetch and build all relevant dependencies
Compilation
There are basically two compilation modes: development and release.
Typing make
builds in development mode, this is a shortcut for:
dune build @install
Typing make RELEASE=yes
builds in release mode, this is a shortcut for:
dune build @install --release --promote-install-files=false
For more precise build configuration, use directly the dune
command.
Testing
Basic tests can be executed using:
make run-ptests
make default-tests
Beware! If the tests fail due to JSON output, it is likely because of the
Yojson package version. Make sure that your opam
dependencies have been
installed with the option --with-test
(see Installing Custom Versions of Frama-C).
Installation
Type make install
(depending on the installation directory, this may require
superuser privileges. The installation directory is chosen through the variable
PREFIX
). This is a shortcut for:
dune install
The Makefile (and dune) supports the DESTDIR
variable, that can be used to
configure the location of the installation.
API Documentation
For plugin developers, the API documentation of the Frama-C kernel and
distributed plugins is available in the _build/default/_doc/_html
directory
after running:
make doc
or:
dune build @doc
Uninstallation
Type make uninstall
to remove Frama-C and all the installed plugins.
(Depending on the installation directory, this may require superuser
privileges.)
Testing the Installation
This step is optional.
Download some test files:
export PREFIX_URL="https://git.frama-c.com/pub/frama-c/raw/master/tests/value"
wget -P test ${PREFIX_URL}/CruiseControl.c
wget -P test ${PREFIX_URL}/CruiseControl_const.c
wget -P test ${PREFIX_URL}/CruiseControl.h
wget -P test ${PREFIX_URL}/CruiseControl_extern.h
wget -P test ${PREFIX_URL}/scade_types.h
wget -P test ${PREFIX_URL}/config_types.h
wget -P test ${PREFIX_URL}/definitions.h
Then test your installation by running:
frama-c -eva test/CruiseControl*.c
# or (if frama-c-gui is available)
frama-c-gui -eva test/CruiseControl*.c
Available resources
Once Frama-C is installed, the following resources should be installed and available:
/INSTALL_DIR/bin
)
Executables: (in frama-c
-
frama-c-gui
if available -
frama-c-config
lightweight wrapper used to display configuration paths -
frama-c-hdrck
header checking tool for Frama-C -
frama-c-ptests
testing tool for Frama-c -
frama-c-wtests
testing tool for Frama-c -
frama-c-script
utilities related to analysis parametrization
/INSTALL_DIR/share/frama-c
and subdirectories)
Shared files: (in - some
.h
and.c
files used as preludes by Frama-C - some
Makefiles
used to compile dynamic plugins - some
.rc
files used to configure Frama-C - some image files used by the Frama-C GUI
- some files for Frama-C/plug-in development (autocomplete scripts, Emacs settings, scripts for running Eva, ...)
- an annotated C standard library (with ACSL annotations) in
libc
- plugin-specific files (in directories
wp
,e-acsl
, etc.)
/INSTALL_DIR/lib/frama-c
)
Object files: (in - object files used to compile dynamic plugins
/INSTALL_DIR/lib/frama-c/plugins
)
Plugin files: (in - object files of available dynamic plugins
/INSTALL_DIR/share/man/man1
)
Man files: (in -
man
files forframa-c
(andframa-c-gui
if available)
Installing Additional Frama-C Plugins
Plugins may be released independently of Frama-C.
The standard way for installing them should be:
dune build @install && dune install
Plugins may have their own custom installation procedures. Consult their specific documentation for details.
Frama-C additional tools
A few additional tools that are unnecessary for most users might be useful for plugin developers. These tools are:
-
frama-c-lint
, used for checking coding conventions -
frama-c-hdrck
, used for checking file license headers
They can be installed either by pinning them via Opam:
opam pin tools/lint
opam pin tools/hdrck
Or by compiling/installing Frama-C manually in developer mode:
FRAMAC_DEVELOPER=yes make
FRAMAC_DEVELOPER=yes make install
# Or:
make -C tools/<the-tool>
make -C tools/<the-tool> install
For convenience, FRAMAC_DEVELOPER
can be exported globally.