#include <java_static_initializers.h>

Collaboration diagram for stub_global_initializer_factoryt:

Public Member Functions
void	create_stub_global_initializer_symbols (symbol_table_baset &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, synthetic_methods_mapt &synthetic_methods)
	Create static initializer symbols for each distinct class that has stub globals. More...

code_blockt	get_stub_initializer_body (const irep_idt &function_id, symbol_table_baset &symbol_table, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
	Create the body of a synthetic static initializer (clinit method), which initialise stub globals in the same manner as java_static_lifetime_init, only delayed until first reference by virtue of being given in a static initializer rather than directly in __CPROVER_initialize. More...

Private Types
typedef std::unordered_multimap< irep_idt, irep_idt >	stub_globals_by_classt
	Maps class symbols onto the stub globals that belong to them. More...

Private Attributes
stub_globals_by_classt	stub_globals_by_class

Detailed Description

Definition at line 95 of file java_static_initializers.h.

Member Typedef Documentation

◆ stub_globals_by_classt

typedef std::unordered_multimap<irep_idt, irep_idt> stub_global_initializer_factoryt::stub_globals_by_classt

private

Maps class symbols onto the stub globals that belong to them.

Definition at line 98 of file java_static_initializers.h.

Member Function Documentation

◆ create_stub_global_initializer_symbols()

void stub_global_initializer_factoryt::create_stub_global_initializer_symbols	(	symbol_table_baset &	symbol_table,
		const std::unordered_set< irep_idt > &	stub_globals_set,
		synthetic_methods_mapt &	synthetic_methods
	)

Create static initializer symbols for each distinct class that has stub globals.

Parameters

symbol_table	global symbol table. Will gain static initializer method symbols for each class that has a stub global in `stub_globals_set`
stub_globals_set	set of stub global symbols
synthetic_methods	map of synthetic method types. We record the new static initialiser such that we get a callback to provide its body as and when it is required.

Definition at line 925 of file java_static_initializers.cpp.

◆ get_stub_initializer_body()

code_blockt stub_global_initializer_factoryt::get_stub_initializer_body	(	const irep_idt &	function_id,
		symbol_table_baset &	symbol_table,
		const java_object_factory_parameterst &	object_factory_parameters,
		const select_pointer_typet &	pointer_type_selector,
		message_handlert &	message_handler
	)

Create the body of a synthetic static initializer (clinit method), which initialise stub globals in the same manner as java_static_lifetime_init, only delayed until first reference by virtue of being given in a static initializer rather than directly in __CPROVER_initialize.

Parameters

function_id	synthetic static initializer id
symbol_table	global symbol table; may gain local variables created for the new static initializer
object_factory_parameters	object factory parameters used to populate the stub globals and objects reachable from them
pointer_type_selector	used to choose concrete types for abstract- typed globals and fields.
message_handler	log output

Returns: synthetic static initializer body.

Definition at line 1002 of file java_static_initializers.cpp.

Member Data Documentation

◆ stub_globals_by_class

stub_globals_by_classt stub_global_initializer_factoryt::stub_globals_by_class

private

Definition at line 99 of file java_static_initializers.h.

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

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

Public Member Functions

Private Types

Private Attributes