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);
35 #define OPT_REACHABILITY_SLICER \ 36 "(reachability-slice)(reachability-slice-fb)" // NOLINT(*) 38 #define HELP_REACHABILITY_SLICER \ 39 " --reachability-slice remove instructions that cannot appear on a " \ 40 "trace from entry point to a property\n" \ 41 " --reachability-slice-fb remove instructions that cannot appear on a " \ 42 "trace from entry point through a property\n" // NOLINT(*) 44 #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...