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 |