31 assert(start->location_number<end->location_number);
32 assert(goto_program.
empty());
35 typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
36 target_mapt target_map;
44 std::vector<goto_programt::targett> target_vector;
45 target_vector.reserve(target_map.size());
46 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]);
90 std::vector<goto_programt::targett> iteration_points;
108 std::vector<goto_programt::targett> &iteration_points)
110 assert(iteration_points.empty());
111 assert(loop_head->location_number<loop_exit->location_number);
121 t->location_number=loop_head->location_number;
133 assert(t->is_backwards_goto());
137 if(!t->get_condition().is_true())
141 else if(loop_head->is_goto())
143 if(loop_head->get_target()==loop_exit)
144 exit_cond = loop_head->get_condition();
160 new_t->source_location_nonconst() = loop_head->source_location();
161 new_t->location_number=loop_head->location_number;
165 assert(!rest_program.
empty());
172 iteration_points.resize(k);
179 if(!t_before->is_goto() || !t_before->get_condition().is_true())
187 t_goto->location_number=loop_exit->location_number;
196 t_skip->location_number=loop_head->location_number;
204 iteration_points[0]=loop_iter;
215 if(t->get_target()==loop_head)
216 t->set_target(loop_iter);
220 for(
unsigned i=1; i<k; i++)
237 t_skip->location_number=loop_head->location_number;
244 if(!instruction.is_goto())
249 if(t->location_number>=loop_head->location_number &&
250 t->location_number<loop_exit->location_number)
252 instruction.set_target(t_skip);
279 std::cout <<
"Instruction:\n";
283 if(!i_it->is_backwards_goto())
292 auto limit=unwindset.
get_limit(loop_id, 0);
294 if(!limit.has_value())
307 function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
323 if(!goto_function.body_available())
327 std::cout <<
"Function: " << gf_entry.first <<
'\n';
332 unwind(gf_entry.first, goto_program, unwindset, unwind_strategy);
342 for(location_mapt::const_iterator it=
location_map.begin();
346 unsigned location_number=it->second;
349 {
"originalLocationNumber",
json_numbert(std::to_string(location_number))},
350 {
"newLocationNumber",
351 json_numbert(std::to_string(target->location_number))}};
353 json_unwound.
push_back(std::move(
object));
356 return std::move(json_result);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & source_location() const
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.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
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()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The Boolean constant true.
optionalt< 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 UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
API to expression classes.
jsont output_log_json() const
void insert(const goto_programt::const_targett target, const unsigned location_number)
location_mapt location_map