Go to the documentation of this file.
41 auto const entry_function_sym =
43 if(entry_function_sym ==
nullptr)
47 std::string{
"couldn't find function with name '"} +
48 id2string(entry_function_name) +
"' in symbol table",
54 entry_language->set_message_handler(message_handler);
55 entry_language->set_language_options(options);
56 return entry_language->generate_support_functions(goto_model.
symbol_table);
60 const std::vector<std::string> &files,
68 "missing program argument",
70 "one or more paths to program files");
73 std::vector<std::string> binaries, sources;
74 binaries.reserve(files.size());
75 sources.reserve(files.size());
77 for(
const auto &
file : files)
80 binaries.push_back(
file);
82 sources.push_back(
file);
92 for(
const auto &filename : sources)
95 std::ifstream infile(
widen(filename));
97 std::ifstream infile(filename);
103 "Failed to open input file '" + filename +
'\'');
112 "Failed to figure out type of file '" + filename +
'\'');
121 if(language.
parse(infile, filename))
137 for(
const auto &
file : binaries)
144 "failed to read object or link in file '" +
file +
'\'');
148 bool binaries_provided_start=
151 bool entry_point_generation_failed=
false;
153 if(binaries_provided_start && options.
is_set(
"function"))
163 entry_point_generation_failed =
168 if(!entry_point_generation_failed)
171 else if(!binaries_provided_start)
173 if(options.
is_set(
"function"))
178 options.
get_option(
"function"), options, goto_model, message_handler);
180 if(entry_point_generation_failed || !options.
is_set(
"function"))
184 entry_point_generation_failed =
189 if(entry_point_generation_failed)
206 if(options.
is_set(
"validate-goto-model"))
209 goto_model_validation_optionst ::set_optionst::all_false};
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.
void unload(const irep_idt &name)
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 std::string get_option(const std::string &option) const
mstreamt & status() const
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Thrown when we can't handle something in an input source file.
bool generate_support_functions(symbol_tablet &symbol_table)
virtual void set_language_options(const optionst &)
Set language-specific options.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
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...
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Initialize a Goto Program.
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...
const std::string & id2string(const irep_idt &d)
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
#define PRECONDITION(CONDITION)
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)
language_filet & add_file(const std::string &filename)
std::unique_ptr< languaget > language
std::wstring widen(const char *s)
bool final(symbol_table_baset &symbol_table)
goto_functionst goto_functions
GOTO functions.
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 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.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Goto Programs with Functions.
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.
symbol_tablet symbol_table
Symbol table.