cprover
Loading...
Searching...
No Matches
ci_lazy_methods_neededt Class Reference

#include <ci_lazy_methods_needed.h>

Collaboration diagram for ci_lazy_methods_neededt:

Public Member Functions

 ci_lazy_methods_neededt (std::unordered_set< irep_idt > &_callable_methods, std::unordered_set< irep_idt > &_instantiated_classes, const symbol_table_baset &_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.
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.
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.

Private Member Functions

void add_clinit_call (const irep_idt &class_id)
 For a given class id, note that its static initializer is needed.
void add_cprover_nondet_initialize_if_it_exists (const irep_idt &class_id)
 For a given class id, if cproverNondetInitialize exists on it or any of its ancestors then note that it is needed.
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 struct_tag_typet &class_type, const namespacet &ns)
 For a given type, gather all fields referenced by that type.

Private Attributes

std::unordered_set< irep_idt > & callable_methods
std::unordered_set< irep_idt > & instantiated_classes
const symbol_table_baset & symbol_table
const select_pointer_typet & pointer_type_selector

Detailed Description

Definition at line 25 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,
const symbol_table_baset & _symbol_table,
const select_pointer_typet & pointer_type_selector )
inline

Definition at line 28 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 94 of file ci_lazy_methods_needed.cpp.

◆ add_clinit_call()

void ci_lazy_methods_neededt::add_clinit_call ( const irep_idt & class_id)
private

For a given class id, note that its static initializer is needed.

This applies the same logic to the given class that java_bytecode_convert_methodt::get_clinit_call applies e.g. to classes whose constructor we call in a method body. This duplication is unavoidable because ci_lazy_methods essentially has to go through the same logic as __CPROVER_start in its initial setup, and because return values of opaque methods need to be considered in ci_lazy_methods too.

Parameters
class_idThe given class id

Definition at line 42 of file ci_lazy_methods_needed.cpp.

◆ add_cprover_nondet_initialize_if_it_exists()

void ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists ( const irep_idt & class_id)
private

For a given class id, if cproverNondetInitialize exists on it or any of its ancestors then note that it is needed.

Parameters
class_idThe given class id

Definition at line 52 of file ci_lazy_methods_needed.cpp.

◆ 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_nameclass name; must exist in symbol table.
Returns
Returns true if class_symbol_name is new (not seen before).

Definition at line 72 of file ci_lazy_methods_needed.cpp.

◆ 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_namemethod name; must exist in symbol table.

Definition at line 28 of file ci_lazy_methods_needed.cpp.

◆ gather_field_types()

void ci_lazy_methods_neededt::gather_field_types ( const struct_tag_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 147 of file ci_lazy_methods_needed.cpp.

◆ 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 116 of file ci_lazy_methods_needed.cpp.

Member Data Documentation

◆ callable_methods

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

Definition at line 51 of file ci_lazy_methods_needed.h.

◆ instantiated_classes

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

Definition at line 55 of file ci_lazy_methods_needed.h.

◆ pointer_type_selector

const select_pointer_typet& ci_lazy_methods_neededt::pointer_type_selector
private

Definition at line 58 of file ci_lazy_methods_needed.h.

◆ symbol_table

const symbol_table_baset& ci_lazy_methods_neededt::symbol_table
private

Definition at line 56 of file ci_lazy_methods_needed.h.

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