cprover
|
Model that holds partially loaded map of functions. More...
#include <lazy_goto_model.h>
Public Types | |
typedef std::function< void(goto_model_functiont &function, const abstract_goto_modelt &)> | post_process_functiont |
typedef std::function< bool(goto_modelt &goto_model)> | post_process_functionst |
typedef lazy_goto_functions_mapt::can_generate_function_bodyt | can_generate_function_bodyt |
typedef lazy_goto_functions_mapt::generate_function_bodyt | generate_function_bodyt |
Static Public Member Functions | |
template<typename THandler > | |
static lazy_goto_modelt | from_handler_object (THandler &handler, const optionst &options, message_handlert &message_handler) |
Create a lazy_goto_modelt from a object that defines function/module pass handlers. More... | |
static std::unique_ptr< goto_modelt > | process_whole_model_and_freeze (lazy_goto_modelt &&model) |
The model returned here has access to the functions we've already loaded but is frozen in the sense that, with regard to the facility to load new functions, it has let it go. More... | |
Public Attributes | |
symbol_tablet & | symbol_table |
Reference to symbol_table in the internal goto_model. More... | |
Private Member Functions | |
bool | finalize () |
Private Attributes | |
std::unique_ptr< goto_modelt > | goto_model |
const lazy_goto_functions_mapt | goto_functions |
language_filest | language_files |
const post_process_functiont | post_process_function |
const post_process_functionst | post_process_functions |
const can_generate_function_bodyt | driver_program_can_generate_function_body |
const generate_function_bodyt | driver_program_generate_function_body |
message_handlert & | message_handler |
Logging helper field. More... | |
Model that holds partially loaded map of functions.
Definition at line 20 of file lazy_goto_model.h.
typedef lazy_goto_functions_mapt::can_generate_function_bodyt lazy_goto_modelt::can_generate_function_bodyt |
Definition at line 28 of file lazy_goto_model.h.
Definition at line 30 of file lazy_goto_model.h.
typedef std::function<bool(goto_modelt &goto_model)> lazy_goto_modelt::post_process_functionst |
Definition at line 26 of file lazy_goto_model.h.
typedef std::function< void(goto_model_functiont &function, const abstract_goto_modelt &)> lazy_goto_modelt::post_process_functiont |
Definition at line 25 of file lazy_goto_model.h.
|
explicit |
Referenced by from_handler_object().
lazy_goto_modelt::lazy_goto_modelt | ( | lazy_goto_modelt && | other | ) |
|
inline |
Definition at line 92 of file lazy_goto_model.h.
References language_filest::add_file(), and language_files.
Referenced by initialize().
|
overridevirtual |
Determines if this model can produce a body for the given function.
id | function ID to query |
Implements abstract_goto_modelt.
Definition at line 268 of file lazy_goto_model.cpp.
References lazy_goto_functions_mapt::can_produce_function(), and goto_functions.
|
private |
Definition at line 243 of file lazy_goto_model.cpp.
References language_filest::clear(), lazy_goto_functions_mapt::ensure_function_loaded(), messaget::eom(), messaget::error(), language_filest::final(), goto_functions, goto_model, symbolt::is_function(), language_files, symbol_table_baset::lookup_ref(), message_handler, post_process_functions, symbol_table, and lazy_goto_functions_mapt::unload().
|
inlinestatic |
Create a lazy_goto_modelt from a object that defines function/module pass handlers.
handler | An object that defines the handlers |
options | The options passed to process_goto_functions |
message_handler | The message_handler to use for logging |
THandler | a type that defines methods process_goto_function and process_goto_functions |
Definition at line 56 of file lazy_goto_model.h.
References goto_model, lazy_goto_modelt(), message_handler, and symbol_table.
Referenced by jbmc_parse_optionst::doit(), and jbmc_parse_optionst::get_goto_program().
|
inlineoverridevirtual |
Get a GOTO function by name, or throw if no such function exists.
May have side-effects on the GOTO function map provided by get_goto_functions, or the symbol table returned by get_symbol_table, so iterators pointing into either may be invalidated.
id | function to get |
Implements abstract_goto_modelt.
Definition at line 129 of file lazy_goto_model.h.
References lazy_goto_functions_mapt::at(), and goto_functions.
|
inlineoverridevirtual |
Accessor to retrieve the internal goto_functionst.
Use with care; concurrent use of get_goto_function will have side-effects on this map which may surprise users, including invalidating any iterators they have stored.
Implements abstract_goto_modelt.
Definition at line 117 of file lazy_goto_model.h.
References goto_model.
|
inlineoverridevirtual |
Accessor to get the symbol table.
Concurrent use of get_goto_function may invalidate iterators or otherwise surprise users by modifying the map underneath them, so this should only be used to lend a reference to code that cannot also call get_goto_function.
Implements abstract_goto_modelt.
Definition at line 122 of file lazy_goto_model.h.
References symbol_table.
void lazy_goto_modelt::initialize | ( | const cmdlinet & | cmdline | ) |
Definition at line 90 of file lazy_goto_model.cpp.
References add_language_file(), cmdlinet::args, config, goto_functionst::entry_point(), messaget::eom(), messaget::error(), language_filest::generate_support_functions(), get_language_from_filename(), languaget::get_language_options(), language_filet::get_modules(), goto_model, symbol_table_baset::has_symbol(), is_goto_binary(), cmdlinet::isset(), language_filet::language, language_files, message_handler, languaget::parse(), read_object_and_link(), source_locationt::set_file(), messaget::set_message_handler(), configt::set_object_bits_from_symbol_table(), language_filest::set_should_generate_opaque_method_stubs(), messaget::mstreamt::source_location, messaget::status(), symbol_table, language_filest::typecheck(), and widen().
Referenced by jbmc_parse_optionst::doit(), and jbmc_parse_optionst::get_goto_program().
void lazy_goto_modelt::load_all_functions | ( | ) | const |
Eagerly loads all functions from the symbol table.
Definition at line 215 of file lazy_goto_model.cpp.
References lazy_goto_functions_mapt::ensure_function_loaded(), goto_functions, goto_model, size_type(), symbol_table, and symbol_table_baset::symbols.
Referenced by jbmc_parse_optionst::get_goto_program().
|
inline |
Definition at line 41 of file lazy_goto_model.h.
References goto_model, and language_files.
|
inlinestatic |
The model returned here has access to the functions we've already loaded but is frozen in the sense that, with regard to the facility to load new functions, it has let it go.
Before freezing the functions all module-level passes are run
model | The lazy_goto_modelt to freeze |
Definition at line 103 of file lazy_goto_model.h.
Referenced by jbmc_parse_optionst::get_goto_program(), and load_java_class().
|
inline |
Definition at line 90 of file lazy_goto_model.h.
References goto_functions, and lazy_goto_functions_mapt::unload().
|
private |
Definition at line 149 of file lazy_goto_model.h.
|
private |
Definition at line 150 of file lazy_goto_model.h.
|
private |
Definition at line 143 of file lazy_goto_model.h.
Referenced by can_produce_function(), finalize(), get_goto_function(), load_all_functions(), and unload().
|
private |
Definition at line 136 of file lazy_goto_model.h.
Referenced by finalize(), from_handler_object(), get_goto_functions(), initialize(), load_all_functions(), and operator=().
|
private |
Definition at line 144 of file lazy_goto_model.h.
Referenced by add_language_file(), finalize(), initialize(), and operator=().
|
private |
Logging helper field.
Definition at line 153 of file lazy_goto_model.h.
Referenced by finalize(), from_handler_object(), and initialize().
|
private |
Definition at line 147 of file lazy_goto_model.h.
|
private |
Definition at line 148 of file lazy_goto_model.h.
Referenced by finalize().
symbol_tablet& lazy_goto_modelt::symbol_table |
Reference to symbol_table in the internal goto_model.
Definition at line 140 of file lazy_goto_model.h.
Referenced by jbmc_parse_optionst::doit(), finalize(), from_handler_object(), jbmc_parse_optionst::get_goto_program(), get_symbol_table(), initialize(), and load_all_functions().