Project

General

Profile

Wiki » History » Version 24

Mikhail Mandrykin, 02/14/2022 07:20 PM

1 8 Alexey Khoroshilov
h1. AstraVer Toolset
2 1 Mikhail Mandrykin
3 16 Mikhail Mandrykin
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.
4 8 Alexey Khoroshilov
5 16 Mikhail Mandrykin
*AstraVer* is a successor of the "Jessie":http://krakatoa.lri.fr/ plug-in for "Frama-C":http://www.frama-c.com/ that allows deductive verification of C programs annotated with "ACSL":http://frama-c.com/acsl.html and is primarily targeted at source code of Linux kernel modules. It uses the language and tools of the "Why3 verification platform":http://why3.lri.fr/. Unlike Jessie, AstraVer is not distributed as part of the "Why2 verification platform":http://why.lri.fr/ and is compiled/installed separately.
6 23 Denis Efremov
*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.
7 1 Mikhail Mandrykin
8
h2. Installation
9
10
h3. Using OPAM
11 16 Mikhail Mandrykin
 
12
  * Install recommended OPAM external (system) dependencies — @gcc@, @m4@, @make@, @git@. For example, on Ubuntu:
13
    <pre><code class="bash">
14
    sudo apt-get install gcc m4 make git
15
    </code></pre>
16
  * Install "OPAM":https://opam.ocaml.org/ as described in the OPAM "documentation":https://opam.ocaml.org/doc/Install.html.
17 1 Mikhail Mandrykin
    For example (installing to @/usr/local/bin@ unsing the binary installer):
18
    <pre><code class="bash">
19 16 Mikhail Mandrykin
    wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
20
    sh install.sh
21 1 Mikhail Mandrykin
    </code></pre>
22 22 Denis Efremov
  * Initialize OPAM to use the OCaml @4.10.0@ compiler.
23 1 Mikhail Mandrykin
    <pre><code class="bash">
24 22 Denis Efremov
    opam init -c 4.10.0
25 13 Mikhail Mandrykin
    </code></pre>
26 16 Mikhail Mandrykin
  * 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@):
27 1 Mikhail Mandrykin
    <pre><code class="bash">
28 16 Mikhail Mandrykin
    eval $(opam env)
29 1 Mikhail Mandrykin
    </code></pre>
30 17 Denis Efremov
  * 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
31 1 Mikhail Mandrykin
    (@ispras@ is just an arbitrary name of the new repository):
32
    <pre><code class="bash">
33 17 Denis Efremov
    opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git
34 15 Grigoriy Volkov
    opam update
35 1 Mikhail Mandrykin
    </code></pre>
36 16 Mikhail Mandrykin
  * Install OPAM @depext@ plug-in for easy extraction and installation of external (system) dependencies for OPAM packages:
37 15 Grigoriy Volkov
    <pre><code class="bash">
38 16 Mikhail Mandrykin
    opam install depext
39 24 Mikhail Mandrykin
    opam install opam-depext # For OPAM >= 1.2
40 1 Mikhail Mandrykin
    </code></pre>
41 16 Mikhail Mandrykin
  * Install external dependencies for the AstraVer and Frama-C build e. g. Gtk2 development files:
42 1 Mikhail Mandrykin
    <pre><code class="bash">
43 16 Mikhail Mandrykin
    opam depext astraver
44 1 Mikhail Mandrykin
    </code></pre>
45 16 Mikhail Mandrykin
  * 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).
46 9 Mikhail Mandrykin
    <pre><code class="bash">
47 16 Mikhail Mandrykin
    opam install astraver
48 13 Mikhail Mandrykin
    </code></pre>
49 16 Mikhail Mandrykin
  * The one using AstraVer would also likely need SMT solvers e.g. "Alt-Ergo":http://alt-ergo.ocamlpro.com/ (also "Z3":https://github.com/Z3Prover/z3, "CVC4":http://cvc4.cs.stanford.edu/web/ and others). Alt-Ergo can be installed via OPAM:
50 2 Mikhail Mandrykin
    <pre><code class="bash">
51 1 Mikhail Mandrykin
     opam install alt-ergo altgr-ergo
52
    </code></pre>
53 20 Denis Efremov
  * Coq, CoqIDE can be installed via OPAM:
54
    <pre><code class="bash">
55
     opam install coq coqide
56
    </code></pre>
57 16 Mikhail Mandrykin
  * The Why3 IDE should be configured to detect available provers (and plugins):
58 3 Alexey Khoroshilov
    <pre><code class="bash">
59 19 Denis Efremov
    why3 config --detect
60 1 Mikhail Mandrykin
    </code></pre>
61
62 14 Mikhail Mandrykin
h2. Our Repositories
63 9 Mikhail Mandrykin
64 16 Mikhail Mandrykin
  * "AstraVer":/projects/astraver/repository (@git clone https://forge.ispras.ru/git/astraver.git@) has the following branches:
65
    -- "@18.0@":/projects/astraver/repository/ -- references the latest released version of the AstraVer plugin
66 5 Mikhail Mandrykin
67 16 Mikhail Mandrykin
  * "QA":/projects/astraver/repository/qa (@git clone https://forge.ispras.ru/git/astraver.qa.git@) is a submodule of the "AstraVer":/projects/astraver/repository repository. It contains several new test sets and the corresponding new testing script (in OCaml) that is based on the "Why3 proof replayer":http://why3.lri.fr/doc/manpages.html#sec62.
68 13 Mikhail Mandrykin
69 7 Mikhail Mandrykin
  * "Frama-C":/projects/astraver/repository/framac (@git clone https://forge.ispras.ru/git/astraver.frama-c.git@) has two branches:
70 5 Mikhail Mandrykin
    -- "@master@":/projects/astraver/repository/framac -- this is a dummy branch with each commit corresponding to an upstream release of Frama-C starting from "@Sodium 20150201@" (commit:framac|1db5542e)
71 16 Mikhail Mandrykin
    -- "@18.0@":/projects/astraver/repository/framac?utf8=✓&rev=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)
72 14 Mikhail Mandrykin
73 7 Mikhail Mandrykin
  * "Why3":/projects/astraver/repository/why3 (@git clone https://forge.ispras.ru/git/astraver.why3.git@) has two branches:
74 16 Mikhail Mandrykin
    -- "@master@":/projects/astraver/repository/why3 -- a periodically updated mirror of the INRIA official Why3 Git repository's "master branch":https://gitlab.inria.fr/why3/why3
75
    -- "@bv_and_lemma_functions_stable-4.07@":/projects/astraver/repository/why3?utf8=✓&rev=bv_and_lemma_functions_stable-4.07 -- patched version of the Why3 platform (version 0.87.3) with several small unmerged changes
76 1 Mikhail Mandrykin
77
  * "OPAM-repository":/projects/astraver/repository/opam-repository (@git clone https://forge.ispras.ru/git/astraver.opam-repository.git@) is the above mentioned OPAM repository