30 assert(start->location_number<end->location_number);
34 typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
35 target_mapt target_map;
43 std::vector<goto_programt::targett> target_vector;
44 target_vector.reserve(target_map.size());
45 assert(target_vector.empty());
52 target_vector.push_back(t_new);
58 for(std::size_t i=0; i<target_vector.size(); i++)
67 target_mapt::const_iterator m_it=target_map.find(tgt);
69 if(m_it!=target_map.end())
71 unsigned j=m_it->second;
73 assert(j<target_vector.size());
74 t->set_target(target_vector[j]);
86 std::vector<goto_programt::targett> iteration_points;
97 std::vector<goto_programt::targett> &iteration_points)
99 assert(iteration_points.empty());
100 assert(loop_head->location_number<loop_exit->location_number);
111 t->source_location=loop_head->source_location;
112 t->function=loop_head->function;
113 t->location_number=loop_head->location_number;
123 assert(t->is_backwards_goto());
128 if(!t->guard.is_true())
131 exit_cond.make_not();
133 else if(loop_head->is_goto())
135 if(loop_head->get_target()==loop_exit)
136 exit_cond=loop_head->guard;
142 new_t->make_assertion(exit_cond);
144 new_t->make_assumption(exit_cond);
148 new_t->source_location=loop_head->source_location;
149 new_t->function=loop_head->function;
150 new_t->location_number=loop_head->location_number;
154 assert(!rest_program.
empty());
161 iteration_points.resize(k);
168 if(!t_before->is_goto() || !t_before->guard.is_true())
174 t_goto->source_location=loop_exit->source_location;
175 t_goto->function=loop_exit->function;
177 t_goto->location_number=loop_exit->location_number;
186 t_skip->source_location=loop_head->source_location;
187 t_skip->function=loop_head->function;
188 t_skip->location_number=loop_head->location_number;
194 iteration_points[0]=loop_iter;
205 if(t->get_target()==loop_head)
206 t->set_target(loop_iter);
210 for(
unsigned i=1; i<k; i++)
218 copies.destructive_append(tmp_program);
229 t_skip->source_location=loop_head->source_location;
230 t_skip->function=loop_head->function;
231 t_skip->location_number=loop_head->location_number;
241 if(t->location_number>=loop_head->location_number &&
242 t->location_number<loop_exit->location_number)
244 i_it->set_target(t_skip);
253 copies.destructive_append(rest_program);
270 std::cout <<
"Instruction:\n";
274 if(!i_it->is_backwards_goto())
281 assert(!func.
empty());
286 auto limit=unwindset.
get_limit(loop_id, 0);
288 if(!limit.has_value())
316 if(!goto_function.body_available())
320 std::cout <<
"Function: " << it->first <<
'\n';
335 for(location_mapt::const_iterator it=
location_map.begin();
341 unsigned location_number=it->second;
346 target->location_number));
void insert(const goto_programt::const_targett target, const unsigned location_number)
const std::string & id2string(const irep_idt &d)
targett insert_before(const_targett target)
Insertion before the given target.
Goto Programs with Functions.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible. ...
json_arrayt & make_array()
jsont & push_back(const jsont &json)
The boolean constant true.
instructionst::iterator targett
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
instructionst::const_iterator const_targett
::goto_functiont goto_functiont
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
location_mapt location_map
Helper functions for k-induction and loop invariants.
A generic container class for the GOTO intermediate representation of one function.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
jsont output_log_json() const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
goto_programt & goto_program
#define Forall_goto_program_instructions(it, program)
json_objectt & make_object()
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
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)