cprover
|
#include <java_static_initializers.h>
Public Member Functions | |
void | create_stub_global_initializer_symbols (symbol_tablet &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... | |
codet | get_stub_initializer_body (const irep_idt &function_id, symbol_table_baset &symbol_table, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) |
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 |
Definition at line 38 of file java_static_initializers.h.
|
private |
Maps class symbols onto the stub globals that belong to them.
Definition at line 41 of file java_static_initializers.h.
void stub_global_initializer_factoryt::create_stub_global_initializer_symbols | ( | symbol_tablet & | 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.
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 672 of file java_static_initializers.cpp.
References symbol_table_baset::add(), advance_to_next_key(), clinit_function_name(), dstringt::empty(), irept::get(), irept::get_bool(), symbol_table_baset::has_symbol(), INVARIANT, irept::is_nil(), symbol_table_baset::lookup_ref(), symbolt::name, STUB_CLASS_STATIC_INITIALIZER, stub_globals_by_class, symbolt::type, and symbolt::value.
Referenced by java_bytecode_languaget::typecheck().
codet stub_global_initializer_factoryt::get_stub_initializer_body | ( | const irep_idt & | function_id, |
symbol_table_baset & | symbol_table, | ||
const object_factory_parameterst & | object_factory_parameters, | ||
const select_pointer_typet & | pointer_type_selector | ||
) |
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.
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. |
Definition at line 756 of file java_static_initializers.cpp.
References DYNAMIC, dstringt::empty(), object_factory_parameterst::function_id, gen_nondet_init(), irept::get(), INVARIANT, is_non_null_library_global(), symbol_table_baset::lookup_ref(), object_factory_parameterst::max_nonnull_tree_depth, NO_UPDATE_IN_PLACE, source_locationt::set_function(), stub_globals_by_class, symbolt::symbol_expr(), and symbolt::type.
Referenced by java_bytecode_languaget::convert_single_method().
|
private |
Definition at line 42 of file java_static_initializers.h.
Referenced by create_stub_global_initializer_symbols(), and get_stub_initializer_body().