6 #ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H 7 #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H 9 #include <unordered_set> 39 typedef std::pair<const key_type, goto_functiont>
value_type;
55 journalling_symbol_tablet &function_symbols)>
57 typedef std::function<bool(const irep_idt &name)>
59 typedef std::function<
145 journalling_symbol_tablet journalling_table =
154 function.body.compute_location_numbers();
157 return named_function;
182 function_symbol_table,
204 #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
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.
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.
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