AstraVer Toolset is built on top of 'Frama-C + Jessie plugin + Why3' deductive verification toolchain, so it can be used to prove properties of Linux kernel code.
Jessie2 is a fork of the Jessie plug-in for Frama-C that allows deductive verification of C programs annotated with ACSL and is primarily targeted at Linux kernel modules source code. It uses the language and tools of the Why3 verification platform. Unlike original Jessie, Jessie2 is not distributed as a part of the Why2 verification platform and is compiled/installed separately.
Note: For now, this fork requires modified version of the Frama-C source code analysis platform, that is based on the
Chlorine 20180501 version of the original platform.
- Install OPAM as described on the OPAM documentation.
For example (installing to
/usr/local/binunsing the binary installer):
* Initialize OPAM to use the OCaml 4.06.0 compiler:
wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh chmod +x opam_installer.sh sudo ./opam_installer.sh /usr/local/bin
* Install Git.
opam init --comp 4.06.0 eval `opam config env`
For example on Ubuntu:
* Add ISPRAS OPAM repository at
sudo apt-get install git
https://forge.ispras.ru/git/astraver.opam-repository.gitwith Jessie2 and modified Frama-C Chlorine packages to the OPAM installation
isprasis just an arbitrary name of the new repository):
* Install external dependencies for the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4.
opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git opam update
* (Temporary workaround) Build and install an older version of the jingoo dependency to avoid a build error:
sudo apt-get install $(opam install -e ubuntu jessie2)
* Build and install the Jessie2 plugin for Frama-C with OPAM (the Frama-C itself will be built and installed automatically). One
opam install -j 1 jingoo.1.2.17
can use the
-joption to speed-up compilation on a multi-core machine:
* Build and install either original or patched (search in task view, empty theory filtering) version of the Why3 verification platform:
opam install -j 1 jessie2
* The one using Jessie would also likely need SMT solvers e.g. Alt-Ergo (also Z3, CVC4 and others). Alt-Ergo can be installed via OPAM:
sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu opam install -j 4 why3
* The Why3 IDE should be initialized to detect available provers (and plugins):
opam install alt-ergo altgr-ergo
why3 config --detect-provers --detect-plugins
- Jessie2 (
git clone https://forge.ispras.ru/git/astraver.jessie2.git) has the following branches:
20180501-- references the latest released version of the Jessie2 plugin (currently `
- QA (
git clone https://forge.ispras.ru/git/astraver.qa.git) is a submodule of the Jessie2 repository. It contains several new test sets and the corresponding new testing script (in OCaml) that is based on the Why3 proof replayer.
- Frama-C (
git clone https://forge.ispras.ru/git/astraver.frama-c.git) has two branches:
master-- this is a dummy branch with each commit corresponding to an upstream release of Frama-C starting from "
Sodium 20150201" (framac|1db5542e)
20180501-- references patched version of Frama-C
Chlorine 20180501required by the latest Jessie2 (
alpha3.20180501) with some significant changes (wrap-around annotations and logic operations on bounded integers, annotation importing -- an order-independent merging of annotations from several C source files)
- Why3 (
git clone https://forge.ispras.ru/git/astraver.why3.git) has two branches:
master-- a periodically updated mirror of the INRIA official Why3 Git repository's master branch
bv_and_lemma_functions_stable-4.06-- patched version of the Why3 platform with several small unmerged changes
- OPAM-repository (
git clone https://forge.ispras.ru/git/astraver.opam-repository.git) is the above mentioned OPAM repository