9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H 10 #define CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H 16 #include <unordered_set> 28 const bool thread_safe);
47 const std::unordered_set<irep_idt> &stub_globals_set,
59 const std::unordered_set<irep_idt> &stub_globals_set,
codet get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Thread safe version of the static initialiser.
codet get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Produces the static initialiser wrapper body for the given function.
void create_static_initializer_wrappers(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Create static initializer wrappers for all classes that need them.
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
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 t...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void create_stub_global_initializers(symbol_tablet &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
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.
stub_globals_by_classt stub_globals_by_class
The symbol table base class interface.
Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types.
std::unordered_multimap< irep_idt, irep_idt > stub_globals_by_classt
Maps class symbols onto the stub globals that belong to them.
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
A statement in a programming language.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...