Wiki » History » Version 2
Mikhail Mandrykin, 01/13/2015 07:00 PM
1 | 1 | Mikhail Mandrykin | h1. Jessie2 |
---|---|---|---|
2 | (fork of the Jessie plugin for Frama-C) |
||
3 | |||
4 | *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 certification platform":http://why.lri.fr/ and is compiled/installed separately. |
||
5 | *Note*: This fork requires modified version of the __Frama-C__ source code analysis platform, based on the @Neon 20140301@ version of the original platform. |
||
6 | |||
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 | * Add ISP RAS 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 | (@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 | <pre><code class="bash"> |
||
54 | why3 config --detect-provers --detect-plugins |
||
55 | </code></pre> |