30 PRECONDITION(start->location_number < end->location_number);
35 map<goto_programt::const_targett, unsigned, goto_programt::target_less_than>
37 target_mapt target_map;
45 std::vector<goto_programt::targett> target_vector;
46 target_vector.reserve(target_map.size());
55 target_vector.push_back(t_new);
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;
78 t->set_target(target_vector[j]);
91 std::vector<goto_programt::targett> iteration_points;
109 std::vector<goto_programt::targett> &iteration_points)
112 PRECONDITION(loop_head->location_number < loop_exit->location_number);
122 t->location_number=loop_head->location_number;
124 unwind_log.insert(t, loop_head->location_number);
143 if(!t->condition().is_true())
147 else if(loop_head->is_goto())
149 if(loop_head->get_target()==loop_exit)
150 exit_cond = loop_head->condition();
157 const std::string loop_number = std::to_string(t->loop_number);
161 "unwinding assertion loop " + loop_number);
164 unwind_log.insert(assertion, loop_head->location_number);
173 exit_cond, loop_head->source_location()));
174 unwind_log.insert(assumption, loop_head->location_number);
186 iteration_points.resize(k);
193 if(!t_before->is_goto() || !t_before->condition().is_true())
200 loop_exit->source_location()));
201 t_goto->location_number=loop_exit->location_number;
203 unwind_log.insert(t_goto, loop_exit->location_number);
210 t_skip->location_number=loop_head->location_number;
212 unwind_log.insert(t_skip, loop_exit->location_number);
218 iteration_points[0]=loop_iter;
229 if(t->get_target()==loop_head)
230 t->set_target(loop_iter);
234 for(
unsigned i=1; i<k; i++)
251 t_skip->location_number=loop_head->location_number;
253 unwind_log.insert(t_skip, loop_head->location_number);
258 if(!instruction.is_goto())
263 if(t->location_number>=loop_head->location_number &&
264 t->location_number<loop_exit->location_number)
266 instruction.set_target(t_skip);
291 std::cout <<
"Instruction:\n";
292 i_it->output(std::cout);
295 if(!i_it->is_backwards_goto())
304 auto limit=unwindset.
get_limit(loop_id, 0);
306 if(!limit.has_value())
319 function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
335 if(!goto_function.body_available())
339 std::cout <<
"Function: " << gf_entry.first <<
'\n';
344 unwind(gf_entry.first, goto_program, unwindset, unwind_strategy);
354 for(location_mapt::const_iterator it=
location_map.begin();
358 unsigned location_number=it->second;
361 {
"originalLocationNumber",
json_numbert(std::to_string(location_number))},
362 {
"newLocationNumber",
363 json_numbert(std::to_string(target->location_number))}};
365 json_unwound.
push_back(std::move(
object));
368 return std::move(json_result);
Base class for all expressions.
The Boolean constant false.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
instructionst::iterator targett
instructionst::const_iterator const_targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
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 & push_back(const jsont &json)
json_arrayt & make_array()
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
The Boolean constant true.
std::optional< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
Goto Programs with Functions.
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.
jsont output_log_json() const
location_mapt location_map