13 #ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H
14 #define CPROVER_GOTO_INSTRUMENT_UNWIND_H
50 std::vector<goto_programt::targett> &iteration_points);
101 const unsigned location_number)
103 auto r=
location_map.insert(std::make_pair(target, location_number));
120 const unsigned loop_id,
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
void operator()(goto_modelt &goto_model, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
int get_k(const irep_idt func, const unsigned loop_id, const unwindsett &unwindset) const
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
void unwind(const irep_idt &function_id, 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)
jsont output_log_json() const
#define forall_goto_program_instructions(it, program)
A total order over targett and const_targett.
jsont output_log_json() const
std::map< goto_programt::const_targett, unsigned, goto_programt::target_less_than > location_mapt
void insert(const goto_programt::const_targett target, const unsigned location_number)
void cleanup(const goto_programt &goto_program)
location_mapt location_map