12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
204 const auto &decl = expr_checked_cast<code_declt>(
code);
206 !decl.initial_value(),
207 "code_declt in goto program may not contain initialization.");
215 auto &decl = expr_checked_cast<code_declt>(
code);
217 !decl.initial_value(),
218 "code_declt in goto program may not contain initialization.");
219 return decl.symbol();
226 auto &decl = expr_checked_cast<code_declt>(
code);
228 !decl.initial_value(),
229 "code_declt in goto program may not contain initialization.");
230 return decl.symbol();
240 "Initialization must be separated from code_declt before adding to "
241 "goto_instructiont.");
360 guard = std::move(c);
365 typedef std::list<instructiont>::iterator
targett;
472 :
code(std::move(_code)),
475 guard(std::move(_guard)),
493 std::numeric_limits<unsigned>::max();
522 std::ostringstream instruction_id_builder;
523 instruction_id_builder <<
type;
524 return instruction_id_builder.str();
544 void apply(std::function<
void(
const exprt &)>)
const;
571 template <
typename Target>
580 const auto next=std::next(target);
589 target->swap(instruction);
602 auto next=std::next(target);
681 std::ostream &out)
const;
684 std::ostream &
output(std::ostream &out)
const
694 const instructionst::value_type &instruction)
const;
705 nr != std::numeric_limits<unsigned>::max(),
706 "Too many location numbers assigned");
707 i.location_number=nr++;
766 "goto program ends on END_FUNCTION");
777 "goto program ends on END_FUNCTION");
804 ins.validate(ns, vm);
1054 template <
typename Target>
1056 Target target)
const
1059 return std::list<Target>();
1061 const auto next=std::next(target);
1067 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1070 successors.push_back(next);
1077 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1080 successors.push_back(next);
1088 return std::list<Target>();
1094 return std::list<Target>();
1100 ? std::list<Target>{next}
1101 : std::list<Target>();
1106 return std::list<Target>{next};
1109 return std::list<Target>();
1127 using hash_typet = decltype(&(*t));
1128 return std::hash<hash_typet>{}(&(*t));
1136 template <
class A,
class B>
1139 return &(*a) == &(*b);
1143 template <
typename GotoFunctionT,
typename PredicateT,
typename HandlerT>
1145 GotoFunctionT &&goto_function,
1146 PredicateT predicate,
1149 auto &&instructions = goto_function.body.instructions;
1150 for(
auto it = instructions.begin(); it != instructions.end(); ++it)
1159 template <
typename GotoFunctionT,
typename HandlerT>
1162 using iterator_t = decltype(goto_function.body.instructions.begin());
1164 goto_function, [](
const iterator_t &) {
return true; }, handler);
1167 #define forall_goto_program_instructions(it, program) \
1168 for(goto_programt::instructionst::const_iterator \
1169 it=(program).instructions.begin(); \
1170 it!=(program).instructions.end(); it++)
1172 #define Forall_goto_program_instructions(it, program) \
1173 for(goto_programt::instructionst::iterator \
1174 it=(program).instructions.begin(); \
1175 it!=(program).instructions.end(); it++)
1188 return &(*i1)<&(*i2);
A codet representing an assignment in the program.
A codet representing the removal of a local variable going out of scope.
A codet representing the declaration of a local variable.
codet representation of a function call statement.
exprt::operandst argumentst
codet representation of a goto statement.
codet representation of a "return from a function" statement.
const exprt & return_value() const
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
This class represents an instruction in the GOTO intermediate representation.
bool is_end_function() const
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.
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
void clear(goto_program_instruction_typet _type)
Clear the node.
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
void complete_goto(targett _target)
bool is_target() const
Is this node a branch target?
codet code
Do not read or modify directly – use get_X() instead.
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
std::list< targett > targetst
const codet & get_other() const
Get the statement for OTHER.
const code_deadt & get_dead() const
Get the dead statement for DEAD.
instructiont(goto_program_instruction_typet _type)
std::set< targett > incoming_edges
source_locationt source_location
The location of the instruction in the source file.
instructiont(codet _code, source_locationt _source_location, goto_program_instruction_typet _type, exprt _guard, targetst _targets)
Constructor that can set all members, passed by value.
bool has_condition() const
Does this instruction have a condition?
goto_program_instruction_typet type
What kind of instruction?
bool is_end_thread() const
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
targetst targets
The list of successor instructions.
unsigned loop_number
Number unique per function to identify loops.
const exprt & return_value() const
Get the return value of a RETURN instruction.
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
exprt & return_value()
Get the return value of a RETURN instruction.
void set_return(code_returnt c)
Set the return statement for READ.
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
bool is_start_thread() const
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
bool is_atomic_end() const
std::string to_string() const
unsigned location_number
A globally unique number to identify a program location.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
void set_dead(code_deadt c)
Set the dead statement for DEAD.
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
std::list< instructiont >::const_iterator const_targett
static const unsigned nil_target
Uniquely identify an invalid target or location.
bool is_atomic_begin() const
std::list< const_targett > const_targetst
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
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 get_condition() to read, and set_condition(c) to write.
bool is_function_call() const
void set_decl(code_declt c)
Set the declaration for DECL.
const code_returnt & get_return() const
Get the return statement for READ.
const code_declt & get_decl() const
Get the declaration for DECL.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
void swap(instructiont &instruction)
Swap two instructions.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
std::list< irep_idt > labelst
Goto target labels.
void set_other(codet &c)
Set the statement for OTHER.
bool is_incomplete_goto() const
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.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
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 insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
static instructiont make_return(const source_locationt &l=source_locationt::nil())
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target, const instructiont &i)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void update()
Update all indices.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
bool has_assertion() const
Does the goto program have an assertion?
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.
targett insert_before(const_targett target, const instructiont &i)
Insertion before the instruction pointed-to by the given instruction iterator target.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
goto_programt & operator=(goto_programt &&other)
instructionst::const_iterator const_targett
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
targett add_instruction()
Adds an instruction at the end.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
goto_programt()
Constructor.
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
std::list< instructiont > instructionst
static instructiont make_function_call(exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
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.
std::list< const_targett > const_targetst
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
goto_programt(const goto_programt &)=delete
Copying is deleted as this class contains pointers that cannot be copied.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
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.
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
goto_programt(goto_programt &&other)
void compute_location_numbers()
Compute location numbers.
void swap(goto_programt &program)
Swap the goto program.
goto_programt & operator=(const goto_programt &)=delete
static instructiont make_location(const source_locationt &l)
static instructiont make_incomplete_goto(const code_gotot &_code, const source_locationt &l=source_locationt::nil())
void compute_target_numbers()
Compute the target numbers.
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?
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_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
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.
static instructiont make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void compute_loop_numbers()
Compute loop numbers.
std::list< targett > targetst
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static const source_locationt & nil()
Expression to hold a symbol (variable)
The Boolean constant true.
#define SINCE(year, month, day, msg)
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
std::list< exprt > expressions_read(const goto_programt::instructiont &)
std::list< exprt > objects_written(const goto_programt::instructiont &)
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
std::list< exprt > expressions_written(const goto_programt::instructiont &)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
std::list< exprt > objects_read(const goto_programt::instructiont &)
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const code_returnt & to_code_return(const codet &code)
const code_deadt & to_code_dead(const codet &code)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
API to expression classes.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t operator()(const goto_programt::const_targett t) const
Functor to check whether iterators from different collections point at the same object.
bool operator()(const A &a, const B &b) const