Project

General

Profile

Wiki » History » Version 16

Mikhail Mandrykin, 03/29/2019 06:04 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
*Note*: This fork requires modified version of the __Frama-C__ source code analysis platform, that is based on the @Argon (18.0)@ version of the original platform.
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 16 Mikhail Mandrykin
  * Initialize OPAM to use the OCaml @4.07.1@ compiler. On Ubuntu you can use @--disable-sandboxing@ to avoid installation of "bubblewrap":https://github.com/projectatomic/bubblewrap, although this is not recommended.
23 1 Mikhail Mandrykin
    <pre><code class="bash">
24 16 Mikhail Mandrykin
    opam init -c 4.07.1 --disable-sandboxing
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 16 Mikhail Mandrykin
  * Add ISPRAS OPAM repository at @https://forge.ispras.ru/git/astraver.opam-repository.git#astraver@ 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 16 Mikhail Mandrykin
    opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git#astraver
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 1 Mikhail Mandrykin
    </code></pre>
40 16 Mikhail Mandrykin
  * Install external dependencies for the AstraVer and Frama-C build e. g. Gtk2 development files:
41 1 Mikhail Mandrykin
    <pre><code class="bash">
42 16 Mikhail Mandrykin
    opam depext astraver
43 1 Mikhail Mandrykin
    </code></pre>
44 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).
45 9 Mikhail Mandrykin
    <pre><code class="bash">
46 16 Mikhail Mandrykin
    opam install astraver
47 13 Mikhail Mandrykin
    </code></pre>
48 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:
49 2 Mikhail Mandrykin
    <pre><code class="bash">
50 1 Mikhail Mandrykin
     opam install alt-ergo altgr-ergo
51
    </code></pre>
52 16 Mikhail Mandrykin
  * The Why3 IDE should be configured to detect available provers (and plugins):
53 3 Alexey Khoroshilov
    <pre><code class="bash">
54
    why3 config --detect-provers --detect-plugins
55 1 Mikhail Mandrykin
    </code></pre>
56
57 14 Mikhail Mandrykin
h2. Our Repositories
58 9 Mikhail Mandrykin
59 16 Mikhail Mandrykin
  * "AstraVer":/projects/astraver/repository (@git clone https://forge.ispras.ru/git/astraver.git@) has the following branches:
60
    -- "@18.0@":/projects/astraver/repository/ -- references the latest released version of the AstraVer plugin
61 5 Mikhail Mandrykin
62 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.
63 13 Mikhail Mandrykin
64 7 Mikhail Mandrykin
  * "Frama-C":/projects/astraver/repository/framac (@git clone https://forge.ispras.ru/git/astraver.frama-c.git@) has two branches:
65 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)
66 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)
67 14 Mikhail Mandrykin
68 7 Mikhail Mandrykin
  * "Why3":/projects/astraver/repository/why3 (@git clone https://forge.ispras.ru/git/astraver.why3.git@) has two branches:
69 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
70
    -- "@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
71 1 Mikhail Mandrykin
72
  * "OPAM-repository":/projects/astraver/repository/opam-repository (@git clone https://forge.ispras.ru/git/astraver.opam-repository.git@) is the above mentioned OPAM repository