24 if(statement==ID_block)
26 else if(statement==ID_label)
41 if(statement==ID_block)
43 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)
90 for(
const auto &statement : extra_block.
statements())
104 if(statement==ID_block &&
109 else if(statement==ID_label)
125 for(
auto &op : result.statements())
128 result.add_source_location() = loc;
136 std::vector<irep_idt> result;
137 result.reserve(sub.size());
138 for(
const auto &s : sub)
139 result.push_back(s.get(ID_identifier));
144 const std::vector<irep_idt> ¶meter_identifiers)
147 sub.reserve(parameter_identifiers.size());
148 for(
const auto &
id : parameter_identifiers)
150 sub.push_back(
irept(ID_parameter));
151 sub.back().set(ID_identifier,
id);
A base class for relations, i.e., binary predicates whose two operands have the same type.
A non-fatal assertion, which checks a condition then permits execution to continue.
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
void add(const codet &code)
code_operandst & statements()
codet & find_last_statement()
codet representation of a for statement.
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
const codet & body() const
A codet representing an assignment in the program.
std::vector< irep_idt > get_parameter_identifiers() const
void set_parameter_identifiers(const std::vector< irep_idt > &)
Data structure for representing an arbitrary statement in a program.
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool has_operands() const
Return true if there is at least one operand.
source_locationt & add_source_location()
typet & type()
Return the type of the expression.
const irept & find(const irep_idt &name) const
irept & add(const irep_idt &name)
The plus expression Associativity is not specified.
A side_effect_exprt that performs an assignment.
Expression to hold a symbol (variable)
#define PRECONDITION(CONDITION)
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.
const code_labelt & to_code_label(const codet &code)
const code_blockt & to_code_block(const codet &code)
const codet & to_code(const exprt &expr)