21 return val.find_first_not_of(
'0')==std::string::npos;
27 vm, !expr.
has_operands(),
"constant expression must not have operands");
33 "bitvector constant must have a non-empty value");
41 "negative bitvector constant must use two's complement");
48 "bitvector constant must not have leading zeros");
81 std::is_base_of<struct_exprt, T>::value,
"T must be a struct_exprt.");
86 "component matching index should exist");
93 return ::component(*
this, name, ns);
100 return ::component(*
this, name, ns);
125 "member must address a struct, union or compatible type");
134 "' must exist on addressed type");
139 "member expression's type must match the addressed struct or union "
152 "number of variables must match number of values");
160 "let binding symbols must be symbols");
165 "let bindings must be type consistent");
175 std::map<symbol_exprt, exprt> value_map;
177 for(std::size_t i = 0; i <
variables.size(); i++)
187 for(std::size_t i = 0; i <
variables.size(); i++)
201 std::vector<exprt> values;
202 values.reserve(new_variables.size());
203 for(
const auto &new_variable : new_variables)
204 values.push_back(new_variable);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
std::vector< symbol_exprt > variablest
const irep_idt & get_value() const
bool value_is_zero_string() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
typet & type()
Return the type of the expression.
The Boolean constant false.
const irep_idt & id() const
static void validate(const exprt &, validation_modet)
binding_exprt & binding()
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
exprt & component(const irep_idt &name, const namespacet &ns)
The Boolean constant true.
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
optionalt< exprt > substitute_symbols(const std::map< irep_idt, exprt > &substitutions, exprt src)
Substitute free occurrences of the variables given by their identifiers in the keys of the map in the...
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...