12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H 13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H 197 typedef std::list<instructiont>::iterator
targett;
355 #if (defined _MSC_VER && _MSC_VER <= 1800) 359 static_cast<unsigned>(-1);
363 std::numeric_limits<unsigned>::max();
393 std::ostringstream instruction_id_builder;
394 instruction_id_builder <<
type;
395 return instruction_id_builder.str();
453 while(!l->is_end_function())
471 template <
typename Target>
480 const auto next=std::next(target);
489 target->swap(instruction);
502 auto next=std::next(target);
559 std::ostream &out)
const;
562 std::ostream &
output(std::ostream &out)
const 572 const instructionst::value_type &instruction)
const;
583 nr != std::numeric_limits<unsigned>::max(),
584 "Too many location numbers assigned");
585 i.location_number=nr++;
598 if(instruction.function.empty())
600 instruction.function = function_id;
659 "goto program ends on END_FUNCTION");
670 "goto program ends on END_FUNCTION");
697 ins.validate(ns, vm);
714 template <
typename Target>
719 return std::list<Target>();
721 const auto next=std::next(target);
730 successors.push_back(next);
740 successors.push_back(next);
748 return std::list<Target>();
754 return std::list<Target>();
761 std::list<Target>{next} :
767 return std::list<Target>{next};
770 return std::list<Target>();
788 using hash_typet = decltype(&(*t));
789 return std::hash<hash_typet>{}(&(*t));
797 template <
class A,
class B>
800 return &(*a) == &(*b);
804 #define forall_goto_program_instructions(it, program) \ 805 for(goto_programt::instructionst::const_iterator \ 806 it=(program).instructions.begin(); \ 807 it!=(program).instructions.end(); it++) 809 #define Forall_goto_program_instructions(it, program) \ 810 for(goto_programt::instructionst::iterator \ 811 it=(program).instructions.begin(); \ 812 it!=(program).instructions.end(); it++) 825 return &(*i1)<&(*i2);
838 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H const irept & get_nil_irep()
goto_programt(goto_programt &&other)
exprt guard
Guard for gotos, assume, assert.
irep_idt function
The function this instruction belongs to.
void update()
Update all indices.
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
std::list< targett > targetst
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
bool is_atomic_end() const
void compute_loop_numbers()
Compute loop numbers.
std::set< targett > incoming_edges
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
std::string to_string() const
void make_assumption(const exprt &g)
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
unsigned location_number
A globally unique number to identify a program location.
goto_program_instruction_typet type
What kind of instruction?
bool is_function_call() const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
std::size_t operator()(const goto_programt::const_targett t) const
bool is_false() const
Return whether the expression is a constant representing false.
bool has_assertion() const
Does the goto program have an assertion?
std::list< exprt > objects_written(const goto_programt::instructiont &)
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible. ...
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
bool is_true() const
Return whether the expression is a constant representing true.
codet representation of a goto statement.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static const unsigned nil_target
Uniquely identify an invalid target or location.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void make_assignment(const codet &_code)
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
bool is_incomplete_goto() const
bool operator()(const A &a, const B &b) const
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
void make_function_call(const codet &_code)
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard, number of targets, and labels.
bool is_atomic_begin() const
targetst targets
The list of successor instructions.
This class represents an instruction in the GOTO intermediate representation.
void clear()
Clear the goto program.
static const irep_idt get_function_id(const goto_programt &p)
Get the id of the function that contains the given goto program.
bool is_end_thread() const
std::list< instructiont > instructionst
std::list< exprt > expressions_read(const goto_programt::instructiont &)
unsigned target_number
A number to identify branch targets.
std::list< instructiont >::const_iterator const_targett
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...
bool is_end_function() const
std::list< const_targett > const_targetst
std::set< irep_idt > decl_identifierst
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
unsigned loop_number
Number unique per function to identify loops.
std::list< exprt > expressions_written(const goto_programt::instructiont &)
The Boolean constant true.
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
instructionst::iterator targett
void complete_goto(targett _target)
void make_location(const source_locationt &l)
std::string as_string(const namespacet &ns, const goto_programt::instructiont &)
void make_other(const codet &_code)
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
instructionst::const_iterator const_targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
goto_programt & operator=(goto_programt &&other)
std::list< exprt > objects_read(const goto_programt::instructiont &)
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
#define PRECONDITION(CONDITION)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Functor to check whether iterators from different collections point at the same object.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
void compute_location_numbers()
Compute location numbers.
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
void swap(goto_programt &program)
Swap the goto program.
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
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
std::list< targett > targetst
std::list< irep_idt > labelst
Goto target labels.
void update_instructions_function(const irep_idt &function_id)
Sets the function member of each instruction if not yet set Note that a goto program need not be a go...
void make_decl(const codet &_code)
source_locationt source_location
The location of the instruction in the source file.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
goto_programt()
Constructor.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
void make_goto(targett _target, const exprt &g)
bool empty() const
Is the program empty?
void compute_target_numbers()
Compute the target numbers.
void swap(instructiont &instruction)
Swap two instructions.
std::list< const_targett > const_targetst
void clear(goto_program_instruction_typet _type)
Clear the node.
static const irep_idt get_function_id(const_targett l)
Get the id of the function that contains the instruction pointed-to by the given instruction iterator...
void make_incomplete_goto(const code_gotot &_code)
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
void make_assertion(const exprt &g)
Data structure for representing an arbitrary statement in a program.
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
bool is_start_thread() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
goto_programt & operator=(const goto_programt &)=delete
instructiont(goto_program_instruction_typet _type)
bool is_target() const
Is this node a branch target?
void make_goto(targett _target)
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.