Commit aaa4b95b authored by François Bobot's avatar François Bobot
Browse files

23.0-rc1-Vanadium release

parent 4b931410
layout: default
date: "20-05-2021"
event: Frama-C 23.0~rc1 (Vanadium)
title: Beta release of Frama-C 23.0~rc1 (Vanadium)
link: /fc-versions/vanadium.html
Frama-C 23.0~rc1 (Vanadium) is out. Download it [here](/fc-versions/vanadium.html).
Main changes with respect to Frama-C 22 (Titanium) include:
#### Kernel
- New `admit` annotations (which already accepted `assert` and `check`) to express hypotheses to be admitted but not verified by Frama-C
- Set default machdep to `x86_64`; allow setting machdep via environment variable FRAMAC_MACHDEP
#### AORAI
- New option for tracking the last N states of the automaton. Easier analysis of instrumented code with Eva.
#### E-ACSL
- Add runtime support for Windows
- Add support for loop variant
- Add support for multiple binders in guarded quantifications
#### EVA
- Partial support for recursion: new option -eva-unroll-recursive-calls to
precisely analyze the n first recursive calls, before using the function
specification to interpret the remaining calls.
- Improved automatic widening thresholds
- Improved automatic loop unroll
#### WP
- New internal WP engine, fixing many issues related to control flow graph and
local variable scoping. Support for stmt contracts has been removed. Support
for looping gotos has been removed. Altough unsound, the legacy engine is
still accessible via -wp-legacy option.
- Bump Why3 version to 1.4.0
- Section « Limitation & Roadmap » added to the WP manual.
layout: version
number: 23
name: Vanadium
beta: true
- number: 0
- name: Frama-C v23.0~rc1 Vanadium
- name: Source distribution
link: /download/frama-c-23.0-rc1-Vanadium.tar.gz
help: Compilation instructions
help_link: /html/installations/vanadium.html
- name: User manual
link: /download/user-manual-23.0-rc1-Vanadium.pdf
- name: Plug-in development guide
link: /download/plugin-development-guide-23.0-rc1-Vanadium.pdf
help: Hello plug-in tutorial archive
help_link: /download/hello-23.0-rc1-Vanadium.tar.gz
- name: API Documentation
link: /download/frama-c-23.0-rc1-Vanadium-api.tar.gz
- name: ACSL 1.16 (Vanadium implementation)
link: /download/acsl-implementation-23.0-rc1-Vanadium.pdf
- name: Plug-in Manuals
sort: true
- name: Aoraï manual
link: /download/aorai-manual-23.0-rc1-Vanadium.pdf
help: Aoraï example
help_link: /download/aorai-example-23.0-rc1-Vanadium.tgz
- name: Metrics manual
link: /download/metrics-manual-23.0-rc1-Vanadium.pdf
- name: Rte manual
link: /download/rte-manual-23.0-rc1-Vanadium.pdf
- name: Eva manual
link: /download/eva-manual-23.0-rc1-Vanadium.pdf
- name: WP manual
link: /download/wp-manual-23.0-rc1-Vanadium.pdf
- name: E-ACSL manual
link: /download/e-acsl/e-acsl-manual-23.0-rc1-Vanadium.pdf
No preview for this file type
layout: installation_page
version: vanadium
title: Installation instructions for Vanadium
# Installing Frama-C Vanadium (released on 2021-05-20)
- [Installing Frama-C](#installing-frama-c)
- [Table of Contents](#table-of-contents)
- [Installing Frama-C via opam](#installing-frama-c-via-opam)
- [Installing opam](#installing-opam)
- [Installing Frama-C from opam repository](#installing-frama-c-from-opam-repository)
- [Installing Custom Versions of Frama-C](#installing-custom-versions-of-frama-c)
- [Installing Frama-C on Windows via WSL](#installing-frama-c-on-windows-via-wsl)
- [Installing Frama-C on macOS](#installing-frama-c-on-macos)
- [Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)](#installing-frama-c-via-your-linux-distribution-debianubuntufedora)
- [Compiling from source](#compiling-from-source)
- [Quick Start](#quick-start)
- [Full Compilation Guide](#full-compilation-guide)
- [Testing the Installation](#testing-the-installation)
- [Available resources](#available-resources)
- [Executables: (in `/INSTALL_DIR/bin`)](#executables-in-install_dirbin)
- [Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)](#shared-files-in-install_dirshareframa-c-and-subdirectories)
- [Documentation files: (in `/INSTALL_DIR/share/frama-c/doc`)](#documentation-files-in-install_dirshareframa-cdoc)
- [Object files: (in `/INSTALL_DIR/lib/frama-c`)](#object-files-in-install_dirlibframa-c)
- [Plugin files: (in `/INSTALL_DIR/lib/frama-c/plugins`)](#plugin-files-in-install_dirlibframa-cplugins)
- [Man files: (in `/INSTALL_DIR/share/man/man1`)](#man-files-in-install_dirsharemanman1)
- [Installing Additional Frama-C Plugins](#installing-additional-frama-c-plugins)
- [HAVE FUN WITH FRAMA-C!](#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.
**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](#compiling-from-source),
or use the provided opam binaries available at:
### 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 [Gitlab 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:
why3 config --detect
### Reference configuration
See file [](
for a set of packages that is known to work with Frama-C 22 (Titanium).
### 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 20.04 LTS;
other distributions/versions should also work,
but the instructions below may require some modifications).
- 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
For installing 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 yaru-theme-gtk yaru-theme-icon
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.
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:
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 DISPLAY=:0
##### WSL 2
export DISPLAY=$(cat /etc/resolv.conf | grep nameserver | awk '{print $2; exit;}'):0.0
### Installing Frama-C on macOS
[opam]( works perfectly on macOS via
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 [opam]( and use it to get all of Frama-C's
dependencies (including some external ones):
opam install depext
opam depext frama-c
opam install --deps-only frama-c
If not using [opam](, you will need to install
the Frama-C dependencies by yourself. The `opam/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` and
`conf-gtksourceview` (or the equivalent Gtk+3 packages).
2. On Linux-like distributions:
./configure && make && sudo make install
See section *Configuration* below for options.
3. On Windows+Cygwin:
./configure --prefix="$(cygpath -a -m <installation path>)" && make && make install
4. The binary `frama-c` (and `frama-c-gui` if you have lablgtk2) is now installed.
### Full Compilation Guide
#### Frama-C Requirements
See the `opam/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).
Section `deptops` lists optional dependencies.
#### 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, unless some optional
dependencies are not met.
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
Type `make` (you can use `-j` for parallelization).
Some Makefile targets of interest are:
- `doc` generates the API documentation.
- `oracles` sets up the Frama-C test suite oracles for your own configuration.
- `tests` performs Frama-C's own tests.
#### Installation
Type `make install`
(depending on the installation directory, this may require superuser
privileges. The installation directory is chosen through `--prefix`).
#### API Documentation
For plugin developers, the API documentation of the Frama-C kernel and
distributed plugins 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 plugins.
(Depending on the installation directory, this may require superuser
# Testing the Installation
This step is optional.
Download some test files:
export PREFIX_URL=""
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
## Executables: (in `/INSTALL_DIR/bin`)
- `frama-c`
- `frama-c-gui` if available
- `frama-c-config` lightweight wrapper used to display configuration paths
- `frama-c.byte` bytecode version of frama-c
- `frama-c-gui.byte` bytecode version of frama-c-gui, if available
- `ptests.opt` testing tool for Frama-c
- `frama-c-script` utilities related to analysis parametrization
## Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)
- 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.)
## Documentation files: (in `/INSTALL_DIR/share/frama-c/doc`)
- files used to generate dynamic plugin documentation
## Object files: (in `/INSTALL_DIR/lib/frama-c`)
- object files used to compile dynamic plugins
## Plugin files: (in `/INSTALL_DIR/lib/frama-c/plugins`)
- object files of available dynamic plugins
## Man files: (in `/INSTALL_DIR/share/man/man1`)
- `man` files for `frama-c` (and `frama-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:
./configure && make && make install
Plugins may have their own custom installation procedures.
Consult their specific documentation for details.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment