Go to the documentation of this file.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
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)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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
static const irep_idt get_function_id(const goto_programt &p)
Get the id of the function that contains the given goto program.
std::list< instructiont > instructionst
goto_program_instruction_typet type
What kind of instruction?
void make_incomplete_goto(const code_gotot &_code)
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.
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 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
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 make_function_call(const codet &_code)
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
bool is_end_thread() const
void make_assignment(const codet &_code)
bool is_atomic_end() const
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.
bool is_false() const
Return whether the expression is a constant representing false.
std::list< instructiont >::const_iterator const_targett
bool is_atomic_begin() const
void make_decl(const codet &_code)
std::list< targett > targetst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
targett add_instruction()
Adds an instruction at the end.
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 compute_target_numbers()
Compute the target numbers.
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.
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.
codet representation of a goto statement.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
void make_goto(targett _target, const exprt &g)
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
bool operator()(const A &a, const B &b) const
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 &)
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
goto_programt()
Constructor.
bool is_end_function() const
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.
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
void make_goto(targett _target)
std::string as_string(const namespacet &ns, const goto_programt::instructiont &)
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...
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.
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.
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)
std::set< targett > incoming_edges
irep_idt function
The function this instruction belongs to.
void make_assumption(const exprt &g)
unsigned location_number
A globally unique number to identify a program location.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
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...
exprt guard
Guard for gotos, assume, assert.
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.
instructionst::const_iterator const_targett
const irept & get_nil_irep()
std::list< const_targett > const_targetst
goto_programt & operator=(const goto_programt &)=delete
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void make_assertion(const exprt &g)
bool is_start_thread() const
The Boolean constant true.
bool is_function_call() const
std::set< irep_idt > decl_identifierst
This class represents an instruction in the GOTO intermediate representation.
bool is_target() const
Is this node a branch target?
static const unsigned nil_target
Uniquely identify an invalid target or location.
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.
instructionst::iterator targett
instructiont(goto_program_instruction_typet _type)
std::size_t operator()(const goto_programt::const_targett t) const
Data structure for representing an arbitrary statement in a program.