Project

General

Profile

Wiki » History » Version 15

Grigoriy Volkov, 09/17/2018 01:30 PM
jingoo 1.2.18 seems to have a bug, add temporary workaround instructions

1 8 Alexey Khoroshilov
h1. AstraVer Toolset
2 1 Mikhail Mandrykin
3 12 Mikhail Mandrykin
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 8 Alexey Khoroshilov
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 13 Mikhail Mandrykin
*Note*: For now, this fork requires modified version of the __Frama-C__ source code analysis platform, that is based on the @Chlorine 20180501@ 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 13 Mikhail Mandrykin
  * Initialize OPAM to use the OCaml 4.06.0 compiler:
20 1 Mikhail Mandrykin
    <pre><code class="bash">
21 13 Mikhail Mandrykin
    opam init --comp 4.06.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 13 Mikhail Mandrykin
  * Add ISPRAS OPAM repository at @https://forge.ispras.ru/git/astraver.opam-repository.git@ with Jessie2 and modified Frama-C Chlorine packages to the OPAM installation
30 9 Mikhail Mandrykin
    (@ispras@ is just an arbitrary name of the new repository):
31 1 Mikhail Mandrykin
    <pre><code class="bash">
32
    opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git
33 13 Mikhail Mandrykin
    opam update
34 1 Mikhail Mandrykin
    </code></pre>
35
  * Install external dependencies for the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4.
36
    Ubuntu example:
37
    <pre><code class="bash">
38
    sudo apt-get install $(opam install -e ubuntu jessie2)
39
    </code></pre>
40 15 Grigoriy Volkov
  * (Temporary workaround) Build and install an older version of the jingoo dependency to avoid a build error:
41
    <pre><code class="bash">
42
    opam install -j 1 jingoo.1.2.17
43
    </code></pre>
44 1 Mikhail Mandrykin
  * Build and install the Jessie2 plugin for Frama-C with OPAM (the Frama-C itself will be built and installed automatically). One
45
    can use the @-j@ option to speed-up compilation on a multi-core machine:
46
    <pre><code class="bash">
47 12 Mikhail Mandrykin
    opam install -j 1 jessie2
48 1 Mikhail Mandrykin
    </code></pre>
49 9 Mikhail Mandrykin
  * Build and install either original or patched (search in task view, empty theory filtering) version of the Why3 verification platform:
50 1 Mikhail Mandrykin
    <pre><code class="bash">
51
    sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu
52
    opam install -j 4 why3
53
    </code></pre>
54 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:
55 1 Mikhail Mandrykin
    <pre><code class="bash">
56 13 Mikhail Mandrykin
     opam install alt-ergo altgr-ergo
57 1 Mikhail Mandrykin
    </code></pre>
58 2 Mikhail Mandrykin
  * The Why3 IDE should be initialized to detect available provers (and plugins):
59 1 Mikhail Mandrykin
    <pre><code class="bash">
60
    why3 config --detect-provers --detect-plugins
61 2 Mikhail Mandrykin
    </code></pre>
62 3 Alexey Khoroshilov
63
h2. Our Repositories
64 1 Mikhail Mandrykin
65
  * "Jessie2":/projects/astraver/repository (@git clone https://forge.ispras.ru/git/astraver.jessie2.git@) has the following branches:
66 14 Mikhail Mandrykin
    -- "@20180501@":/projects/astraver/repository/jessie2?utf8=✓&rev=20180501 -- references the latest released version of the Jessie2 plugin (currently `@alpha3.20180501@')
67 9 Mikhail Mandrykin
68 1 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.
69 7 Mikhail Mandrykin
70 5 Mikhail Mandrykin
  * "Frama-C":/projects/astraver/repository/framac (@git clone https://forge.ispras.ru/git/astraver.frama-c.git@) has two branches:
71 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)
72 13 Mikhail Mandrykin
    -- "@20180501@":/projects/astraver/repository/framac?utf8=✓&rev=20180501 -- references patched version of Frama-C @Chlorine 20180501@ required by the latest Jessie2 (@alpha3.20180501@) 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)
73 7 Mikhail Mandrykin
74 5 Mikhail Mandrykin
  * "Why3":/projects/astraver/repository/why3 (@git clone https://forge.ispras.ru/git/astraver.why3.git@) has two branches:
75 12 Mikhail Mandrykin
    -- "@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
76 14 Mikhail Mandrykin
    -- "@bv_and_lemma_functions_stable-4.06@":/projects/astraver/repository/why3?utf8=✓&rev=bv_and_lemma_functions_stable-4.06 -- patched version of the Why3 platform  with several small unmerged changes
77 7 Mikhail Mandrykin
78
  * "OPAM-repository":/projects/astraver/repository/opam-repository (@git clone https://forge.ispras.ru/git/astraver.opam-repository.git@) is the above mentioned OPAM repository