Go to the documentation of this file.
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 =
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};
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.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.