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 bool include_forward_reachability);
32 const std::list<std::string> &properties,
33 const bool include_forward_reachability);
36 #define OPT_REACHABILITY_SLICER \ 37 "(reachability-slice)(reachability-slice-fb)" // NOLINT(*) 39 #define HELP_REACHABILITY_SLICER \ 40 " --reachability-slice remove instructions that cannot appear on\n" \ 41 " a trace from entry point to a property\n" \ 42 " --reachability-slice-fb remove instructions that cannot appear on\n" \ 43 " a trace from entry point through a property\n" // NOLINT(*) 45 #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...