Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
295 guard = std::move(c);
300 typedef std::list<instructiont>::iterator
targett;
356 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_return() instead"))
359 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_skip() instead"))
362 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_location() instead"))
366 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_throw() instead"))
369 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_catch() instead"))
373 SINCE(2019, 2, 13,
"use goto_programt::make_assertion() instead"))
377 SINCE(2019, 2, 13,
"use goto_programt::make_assumption() instead"))
381 SINCE(2019, 2, 13,
"use goto_programt::make_assignment() instead"))
384 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_other() instead"))
387 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_decl() instead"))
390 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_dead() instead"))
394 SINCE(2019, 2, 13,
"use goto_programt::make_atomic_begin() instead"))
398 SINCE(2019, 2, 13,
"use goto_programt::make_atomic_end() instead"))
402 SINCE(2019, 2, 13,
"use goto_programt::make_end_function() instead"))
406 SINCE(2019, 2, 13,
"use goto_programt::make_incomplete_goto() instead"))
413 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_goto() instead"))
420 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_goto() instead"))
436 SINCE(2019, 2, 13,
"use goto_programt::make_assignment() instead"))
443 DEPRECATED(
SINCE(2019, 2, 13,
"use goto_programt::make_decl() instead"))
451 SINCE(2019, 2, 13,
"use goto_programt::make_function_call() instead"))
501 :
code(std::move(_code)),
504 guard(std::move(_guard)),
522 std::numeric_limits<unsigned>::max();
551 std::ostringstream instruction_id_builder;
552 instruction_id_builder <<
type;
553 return instruction_id_builder.str();
573 void apply(std::function<
void(
const exprt &)>)
const;
600 template <
typename Target>
609 const auto next=std::next(target);
618 target->swap(instruction);
631 auto next=std::next(target);
710 std::ostream &out)
const;
713 std::ostream &
output(std::ostream &out)
const
723 const instructionst::value_type &instruction)
const;
734 nr != std::numeric_limits<unsigned>::max(),
735 "Too many location numbers assigned");
736 i.location_number=nr++;
795 "goto program ends on END_FUNCTION");
806 "goto program ends on END_FUNCTION");
833 ins.validate(ns, vm);
1083 template <
typename Target>
1085 Target target)
const
1088 return std::list<Target>();
1090 const auto next=std::next(target);
1096 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1099 successors.push_back(next);
1106 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1109 successors.push_back(next);
1117 return std::list<Target>();
1123 return std::list<Target>();
1129 ? std::list<Target>{next}
1130 : std::list<Target>();
1135 return std::list<Target>{next};
1138 return std::list<Target>();
1156 using hash_typet = decltype(&(*t));
1157 return std::hash<hash_typet>{}(&(*t));
1165 template <
class A,
class B>
1168 return &(*a) == &(*b);
1172 template <
typename GotoFunctionT,
typename PredicateT,
typename HandlerT>
1174 GotoFunctionT &&goto_function,
1175 PredicateT predicate,
1178 auto &&instructions = goto_function.body.instructions;
1179 for(
auto it = instructions.begin(); it != instructions.end(); ++it)
1188 template <
typename GotoFunctionT,
typename HandlerT>
1191 using iterator_t = decltype(goto_function.body.instructions.begin());
1193 goto_function, [](
const iterator_t &) {
return true; }, handler);
1196 #define forall_goto_program_instructions(it, program) \
1197 for(goto_programt::instructionst::const_iterator \
1198 it=(program).instructions.begin(); \
1199 it!=(program).instructions.end(); it++)
1201 #define Forall_goto_program_instructions(it, program) \
1202 for(goto_programt::instructionst::iterator \
1203 it=(program).instructions.begin(); \
1204 it!=(program).instructions.end(); it++)
1217 return &(*i1)<&(*i2);
1231 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
const code_deadt & get_dead() const
Get the dead statement for DEAD.
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 make_function_call(const code_function_callt &_code)
const code_declt & to_code_decl(const codet &code)
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 READ.
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?
void make_incomplete_goto(const code_gotot &_code)
static const source_locationt & nil()
std::list< exprt > expressions_read(const goto_programt::instructiont &)
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())
bool is_atomic_end() const
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.
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.
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 make_other(const codet &_code)
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 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.
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?
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.
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.
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)
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
nonstd::optional< T > optionalt
void make_goto(targett _target)
std::list< targett > targetst
void clear()
Clear the goto program.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
static instructiont make_return(const source_locationt &l=source_locationt::nil())
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)
void make_assumption(const exprt &g)
static instructiont make_function_call(exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
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 &)
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.
void make_location(const source_locationt &l)
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())
void set_dead(code_deadt c)
Set the dead statement for DEAD.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void make_assertion(const exprt &g)
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
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.
API to expression classes.
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.
static const unsigned nil_target
Uniquely identify an invalid target or location.
static instructiont make_location(const source_locationt &l)
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.