27 post_process_functiont post_process_function,
28 post_process_functionst post_process_functions,
29 can_generate_function_bodyt driver_program_can_generate_function_body,
30 generate_function_bodyt driver_program_generate_function_body,
33 symbol_table(goto_model->symbol_table),
35 goto_model->goto_functions.function_map,
43 journalling_symbol_table,
44 goto_model->goto_functions,
47 this->post_process_function(model_function, *
this);
49 driver_program_can_generate_function_body,
50 driver_program_generate_function_body,
52 post_process_function(post_process_function),
53 post_process_functions(post_process_functions),
54 driver_program_can_generate_function_body(
55 driver_program_can_generate_function_body),
56 driver_program_generate_function_body(
57 driver_program_generate_function_body),
58 message_handler(message_handler)
63 : goto_model(
std::move(other.goto_model)),
64 symbol_table(goto_model->symbol_table),
66 goto_model->goto_functions.function_map,
74 journalling_symbol_table,
75 goto_model->goto_functions,
78 this->post_process_function(model_function, *
this);
80 other.driver_program_can_generate_function_body,
81 other.driver_program_generate_function_body,
82 other.message_handler),
83 language_files(std::move(other.language_files)),
84 post_process_function(other.post_process_function),
85 post_process_functions(other.post_process_functions),
86 message_handler(other.message_handler)
111 const std::vector<std::string> &files,
116 if(files.empty() &&
config.java.main_class.empty())
119 "no program provided",
121 "one or more paths to a goto binary or a source file in a supported "
125 std::list<std::string> binaries, sources;
127 for(
const auto &
file : files)
130 binaries.push_back(
file);
132 sources.push_back(
file);
135 if(sources.empty() && !
config.java.main_class.empty())
138 const std::string filename =
"";
148 std::istringstream unused;
185 symbol_tablet::symbolst::size_type table_size;
186 symbol_tablet::symbolst::size_type new_table_size =
190 table_size = new_table_size;
193 std::vector<irep_idt> fn_ids_to_convert;
196 if(named_symbol.second.is_function())
197 fn_ids_to_convert.push_back(named_symbol.first);
200 for(
const irep_idt &symbol_name : fn_ids_to_convert)
207 }
while(new_table_size != table_size);
209 goto_model->goto_functions.compute_location_numbers();
A collection of goto functions.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
const changesett & get_updated() const
std::unique_ptr< languaget > language
virtual bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler)=0
virtual void set_language_options(const optionst &, message_handlert &)
Set language-specific options.
A GOTO model that produces function bodies on demand.
language_filet & add_language_file(const std::string &filename)
void load_all_functions() const
Eagerly loads all functions from the symbol table.
std::unique_ptr< goto_modelt > goto_model
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
const lazy_goto_functions_mapt goto_functions
language_filest language_files
const post_process_functionst post_process_functions
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)
Construct a lazy GOTO model, supplying callbacks that customise its behaviour.
message_handlert & message_handler
Logging helper field.
void initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
Class that provides messages with a built-in verbosity 'level'.
mstreamt & status() const
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
void initialize_from_source_files(const std::list< std::string > &sources, const optionst &options, language_filest &language_files, symbol_tablet &symbol_table, message_handlert &message_handler)
Populate symbol_table from sources by parsing and type checking via language_files.
void set_up_custom_entry_point(language_filest &language_files, symbol_tablet &symbol_table, const std::function< std::size_t(const irep_idt &)> &unload, const optionst &options, bool try_mode_lookup, message_handlert &message_handler)
Process the "function" option in options to prepare a custom entry point to replace __CPROVER_start.
Initialize a Goto Program.
Abstract interface to support a programming language.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
bool read_objects_and_link(const std::list< std::string > &file_names, goto_modelt &dest, message_handlert &message_handler)
Reads object files and updates the config if any files were read.
#define CHECK_RETURN(CONDITION)