12 #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H 13 #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H 32 slice(goto_functions);
48 typedef std::stack<cfgt::entryt>
queuet;
57 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
Over-approximate Concurrency for Threaded Goto Programs.
Goto Programs with Functions.
void operator()(goto_functionst &goto_functions, slicing_criteriont &criterion)
void fixedpoint_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
std::stack< cfgt::entryt > queuet
void slice(goto_functionst &goto_functions)
cfg_baset< slicer_entryt > cfgt