6 #ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H 7 #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H 9 #include <unordered_set> 40 typedef std::pair<const key_type, goto_functiont>
value_type;
58 typedef std::function<bool(const irep_idt &name)>
60 typedef std::function<
158 function.body.compute_location_numbers();
161 return named_function;
186 function_symbol_table,
208 #endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
std::unordered_set< irep_idt > processed_functions
Names of functions that are already fully available in the programt state.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const value_type * const_pointer
std::function< bool(const irep_idt &name)> can_generate_function_bodyt
mapped_type at(const key_type &name)
Gets the body for a given function.
symbol_tablet & symbol_table
Goto Programs with Functions.
exprt value
Initial value of symbol.
std::pair< const key_type, goto_functiont > value_type
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
goto_functiont & mapped_type
std::map< key_type, goto_functiont > underlying_mapt
const goto_functiont & const_mapped_type
The type of elements returned by const members.
bool can_convert_lazy_method(const irep_idt &id) const
std::function< bool(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)> generate_function_bodyt
void unload(const key_type &name) const
underlying_mapt & goto_functions
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
const value_type & const_reference
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.
const_mapped_type at(const key_type &name) const
Gets the body for a given function.
::goto_functiont goto_functiont
Provides a wrapper for a map of lazily loaded goto_functiont.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
bool can_produce_function(const key_type &name) const
Determines if this lazy GOTO functions map can produce a body for the given function.
void ensure_function_loaded(const key_type &name) const
Goto Programs with Functions.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
message_handlert & message_handler
The symbol table base class interface.
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...
const post_process_functiont post_process_function
const can_generate_function_bodyt driver_program_can_generate_function_body
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table)
language_filest & language_files
const generate_function_bodyt driver_program_generate_function_body
std::function< void(const irep_idt &name, goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols)> post_process_functiont
reference ensure_function_loaded_internal(const key_type &name) const