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)
60 language_files.set_message_handler(message_handler);
64 : goto_model(std::move(other.goto_model)),
65 symbol_table(goto_model->symbol_table),
67 goto_model->goto_functions.function_map,
75 journalling_symbol_table,
76 goto_model->goto_functions,
79 this->post_process_function(model_function, *
this);
81 other.driver_program_can_generate_function_body,
82 other.driver_program_generate_function_body,
83 other.message_handler),
84 language_files(std::move(other.language_files)),
85 post_process_function(other.post_process_function),
86 post_process_functions(other.post_process_functions),
87 message_handler(other.message_handler)
112 const std::vector<std::string> &files,
120 "no program provided",
122 "one or more paths to a goto binary or a source file in a supported "
126 std::vector<std::string> binaries, sources;
127 binaries.reserve(files.size());
128 sources.reserve(files.size());
130 for(
const auto &
file : files)
133 binaries.push_back(
file);
135 sources.push_back(
file);
141 const std::string filename =
"";
166 for(
const auto &filename : sources)
169 std::ifstream infile(
widen(filename));
171 std::ifstream infile(filename);
177 "failed to open input file '" + filename +
'\'');
186 "failed to figure out type of file '" + filename +
'\'');
195 if(language.
parse(infile, filename))
211 for(
const std::string &
file : binaries)
220 "failed to read/link goto model", source_location);
224 bool binaries_provided_start =
227 bool entry_point_generation_failed =
false;
229 if(binaries_provided_start && options.
is_set(
"function"))
236 std::unique_ptr<languaget> language =
243 entry_point_generation_failed =
248 if(!entry_point_generation_failed)
251 else if(!binaries_provided_start)
255 entry_point_generation_failed =
259 if(entry_point_generation_failed)
276 table_size = new_table_size;
279 std::vector<irep_idt> fn_ids_to_convert;
282 if(named_symbol.second.is_function())
283 fn_ids_to_convert.push_back(named_symbol.first);
286 for(
const irep_idt &symbol_name : fn_ids_to_convert)
293 }
while(new_table_size != table_size);
295 goto_model->goto_functions.compute_location_numbers();
unsignedbv_typet size_type()
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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 ...
Thrown when we can't handle something in an input source file.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
const changesett & get_updated() const
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
bool generate_support_functions(symbol_tablet &symbol_table)
bool final(symbol_table_baset &symbol_table)
std::unique_ptr< languaget > language
virtual void set_language_options(const optionst &)
Set language-specific options.
virtual bool parse(std::istream &instream, const std::string &path)=0
void ensure_function_loaded(const key_type &name) const
void unload(const key_type &name) const
bool can_produce_function(const key_type &name) const
Determines if this lazy GOTO functions map can produce a body for the given function.
A GOTO model that produces function bodies on demand.
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
void unload(const irep_idt &name) const
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.
language_filet & add_language_file(const std::string &filename)
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
virtual void set_message_handler(message_handlert &_message_handler)
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
void set_file(const irep_idt &file)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Thrown when some external system fails unexpectedly.
Abstract interface to support a programming language.
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
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_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file, and also updates config
void remove_existing_entry_point(symbol_table_baset &symbol_table)
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
std::unique_ptr< languaget > get_entry_point_language(const symbol_table_baset &symbol_table, const optionst &options, message_handlert &message_handler)
Find the language corresponding to the __CPROVER_start function.
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
#define CHECK_RETURN(CONDITION)
std::wstring widen(const char *s)