22 return val.find_first_not_of(
'0')==std::string::npos;
27 if(
type().
id() != ID_pointer)
37 "front-end should use ID_NULL");
45 const auto value = expr.
get(ID_value);
50 "bitvector constant must have a non-empty value");
56 expr.
type().
id() == ID_verilog_unsignedbv ||
57 expr.
type().
id() == ID_verilog_signedbv ||
58 id2string(value).find_first_not_of(
"0123456789ABCDEF") ==
60 "negative bitvector constant must use two's complement");
65 expr.
type().
id() == ID_verilog_unsignedbv ||
66 expr.
type().
id() == ID_verilog_signedbv || value == ID_0 ||
68 "bitvector constant must not have leading zeros");
103 return and_exprt{std::move(a), std::move(b)};
110 else if(op.size()==1)
112 else if(op.size() == 2)
123 ->
decltype(struct_expr.op0())
126 std::is_base_of<struct_exprt, T>::value,
"T must be a struct_exprt.");
128 struct_expr.type().
id() == ID_struct_tag
133 index < struct_expr.operands().size(),
134 "component matching index should exist");
135 return struct_expr.operands()[index];
141 return ::component(*
this, name, ns);
148 return ::component(*
this, name, ns);
167 const typet &compound_type = member_expr.compound().type();
168 const auto *struct_union_type =
169 (compound_type.
id() == ID_struct_tag || compound_type.
id() == ID_union_tag)
174 struct_union_type !=
nullptr,
175 "member must address a struct, union or compatible type");
178 struct_union_type->get_component(member_expr.get_component_name());
183 "member component '" +
id2string(member_expr.get_component_name()) +
184 "' must exist on addressed type");
189 "member expression's type must match the addressed struct or union "
201 let_expr.values().size() == let_expr.variables().size(),
202 "number of variables must match number of values");
205 make_range(let_expr.variables()).zip(let_expr.values()))
209 binding.first.id() == ID_symbol,
210 "let binding symbols must be symbols");
215 "let bindings must be type consistent");
225 exprt *dest = &result;
227 for(
const auto &expr : designators)
231 if(expr.id() == ID_index_designator)
235 else if(expr.id() == ID_member_designator)
256 std::map<symbol_exprt, exprt> value_map;
258 for(std::size_t i = 0; i <
variables.size(); i++)
266 std::map<irep_idt, exprt> substitutions;
268 for(std::size_t i = 0; i <
variables.size(); i++)
269 substitutions[
variables[i].get_identifier()] = values[i];
274 if(substitute_result.has_value())
275 return substitute_result.value();
282 std::vector<exprt> values;
283 values.reserve(new_variables.size());
284 for(
const auto &new_variable : new_variables)
285 values.push_back(new_variable);
292 operands().size() % 2 == 0,
"cond must have even number of operands");
299 for(std::size_t i =
operands.size(); i != 0; i -= 2)
303 "since the number of operands is even if i is nonzero it must be "
312 result =
if_exprt{cond, value, std::move(result)};
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
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Base class for all expressions.
std::vector< exprt > operandst
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
The trinary if-then-else operator.
const exprt & index() const
const irep_idt & get(const irep_idt &name) const
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 union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
exprt & component(const irep_idt &name, const namespacet &ns)
Structure type, corresponds to C style structs.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
The Boolean constant true.
The type of an expression, extends irept.
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
exprt::operandst & designator()
Operator to update elements in structs and arrays.
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
const std::string & id2string(const irep_idt &d)
bool is_false(const literalt &l)
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 UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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())
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
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 index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
std::optional< 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,...