Available slicing methods Syntactic: Use syntactic slicing IAA - Impact Analysis for Assignments: does an information flow check from each assignment to the criterion, for each assignment. If there is no information flow the assignment is removed. SLE - Single Line Elimination: try to removes a lines and verifies if the slice candidate is still a valid slice. If it is not, then the line is added again. Repeated until no further lines can be removed. CGS - Counterexample Guided Slicing: Union of dynamic slices generated from counter examples until the slice is valid. Note, that this method is not yet able to deal with arrays and heaps.
Explanation of additional Options Activate heap: It is necessary to activate this option, if you use arrays or pointer. Replace undefined values by zero: In SSA we can not simply delete instructions, if there is no previous value to a variable we will replace the variable with zero if this option is activated. This option will also help if you see "marked but not sliced" in the slice. syntactic post processing: Removes unnecessary loops, with syntactic slicing.