13 #ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H 14 #define CPROVER_GOTO_INSTRUMENT_UNWIND_H 44 std::vector<goto_programt::targett> &iteration_points);
94 const unsigned location_number)
96 auto r=
location_map.insert(std::make_pair(target, location_number));
109 const unsigned loop_id,
119 #endif // CPROVER_GOTO_INSTRUMENT_UNWIND_H jsont output_log_json() const
void insert(const goto_programt::const_targett target, const unsigned location_number)
instructionst::const_iterator const_targett
A collection of goto functions.
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
location_mapt location_map
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void operator()(goto_modelt &goto_model, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
A generic container class for the GOTO intermediate representation of one function.
void cleanup(const goto_programt &goto_program)
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
jsont output_log_json() const
int get_k(const irep_idt func, const unsigned loop_id, const unwindsett &unwindset) const
std::map< goto_programt::const_targett, unsigned > location_mapt
void unwind(goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy)
#define forall_goto_program_instructions(it, program)
goto_functionst goto_functions
GOTO functions.