Wiki » History » Version 11
Mikhail Mandrykin, 11/30/2016 09:22 PM
1 | 8 | Alexey Khoroshilov | h1. AstraVer Toolset |
---|---|---|---|
2 | 1 | Mikhail Mandrykin | |
3 | 8 | Alexey Khoroshilov | AstraVer Toolset is built on top of ''Frama-C + Jessie plugin + Why3'' deductive verification toolchain, so it can be used to prove properties of Linux kernel code. |
4 | |||
5 | *Jessie2* is a fork of the Jessie plug-in for Frama-C that allows deductive verification of C programs annotated with "ACSL":http://frama-c.com/acsl.html and is primarily targeted at Linux kernel modules source code. It uses the language and tools of the "Why3 verification platform":http://why3.lri.fr/. Unlike original Jessie, Jessie2 is not distributed as a part of the "Why2 verification platform":http://why.lri.fr/ and is compiled/installed separately. |
||
6 | 9 | Mikhail Mandrykin | *Note*: For now, this fork requires modified version of the __Frama-C__ source code analysis platform, that is based on the @Sodium 20150201@ version of the original platform. |
7 | 1 | Mikhail Mandrykin | |
8 | h2. Installation |
||
9 | |||
10 | h3. Using OPAM |
||
11 | |||
12 | * Install "OPAM":https://opam.ocaml.org/ as described on the OPAM "documentation":https://opam.ocaml.org/doc/Install.html. |
||
13 | For example (installing to @/usr/local/bin@ unsing the binary installer): |
||
14 | <pre><code class="bash"> |
||
15 | wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh |
||
16 | chmod +x opam_installer.sh |
||
17 | sudo ./opam_installer.sh /usr/local/bin |
||
18 | </code></pre> |
||
19 | 11 | Mikhail Mandrykin | * Initialize OPAM to use the OCaml 4.03.0 compiler: |
20 | 1 | Mikhail Mandrykin | <pre><code class="bash"> |
21 | 11 | Mikhail Mandrykin | opam init --comp 4.03.0 |
22 | 1 | Mikhail Mandrykin | eval `opam config env` |
23 | </code></pre> |
||
24 | * Install "Git":http://git-scm.com/. |
||
25 | For example on Ubuntu: |
||
26 | <pre><code class="bash"> |
||
27 | sudo apt-get install git |
||
28 | </code></pre> |
||
29 | 9 | Mikhail Mandrykin | * Add ISPRAS OPAM repository at @https://forge.ispras.ru/git/astraver.opam-repository.git@ with Jessie2 and modified Frama-C Sodium packages to the OPAM installation |
30 | 1 | Mikhail Mandrykin | (@ispras@ is just an arbitrary name of the new repository): |
31 | <pre><code class="bash"> |
||
32 | opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git |
||
33 | </code></pre> |
||
34 | * Install external dependencies for the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4. |
||
35 | Ubuntu example: |
||
36 | <pre><code class="bash"> |
||
37 | sudo apt-get install $(opam install -e ubuntu jessie2) |
||
38 | </code></pre> |
||
39 | * Build and install the Jessie2 plugin for Frama-C with OPAM (the Frama-C itself will be built and installed automatically). One |
||
40 | can use the @-j@ option to speed-up compilation on a multi-core machine: |
||
41 | <pre><code class="bash"> |
||
42 | opam install -j 4 jessie2 |
||
43 | </code></pre> |
||
44 | 9 | Mikhail Mandrykin | * Build and install either original or patched (search in task view, empty theory filtering) version of the Why3 verification platform: |
45 | 1 | Mikhail Mandrykin | <pre><code class="bash"> |
46 | sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu |
||
47 | opam install -j 4 why3 |
||
48 | </code></pre> |
||
49 | 9 | Mikhail Mandrykin | * The one using Jessie 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.nyu.edu/web/ and others). Alt-Ergo can be installed via OPAM: |
50 | 1 | Mikhail Mandrykin | <pre><code class="bash"> |
51 | opam install alt-ergo altgr-ergo satML-plugin |
||
52 | </code></pre> |
||
53 | 2 | Mikhail Mandrykin | * The Why3 IDE should be initialized to detect available provers (and plugins): |
54 | 1 | Mikhail Mandrykin | <pre><code class="bash"> |
55 | why3 config --detect-provers --detect-plugins |
||
56 | 2 | Mikhail Mandrykin | </code></pre> |
57 | 3 | Alexey Khoroshilov | |
58 | h2. Our Repositories |
||
59 | 1 | Mikhail Mandrykin | |
60 | * "Jessie2":/projects/astraver/repository (@git clone https://forge.ispras.ru/git/astraver.jessie2.git@) has the following branches: |
||
61 | 11 | Mikhail Mandrykin | -- "@master@":/projects/astraver/repository -- references the latest released version of the Jessie2 plugin (currently `@astraver-v1.1@'') |
62 | 9 | Mikhail Mandrykin | |
63 | 11 | Mikhail Mandrykin | * "QA":/projects/astraver/repository/qa (@git clone https://forge.ispras.ru/git/astraver.qa.git@) is a submodule of the "Jessie2":/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-0.87.2/manual007.html#sec56. |
64 | 7 | Mikhail Mandrykin | |
65 | 5 | Mikhail Mandrykin | * "Frama-C":/projects/astraver/repository/framac (@git clone https://forge.ispras.ru/git/astraver.frama-c.git@) has two branches: |
66 | 11 | 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) |
67 | -- "@20150201@":/projects/astraver/repository/framac?utf8=✓&rev=20150201 -- references patched version of Frama-C @Sodium 20150201@ required by the latest Jessie2 (@astraver-v1.1@) 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) |
||
68 | 7 | Mikhail Mandrykin | |
69 | 5 | Mikhail Mandrykin | * "Why3":/projects/astraver/repository/why3 (@git clone https://forge.ispras.ru/git/astraver.why3.git@) has two branches: |
70 | -- "@master@":/projects/astraver/repository/why3 -- a periodically updated mirror of the INRIA official Why3 Git repository''s "master branch":https://gforge.inria.fr/scm/browser.php?group_id=2990 |
||
71 | 10 | Mikhail Mandrykin | -- "@patched@":/projects/astraver/repository/why3?utf8=✓&rev=patched -- the periodically merged patched version of the Why3 platform with several small unmerged changes |
72 | 7 | Mikhail Mandrykin | |
73 | * "OPAM-repository":/projects/astraver/repository/opam-repository (@git clone https://forge.ispras.ru/git/astraver.opam-repository.git@) is the above mentioned OPAM repository |