12 #include <unordered_set> 24 if(expr.
id() == ID_index)
26 else if(expr.
id() == ID_member)
28 else if(expr.
id() == ID_dereference)
30 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();
57 tmp.operands().resize(2);
58 tmp.op0().swap(previous);
78 if(it->id()==ID_index_designator)
82 else if(it->id()==ID_member_designator)
106 const typet &src_type=
107 src.
type().
id()==ID_c_enum_tag?
111 if(src_type.
id()==ID_bool)
115 src_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
128 if(src.
id()==ID_not && src.
operands().size()==1)
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())
173 else if(top.
id() == ID_symbol)
174 push_if_not_visited(ns.
follow(top));
175 else if(top.
id() == ID_c_enum_tag)
177 else if(top.
id() == ID_struct || top.
id() == ID_union)
180 push_if_not_visited(comp.type());
184 for(
const auto &subtype : top.
subtypes())
185 push_if_not_visited(subtype);
195 type, [&](
const typet &subtype) {
return subtype.
id() == id; }, ns);
204 const exprt true_case=if_expr.true_case();
205 const exprt false_case=if_expr.false_case();
208 result.
cond()=if_expr.cond();
220 if(expr.
id()!=ID_typecast)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
Operator to update elements in structs and arrays.
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.
#define forall_expr(it, expr)
exprt::operandst & designator()
const componentst & components() const
The trinary if-then-else operator.
depth_iteratort depth_begin()
#define CHECK_RETURN(CONDITION)
const typet & follow_tag(const union_tag_typet &) const
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
const exprt & compound() const
const irep_idt & id() const
The boolean constant true.
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
A generic base class for 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
API to expression classes.
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const typet & follow(const typet &) const
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
const exprt & index() const
The boolean constant false.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
std::vector< exprt > operandst
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Base class for all expressions.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Operator to update elements in structs and arrays.
const source_locationt & source_location() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
depth_iteratort depth_end()
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions