37 std::unordered_set<irep_idt> &bindings,
38 const std::vector<irep_idt> &subs_to_find);
44 std::unordered_set<irep_idt> &bindings,
45 const std::vector<irep_idt> &subs_to_find)
49 if(src.
id() == ID_forall || src.
id() == ID_exists || src.
id() == ID_lambda)
52 std::unordered_set<irep_idt> new_bindings{bindings};
53 for(
const auto &v : binding_expr.variables())
54 new_bindings.insert(v.get_identifier());
57 kind, binding_expr.where(), op, new_bindings, subs_to_find))
61 kind, binding_expr.type(), op, bindings, subs_to_find);
63 else if(src.
id() == ID_let)
66 std::unordered_set<irep_idt> new_bindings{bindings};
67 for(
const auto &v : let_expr.variables())
68 new_bindings.insert(v.get_identifier());
70 if(!
find_symbols(kind, let_expr.where(), op, new_bindings, subs_to_find))
73 if(!
find_symbols(kind, let_expr.op1(), op, new_bindings, subs_to_find))
76 return find_symbols(kind, let_expr.type(), op, bindings, subs_to_find);
80 for(
const auto &src_op : src.
operands())
82 if(!
find_symbols(kind, src_op, op, bindings, subs_to_find))
88 for(
const auto &sub_to_find : subs_to_find)
90 auto sub_expr =
static_cast<const exprt &
>(src.
find(sub_to_find));
91 if(sub_expr.is_not_nil())
93 for(
const auto &sub_op : sub_expr.operands())
95 if(!
find_symbols(kind, sub_op, op, bindings, subs_to_find))
104 if(src.
id() == ID_symbol)
120 const irept &c_sizeof_type = src.
find(ID_C_c_sizeof_type);
125 static_cast<const typet &
>(c_sizeof_type),
133 const irept &va_arg_type=src.
find(ID_C_va_arg_type);
138 static_cast<const typet &
>(va_arg_type),
156 std::unordered_set<irep_idt> &bindings,
157 const std::vector<irep_idt> &subs_to_find)
171 if(!
find_symbols(kind, subtype, op, bindings, subs_to_find))
179 const irep_idt &typedef_name = src.
get(ID_C_typedef);
185 if(src.
id()==ID_struct ||
190 for(
const auto &c : struct_union_type.
components())
196 else if(src.
id()==ID_code)
208 else if(src.
id()==ID_array)
212 kind,
to_array_type(src).size(), op, bindings, subs_to_find))
219 if(src.
id() == ID_c_enum_tag)
224 else if(src.
id() == ID_struct_tag)
229 else if(src.
id() == ID_union_tag)
243 const std::vector<irep_idt> &subs_to_find = {})
245 std::unordered_set<irep_idt> bindings;
246 return find_symbols(kind, type, op, bindings, subs_to_find);
253 const std::vector<irep_idt> &subs_to_find = {})
255 std::unordered_set<irep_idt> bindings;
256 return find_symbols(kind, src, op, bindings, subs_to_find);
270 bool include_bound_symbols)
321 const std::vector<irep_idt> &subs_to_find)
336 const std::vector<irep_idt> &subs_to_find)
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.
const typet & return_type() const
const parameterst & parameters() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
Base type for structs and unions.
const componentst & components() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const irep_idt & get_identifier() const
The type of an expression, extends irept.
symbol_kindt
Kinds of symbols to be considered by find_symbols.
@ F_TYPE_NON_PTR
Struct, union, or enum tag symbols when the expression using them is not a pointer.
@ F_TYPE
Struct, union, or enum tag symbols.
@ F_EXPR_FREE
Symbol expressions, but excluding bound variables.
@ F_EXPR
Symbol expressions.
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
Collect type tags contained in src when the expression of such a type is not a pointer,...
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
Collect all type tags contained in src and add them to dest.
bool has_symbol_expr(const exprt &src, const irep_idt &identifier, bool include_bound_symbols)
Returns true if one of the symbol expressions in src has identifier identifier; if include_bound_symb...
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
std::unordered_set< irep_idt > find_symbols_sett
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
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)
const type_with_subtypet & to_type_with_subtype(const typet &type)