12#ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
13#define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
230 auto &decl = expr_checked_cast<code_declt>(
code);
231 return decl.symbol();
238 auto &decl = expr_checked_cast<code_declt>(
code);
239 return decl.symbol();
378 guard = std::move(c);
397 typedef std::list<instructiont>::iterator
targett;
535 std::numeric_limits<unsigned>::max();
564 std::ostringstream instruction_id_builder;
565 instruction_id_builder <<
_type;
566 return instruction_id_builder.str();
586 void apply(std::function<
void(
const exprt &)>)
const;
613 template <
typename Target>
622 const auto next=std::next(target);
647 target->swap(instruction);
660 auto next=std::next(target);
739 std::ostream &out)
const;
742 std::ostream &
output(std::ostream &out)
const;
749 const instructionst::value_type &instruction)
const;
760 nr != std::numeric_limits<unsigned>::max(),
761 "Too many location numbers assigned");
762 i.location_number=nr++;
821 "goto program ends on END_FUNCTION");
832 "goto program ends on END_FUNCTION");
859 ins.validate(ns, vm);
1110template <
typename Target>
1112 Target target)
const
1115 return std::list<Target>();
1117 const auto next=std::next(target);
1123 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1126 successors.push_back(next);
1133 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1136 successors.push_back(next);
1144 return std::list<Target>();
1150 return std::list<Target>();
1156 ? std::list<Target>{next}
1157 : std::list<Target>();
1162 return std::list<Target>{next};
1165 return std::list<Target>();
1183 using hash_typet =
decltype(&(*t));
1184 return std::hash<hash_typet>{}(&(*t));
1192 template <
class A,
class B>
1195 return &(*a) == &(*b);
1199template <
typename GotoFunctionT,
typename PredicateT,
typename HandlerT>
1201 GotoFunctionT &&goto_function,
1202 PredicateT predicate,
1205 auto &&instructions = goto_function.body.instructions;
1206 for(
auto it = instructions.begin(); it != instructions.end(); ++it)
1215template <
typename GotoFunctionT,
typename HandlerT>
1218 using iterator_t =
decltype(goto_function.body.instructions.begin());
1220 goto_function, [](
const iterator_t &) {
return true; }, handler);
1223#define forall_goto_program_instructions(it, program) \
1224 for(goto_programt::instructionst::const_iterator \
1225 it=(program).instructions.begin(); \
1226 it!=(program).instructions.end(); it++)
1228#define Forall_goto_program_instructions(it, program) \
1229 for(goto_programt::instructionst::iterator \
1230 it=(program).instructions.begin(); \
1231 it!=(program).instructions.end(); it++)
1244 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.
std::vector< exprt > operandst
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.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
bool is_end_function() const
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.
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
exprt & call_lhs()
Get the lhs of a FUNCTION_CALL (may be nil)
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.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
std::list< targett > targetst
bool is_set_return_value() const
std::set< targett > incoming_edges
const codet & get_code() const
Get the code represented by this instruction.
bool has_condition() const
Does this instruction have a condition?
codet & code_nonconst()
Set the code represented by this instruction.
bool is_end_thread() const
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.
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
unsigned loop_number
Number unique per function to identify loops.
exprt::operandst & call_arguments()
Get the arguments of a FUNCTION_CALL.
void turn_into_assume()
Transforms either an assertion or a GOTO instruction into an assumption, with the same condition.
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,...
bool is_start_thread() const
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
bool is_atomic_end() const
std::string to_string() const
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.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
source_locationt _source_location
The location of the instruction in the source file.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
std::list< instructiont >::const_iterator const_targett
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.
bool is_atomic_begin() const
std::list< const_targett > const_targetst
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.
void clear(goto_program_instruction_typet __type)
Clear the node.
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.
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.
bool is_function_call() const
const exprt & condition() const
Get the condition of gotos, assume, assert.
instructiont(goto_program_instruction_typet __type)
void swap(instructiont &instruction)
Swap two instructions.
exprt & condition_nonconst()
Get the condition of gotos, assume, assert.
std::list< irep_idt > labelst
Goto target labels.
source_locationt & source_location_nonconst()
exprt & return_value()
Get the return value of a SET_RETURN_VALUE instruction.
exprt & call_function()
Get the function that is called for FUNCTION_CALL.
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
void set_other(codet &c)
Set the statement for OTHER.
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.
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
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.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
void clear()
Clear the goto program.
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
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.
goto_programt & operator=(goto_programt &&other)
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.
goto_programt & operator=(const goto_programt &)=delete
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
instructionst::const_iterator const_targett
static instructiont make_set_return_value(const code_returnt &code, const source_locationt &l=source_locationt::nil())=delete
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())
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
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())
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.
static instructiont make_location(const source_locationt &l)
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_function_call(exprt lhs, exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
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)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
const code_returnt & to_code_return(const codet &code)
const code_deadt & to_code_dead(const codet &code)
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
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_read(const goto_programt::instructiont &)
std::list< exprt > objects_written(const goto_programt::instructiont &)
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.
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
std::list< exprt > expressions_written(const goto_programt::instructiont &)
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
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)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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