AstraVer Toolset¶

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.

Installation¶

Using OPAM¶

• Install recommended OPAM external (system) dependencies — gcc, m4, make, git. For example, on Ubuntu:
  

      sudo apt-get install gcc m4 make git
      

• Install OPAM as described in the OPAM documentation.
  For example (installing to /usr/local/bin unsing the binary installer):
  

      wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
      sh install.sh
      

• Initialize OPAM to use the OCaml 4.14.1 compiler.
  

      opam init -c 4.14.1
      

• 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):
  

      eval $(opam env)
      

• Add ISPRAS OPAM repository at https://forge.ispras.ru/git/astraver.opam-repository.git with AstraVer and modified Frama-C v18.0 packages to the OPAM installation
  (ispras is just an arbitrary name of the new repository):
  

      opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git
      opam update
      

• 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 install 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 alt-ergo
      

• Coq, CoqIDE can be installed via OPAM:
  

       opam install coq coqide
      

• The Why3 IDE should be configured to detect available provers (and plugins):
  

      why3 config --detect
      

Our Repositories¶

• 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.0 required 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