12 #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H 13 #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H 24 const std::list<std::string> &properties);
28 const std::list<std::string> &functions_list);
32 const bool include_forward_reachability);
36 const std::list<std::string> &properties,
37 const bool include_forward_reachability);
40 #define OPT_REACHABILITY_SLICER \ 41 "(fp-reachability-slice):(reachability-slice)(reachability-slice-fb)" // NOLINT(*) 43 #define HELP_REACHABILITY_SLICER \ 44 " --fp-reachability-slice f remove instructions that cannot appear on a trace\n" \ 45 " that visits all given functions. The list of\n" \ 46 " functions has to be given as a comma separated\n" \ 48 " --reachability-slice remove instructions that cannot appear on a trace\n" \ 49 " from entry point to a property\n" // NOLINT(*) 50 #define HELP_REACHABILITY_SLICER_FB \ 51 " --reachability-slice-fb remove instructions that cannot appear on a trace\n" \ 52 " from entry point through a property\n" // NOLINT(*) 54 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H
void reachability_slicer(goto_modelt &)
Perform reachability slicing on goto_model, with respect to criterion comprising all properties...
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list)
Perform reachability slicing on goto_model for selected functions.