49 if(!instruction.
labels.empty())
52 for(
const auto &label : instruction.
labels)
63 switch(instruction.
type)
66 out <<
"NO INSTRUCTION TYPE SET" <<
'\n';
79 for(instructiont::targetst::const_iterator
80 gt_it=instruction.
targets.begin();
81 gt_it!=instruction.
targets.end();
84 if(gt_it!=instruction.
targets.begin())
86 out << (*gt_it)->target_number;
120 out <<
"SKIP" <<
'\n';
124 out <<
"END_FUNCTION" <<
'\n';
128 out <<
"LOCATION" <<
'\n';
138 for(
const auto &ex : exception_list)
139 out <<
" " << ex.id();
153 out <<
"EXCEPTION LANDING PAD (" 154 <<
from_type(ns, identifier, landingpad.catch_expr().type())
156 <<
from_expr(ns, identifier, landingpad.catch_expr())
161 out <<
"CATCH-PUSH ";
167 "size of target list");
168 for(instructiont::targetst::const_iterator
169 gt_it=instruction.
targets.begin();
170 gt_it!=instruction.
targets.end();
173 if(gt_it!=instruction.
targets.begin())
175 out << exception_list[i].id() <<
"->" 176 << (*gt_it)->target_number;
193 out <<
"ATOMIC_BEGIN" <<
'\n';
197 out <<
"ATOMIC_END" <<
'\n';
201 out <<
"START THREAD " 207 out <<
"END THREAD" <<
'\n';
211 throw "unknown statement";
225 "declaration statements");
227 "operand of declaration statement");
229 decl_identifiers.insert(symbol_expr.get_identifier());
236 if(src.
id()==ID_dereference)
239 dest.push_back(src.
op0());
241 else if(src.
id()==ID_index)
244 dest.push_back(src.
op1());
247 else if(src.
id()==ID_member)
252 else if(src.
id()==ID_if)
255 dest.push_back(src.
op0());
264 std::list<exprt> dest;
266 switch(instruction.
type)
271 dest.push_back(instruction.
guard);
293 dest.push_back(assignment.
rhs());
309 std::list<exprt> dest;
311 switch(instruction.
type)
318 dest.push_back(function_call.
lhs());
336 std::list<exprt> &dest)
338 if(src.
id()==ID_symbol)
340 else if(src.
id()==ID_address_of)
344 else if(src.
id()==ID_dereference)
363 std::list<exprt> dest;
365 for(
const auto &expr : expressions)
373 std::list<exprt> &dest)
390 std::list<exprt> dest;
392 for(
const auto &expr : expressions)
407 return "(NO INSTRUCTION TYPE)";
419 for(goto_programt::instructiont::targetst::const_iterator
458 return "END_FUNCTION";
470 return "ATOMIC_BEGIN";
476 result+=
"START THREAD ";
486 throw "unknown statement";
494 if(i.is_backwards_goto())
509 std::ostream &out)
const 530 for(
const auto &t : i.targets)
544 i.target_number=++cnt;
554 for(
const auto &t : i.targets)
570 typedef std::map<const_targett, targett> targets_mappingt;
571 targets_mappingt targets_mapping;
577 for(instructionst::const_iterator
583 targets_mapping[it]=new_instruction;
584 *new_instruction=*it;
591 for(
auto &t : i.targets)
593 targets_mappingt::iterator
594 m_target_it=targets_mapping.find(t);
596 if(m_target_it==targets_mapping.end())
597 throw "copy_from: target not found";
599 t=m_target_it->second;
611 if(i.is_assert() && !i.guard.is_true())
621 i.incoming_edges.clear();
624 for(instructionst::iterator
632 s->incoming_edges.insert(it);
exprt guard
Guard for gotos, assume, assert.
const irep_idt & get_statement() const
irep_idt function
The function this instruction belongs to.
void update()
Update all indices.
const exprt & return_value() const
const std::string & id2string(const irep_idt &d)
void compute_loop_numbers()
Compute loop numbers.
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
unsigned location_number
A globally unique number to identify a program location.
std::vector< irept > subt
std::string comment(const rw_set_baset::entryt &entry, bool write)
goto_program_instruction_typet type
What kind of instruction?
#define forall_expr(it, expr)
std::string as_string() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool has_assertion() const
Does the goto program have an assertion?
static const unsigned nil_target
Uniquely identify an invalid target or location.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
targetst targets
The list of successor instructions.
This class represents an instruction in the GOTO intermediate representation.
void clear()
Clear the goto program.
unsigned target_number
A number to identify branch targets.
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
const code_assignt & to_code_assign(const codet &code)
std::set< irep_idt > decl_identifierst
const irep_idt & id() const
void compute_incoming_edges()
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
std::list< Target > get_successors(Target target) const
const code_returnt & to_code_return(const codet &code)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void objects_read(const exprt &src, std::list< exprt > &dest)
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void compute_location_numbers()
Compute location numbers.
A generic container class for the GOTO intermediate representation of one function.
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
static code_landingpadt & to_code_landingpad(codet &code)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
source_locationt source_location
The location of the instruction in the source file.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
void compute_target_numbers()
Compute the target numbers.
void objects_written(const exprt &src, std::list< exprt > &dest)
Expression to hold a symbol (variable)
const irep_idt & get_comment() const
#define DATA_INVARIANT(CONDITION, REASON)
#define forall_goto_program_instructions(it, program)
bool is_target() const
Is this node a branch target?
const irept & find(const irep_namet &name) const
const code_function_callt & to_code_function_call(const codet &code)