Project

General

Profile

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