cprover
|
Provides a wrapper for a map of lazily loaded goto_functiont. More...
#include <lazy_goto_functions_map.h>
Public Types | |
typedef irep_idt | key_type |
typedef goto_functiont & | mapped_type |
typedef const goto_functiont & | const_mapped_type |
The type of elements returned by const members. More... | |
typedef std::pair< const key_type, goto_functiont > | value_type |
typedef value_type & | reference |
typedef const value_type & | const_reference |
typedef value_type * | pointer |
typedef const value_type * | const_pointer |
typedef std::size_t | size_type |
typedef std::function< void(const irep_idt &name, goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols)> | post_process_functiont |
typedef std::function< bool(const irep_idt &name)> | can_generate_function_bodyt |
typedef std::function< bool(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)> | generate_function_bodyt |
Public Member Functions | |
lazy_goto_functions_mapt (underlying_mapt &goto_functions, language_filest &language_files, symbol_tablet &symbol_table, post_process_functiont post_process_function, can_generate_function_bodyt driver_program_can_generate_function_body, generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler) | |
Creates a lazy_goto_functions_mapt. More... | |
const_mapped_type | at (const key_type &name) const |
Gets the body for a given function. More... | |
mapped_type | at (const key_type &name) |
Gets the body for a given function. More... | |
bool | can_produce_function (const key_type &name) const |
Determines if this lazy GOTO functions map can produce a body for the given function. More... | |
void | unload (const key_type &name) const |
void | ensure_function_loaded (const key_type &name) const |
Private Types | |
typedef std::map< key_type, goto_functiont > | underlying_mapt |
Private Member Functions | |
reference | ensure_function_loaded_internal (const key_type &name) const |
reference | ensure_entry_converted (const key_type &name, symbol_table_baset &function_symbol_table) const |
Convert a function if not already converted, then return a reference to its goto_functionst map entry. More... | |
Private Attributes | |
underlying_mapt & | goto_functions |
std::unordered_set< irep_idt > | processed_functions |
Names of functions that are already fully available in the programt state. More... | |
language_filest & | language_files |
symbol_tablet & | symbol_table |
const post_process_functiont | post_process_function |
const can_generate_function_bodyt | driver_program_can_generate_function_body |
const generate_function_bodyt | driver_program_generate_function_body |
message_handlert & | message_handler |
Provides a wrapper for a map of lazily loaded goto_functiont.
This incrementally builds a goto-functions object, while permitting access to goto programs while they are still under construction. The intended workflow:
at
function bodyt | The type of the function bodies, usually goto_programt |
Definition at line 28 of file lazy_goto_functions_map.h.
typedef std::function<bool(const irep_idt &name)> lazy_goto_functions_mapt::can_generate_function_bodyt |
Definition at line 58 of file lazy_goto_functions_map.h.
typedef const goto_functiont& lazy_goto_functions_mapt::const_mapped_type |
The type of elements returned by const members.
Definition at line 37 of file lazy_goto_functions_map.h.
typedef const value_type* lazy_goto_functions_mapt::const_pointer |
Definition at line 47 of file lazy_goto_functions_map.h.
typedef const value_type& lazy_goto_functions_mapt::const_reference |
Definition at line 43 of file lazy_goto_functions_map.h.
typedef std::function< bool( const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)> lazy_goto_functions_mapt::generate_function_bodyt |
Definition at line 65 of file lazy_goto_functions_map.h.
Definition at line 32 of file lazy_goto_functions_map.h.
Definition at line 34 of file lazy_goto_functions_map.h.
Definition at line 45 of file lazy_goto_functions_map.h.
typedef std::function<void( const irep_idt &name, goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols)> lazy_goto_functions_mapt::post_process_functiont |
Definition at line 56 of file lazy_goto_functions_map.h.
Definition at line 41 of file lazy_goto_functions_map.h.
typedef std::size_t lazy_goto_functions_mapt::size_type |
Definition at line 49 of file lazy_goto_functions_map.h.
|
private |
Definition at line 68 of file lazy_goto_functions_map.h.
typedef std::pair<const key_type, goto_functiont> lazy_goto_functions_mapt::value_type |
Definition at line 39 of file lazy_goto_functions_map.h.
|
inline |
Creates a lazy_goto_functions_mapt.
Definition at line 84 of file lazy_goto_functions_map.h.
|
inline |
Gets the body for a given function.
name | The name of the function to search for. |
Definition at line 107 of file lazy_goto_functions_map.h.
References ensure_function_loaded_internal().
Referenced by lazy_goto_modelt::get_goto_function().
|
inline |
Gets the body for a given function.
name | The name of the function to search for. |
Definition at line 115 of file lazy_goto_functions_map.h.
References ensure_function_loaded_internal().
|
inline |
Determines if this lazy GOTO functions map can produce a body for the given function.
name | function ID to query |
Definition at line 125 of file lazy_goto_functions_map.h.
References language_filest::can_convert_lazy_method(), driver_program_can_generate_function_body, and language_files.
Referenced by lazy_goto_modelt::can_produce_function().
|
inlineprivate |
Convert a function if not already converted, then return a reference to its goto_functionst map entry.
name | ID of the function to convert |
function_symbol_table | mutable symbol table reference to be used when converting the function (e.g. to add new local variables). Note we should not use a global pre-cached symbol table reference for this so that our callers can insert a journalling table here if needed. |
Definition at line 168 of file lazy_goto_functions_map.h.
References language_filest::can_convert_lazy_method(), goto_convert_functionst::convert_function(), language_filest::convert_lazy_method(), driver_program_generate_function_body, goto_functions, irept::is_not_nil(), language_files, symbol_table_baset::lookup_ref(), message_handler, and symbolt::value.
Referenced by ensure_function_loaded_internal().
|
inline |
Definition at line 134 of file lazy_goto_functions_map.h.
References ensure_function_loaded_internal().
Referenced by lazy_goto_modelt::finalize(), and lazy_goto_modelt::load_all_functions().
|
inlineprivate |
Definition at line 143 of file lazy_goto_functions_map.h.
References ensure_entry_converted(), post_process_function, processed_functions, and symbol_table.
Referenced by at(), and ensure_function_loaded().
|
inline |
Definition at line 132 of file lazy_goto_functions_map.h.
References goto_functions.
Referenced by lazy_goto_modelt::finalize(), and lazy_goto_modelt::unload().
|
private |
Definition at line 78 of file lazy_goto_functions_map.h.
Referenced by can_produce_function().
|
private |
Definition at line 79 of file lazy_goto_functions_map.h.
Referenced by ensure_entry_converted().
|
private |
Definition at line 69 of file lazy_goto_functions_map.h.
Referenced by ensure_entry_converted(), and unload().
|
private |
Definition at line 75 of file lazy_goto_functions_map.h.
Referenced by can_produce_function(), and ensure_entry_converted().
|
private |
Definition at line 80 of file lazy_goto_functions_map.h.
Referenced by ensure_entry_converted().
|
private |
Definition at line 77 of file lazy_goto_functions_map.h.
Referenced by ensure_function_loaded_internal().
|
mutableprivate |
Names of functions that are already fully available in the programt state.
Definition at line 73 of file lazy_goto_functions_map.h.
Referenced by ensure_function_loaded_internal().
|
private |
Definition at line 76 of file lazy_goto_functions_map.h.
Referenced by ensure_function_loaded_internal().