cprover
|
#include <ci_lazy_methods_needed.h>
Public Member Functions | |
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) | |
void | add_needed_method (const irep_idt &) |
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborated. More... | |
bool | add_needed_class (const irep_idt &) |
Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accessed. More... | |
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, and all fields it contains. More... | |
Private Member Functions | |
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. More... | |
void | gather_field_types (const typet &class_type, const namespacet &ns) |
For a given type, gather all fields referenced by that type. More... | |
Private Attributes | |
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 |
Definition at line 23 of file ci_lazy_methods_needed.h.
|
inline |
Definition at line 26 of file ci_lazy_methods_needed.h.
void ci_lazy_methods_neededt::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, and all fields it contains.
pointer_type | The type to add |
Definition at line 51 of file ci_lazy_methods_needed.cpp.
References select_pointer_typet::convert_pointer_type(), initialize_instantiated_classes_from_pointer(), pointer_type(), pointer_type_selector, and symbol_table.
Referenced by gather_field_types(), and ci_lazy_methodst::initialize_instantiated_classes().
bool ci_lazy_methods_neededt::add_needed_class | ( | const irep_idt & | class_symbol_name | ) |
Notes class class_symbol_name
will be instantiated, or a static field belonging to it will be accessed.
Also notes that its static initializer is therefore reachable.
class_symbol_name : class name; must exist in symbol table. |
class_symbol_name
is new (not seen before). Definition at line 33 of file ci_lazy_methods_needed.cpp.
References add_needed_method(), id2string(), instantiated_classes, symbol_table, and symbol_table_baset::symbols.
Referenced by ci_lazy_methodst::initialize_instantiated_classes(), and initialize_instantiated_classes_from_pointer().
void ci_lazy_methods_neededt::add_needed_method | ( | const irep_idt & | method_symbol_name | ) |
Notes method_symbol_name
is referenced from some reachable function, and should therefore be elaborated.
method_symbol_name : method name; must exist in symbol table. |
Definition at line 22 of file ci_lazy_methods_needed.cpp.
References callable_methods.
Referenced by add_needed_class().
|
private |
For a given type, gather all fields referenced by that type.
class_type | root of class tree to search |
ns | global namespaces. |
Definition at line 106 of file ci_lazy_methods_needed.cpp.
References add_all_needed_classes(), namespace_baset::follow(), irept::id(), INVARIANT, is_java_array_tag(), java_array_element_type(), to_pointer_type(), to_struct_type(), and to_symbol_type().
Referenced by initialize_instantiated_classes_from_pointer().
|
private |
Build up list of methods for types for a specific pointer type.
See add_all_needed_classes
for more details.
pointer_type | The type to gather methods for. |
ns | global namespace |
Definition at line 73 of file ci_lazy_methods_needed.cpp.
References add_needed_class(), gather_field_types(), java_generic_typet::generic_type_arguments(), symbol_typet::get_identifier(), is_java_array_tag(), is_java_generic_parameter(), is_java_generic_type(), pointer_type(), typet::subtype(), to_java_generic_type(), and to_symbol_type().
Referenced by add_all_needed_classes().
|
private |
Definition at line 49 of file ci_lazy_methods_needed.h.
Referenced by add_needed_method().
|
private |
Definition at line 53 of file ci_lazy_methods_needed.h.
Referenced by add_needed_class().
|
private |
Definition at line 56 of file ci_lazy_methods_needed.h.
Referenced by add_all_needed_classes().
|
private |
Definition at line 54 of file ci_lazy_methods_needed.h.
Referenced by add_all_needed_classes(), and add_needed_class().