Project

General

Profile

Wiki » History » Version 5

Mikhail Mandrykin, 01/26/2015 06:42 PM

1 1 Mikhail Mandrykin
h1. Jessie2
2
 (fork of the Jessie plugin for Frama-C)
3
4 3 Alexey Khoroshilov
*Jessie2* is a fork of the Jessie plug-in 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.
5 4 Alexey Khoroshilov
*Note*: For now, this fork requires modified version of the __Frama-C__ source code analysis platform, that is based on the @Neon 20140301@ version of the original platform.
6 1 Mikhail Mandrykin
7
h2. Installation
8
9
h3. Using OPAM
10
11
  * Install "OPAM":https://opam.ocaml.org/ as described on the OPAM "documentation":https://opam.ocaml.org/doc/Install.html.
12
    For example (installing to @/usr/local/bin@ unsing the binary installer):
13
    <pre><code class="bash">
14
    wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh
15
    chmod +x opam_installer.sh
16
    sudo ./opam_installer.sh /usr/local/bin
17
    </code></pre>
18
  * Initialize OPAM to use the OCaml 4.02.1 compiler:
19
    <pre><code class="bash">
20
    opam init --comp 4.02.1
21
    eval `opam config env`
22
    </code></pre>
23
  * Install "Git":http://git-scm.com/.
24
    For example on Ubuntu:
25
    <pre><code class="bash">
26
    sudo apt-get install git
27
    </code></pre>
28 3 Alexey Khoroshilov
  * Add ISPRAS OPAM repository at @https://forge.ispras.ru/git/astraver.opam-repository.git@ with Jessie2 and modified Frama-C Neon packages to the OPAM installation
29 1 Mikhail Mandrykin
    (@ispras@ is just an arbitrary name of the new repository):
30
    <pre><code class="bash">
31
    opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git
32
    </code></pre>
33
  * Install external dependencies for the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4.
34
    Ubuntu example:
35
    <pre><code class="bash">
36
    sudo apt-get install $(opam install -e ubuntu jessie2)
37
    </code></pre>
38
  * Build and install the Jessie2 plugin for Frama-C with OPAM (the Frama-C itself will be built and installed automatically). One
39
    can use the @-j@ option to speed-up compilation on a multi-core machine:
40
    <pre><code class="bash">
41
    opam install -j 4 jessie2
42
    </code></pre>
43
  * Build and install either original or patched (negative assumption highlighting and minor explanation fixes) version of the Why3 verification platform:
44
    <pre><code class="bash">
45
    sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu
46
    opam install -j 4 why3
47
    </code></pre>
48
  * The one using Jessie would also likely need SMT solvers e.g. "Alt-Ergo":http://alt-ergo.ocamlpro.com/ (also "Z3":http://http://z3.codeplex.com/, "CVC4":http://cvc4.cs.nyu.edu/web/ and others). Alt-Ergo can be installed via OPAM:
49
    <pre><code class="bash">
50
     opam install alt-ergo altgr-ergo satML-plugin
51
    </code></pre>
52 2 Mikhail Mandrykin
  * The Why3 IDE should be initialized to detect available provers (and plugins):
53 1 Mikhail Mandrykin
    <pre><code class="bash">
54
    why3 config --detect-provers --detect-plugins
55 2 Mikhail Mandrykin
    </code></pre>
56 3 Alexey Khoroshilov
57
h2. Our Repositories
58 5 Mikhail Mandrykin
59
  * "Jessie2":/projects/astraver/repository (@git clone https://forge.ispras.ru/git/astraver.jessie2.git@) has the following branches:
60
    -- "@master@":/projects/astraver/repository -- references the latest released version of the Jessie2 plugin (currently `@alpha0@'')
61
    -- "@alpha0@":/projects/astraver/repository?utf8=✓&rev=alpha0 -- references the branch with the `@alpha0@'' released version of the plugin
62
    -- other branches are referencing the corresponding released versions
63
  * "QA":/projects/astraver/repository/qa 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 usage of the "Why3 proof replayer":http://why3.lri.fr/doc-0.85/manual007.html#sec53.
64
  * "Frama-C":/projects/astraver/repository/framac (@git clone https://forge.ispras.ru/git/astraver.frama-c.git@) has two branches:
65
    -- "@master@":/projects/astraver/repository/framac -- this is a dummy branch with each commit corresponding to an upstream release of Frama-C starting from "@Fluorine 3 20130601@" (commit:framac|16a2903f)
66
    -- "@20140301@":/projects/astraver/repository/framac?utf8=✓&rev=20140301 -- references the patched version of Frama-C @Fluorine 3 20130601@ which is required by Jessie2 (due to several small extensions to the ACSL specification language such as named string literals)
67
  * "Why3":/projects/astraver/repository/why3 (@git clone https://forge.ispras.ru/git/astraver.why3.git@) has two branches:
68
    -- "@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
69
    -- "@patched@":/projects/astraver/repository/why3?utf8=✓&rev=patched -- the periodically merged patched version of the Why3 platform  with several small unmerged changes (primarily explanation fixes)