Go to the documentation of this file.
28 if(statement==ID_block)
30 else if(statement==ID_label)
45 if(statement==ID_block)
47 else if(statement==ID_label)
62 if(statement==ID_block)
64 else if(statement==ID_label)
79 if(statement==ID_block)
81 else if(statement==ID_label)
94 for(
const auto &statement : extra_block.
statements())
108 if(statement==ID_block &&
113 else if(statement==ID_label)
129 for(
auto &op : result.statements())
132 result.add_source_location() = loc;
140 std::vector<irep_idt> result;
141 result.reserve(sub.size());
142 for(
const auto &s : sub)
143 result.push_back(s.get(ID_identifier));
148 const std::vector<irep_idt> ¶meter_identifiers)
151 sub.reserve(parameter_identifiers.size());
152 for(
const auto &
id : parameter_identifiers)
154 sub.push_back(
irept(ID_parameter));
155 sub.back().set(ID_identifier,
id);
160 std::vector<exprt> arguments,
162 :
codet{ID_input, std::move(arguments)}
165 add_source_location() = std::move(*location);
176 std::move(expression)},
184 vm, code.
operands().size() >= 2,
"input must have at least two operands");
188 std::vector<exprt> arguments,
190 :
codet{ID_output, std::move(arguments)}
193 add_source_location() = std::move(*location);
204 std::move(expression)},
212 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.
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)
API to expression classes for Pointers.
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.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.