SemSlice

Usage

To test our slicing tool simply chose a predefined example or enter your one code in the edit field. The Result will be presented in a simplified version of the LLVM-IR. In the left panel you will see the LLVM-IR of the sliced program. The right panel shows the slice. Differences are highlighted with colors (red -> removed or changed, green -> changed). The timeout is 5 minutes.

The default criterion is the return value. If you want to specify another variable and a specific location you can use the __criterion function. It is possible to place assignments like x = 3; inside the function __assert_sliced: __assert_sliced(x = 3); This way the relevant instruction will be highlighted in the LLVM-IR with "!assert_sliced".

To use __assert_sliced or __criterion please

#include "slicing_marks.h"

Available slicing methods

Explanation of additional Options

Supported Language Features

We only support integer which are interpreted without overflow and without a bit representation. Bit operations on integers (&,|,...) do therefore not work. Pointer and arrays are also supported if you activate the heap option. Functions are supported, but only statements from the sliced function will be removed. If extern functions are used, then the relational invariant same input result in same output is assumed. We can not remove whole loops unless the syntactic post processing option is activated, for reasons see our paper. Branches are only removed if they do not contain any statements.