23 post_process_functiont post_process_function,
24 post_process_functionst post_process_functions,
25 can_generate_function_bodyt driver_program_can_generate_function_body,
26 generate_function_bodyt driver_program_generate_function_body,
29 symbol_table(goto_model->symbol_table),
31 goto_model->goto_functions.function_map,
37 journalling_symbol_tablet &journalling_symbol_table) -> void
40 journalling_symbol_table,
41 goto_model->goto_functions,
46 driver_program_can_generate_function_body,
47 driver_program_generate_function_body,
49 post_process_function(post_process_function),
50 post_process_functions(post_process_functions),
51 driver_program_can_generate_function_body(
52 driver_program_can_generate_function_body),
53 driver_program_generate_function_body(
54 driver_program_generate_function_body),
61 : goto_model(
std::move(other.goto_model)),
62 symbol_table(goto_model->symbol_table),
64 goto_model->goto_functions.function_map,
70 journalling_symbol_tablet &journalling_symbol_table) -> void
73 journalling_symbol_table,
74 goto_model->goto_functions,
79 other.driver_program_can_generate_function_body,
80 other.driver_program_generate_function_body,
81 other.message_handler),
82 language_files(std::move(other.language_files)),
83 post_process_function(other.post_process_function),
84 post_process_functions(other.post_process_functions),
94 const std::vector<std::string> &files=cmdline.
args;
101 std::vector<std::string> binaries, sources;
102 binaries.reserve(files.size());
103 sources.reserve(files.size());
105 for(
const auto &
file : files)
108 binaries.push_back(
file);
110 sources.push_back(
file);
115 for(
const auto &filename : sources)
118 std::ifstream infile(
widen(filename));
120 std::ifstream infile(filename);
125 msg.
error() <<
"failed to open input file `" << filename
148 if(language.
parse(infile, filename))
166 for(
const std::string &
file : binaries)
174 bool binaries_provided_start =
177 bool entry_point_generation_failed=
false;
179 if(binaries_provided_start && cmdline.
isset(
"function"))
185 entry_point_generation_failed=rebuild_existing_start();
187 else if(!binaries_provided_start)
194 bool stubs_enabled=cmdline.
isset(
"generate-opaque-stubs");
200 entry_point_generation_failed=
204 if(entry_point_generation_failed)
221 table_size=new_table_size;
224 std::vector<irep_idt> fn_ids_to_convert;
227 if(named_symbol.second.is_function())
228 fn_ids_to_convert.push_back(named_symbol.first);
231 for(
const irep_idt &symbol_name : fn_ids_to_convert)
238 }
while(new_table_size!=table_size);
240 goto_model->goto_functions.compute_location_numbers();
247 journalling_symbol_tablet::wrap(this->symbol_table);
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool final(symbol_table_baset &symbol_table)
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
std::wstring widen(const char *s)
const post_process_functionst post_process_functions
virtual void get_language_options(const cmdlinet &)
const lazy_goto_functions_mapt goto_functions
bool is_goto_binary(const std::string &filename)
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)
unsignedbv_typet size_type()
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Model that holds partially loaded map of functions.
static mstreamt & eom(mstreamt &m)
void unload(const key_type &name) const
std::unique_ptr< languaget > language
message_handlert & message_handler
Logging helper field.
language_filest language_files
virtual bool isset(char option) const
source_locationt source_location
void set_file(const irep_idt &file)
void initialize(const cmdlinet &cmdline)
Abstract interface to support a programming language.
bool typecheck(symbol_tablet &symbol_table)
virtual void set_message_handler(message_handlert &_message_handler)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void set_should_generate_opaque_method_stubs(bool stubs_enabled)
Turn on or off stub generation for all the languages.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
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
static irep_idt entry_point()
mstreamt & status() const
std::unique_ptr< goto_modelt > goto_model
const post_process_functiont post_process_function
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
language_filet & add_language_file(const std::string &filename)
goto_programt coverage_criteriont message_handlert & message_handler
virtual bool parse(std::istream &instream, const std::string &path)=0
bool generate_support_functions(symbol_tablet &symbol_table)
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...