Installation with OPAM

  • Install and initialize OPAM
      opam init
      eval $(opam env)
  • Add ISPRAS remote with patched Frama-C and Crude_slicer packages
      opam remote add ispras
      opam update
    • The next step may require external dependencies depending on on the current system installation, so
      OPAM depext may de used to help resolving these dependencies
        opam install opam-depext
        opam depext crude_slicer
  • Install Crude_slicer plugin (this should automatically install Frama-C and all the dependencies)
      opam install crude_slicer

Running the installed version with configuration from SV-COMP

  frama-c -machdep gcc_x86_64 \
          -crude_slicer \
          -timeout 400 \
          -no-recognize_wrecked_container_of \
          -widening_threshold 2000 \
          -no-summaries \
          -no-assert_stratification \
          -print -ocode <slice-file.c> <input-file.c>

Creating a standalone executable e.g. for SV-COMP

  • Checkout sources of patched Frama-C from the ISPRAS remote
      opam source frama-c
      cd frama-c.astraver.20180501
  • Build and install patched Frama-C (with or without plugins)
      ./configure --prefix $(opam var prefix) --with-no-plugin
      make -j4
      make install
  • Checkout sources of Crude_slicer from the development repository
      opam source crude_slicer
      cd crude_slicer.~dev/
  • Build Crude_slicer
  • Prepare standalone executable
      mkdir frama-c-minimal
      export FRAMAC=<path/to/frama-c.astraver.20180501>
      cp $FRAMAC/bin/frama-c $FRAMAC/bin/toplevel.opt $FRAMAC/bin/ frama-c-minimal/
      cp <path/to/crude_slicer.~dev>/top/Crude_slicer.cmxs frama-c-minimal/

Now the slicer can be executed from frama-c-minimal using the following command:

  ./frama-c -no-autoload-plugins \
            -no-findlib \
            -load-module Crude_slicer.cmxs \
            -machdep gcc_x86_64 \
            -crude_slicer \
            -timeout 400 \
            -no-recognize_wrecked_container_of \
            -widening_threshold 2000 \
            -no-summaries \
            -no-assert_stratification \
            -print -ocode <slice-file.c> <input-file.c>

Updated by Mikhail Mandrykin about 1 year ago ยท 1 revisions