cprover
ci_lazy_methods_neededt Class Reference

#include <ci_lazy_methods_needed.h>

Collaboration diagram for ci_lazy_methods_neededt:
[legend]

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_tabletsymbol_table
 
const select_pointer_typetpointer_type_selector
 

Detailed Description

Definition at line 23 of file ci_lazy_methods_needed.h.

Constructor & Destructor Documentation

◆ ci_lazy_methods_neededt()

ci_lazy_methods_neededt::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 
)
inline

Definition at line 26 of file ci_lazy_methods_needed.h.

Member Function Documentation

◆ add_all_needed_classes()

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.

Parameters
pointer_typeThe 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().

◆ add_needed_class()

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.

Parameters
class_symbol_name: class name; must exist in symbol table.
Returns
Returns true if 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().

◆ add_needed_method()

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.

Parameters
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().

◆ gather_field_types()

void ci_lazy_methods_neededt::gather_field_types ( const typet class_type,
const namespacet ns 
)
private

For a given type, gather all fields referenced by that type.

Parameters
class_typeroot of class tree to search
nsglobal 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().

◆ initialize_instantiated_classes_from_pointer()

void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer ( const pointer_typet pointer_type,
const namespacet ns 
)
private

Build up list of methods for types for a specific pointer type.

See add_all_needed_classes for more details.

Parameters
pointer_typeThe type to gather methods for.
nsglobal 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().

Member Data Documentation

◆ callable_methods

std::unordered_set<irep_idt>& ci_lazy_methods_neededt::callable_methods
private

Definition at line 49 of file ci_lazy_methods_needed.h.

Referenced by add_needed_method().

◆ instantiated_classes

std::unordered_set<irep_idt>& ci_lazy_methods_neededt::instantiated_classes
private

Definition at line 53 of file ci_lazy_methods_needed.h.

Referenced by add_needed_class().

◆ pointer_type_selector

const select_pointer_typet& ci_lazy_methods_neededt::pointer_type_selector
private

Definition at line 56 of file ci_lazy_methods_needed.h.

Referenced by add_all_needed_classes().

◆ symbol_table

symbol_tablet& ci_lazy_methods_neededt::symbol_table
private

Definition at line 54 of file ci_lazy_methods_needed.h.

Referenced by add_all_needed_classes(), and add_needed_class().


The documentation for this class was generated from the following files: