AstraVer Toolset is built on top of 'Frama-C + AstraVer plugin + Why3' deductive verification toolchain, so it can be used to prove properties of Linux kernel code.
AstraVer is a successor of the Jessie plug-in for Frama-C that allows deductive verification of C programs annotated with ACSL and is primarily targeted at source code of Linux kernel modules. It uses the language and tools of the Why3 verification platform. Unlike Jessie, AstraVer is not distributed as part of the Why2 verification platform and is compiled/installed separately.
Note: This fork requires modified version of the Frama-C source code analysis platform, that is based on the
Calcium (20.0) version of the original platform. The modifications don't affect other plugins. Thus WP, EVA, RTE of this forked version can be used the same way as in vanilla version. If it is required to keep 2 versions of Frama-C (the original one and this one) different switches can be used.
- Install recommended OPAM external (system) dependencies —
git. For example, on Ubuntu:
* Install OPAM as described in the OPAM documentation.
sudo apt-get install gcc m4 make git
For example (installing to
/usr/local/binunsing the binary installer):
* Initialize OPAM to use the OCaml
wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh sh install.sh
* Configure current shell environment to use the newly created OPAM switch (may not be needed if OPAM shell hooks were installed successfully during
opam init -c 4.10.0
* Add ISPRAS OPAM repository at
eval $(opam env)
https://forge.ispras.ru/git/astraver.opam-repository.gitwith AstraVer and modified Frama-C v18.0 packages to the OPAM installation
isprasis just an arbitrary name of the new repository):
* Install OPAM
opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git opam update
depextplug-in for easy extraction and installation of external (system) dependencies for OPAM packages:
* Install external dependencies for the AstraVer and Frama-C build e. g. Gtk2 development files:
opam install depext
* Build and install the AstraVer plugin for Frama-C with OPAM (the patched versions of Frama-C and Why3 platforms will be built and installed automatically).
opam depext astraver
* The one using AstraVer would also likely need SMT solvers e.g. Alt-Ergo (also Z3, CVC4 and others). Alt-Ergo can be installed via OPAM:
opam install astraver
* Coq, CoqIDE can be installed via OPAM:
opam install alt-ergo altgr-ergo
* The Why3 IDE should be configured to detect available provers (and plugins):
opam install coq coqide
why3 config --detect
- AstraVer (
git clone https://forge.ispras.ru/git/astraver.git) has the following branches:
18.0-- references the latest released version of the AstraVer plugin
- QA (
git clone https://forge.ispras.ru/git/astraver.qa.git) is a submodule of the AstraVer 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)
18.0-- references patched version of Frama-C
Argon v18.0required by the latest AstraVer 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.07-- patched version of the Why3 platform (version 0.87.3) with several small unmerged changes
- OPAM-repository (
git clone https://forge.ispras.ru/git/astraver.opam-repository.git) is the above mentioned OPAM repository