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;
71 target_mapt::const_iterator
m_it=target_map.find(
tgt);
73 if(
m_it!=target_map.end())
75 unsigned j=
m_it->second;
122 t->location_number=
loop_head->location_number;
143 if(!t->condition().is_true())
157 const std::string loop_number = std::to_string(t->loop_number);
161 "unwinding assertion loop " + loop_number);
234 for(
unsigned i=1; i<k; i++)
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";
295 if(!
i_it->is_backwards_goto())
306 if(!
limit.has_value())
335 if(!goto_function.body_available())
339 std::cout <<
"Function: " <<
gf_entry.first <<
'\n';
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))}};
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
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
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)
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
void insert(const goto_programt::const_targett target, const unsigned location_number)
location_mapt location_map