22#include <unordered_set>
42 if(operands.size()<=2)
48 exprt previous=operands.front();
51 for(exprt::operandst::const_iterator
52 it=++operands.begin();
60 tmp.operands().resize(2);
117 const std::function<
bool(
const exprt &)> &
pred)
131 const std::function<
bool(
const typet &)> &
pred,
134 std::vector<std::reference_wrapper<const typet>> stack;
135 std::unordered_set<typet, irep_hash> visited;
138 if(visited.insert(t).second)
139 stack.emplace_back(t);
143 while(!stack.empty())
145 const typet &top = stack.back().
get();
174 type, [&](
const typet &subtype) {
return subtype.
id() ==
id; }, ns);
218 if(!
is_constant(index->array()) || !index->index().is_constant())
247 be->get_bits_per_byte();
270 return lower_bound >= 0 && lower_bound <= upper_bound &&
278 return is_constant(e);
338 b.add_to_operands(std::move(
a));
API to expression classes for bitvectors.
Expression classes for byte-level operators.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
A constant literal expression.
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...
Operator to dereference a pointer.
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 is_true() const
Return whether the expression is a constant representing true.
depth_iteratort depth_end()
depth_iteratort depth_begin()
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
The Boolean constant false.
The trinary if-then-else operator.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
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...
The Boolean constant true.
The type of an expression, extends irept.
Operator to update elements in structs and arrays.
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Operator to update elements in structs and arrays.
Forward depth-first search iterators These iterators' copy operations are expensive,...
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
#define PRECONDITION(CONDITION)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_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 not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const type_with_subtypest & to_type_with_subtypes(const typet &type)