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());
54 target_vector.push_back(t_new);
57 assert(goto_program.
instructions.size()==target_vector.size());
60 for(std::size_t target_index = 0; target_index < target_vector.size();
70 target_mapt::const_iterator m_it=target_map.find(tgt);
72 if(m_it!=target_map.end())
74 unsigned j=m_it->second;
76 assert(j<target_vector.size());
77 t->set_target(target_vector[j]);
89 std::vector<goto_programt::targett> iteration_points;
90 unwind(goto_program, loop_head, loop_exit, k, unwind_strategy,
100 std::vector<goto_programt::targett> &iteration_points)
102 assert(iteration_points.empty());
103 assert(loop_head->location_number<loop_exit->location_number);
114 t->source_location=loop_head->source_location;
115 t->function=loop_head->function;
116 t->location_number=loop_head->location_number;
126 assert(t->is_backwards_goto());
130 if(!t->guard.is_true())
134 else if(loop_head->is_goto())
136 if(loop_head->get_target()==loop_exit)
137 exit_cond=loop_head->guard;
143 new_t->make_assertion(exit_cond);
145 new_t->make_assumption(exit_cond);
149 new_t->source_location=loop_head->source_location;
150 new_t->function=loop_head->function;
151 new_t->location_number=loop_head->location_number;
155 assert(!rest_program.
empty());
162 iteration_points.resize(k);
169 if(!t_before->is_goto() || !t_before->guard.is_true())
175 t_goto->source_location=loop_exit->source_location;
176 t_goto->function=loop_exit->function;
178 t_goto->location_number=loop_exit->location_number;
187 t_skip->source_location=loop_head->source_location;
188 t_skip->function=loop_head->function;
189 t_skip->location_number=loop_head->location_number;
195 iteration_points[0]=loop_iter;
206 if(t->get_target()==loop_head)
207 t->set_target(loop_iter);
211 for(
unsigned i=1; i<k; i++)
230 t_skip->source_location=loop_head->source_location;
231 t_skip->function=loop_head->function;
232 t_skip->location_number=loop_head->location_number;
242 if(t->location_number>=loop_head->location_number &&
243 t->location_number<loop_exit->location_number)
245 i_it->set_target(t_skip);
271 std::cout <<
"Instruction:\n";
275 if(!i_it->is_backwards_goto())
282 assert(!func.
empty());
287 auto limit=unwindset.
get_limit(loop_id, 0);
289 if(!limit.has_value())
301 unwind(goto_program, loop_head, loop_exit, *limit, unwind_strategy);
317 if(!goto_function.body_available())
321 std::cout <<
"Function: " << it->first <<
'\n';
326 unwind(goto_program, unwindset, unwind_strategy);
336 for(location_mapt::const_iterator it=
location_map.begin();
342 unsigned location_number=it->second;
347 target->location_number));
350 return std::move(json_result);