Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
245 const auto &decl = expr_checked_cast<code_declt>(
code);
247 !decl.initial_value(),
248 "code_declt in goto program may not contain initialization.");
256 auto &decl = expr_checked_cast<code_declt>(
code);
258 !decl.initial_value(),
259 "code_declt in goto program may not contain initialization.");
260 return decl.symbol();
267 auto &decl = expr_checked_cast<code_declt>(
code);
269 !decl.initial_value(),
270 "code_declt in goto program may not contain initialization.");
271 return decl.symbol();
281 "Initialization must be separated from code_declt before adding to "
282 "goto_instructiont.");
352 "Use call_function(), call_lhs(), call_arguments() instead"))
408 "Use call_function(), call_lhs(), call_arguments() instead"))
457 guard = std::move(c);
462 typedef std::list<instructiont>::iterator
targett;
568 :
code(std::move(_code)),
571 guard(std::move(_guard)),
589 std::numeric_limits<unsigned>::max();
618 std::ostringstream instruction_id_builder;
619 instruction_id_builder <<
type;
620 return instruction_id_builder.str();
640 void apply(std::function<
void(
const exprt &)>)
const;
667 template <
typename Target>
676 const auto next=std::next(target);
685 target->swap(instruction);
698 auto next=std::next(target);
777 std::ostream &out)
const;
780 std::ostream &
output(std::ostream &out)
const;
787 const instructionst::value_type &instruction)
const;
798 nr != std::numeric_limits<unsigned>::max(),
799 "Too many location numbers assigned");
800 i.location_number=nr++;
859 "goto program ends on END_FUNCTION");
870 "goto program ends on END_FUNCTION");
897 ins.validate(ns, vm);
1142 template <
typename Target>
1144 Target target)
const
1147 return std::list<Target>();
1149 const auto next=std::next(target);
1155 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1158 successors.push_back(next);
1165 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1168 successors.push_back(next);
1176 return std::list<Target>();
1182 return std::list<Target>();
1188 ? std::list<Target>{next}
1189 : std::list<Target>();
1194 return std::list<Target>{next};
1197 return std::list<Target>();
1215 using hash_typet = decltype(&(*t));
1216 return std::hash<hash_typet>{}(&(*t));
1224 template <
class A,
class B>
1227 return &(*a) == &(*b);
1231 template <
typename GotoFunctionT,
typename PredicateT,
typename HandlerT>
1233 GotoFunctionT &&goto_function,
1234 PredicateT predicate,
1237 auto &&instructions = goto_function.body.instructions;
1238 for(
auto it = instructions.begin(); it != instructions.end(); ++it)
1247 template <
typename GotoFunctionT,
typename HandlerT>
1250 using iterator_t = decltype(goto_function.body.instructions.begin());
1252 goto_function, [](
const iterator_t &) {
return true; }, handler);
1255 #define forall_goto_program_instructions(it, program) \
1256 for(goto_programt::instructionst::const_iterator \
1257 it=(program).instructions.begin(); \
1258 it!=(program).instructions.end(); it++)
1260 #define Forall_goto_program_instructions(it, program) \
1261 for(goto_programt::instructionst::iterator \
1262 it=(program).instructions.begin(); \
1263 it!=(program).instructions.end(); it++)
1276 return &(*i1)<&(*i2);
1290 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
const code_deadt & get_dead() const
Get the dead statement for DEAD.
exprt::operandst & call_arguments()
Get the arguments of a FUNCTION_CALL.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void set_other(codet &c)
Set the statement for OTHER.
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
source_locationt source_location
The location of the instruction in the source file.
std::list< irep_idt > labelst
Goto target labels.
void complete_goto(targett _target)
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 set_assign(code_assignt c)
Set the assignment for ASSIGN.
std::string to_string() const
void swap(instructiont &instruction)
Swap two instructions.
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
void clear(goto_program_instruction_typet _type)
Clear the node.
void compute_loop_numbers()
Compute loop numbers.
std::list< const_targett > const_targetst
const code_returnt & get_return() const
Get the return statement for READ.
goto_programt(const goto_programt &)=delete
Copying is deleted as this class contains pointers that cannot be copied.
void set_return(code_returnt c)
Set the return statement for SET_RETURN_VALUE.
std::list< instructiont > instructionst
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
goto_program_instruction_typet type
What kind of instruction?
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
static const source_locationt & nil()
std::list< exprt > expressions_read(const goto_programt::instructiont &)
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
void update()
Update all indices.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
A codet representing the declaration of a local variable.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
bool empty() const
Is the program empty?
Base class for all expressions.
Functor to check whether iterators from different collections point at the same object.
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
void set_decl(code_declt c)
Set the declaration for DECL.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
std::list< exprt > objects_written(const goto_programt::instructiont &)
bool has_assertion() const
Does the goto program have an assertion?
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
targetst targets
The list of successor instructions.
bool is_incomplete_goto() const
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
bool is_true() const
Return whether the expression is a constant representing true.
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
bool is_end_thread() const
Expression to hold a symbol (variable)
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
bool is_atomic_end() const
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
std::list< exprt > objects_read(const goto_programt::instructiont &)
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool is_false() const
Return whether the expression is a constant representing false.
const codet & get_other() const
Get the statement for OTHER.
const codet & get_code() const
Get the code represented by this instruction.
std::list< instructiont >::const_iterator const_targett
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
bool is_atomic_begin() const
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
std::list< targett > targetst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add_instruction()
Adds an instruction at the end.
typet & type()
Return the type of the expression.
codet representation of a function call statement.
static instructiont make_function_call(exprt lhs, exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
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...
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void compute_target_numbers()
Compute the target numbers.
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const std::string & id2string(const irep_idt &d)
goto_programt(goto_programt &&other)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
codet code
Do not read or modify directly – use get_X() instead.
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
exprt & call_function()
Get the function that is called for FUNCTION_CALL.
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
codet representation of a goto statement.
#define PRECONDITION(CONDITION)
void compute_location_numbers(unsigned &nr)
Compute location numbers.
const code_deadt & to_code_dead(const codet &code)
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
bool operator()(const A &a, const B &b) const
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
std::list< exprt > expressions_written(const goto_programt::instructiont &)
bool has_condition() const
Does this instruction have a condition?
bool is_set_return_value() const
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
goto_programt()
Constructor.
const irep_idt & id() const
bool is_end_function() const
const code_function_callt & to_code_function_call(const codet &code)
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
std::vector< exprt > operandst
exprt::operandst argumentst
const code_returnt & to_code_return(const codet &code)
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
A codet representing the removal of a local variable going out of scope.
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
#define SINCE(year, month, day, msg)
exprt & return_value()
Get the return value of a SET_RETURN_VALUE instruction.
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
nonstd::optional< T > optionalt
std::list< targett > targetst
void clear()
Clear the goto program.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const code_declt & get_decl() const
Get the declaration for DECL.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
void compute_location_numbers()
Compute location numbers.
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
unsigned target_number
A number to identify branch targets.
goto_programt & operator=(goto_programt &&other)
codet representation of a "return from a function" statement.
std::set< targett > incoming_edges
const code_assignt & to_code_assign(const codet &code)
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
unsigned location_number
A globally unique number to identify a program location.
targett insert_before(const_targett target, const instructiont &i)
Insertion before the instruction pointed-to by the given instruction iterator target.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
exprt & call_lhs()
Get the lhs of a FUNCTION_CALL (may be nil)
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const source_locationt &l=source_locationt::nil())
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
unsigned loop_number
Number unique per function to identify loops.
A generic container class for the GOTO intermediate representation of one function.
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
instructionst::const_iterator const_targett
const irept & get_nil_irep()
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
std::list< const_targett > const_targetst
goto_programt & operator=(const goto_programt &)=delete
static instructiont make_incomplete_goto(const code_gotot &_code, const source_locationt &l=source_locationt::nil())
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void set_dead(code_deadt c)
Set the dead statement for DEAD.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
const exprt & return_value() const
A codet representing an assignment in the program.
bool is_start_thread() const
The Boolean constant true.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
bool is_function_call() const
std::set< irep_idt > decl_identifierst
This class represents an instruction in the GOTO intermediate representation.
bool is_target() const
Is this node a branch target?
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.
codet & code_nonconst()
Set the code represented by this instruction.
static const unsigned nil_target
Uniquely identify an invalid target or location.
static instructiont make_location(const source_locationt &l)
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.
void swap(goto_programt &program)
Swap the goto program.
static instructiont make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
instructionst::iterator targett
instructiont(goto_program_instruction_typet _type)
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
std::size_t operator()(const goto_programt::const_targett t) const
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Data structure for representing an arbitrary statement in a program.