#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. 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	add_clinit_call (const irep_idt &class_id)
	For a given class id, note that its static initializer is needed. More...

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. More...

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 struct_tag_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

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_type The 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_id The 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_id The 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_name class 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_name method 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_type	root of class tree to search
ns	global 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_type	The type to gather methods for.
ns	global 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:

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/ci_lazy_methods_needed.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ ci_lazy_methods_neededt()

Member Function Documentation

◆ add_all_needed_classes()

◆ add_clinit_call()

◆ add_cprover_nondet_initialize_if_it_exists()

◆ add_needed_class()

◆ add_needed_method()

◆ gather_field_types()

◆ initialize_instantiated_classes_from_pointer()

Member Data Documentation

◆ callable_methods

◆ instantiated_classes

◆ pointer_type_selector

◆ symbol_table