31 assert(
start->location_number<end->location_number);
35 typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
36 target_mapt target_map;
70 target_mapt::const_iterator
m_it=target_map.find(
tgt);
72 if(
m_it!=target_map.end())
74 unsigned j=
m_it->second;
121 t->location_number=
loop_head->location_number;
133 assert(t->is_backwards_goto());
137 if(!t->get_condition().is_true())
220 for(
unsigned i=1;
i<k;
i++)
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())
294 if(!
limit.has_value())
323 if(!goto_function.body_available())
327 std::cout <<
"Function: " <<
gf_entry.first <<
'\n';
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))}};
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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
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)
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