12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H 13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H 192 typedef std::list<instructiont>::iterator
targett;
350 #if (defined _MSC_VER && _MSC_VER <= 1800) 354 static_cast<unsigned>(-1);
358 std::numeric_limits<unsigned>::max();
388 std::ostringstream instruction_id_builder;
389 instruction_id_builder <<
type;
390 return instruction_id_builder.str();
421 while(!l->is_end_function())
435 template <
typename Target>
444 const auto next=std::next(target);
453 target->swap(instruction);
466 auto next=std::next(target);
523 std::ostream &out)
const;
526 std::ostream &
output(std::ostream &out)
const 536 const instructionst::value_type &it)
const;
547 nr != std::numeric_limits<unsigned>::max(),
548 "Too many location numbers assigned");
549 i.location_number=nr++;
562 if(instruction.function.empty())
564 instruction.function = function_id;
621 "goto program ends on END_FUNCTION");
630 "goto program ends on END_FUNCTION");
645 template <
typename Target>
650 return std::list<Target>();
652 const auto next=std::next(target);
661 successors.push_back(next);
671 successors.push_back(next);
679 return std::list<Target>();
685 return std::list<Target>();
692 std::list<Target>{next} :
698 return std::list<Target>{next};
701 return std::list<Target>();
719 using hash_typet = decltype(&(*t));
720 return std::hash<hash_typet>{}(&(*t));
728 template <
class A,
class B>
731 return &(*a) == &(*b);
735 #define forall_goto_program_instructions(it, program) \ 736 for(goto_programt::instructionst::const_iterator \ 737 it=(program).instructions.begin(); \ 738 it!=(program).instructions.end(); it++) 740 #define Forall_goto_program_instructions(it, program) \ 741 for(goto_programt::instructionst::iterator \ 742 it=(program).instructions.begin(); \ 743 it!=(program).instructions.end(); it++) 756 return &(*i1)<&(*i2);
769 #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 given target.
bool is_atomic_end() const
void compute_loop_numbers()
Compute loop numbers.
std::set< targett > incoming_edges
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
void compute_location_numbers(unsigned &nr)
Compute location numbers.
std::size_t operator()(const goto_programt::const_targett t) const
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, which 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)
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)
#define INVARIANT(CONDITION, REASON)
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)
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 is_end_function() const
std::list< const_targett > const_targetst
std::set< irep_idt > decl_identifierst
const_targett get_end_function() const
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()
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
goto_programt & operator=(goto_programt &&other)
std::list< exprt > objects_read(const goto_programt::instructiont &)
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 given target.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
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)
std::list< targett > targetst
std::list< irep_idt > labelst
Goto target labels.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
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()
void make_goto(targett _target, const exprt &g)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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)
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)
A statement in a programming language.
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)
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.