Go to the documentation of this file.
31 *
this =
codet(ID_block);
45 if(statement==ID_block)
47 else if(statement==ID_label)
61 if(statement==ID_block)
63 else if(statement==ID_label)
78 if(statement==ID_block)
80 else if(statement==ID_label)
94 if(statement==ID_block)
96 else if(statement==ID_label)
109 for(
const auto &statement : extra_block.
statements())
123 if(statement==ID_block &&
128 else if(statement==ID_label)
144 for(
auto &op : result.statements())
147 result.add_source_location() =
loc;
155 std::vector<irep_idt> result;
156 result.reserve(sub.size());
157 for(
const auto &s : sub)
158 result.push_back(s.get(ID_identifier));
163 const std::vector<irep_idt> ¶meter_identifiers)
166 sub.reserve(parameter_identifiers.size());
167 for(
const auto &
id : parameter_identifiers)
169 sub.push_back(
irept(ID_parameter));
170 sub.back().set(ID_identifier,
id);
175 std::vector<exprt> arguments,
177 :
codet{ID_input, std::move(arguments)}
180 add_source_location() = std::move(*location);
191 std::move(expression)},
199 vm, code.
operands().size() >= 2,
"input must have at least two operands");
203 std::vector<exprt> arguments,
205 :
codet{ID_output, std::move(arguments)}
208 add_source_location() = std::move(*location);
219 std::move(expression)},
227 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
codet(const irep_idt &statement)
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.
class code_blockt & make_block()
If this codet is a code_blockt (i.e. it represents a block of statements), return the unmodified inpu...
#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.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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
Data structure for representing an arbitrary statement in a program.