Wiki » History » Version 1
Mikhail Mandrykin, 07/20/2018 06:55 PM
| 1 | 1 | Mikhail Mandrykin | h1. Wiki |
|---|---|---|---|
| 2 | |||
| 3 | h2. Installation with OPAM |
||
| 4 | |||
| 5 | * Install and initialize "OPAM":https://opam.ocaml.org/doc/2.0/Install.html |
||
| 6 | <pre><code class="bash"> |
||
| 7 | opam init |
||
| 8 | eval $(opam env) |
||
| 9 | </code></pre> |
||
| 10 | * Add ISPRAS remote with patched Frama-C and Crude_slicer packages |
||
| 11 | <pre><code class="bash"> |
||
| 12 | opam remote add ispras https://forge.ispras.ru/git/astraver.opam-repository.git |
||
| 13 | opam update |
||
| 14 | </code></pre> |
||
| 15 | ** The next step may require external dependencies depending on on the current system installation, so |
||
| 16 | OPAM depext may de used to help resolving these dependencies |
||
| 17 | <pre><code class="bash"> |
||
| 18 | opam install opam-depext |
||
| 19 | opam depext crude_slicer |
||
| 20 | </code></pre> |
||
| 21 | * Install Crude_slicer plugin (this should automatically install Frama-C and all the dependencies) |
||
| 22 | <pre><code class="bash"> |
||
| 23 | opam install crude_slicer |
||
| 24 | </code></pre> |
||
| 25 | |||
| 26 | h3. Running the _installed_ version with configuration from SV-COMP |
||
| 27 | |||
| 28 | <pre><code class="bash"> |
||
| 29 | frama-c -machdep gcc_x86_64 \ |
||
| 30 | -crude_slicer \ |
||
| 31 | -timeout 400 \ |
||
| 32 | -no-recognize_wrecked_container_of \ |
||
| 33 | -widening_threshold 2000 \ |
||
| 34 | -no-summaries \ |
||
| 35 | -no-assert_stratification \ |
||
| 36 | -print -ocode <slice-file.c> <input-file.c> |
||
| 37 | </code></pre> |
||
| 38 | |||
| 39 | h2. Creating a standalone executable e.g. for SV-COMP |
||
| 40 | |||
| 41 | * Checkout sources of patched Frama-C from the ISPRAS remote |
||
| 42 | <pre><code class="bash"> |
||
| 43 | opam source frama-c |
||
| 44 | cd frama-c.astraver.20180501 |
||
| 45 | </code></pre> |
||
| 46 | * Build and install patched Frama-C (with or without plugins) |
||
| 47 | <pre><code class="bash"> |
||
| 48 | ./configure --prefix $(opam var prefix) --with-no-plugin |
||
| 49 | make -j4 |
||
| 50 | make install |
||
| 51 | </code></pre> |
||
| 52 | * Checkout sources of Crude_slicer from the development repository |
||
| 53 | <pre><code class="bash"> |
||
| 54 | opam source crude_slicer |
||
| 55 | cd crude_slicer.~dev/ |
||
| 56 | </code></pre> |
||
| 57 | * Build Crude_slicer |
||
| 58 | <pre><code class="bash"> |
||
| 59 | make |
||
| 60 | </code></pre> |
||
| 61 | * Prepare standalone executable |
||
| 62 | <pre><code class="bash"> |
||
| 63 | mkdir frama-c-minimal |
||
| 64 | export FRAMAC=<path/to/frama-c.astraver.20180501> |
||
| 65 | cp $FRAMAC/bin/frama-c $FRAMAC/bin/toplevel.opt $FRAMAC/bin/local_export.sh frama-c-minimal/ |
||
| 66 | cp <path/to/crude_slicer.~dev>/top/Crude_slicer.cmxs frama-c-minimal/ |
||
| 67 | </code></pre> |
||
| 68 | |||
| 69 | Now the slicer can be executed from @frama-c-minimal@ using the following command: |
||
| 70 | <pre><code class="bash"> |
||
| 71 | ./frama-c -no-autoload-plugins \ |
||
| 72 | -no-findlib \ |
||
| 73 | -load-module Crude_slicer.cmxs \ |
||
| 74 | -machdep gcc_x86_64 \ |
||
| 75 | -crude_slicer \ |
||
| 76 | -timeout 400 \ |
||
| 77 | -no-recognize_wrecked_container_of \ |
||
| 78 | -widening_threshold 2000 \ |
||
| 79 | -no-summaries \ |
||
| 80 | -no-assert_stratification \ |
||
| 81 | -print -ocode <slice-file.c> <input-file.c> |
||
| 82 | </code></pre> |
||
| 83 |