Go to the documentation of this file.
27 if(statement==ID_block)
29 else if(statement==ID_label)
43 if(statement==ID_block)
45 else if(statement==ID_label)
60 if(statement==ID_block)
62 else if(statement==ID_label)
76 if(statement==ID_block)
78 else if(statement==ID_label)
91 for(
const auto &statement : extra_block.
statements())
105 if(statement==ID_block &&
110 else if(statement==ID_label)
126 for(
auto &op : result.statements())
129 result.add_source_location() = loc;
137 std::vector<irep_idt> result;
138 result.reserve(sub.size());
139 for(
const auto &s : sub)
140 result.push_back(s.get(ID_identifier));
145 const std::vector<irep_idt> ¶meter_identifiers)
148 sub.reserve(parameter_identifiers.size());
149 for(
const auto &
id : parameter_identifiers)
151 sub.push_back(
irept(ID_parameter));
152 sub.back().set(ID_identifier,
id);
157 std::vector<exprt> arguments,
159 :
codet{ID_input, std::move(arguments)}
162 add_source_location() = std::move(*location);
173 std::move(expression)},
181 vm, code.
operands().size() >= 2,
"input must have at least two operands");
185 std::vector<exprt> arguments,
187 :
codet{ID_output, std::move(arguments)}
190 add_source_location() = std::move(*location);
201 std::move(expression)},
209 vm, code.
operands().size() >= 2,
"output must have at least two operands");
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
void set_parameter_identifiers(const std::vector< irep_idt > &)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
codet representation of a for statement.
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
std::size_t size() const
Amount of nodes this expression tree contains.
irept & add(const irep_namet &name)
const irept & find(const irep_namet &name) const
A non-fatal assertion, which checks a condition then permits execution to continue.
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
The plus expression Associativity is not specified.
Base class for all expressions.
Expression to hold a symbol (variable)
bitvector_typet index_type()
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 codet & to_code(const exprt &expr)
code_operandst & statements()
A codet representing the declaration that an output of a particular description has a value which cor...
typet & type()
Return the type of the expression.
code_outputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
std::vector< irep_idt > get_parameter_identifiers() const
bool has_operands() const
Return true if there is at least one operand.
#define PRECONDITION(CONDITION)
An assumption, which must hold in subsequent code.
const code_labelt & to_code_label(const codet &code)
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
A side_effect_exprt that performs an assignment.
void add(const codet &code)
nonstd::optional< T > optionalt
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
const codet & body() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
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 code_blockt & to_code_block(const codet &code)
codet & find_last_statement()
Operator to return the address of an object.
source_locationt & add_source_location()
A codet representing an assignment in the program.
const irep_idt & get_statement() const
API to expression classes.
Data structure for representing an arbitrary statement in a program.