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();
77 for(
const auto &expr : designator)
81 if(expr.id() == ID_index_designator)
85 else if(expr.id() == ID_member_designator)
109 const typet &src_type = src.
type().
id() == ID_c_enum_tag
113 if(src_type.
id()==ID_bool)
117 src_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
126 return std::move(comparison);
131 if(src.
id() == ID_not)
143 const std::function<
bool(
const exprt &)> &pred)
152 src, [&](
const exprt &subexpr) {
return subexpr.
id() ==
id; });
157 const std::function<
bool(
const typet &)> &pred,
160 std::vector<std::reference_wrapper<const typet>> stack;
161 std::unordered_set<typet, irep_hash> visited;
163 const auto push_if_not_visited = [&](
const typet &t) {
164 if(visited.insert(t).second)
165 stack.emplace_back(t);
168 push_if_not_visited(type);
169 while(!stack.empty())
171 const typet &top = stack.back().
get();
176 else if(top.
id() == ID_c_enum_tag)
178 else if(top.
id() == ID_struct_tag)
180 else if(top.
id() == ID_union_tag)
182 else if(top.
id() == ID_struct || top.
id() == ID_union)
185 push_if_not_visited(comp.type());
190 push_if_not_visited(subtype);
200 type, [&](
const typet &subtype) {
return subtype.
id() ==
id; }, ns);
221 if(expr.
id()!=ID_typecast)
232 expr.
id() == ID_symbol || expr.
id() == ID_nondet_symbol ||
233 expr.
id() == ID_side_effect)
238 if(expr.
id() == ID_address_of)
242 else if(
auto index = expr_try_dynamic_cast<index_exprt>(expr))
244 if(!
is_constant(index->array()) || !index->index().is_constant())
247 const auto &array_type =
to_array_type(index->array().type());
248 if(!array_type.size().is_constant())
256 return index_int >= 0 && index_int < size;
258 else if(
auto be = expr_try_dynamic_cast<byte_extract_exprt>(expr))
260 if(!
is_constant(be->op()) || !be->offset().is_constant())
264 if(!op_bits.has_value())
268 if(!extract_bits.has_value())
273 be->get_bits_per_byte();
275 return offset_bits >= 0 && offset_bits + *extract_bits <= *op_bits;
277 else if(
auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
280 !
is_constant(eb->src()) || !eb->lower().is_constant() ||
281 !eb->upper().is_constant())
287 if(!src_bits.has_value())
295 return lower_bound >= 0 && lower_bound <= upper_bound &&
296 upper_bound < src_bits;
303 return is_constant(e);
311 if(expr.
id() == ID_symbol)
315 else if(expr.
id() == ID_index)
322 else if(expr.
id() == ID_member)
326 else if(expr.
id() == ID_dereference)
332 else if(expr.
id() == ID_string_constant)
351 if(b.
get(ID_value) == ID_false)
357 if(a.
get(ID_value) == ID_false)
366 return and_exprt{std::move(a), std::move(b)};
371 if(expr.
type().
id() != ID_pointer)
384 "front-end should use ID_NULL");
API to expression classes for bitvectors.
Expression classes for byte-level operators.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_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".
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
bool value_is_zero_string() const
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()
source_locationt & add_source_location()
bool is_boolean() const
Return whether the expression represents a Boolean.
depth_iteratort depth_begin()
const source_locationt & source_location() const
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
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
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.
exprt::operandst & designator()
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
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
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const type_with_subtypest & to_type_with_subtypes(const typet &type)