12 #include <unordered_set>
23 if(expr.
id() == ID_index)
25 else if(expr.
id() == ID_member)
27 else if(expr.
id() == ID_dereference)
29 else if(expr.
id() == ID_symbol)
38 if(operands.size()<=2)
44 exprt previous=operands.front();
47 for(exprt::operandst::const_iterator
48 it=++operands.begin();
73 for(
const auto &expr : designator)
77 if(expr.id() == ID_index_designator)
81 else if(expr.id() == ID_member_designator)
105 const typet &src_type = src.
type().
id() == ID_c_enum_tag
109 if(src_type.
id()==ID_bool)
113 src_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
122 return std::move(comparison);
127 if(src.
id() == ID_not)
139 const std::function<
bool(
const exprt &)> &pred)
148 src, [&](
const exprt &subexpr) {
return subexpr.
id() ==
id; });
153 const std::function<
bool(
const typet &)> &pred,
156 std::vector<std::reference_wrapper<const typet>> stack;
157 std::unordered_set<typet, irep_hash> visited;
159 const auto push_if_not_visited = [&](
const typet &t) {
160 if(visited.insert(t).second)
161 stack.emplace_back(t);
164 push_if_not_visited(type);
165 while(!stack.empty())
167 const typet &top = stack.back().
get();
172 else if(top.
id() == ID_c_enum_tag)
174 else if(top.
id() == ID_struct_tag)
176 else if(top.
id() == ID_union_tag)
178 else if(top.
id() == ID_struct || top.
id() == ID_union)
181 push_if_not_visited(comp.type());
186 push_if_not_visited(subtype);
196 type, [&](
const typet &subtype) {
return subtype.
id() ==
id; }, ns);
217 if(expr.
id()!=ID_typecast)
230 if(expr.
id() == ID_address_of)
235 expr.
id() == ID_typecast || expr.
id() == ID_array_of ||
236 expr.
id() == ID_plus || expr.
id() == ID_mult || expr.
id() == ID_array ||
237 expr.
id() == ID_with || expr.
id() == ID_struct || expr.
id() == ID_union ||
239 expr.
id() == ID_byte_update_big_endian ||
240 expr.
id() == ID_byte_update_little_endian)
244 return is_constant(e);
254 if(expr.
id() == ID_symbol)
258 else if(expr.
id() == ID_index)
265 else if(expr.
id() == ID_member)
269 else if(expr.
id() == ID_dereference)
275 else if(expr.
id() == ID_string_constant)
294 if(b.
get(ID_value) == ID_false)
300 if(a.
get(ID_value) == ID_false)
309 return and_exprt{std::move(a), std::move(b)};
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.
A constant literal expression.
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()
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 & id() const
const irep_idt & get(const irep_namet &name) const
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
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
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 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
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
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.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
API to expression classes.
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 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 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)