72 if(!instruction.
labels.empty())
75 for(
const auto &label : instruction.
labels)
86 switch(instruction.
type())
89 out <<
"NO INSTRUCTION TYPE SET" <<
'\n';
103 out <<
"(incomplete)";
113 out << (*gt_it)->target_number;
123 const auto &code = instruction.
get_other();
126 out <<
"HAVOC_OBJECT " <<
format(code.op0()) <<
'\n';
193 out <<
"SKIP" <<
'\n';
197 out <<
"END_FUNCTION" <<
'\n';
201 out <<
"LOCATION" <<
'\n';
211 for(
const auto &
ex : exception_list)
212 out <<
" " <<
ex.id();
231 out <<
"CATCH-PUSH ";
237 instruction.
targets.size() == exception_list.size(),
238 "unexpected discrepancy between sizes of instruction"
239 "targets and exception list");
240 for(instructiont::targetst::const_iterator
247 out << exception_list[
i].id() <<
"->"
248 << (*gt_it)->target_number;
265 out <<
"ATOMIC_BEGIN" <<
'\n';
269 out <<
"ATOMIC_END" <<
'\n';
273 out <<
"START THREAD "
279 out <<
"END THREAD" <<
'\n';
291 if(instruction.is_decl())
294 instruction.get_code().get_statement() ==
ID_decl,
295 "expected statement to be declaration statement");
297 instruction.get_code().operands().size() == 1,
298 "declaration statement expects one operand");
332 std::list<exprt>
dest;
334 switch(instruction.
type())
381 std::list<exprt>
dest;
383 switch(instruction.
type())
420 std::list<exprt> &
dest)
447 std::list<exprt>
dest;
449 for(
const auto &expr : expressions)
457 std::list<exprt> &
dest)
474 std::list<exprt>
dest;
476 for(
const auto &expr : expressions)
492 return "(NO INSTRUCTION TYPE)";
495 if(!
i.get_condition().is_true())
497 result +=
"IF " +
from_expr(ns, function,
i.get_condition()) +
" THEN ";
502 for(goto_programt::instructiont::targetst::const_iterator
507 if(
gt_it!=
i.targets.begin())
509 result+=std::to_string((*gt_it)->target_number);
528 result +=
from_expr(ns, function,
i.get_condition());
541 return "END_FUNCTION";
553 return "ATOMIC_BEGIN";
559 result+=
"START THREAD ";
561 if(
i.targets.size()==1)
562 result+=std::to_string(
i.targets.front()->target_number);
582 if(
i.is_backwards_goto())
597 std::ostream &out)
const
628 for(
const auto &t :
i.targets)
642 i.target_number=++
cnt;
644 i.target_number != 0,
"GOTO instruction target cannot be zero");
653 for(
const auto &t :
i.targets)
658 t->target_number != 0,
"instruction's number cannot be zero");
661 "GOTO instruction target cannot be nil_target");
681 for(instructionst::const_iterator
688 *new_instruction=*it;
695 for(
auto &t :
i.targets)
697 targets_mappingt::iterator
715 if(
i.is_assert() && !
i.get_condition().is_true())
729 for(instructionst::iterator
737 s->incoming_edges.insert(it);
766 for(
const auto &identifier :
typetags)
770 !ns.
lookup(identifier, symbol),
838 "\n" +
"symbol table type: " +
table_symbol->type.id_string(),
853 "goto instruction expects at least one target",
858 get_target()->is_target() && get_target()->target_number != 0,
859 "goto target has to be a target",
866 "assume instruction should not have a target",
873 "assert instruction should not have a target",
877 std::for_each(guard.depth_begin(), guard.depth_end(),
type_finder);
899 "SET_RETURN_VALUE instruction should contain a return statement",
906 "assign instruction should contain an assign statement");
908 vm, targets.empty(),
"assign instruction should not have a target");
913 code.get_statement() ==
ID_decl,
914 "declaration instructions should contain a declaration statement",
919 "declared symbols should be known",
926 code.get_statement() ==
ID_dead,
927 "dead instructions should contain a dead statement",
932 "removed symbols should be known",
940 "function call instruction should contain a call statement",
944 std::for_each(code.depth_begin(), code.depth_end(),
type_finder);
994 auto new_symbol = f(decl_symbol());
995 if(new_symbol.has_value())
1002 auto new_symbol = f(dead_symbol());
1003 if(new_symbol.has_value())
1024 if(
new_a.has_value())
1060 std::function<
void(
const exprt &)> f)
const
1088 for(
auto &
a : call_arguments())
1124 for(
const auto &t :
ins.targets)
1127 t->location_number -
ins.location_number !=
1128 (*other_target_it)->location_number -
other_it->location_number)
1148 out <<
"NO_INSTRUCTION_TYPE";
1172 out <<
"START_THREAD";
1175 out <<
"END_THREAD";
1181 out <<
"END_FUNCTION";
1184 out <<
"ATOMIC_BEGIN";
1187 out <<
"ATOMIC_END";
1190 out <<
"SET_RETURN_VALUE";
1196 out <<
"FUNCTION_CALL";
1205 out <<
"INCOMPLETE_GOTO";
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
bool is_incomplete() const
codet representation of a goto statement.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
unsigned target_number
A number to identify branch targets.
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
bool is_target() const
Is this node a branch target?
codet code
Do not read or modify directly – use get_X() instead.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const codet & get_code() const
Get the code represented by this instruction.
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
targetst targets
The list of successor instructions.
const codet & get_other() const
Get the statement for OTHER.
goto_program_instruction_typet _type
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
unsigned location_number
A globally unique number to identify a program location.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
static const unsigned nil_target
Uniquely identify an invalid target or location.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
const source_locationt & source_location() const
bool is_incomplete_goto() const
goto_program_instruction_typet type() const
What kind of instruction?
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
void update()
Update all indices.
bool has_assertion() const
Does the goto program have an assertion?
instructionst::const_iterator const_targett
targett add_instruction()
Adds an instruction at the end.
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
std::set< irep_idt > decl_identifierst
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
void compute_location_numbers()
Compute location numbers.
void compute_target_numbers()
Compute the target numbers.
bool equals(const goto_programt &other) const
Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instruc...
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void compute_loop_numbers()
Compute loop numbers.
const irept & find(const irep_idt &name) const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
std::string as_string() const
const irep_idt & get_comment() const
The Boolean constant true.
#define forall_operands(it, expr)
Forward depth-first search iterators These iterators' copy operations are expensive,...
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
std::unordered_set< irep_idt > find_symbols_sett
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
std::string as_string(const class namespacet &ns, const irep_idt &function, const goto_programt::instructiont &i)
void objects_read(const exprt &src, std::list< exprt > &dest)
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
void objects_written(const exprt &src, std::list< exprt > &dest)
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
static code_landingpadt & to_code_landingpad(codet &code)
code_expressiont & to_code_expression(codet &code)
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...