23 std::vector<exprt> arguments,
24 std::optional<source_locationt> location)
25 :
codet{ID_input,
std::move(arguments)}
35 std::optional<source_locationt> location)
40 std::move(expression)},
48 vm, code.
operands().size() >= 2,
"input must have at least two operands");
52 std::vector<exprt> arguments,
53 std::optional<source_locationt> location)
54 :
codet{ID_output,
std::move(arguments)}
64 std::optional<source_locationt> location)
69 std::move(expression)},
77 vm, code.
operands().size() >= 2,
"output must have at least two operands");
87 std::move(arguments)};
bitvector_typet c_index_type()
Operator to return the address of an object.
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
code_outputt(std::vector< exprt > arguments, std::optional< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
static void check(const goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
codet(const irep_idt &statement)
Base class for all expressions.
source_locationt & add_source_location()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
code_function_callt havoc_slice_call(const exprt &p, const exprt &size, const namespacet &ns)
Builds a code_function_callt to __CPROVER_havoc_slice(p, size).
API to expression classes.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...