Wiki » History » Version 20
Denis Efremov, 04/15/2019 03:47 PM
coq, coqide installation
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 | 18 | Denis Efremov | *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. The modifications don't affect other plugins. Thus WP, EVA, RTE of this forked version can be used the same way as in vanilla version. If it is required to keep 2 versions of Frama-C (the original one and this one) different switches can be used. |
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 | 17 | Denis Efremov | * Add ISPRAS OPAM repository at @https://forge.ispras.ru/git/astraver.opam-repository.git@ 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 | 17 | Denis Efremov | opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git |
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 | 20 | Denis Efremov | * Coq, CoqIDE can be installed via OPAM: |
53 | <pre><code class="bash"> |
||
54 | opam install coq coqide |
||
55 | </code></pre> |
||
56 | 16 | Mikhail Mandrykin | * The Why3 IDE should be configured to detect available provers (and plugins): |
57 | 3 | Alexey Khoroshilov | <pre><code class="bash"> |
58 | 19 | Denis Efremov | why3 config --detect |
59 | 1 | Mikhail Mandrykin | </code></pre> |
60 | |||
61 | 14 | Mikhail Mandrykin | h2. Our Repositories |
62 | 9 | Mikhail Mandrykin | |
63 | 16 | Mikhail Mandrykin | * "AstraVer":/projects/astraver/repository (@git clone https://forge.ispras.ru/git/astraver.git@) has the following branches: |
64 | -- "@18.0@":/projects/astraver/repository/ -- references the latest released version of the AstraVer plugin |
||
65 | 5 | Mikhail Mandrykin | |
66 | 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. |
67 | 13 | Mikhail Mandrykin | |
68 | 7 | Mikhail Mandrykin | * "Frama-C":/projects/astraver/repository/framac (@git clone https://forge.ispras.ru/git/astraver.frama-c.git@) has two branches: |
69 | 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) |
70 | 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) |
71 | 14 | Mikhail Mandrykin | |
72 | 7 | Mikhail Mandrykin | * "Why3":/projects/astraver/repository/why3 (@git clone https://forge.ispras.ru/git/astraver.why3.git@) has two branches: |
73 | 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 |
74 | -- "@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 |
||
75 | 1 | Mikhail Mandrykin | |
76 | * "OPAM-repository":/projects/astraver/repository/opam-repository (@git clone https://forge.ispras.ru/git/astraver.opam-repository.git@) is the above mentioned OPAM repository |