35 switch(instruction.
type())
41 for(
const auto &target : instruction.
targets)
51 for(
const auto &target : instruction.
targets)
81 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
bool is_true() const
Return whether the expression is a constant representing true.
This class represents an instruction in the GOTO intermediate representation.
const exprt & condition() const
Get the condition of gotos, assume, assert.
targetst targets
The list of successor instructions.
goto_program_instruction_typet type() const
What kind of instruction?
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
goto_programt::const_targett t
void build(const goto_programt &goto_program)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...