32 assert(start->location_number<end->location_number);
33 assert(goto_program.
empty());
36 typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
37 target_mapt target_map;
45 std::vector<goto_programt::targett> target_vector;
46 target_vector.reserve(target_map.size());
47 assert(target_vector.empty());
55 target_vector.push_back(t_new);
58 assert(goto_program.
instructions.size()==target_vector.size());
61 for(std::size_t target_index = 0; target_index < target_vector.size();
71 target_mapt::const_iterator m_it=target_map.find(tgt);
73 if(m_it!=target_map.end())
75 unsigned j=m_it->second;
77 assert(j<target_vector.size());
78 t->set_target(target_vector[j]);
91 std::vector<goto_programt::targett> iteration_points;
109 std::vector<goto_programt::targett> &iteration_points)
111 assert(iteration_points.empty());
112 assert(loop_head->location_number<loop_exit->location_number);
122 t->location_number=loop_head->location_number;
134 assert(t->is_backwards_goto());
138 if(!t->get_condition().is_true())
142 else if(loop_head->is_goto())
144 if(loop_head->get_target()==loop_exit)
145 exit_cond = loop_head->get_condition();
161 new_t->source_location=loop_head->source_location;
162 new_t->location_number=loop_head->location_number;
166 assert(!rest_program.
empty());
173 iteration_points.resize(k);
180 if(!t_before->is_goto() || !t_before->get_condition().is_true())
188 t_goto->location_number=loop_exit->location_number;
197 t_skip->location_number=loop_head->location_number;
205 iteration_points[0]=loop_iter;
216 if(t->get_target()==loop_head)
217 t->set_target(loop_iter);
221 for(
unsigned i=1; i<k; i++)
238 t_skip->location_number=loop_head->location_number;
250 if(t->location_number>=loop_head->location_number &&
251 t->location_number<loop_exit->location_number)
253 i_it->set_target(t_skip);
280 std::cout <<
"Instruction:\n";
284 if(!i_it->is_backwards_goto())
293 auto limit=unwindset.
get_limit(loop_id, 0);
295 if(!limit.has_value())
308 function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
324 if(!goto_function.body_available())
328 std::cout <<
"Function: " << it->first <<
'\n';
333 unwind(it->first, goto_program, unwindset, unwind_strategy);
343 for(location_mapt::const_iterator it=
location_map.begin();
347 unsigned location_number=it->second;
351 {
"newLocationNumber",
354 json_unwound.
push_back(std::move(
object));
357 return std::move(json_result);