Go to the documentation of this file.
30 post_process_functiont post_process_function,
31 post_process_functionst post_process_functions,
32 can_generate_function_bodyt driver_program_can_generate_function_body,
33 generate_function_bodyt driver_program_generate_function_body,
36 symbol_table(goto_model->symbol_table),
38 goto_model->goto_functions.function_map,
46 journalling_symbol_table,
47 goto_model->goto_functions,
52 driver_program_can_generate_function_body,
53 driver_program_generate_function_body,
55 post_process_function(post_process_function),
56 post_process_functions(post_process_functions),
57 driver_program_can_generate_function_body(
58 driver_program_can_generate_function_body),
59 driver_program_generate_function_body(
60 driver_program_generate_function_body),
61 message_handler(message_handler)
63 language_files.set_message_handler(message_handler);
67 : goto_model(std::move(other.goto_model)),
68 symbol_table(goto_model->symbol_table),
70 goto_model->goto_functions.function_map,
78 journalling_symbol_table,
79 goto_model->goto_functions,
84 other.driver_program_can_generate_function_body,
85 other.driver_program_generate_function_body,
86 other.message_handler),
87 language_files(std::move(other.language_files)),
88 post_process_function(other.post_process_function),
89 post_process_functions(other.post_process_functions),
90 message_handler(other.message_handler)
115 const std::vector<std::string> &files,
123 "no program provided",
125 "one or more paths to a goto binary or a source file in a supported "
129 std::vector<std::string> binaries, sources;
130 binaries.reserve(files.size());
131 sources.reserve(files.size());
133 for(
const auto &
file : files)
136 binaries.push_back(
file);
138 sources.push_back(
file);
144 const std::string filename =
"";
169 for(
const auto &filename : sources)
172 std::ifstream infile(
widen(filename));
174 std::ifstream infile(filename);
180 "failed to open input file '" + filename +
'\'');
189 "failed to figure out type of file '" + filename +
'\'');
198 if(language.
parse(infile, filename))
214 for(
const std::string &
file : binaries)
223 "failed to read/link goto model", source_location);
227 bool binaries_provided_start =
230 bool entry_point_generation_failed =
false;
232 if(binaries_provided_start && options.
is_set(
"function"))
239 std::unique_ptr<languaget> language =
246 entry_point_generation_failed =
251 if(!entry_point_generation_failed)
254 else if(!binaries_provided_start)
258 entry_point_generation_failed =
262 if(entry_point_generation_failed)
279 table_size = new_table_size;
282 std::vector<irep_idt> fn_ids_to_convert;
285 if(named_symbol.second.is_function())
286 fn_ids_to_convert.push_back(named_symbol.first);
289 for(
const irep_idt &symbol_name : fn_ids_to_convert)
296 }
while(new_table_size != table_size);
298 goto_model->goto_functions.compute_location_numbers();
Class that provides messages with a built-in verbosity 'level'.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool can_produce_function(const key_type &name) const
Determines if this lazy GOTO functions map can produce a body for the given function.
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
const post_process_functiont post_process_function
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.
#define CHECK_RETURN(CONDITION)
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
const lazy_goto_functions_mapt goto_functions
mstreamt & status() const
language_filet & add_language_file(const std::string &filename)
language_filest language_files
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
const changesett & get_updated() const
void unload(const key_type &name) const
Thrown when we can't handle something in an input source file.
bool generate_support_functions(symbol_tablet &symbol_table)
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
message_handlert & message_handler
Logging helper field.
virtual void set_language_options(const optionst &)
Set language-specific options.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
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...
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
A GOTO model that produces function bodies on demand.
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)
Thrown when some external system fails unexpectedly.
virtual bool parse(std::istream &instream, const std::string &path)=0
Abstract interface to support a programming language.
virtual void set_message_handler(message_handlert &_message_handler)
std::unique_ptr< goto_modelt > goto_model
void unload(const irep_idt &name) const
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
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 ...
std::unique_ptr< languaget > language
std::wstring widen(const char *s)
const post_process_functionst post_process_functions
bool final(symbol_table_baset &symbol_table)
A collection of goto functions.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
void ensure_function_loaded(const key_type &name) const
struct configt::javat java
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
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
void load_all_functions() const
Eagerly loads all functions from the symbol table.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
unsignedbv_typet size_type()
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
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.