22#include <unordered_set>
26 if(expr.
id() == ID_index)
28 else if(expr.
id() == ID_member)
30 else if(expr.
id() == ID_dereference)
32 else if(expr.
id() == ID_symbol)
42 if(operands.size()<=2)
48 exprt previous=operands.front();
51 for(exprt::operandst::const_iterator
52 it=++operands.begin();
83 const typet &src_type = src.
type().
id() == ID_c_enum_tag
87 if(src_type.
id()==ID_bool)
91 src_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
100 return std::move(comparison);
105 if(src.
id() == ID_not)
117 const std::function<
bool(
const exprt &)> &pred)
126 src, [&](
const exprt &subexpr) {
return subexpr.
id() == id; });
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;
137 const auto push_if_not_visited = [&](
const typet &t) {
138 if(visited.insert(t).second)
139 stack.emplace_back(t);
142 push_if_not_visited(type);
143 while(!stack.empty())
145 const typet &top = stack.back().get();
150 else if(top.
id() == ID_c_enum_tag)
152 else if(top.
id() == ID_struct_tag)
154 else if(top.
id() == ID_union_tag)
156 else if(top.
id() == ID_struct || top.
id() == ID_union)
159 push_if_not_visited(comp.type());
164 push_if_not_visited(subtype);
174 type, [&](
const typet &subtype) {
return subtype.
id() == id; }, ns);
195 if(expr.
id()!=ID_typecast)
206 expr.
id() == ID_symbol || expr.
id() == ID_nondet_symbol ||
207 expr.
id() == ID_side_effect)
212 if(expr.
id() == ID_address_of)
218 if(!
is_constant(index->array()) || !index->index().is_constant())
221 const auto &array_type =
to_array_type(index->array().type());
222 if(!array_type.size().is_constant())
230 return index_int >= 0 && index_int < size;
234 if(!
is_constant(be->op()) || !be->offset().is_constant())
238 if(!op_bits.has_value())
242 if(!extract_bits.has_value())
247 be->get_bits_per_byte();
249 return offset_bits >= 0 && offset_bits + *extract_bits <= *op_bits;
253 if(!
is_constant(eb->src()) || !eb->index().is_constant())
259 if(!eb_bits.has_value())
263 if(!src_bits.has_value())
268 const mp_integer upper_bound = lower_bound + eb_bits.value() - 1;
270 return lower_bound >= 0 && lower_bound <= upper_bound &&
271 upper_bound < src_bits.value();
278 return is_constant(e);
286 if(expr.
id() == ID_symbol)
290 else if(expr.
id() == ID_index)
297 else if(expr.
id() == ID_member)
301 else if(expr.
id() == ID_dereference)
307 else if(expr.
id() == ID_string_constant)
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.
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.
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
source_locationt & add_source_location()
The Boolean constant false.
The trinary if-then-else operator.
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.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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)
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
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)