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)
39 if(operands.size()<=2)
45 exprt previous=operands.front();
48 for(exprt::operandst::const_iterator
49 it=++operands.begin();
74 for(
const auto &expr : designator)
78 if(expr.id() == ID_index_designator)
82 else if(expr.id() == ID_member_designator)
106 const typet &src_type = src.
type().
id() == ID_c_enum_tag
110 if(src_type.
id()==ID_bool)
114 src_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
123 return std::move(comparison);
128 if(src.
id() == ID_not)
140 const std::function<
bool(
const exprt &)> &pred)
149 src, [&](
const exprt &subexpr) {
return subexpr.
id() ==
id; });
154 const std::function<
bool(
const typet &)> &pred,
157 std::vector<std::reference_wrapper<const typet>> stack;
158 std::unordered_set<typet, irep_hash> visited;
160 const auto push_if_not_visited = [&](
const typet &t) {
161 if(visited.insert(t).second)
162 stack.emplace_back(t);
165 push_if_not_visited(type);
166 while(!stack.empty())
168 const typet &top = stack.back().
get();
173 else if(top.
id() == ID_c_enum_tag)
175 else if(top.
id() == ID_struct_tag)
177 else if(top.
id() == ID_union_tag)
179 else if(top.
id() == ID_struct || top.
id() == ID_union)
182 push_if_not_visited(comp.type());
187 push_if_not_visited(subtype);
197 type, [&](
const typet &subtype) {
return subtype.
id() ==
id; }, ns);
218 if(expr.
id()!=ID_typecast)
231 if(expr.
id() == ID_address_of)
236 expr.
id() == ID_typecast || expr.
id() == ID_array_of ||
237 expr.
id() == ID_plus || expr.
id() == ID_mult || expr.
id() == ID_array ||
238 expr.
id() == ID_with || expr.
id() == ID_struct || expr.
id() == ID_union ||
239 expr.
id() == ID_empty_union ||
241 expr.
id() == ID_byte_update_big_endian ||
242 expr.
id() == ID_byte_update_little_endian)
246 return is_constant(e);
256 if(expr.
id() == ID_symbol)
260 else if(expr.
id() == ID_index)
267 else if(expr.
id() == ID_member)
271 else if(expr.
id() == ID_dereference)
277 else if(expr.
id() == ID_string_constant)
296 if(b.
get(ID_value) == ID_false)
302 if(a.
get(ID_value) == ID_false)
311 return and_exprt{std::move(a), std::move(b)};
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.
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()
depth_iteratort depth_begin()
bool is_false() const
Return whether the expression is a constant representing false.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
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
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...
const componentst & components() const
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
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 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.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
API to expression classes.
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 index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_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)