42 auto const entry_function_sym =
44 if(entry_function_sym ==
nullptr)
48 std::string{
"couldn't find function with name '"} +
49 id2string(entry_function_name) +
"' in symbol table",
55 entry_language->set_message_handler(message_handler);
56 entry_language->set_language_options(options);
57 return entry_language->generate_support_functions(goto_model.
symbol_table);
61 const std::vector<std::string> &files,
69 "missing program argument",
71 "one or more paths to program files");
74 std::vector<std::string> binaries, sources;
75 binaries.reserve(files.size());
76 sources.reserve(files.size());
78 for(
const auto &
file : files)
81 binaries.push_back(
file);
83 sources.push_back(
file);
93 for(
const auto &filename : sources)
96 std::ifstream infile(
widen(filename));
98 std::ifstream infile(filename);
104 "Failed to open input file '" + filename +
'\'');
113 "Failed to figure out type of file '" + filename +
'\'');
122 if(language.
parse(infile, filename))
138 for(
const auto &
file : binaries)
145 "failed to read object or link in file '" +
file +
'\'');
149 bool binaries_provided_start=
152 bool entry_point_generation_failed=
false;
154 if(binaries_provided_start && options.
is_set(
"function"))
164 entry_point_generation_failed =
165 language->generate_support_functions(goto_model.
symbol_table);
169 if(!entry_point_generation_failed)
172 else if(!binaries_provided_start)
174 if(options.
is_set(
"function"))
179 options.
get_option(
"function"), options, goto_model, message_handler);
181 if(entry_point_generation_failed || !options.
is_set(
"function"))
185 entry_point_generation_failed =
190 if(entry_point_generation_failed)
207 if(options.
is_set(
"validate-goto-model"))
210 goto_model_validation_optionst ::set_optionst::all_false};
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void unload(const irep_idt &name)
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
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.
language_filet & add_file(const std::string &filename)
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
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")
const std::string get_option(const std::string &option) const
const symbolt * lookup(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.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
static bool generate_entry_point_for_function(const irep_idt &entry_function_name, const optionst &options, goto_modelt &goto_model, message_handlert &message_handler)
Generate an entry point that calls a function with the given name, based on the functions language mo...
Initialize a Goto Program.
const std::string & id2string(const irep_idt &d)
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)
#define PRECONDITION(CONDITION)
std::wstring widen(const char *s)