6 #ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H 7 #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H 23 typedef std::function<
55 template<
typename THandler>
64 handler.process_goto_function(fun, model, options);
67 return handler.process_goto_functions(
goto_model, options);
69 [&handler](
const irep_idt &name) ->
bool {
70 return handler.can_generate_function_body(name);
79 handler.generate_function_body(
108 return std::move(model.goto_model);
158 #endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H lazy_goto_functions_mapt::can_generate_function_bodyt can_generate_function_bodyt
Abstract interface to eager or lazy GOTO models.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
void unload(const irep_idt &name) const
std::function< bool(const irep_idt &name)> can_generate_function_bodyt
const post_process_functionst post_process_functions
const lazy_goto_functions_mapt goto_functions
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.
lazy_goto_modelt(post_process_functiont post_process_function, post_process_functionst post_process_functions, can_generate_function_bodyt driver_program_can_generate_function_body, generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler)
language_filet & add_file(const std::string &filename)
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
Model that holds partially loaded map of functions.
const generate_function_bodyt driver_program_generate_function_body
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
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
Abstract interface to eager or lazy GOTO models.
message_handlert & message_handler
Logging helper field.
language_filest language_files
std::function< bool(goto_modelt &goto_model)> post_process_functionst
lazy_goto_functions_mapt::generate_function_bodyt generate_function_bodyt
const_mapped_type at(const key_type &name) const
Gets the body for a given function.
void initialize(const cmdlinet &cmdline)
const goto_functionst & get_goto_functions() const override
Accessor to retrieve the internal goto_functionst.
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 t...
::goto_functiont goto_functiont
Provides a wrapper for a map of lazily loaded goto_functiont.
std::function< void(goto_model_functiont &function, const abstract_goto_modelt &)> post_process_functiont
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Goto Programs with Functions.
The symbol table base class interface.
std::unique_ptr< goto_modelt > goto_model
const can_generate_function_bodyt driver_program_can_generate_function_body
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
language_filet & add_language_file(const std::string &filename)
lazy_goto_modelt & operator=(lazy_goto_modelt &&other)
const post_process_functiont post_process_function
Interface providing access to a single function in a GOTO model, plus its associated symbol table...