CBMC
find_symbols.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_FIND_SYMBOLS_H
11 #define CPROVER_UTIL_FIND_SYMBOLS_H
12 
13 #include "irep.h"
14 
15 #include <set>
16 #include <unordered_set>
17 
18 class exprt;
19 class symbol_exprt; // IWYU pragma: keep
20 class typet;
21 
22 typedef std::unordered_set<irep_idt> find_symbols_sett;
23 
27 bool has_symbol_expr(
28  const exprt &src,
29  const irep_idt &identifier,
30  bool include_bound_symbols);
31 
34 void find_symbols(const exprt &src, find_symbols_sett &dest);
35 
38 void find_symbols(
39  const exprt &src,
40  std::set<symbol_exprt> &dest);
41 
44 inline std::set<symbol_exprt> find_symbols(const exprt &src)
45 {
46  std::set<symbol_exprt> syms;
47  find_symbols(src, syms);
48  return syms;
49 }
50 
53 inline find_symbols_sett find_symbol_identifiers(const exprt &src)
54 {
55  find_symbols_sett identifiers;
56  find_symbols(src, identifiers);
57  return identifiers;
58 }
59 
61 void find_type_symbols(
62  const typet &src,
63  find_symbols_sett &dest);
64 
66 void find_type_symbols(
67  const exprt &src,
68  find_symbols_sett &dest);
69 
72 void find_non_pointer_type_symbols(
73  const typet &src,
74  find_symbols_sett &dest);
75 
78 void find_non_pointer_type_symbols(
79  const exprt &src,
80  find_symbols_sett &dest);
81 
85 void find_type_and_expr_symbols(
86  const typet &src,
87  find_symbols_sett &dest,
88  const std::vector<irep_idt> &subs_to_find = {});
89 
93 void find_type_and_expr_symbols(
94  const exprt &src,
95  find_symbols_sett &dest,
96  const std::vector<irep_idt> &subs_to_find = {});
97 
98 #endif // CPROVER_UTIL_FIND_SYMBOLS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
exprt
Base class for all expressions.
Definition: expr.h:56
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:131
typet
The type of an expression, extends irept.
Definition: type.h:29
find_symbol_identifiers
find_symbols_sett find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables.
Definition: find_symbols.h:53
find_type_and_expr_symbols
void find_type_and_expr_symbols(const typet &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...
Definition: find_symbols.cpp:333
find_non_pointer_type_symbols
void find_non_pointer_type_symbols(const typet &src, find_symbols_sett &dest)
Collect type tags contained in src when the expression of such a type is not a pointer,...
Definition: find_symbols.cpp:307
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
has_symbol_expr
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...
Definition: find_symbols.cpp:267
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol, for both free and bound variables.
Definition: find_symbols.cpp:348
find_type_symbols
void find_type_symbols(const typet &src, find_symbols_sett &dest)
Collect all type tags contained in src and add them to dest.
Definition: find_symbols.cpp:288