Go to the documentation of this file.
33 const std::vector<std::string> &files,
41 "missing program argument",
43 "one or more paths to program files");
46 std::vector<std::string> binaries, sources;
47 binaries.reserve(files.size());
48 sources.reserve(files.size());
50 for(
const auto &
file : files)
53 binaries.push_back(
file);
55 sources.push_back(
file);
65 for(
const auto &filename : sources)
68 std::ifstream infile(
widen(filename));
70 std::ifstream infile(filename);
76 "Failed to open input file `" + filename +
'\'');
85 "Failed to figure out type of file `" + filename +
'\'');
94 if(language.
parse(infile, filename))
110 for(
const auto &
file : binaries)
117 "failed to read object or link in file `" +
file +
'\'');
121 bool binaries_provided_start=
124 bool entry_point_generation_failed=
false;
126 if(binaries_provided_start && options.
is_set(
"function"))
132 entry_point_generation_failed=rebuild_existing_start();
134 else if(!binaries_provided_start)
138 entry_point_generation_failed=
142 if(entry_point_generation_failed)
159 if(options.
is_set(
"validate-goto-model"))
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.
bool is_goto_binary(const std::string &filename)
bool typecheck(symbol_tablet &symbol_table)
mstreamt & status() const
Thrown when we can't handle something in an input source file.
bool generate_support_functions(symbol_tablet &symbol_table)
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
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)
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Thrown when some external system fails unexpectedly.
virtual bool parse(std::istream &instream, const std::string &path)=0
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)
message_handlert & get_message_handler()
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
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)
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.