cprover
ci_lazy_methods_needed.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Context-insensitive lazy methods container
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
13 #define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
14 
15 #include <vector>
16 #include <set>
17 #include <unordered_set>
18 #include <util/symbol_table.h>
19 
21 class pointer_typet;
22 
24 {
25 public:
27  std::unordered_set<irep_idt> &_callable_methods,
28  std::unordered_set<irep_idt> &_instantiated_classes,
29  symbol_tablet &_symbol_table,
31  : callable_methods(_callable_methods),
32  instantiated_classes(_instantiated_classes),
33  symbol_table(_symbol_table),
35  {}
36 
37  void add_needed_method(const irep_idt &);
38  // Returns true if new
39  bool add_needed_class(const irep_idt &);
40 
42 
43 private:
44  // callable_methods is a vector because it's used as a work-list
45  // which is periodically cleared. It can't be relied upon to
46  // contain all methods that have previously been elaborated.
47  // It should be changed to a set if we develop the need to use
48  // it that way.
49  std::unordered_set<irep_idt> &callable_methods;
50  // instantiated_classes on the other hand is a true set of every class
51  // found so far, so we can use a membership test to avoid
52  // repeatedly exploring a class hierarchy.
53  std::unordered_set<irep_idt> &instantiated_classes;
55 
57 
60  const namespacet &ns);
61 
62  void gather_field_types(const typet &class_type, const namespacet &ns);
63 };
64 
65 #endif
The type of an expression.
Definition: type.h:22
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
const select_pointer_typet & pointer_type_selector
std::unordered_set< irep_idt > & instantiated_classes
The pointer type.
Definition: std_types.h:1435
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void add_needed_method(const irep_idt &)
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborat...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
void initialize_instantiated_classes_from_pointer(const pointer_typet &pointer_type, const namespacet &ns)
Build up list of methods for types for a specific pointer type.
void gather_field_types(const typet &class_type, const namespacet &ns)
For a given type, gather all fields referenced by that type.
bool add_needed_class(const irep_idt &)
Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accesse...
std::unordered_set< irep_idt > & callable_methods
void add_all_needed_classes(const pointer_typet &pointer_type)
Add to the needed classes all classes specified, the replacement type if it will be replaced...
ci_lazy_methods_neededt(std::unordered_set< irep_idt > &_callable_methods, std::unordered_set< irep_idt > &_instantiated_classes, symbol_tablet &_symbol_table, const select_pointer_typet &pointer_type_selector)