22 std::vector<exprt> arguments,
24 :
codet{ID_input,
std::move(arguments)}
28 check(*
this, validation_modet::INVARIANT);
38 std::move(expression)},
46 vm, code.
operands().size() >= 2,
"input must have at least two operands");
50 std::vector<exprt> arguments,
52 :
codet{ID_output,
std::move(arguments)}
56 check(*
this, validation_modet::INVARIANT);
66 std::move(expression)},
74 vm, code.
operands().size() >= 2,
"output must have at least two operands");
84 std::move(arguments)};
bitvector_typet c_index_type()
Operator to return the address of an object.
codet representation of a function call statement.
exprt::operandst argumentst
A codet representing the declaration that an output of a particular description has a value which cor...
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_outputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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).
nonstd::optional< T > optionalt
API to expression classes.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...