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.
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.