28 *
this =
codet(ID_block);
42 if(statement==ID_block)
44 else if(statement==ID_label)
58 if(statement==ID_block)
60 else if(statement==ID_label)
75 if(statement==ID_block)
77 else if(statement==ID_label)
91 if(statement==ID_block)
93 else if(statement==ID_label)
106 for(
const auto &statement : extra_block.
statements())
120 if(statement==ID_block &&
125 else if(statement==ID_label)
141 for(
auto &op : result.statements())
144 result.add_source_location() =
loc;
const irep_idt & get_statement() const
codet & find_last_statement()
code_operandst & statements()
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them...
void add(const codet &code)
class code_blockt & make_block()
If this codet is a code_blockt (i.e. it represents a block of statements), return the unmodified inpu...
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them...
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &loc)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
API to expression classes.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool has_operands() const
Return true if there is at least one operand.
A non-fatal assertion, which checks a condition then permits execution to continue.
An assumption, which must hold in subsequent code.
Base class for all expressions.
source_locationt & add_source_location()
A codet representing sequential composition of program statements.
const codet & to_code(const exprt &expr)
const code_blockt & to_code_block(const codet &code)
Data structure for representing an arbitrary statement in a program.
const code_labelt & to_code_label(const codet &code)