13 #ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H 14 #define CPROVER_GOTO_INSTRUMENT_UNWIND_H 23 typedef std::map<irep_idt, std::map<unsigned, int>>
unwind_sett;
47 std::vector<goto_programt::targett> &iteration_points);
65 operator()(goto_functions, unwind_set, k, unwind_strategy);
100 const unsigned location_number)
102 auto r=
location_map.insert(std::make_pair(target, location_number));
115 const unsigned loop_id,
126 #endif // CPROVER_GOTO_INSTRUMENT_UNWIND_H jsont output_log_json() const
void insert(const goto_programt::const_targett target, const unsigned location_number)
void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
void operator()(goto_functionst &goto_functions, const unsigned k, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
instructionst::const_iterator const_targett
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
location_mapt location_map
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void cleanup(const goto_programt &goto_program)
int get_k(const irep_idt func, const unsigned loop_id, const int global_k, const unwind_sett &unwind_set) const
jsont output_log_json() const
std::map< irep_idt, std::map< unsigned, int > > unwind_sett
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)