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 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 & 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...
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 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.
#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)