Wiki¶

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 https://forge.ispras.ru/git/astraver.opam-repository.git
    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
  

    make
    

• 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/local_export.sh 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>