50 std::string(
"couldn't find entry with name '") +
60 symbol_table, message_handler);
64 const std::list<std::string> &
sources,
75 for(
const auto &filename :
sources)
87 if(
lf.language ==
nullptr)
90 "Failed to figure out type of file", filename};
98 if(language.
parse(
infile, filename, message_handler))
108 if(language_files.
typecheck(symbol_table, message_handler))
117 const std::function<std::size_t(
const irep_idt &)> &unload,
134 std::unique_ptr<languaget> language =
142 language->generate_support_functions(symbol_table, message_handler);
156 options, symbol_table, message_handler);
160 !options.
is_set(
"function"))
165 symbol_table, message_handler);
176 const std::vector<std::string> &
files,
184 "missing program argument",
186 "one or more paths to program files");
191 for(
const auto &file :
files)
210 [&goto_model](
const irep_idt &
id) { return goto_model.unload(id); },
227 if(options.
is_set(
"validate-goto-model"))
230 goto_model_validation_optionst ::set_optionst::all_false};
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
mp_integer max_malloc_size() const
The maximum allocation size is determined by the number of bits that are left in the pointer of width...
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 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.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool typecheck(symbol_table_baset &symbol_table, const bool keep_file_local, message_handlert &message_handler)
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler)
language_filet & add_file(const std::string &filename)
bool final(symbol_table_baset &symbol_table)
virtual bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler)=0
virtual void set_language_options(const optionst &, message_handlert &)
Set language-specific options.
Class that provides messages with a built-in verbosity 'level'.
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
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::list< symbolst::const_iterator > match_name_or_base_name(const irep_idt &id) const
Collect all symbols the name of which matches id or the base name of which matches id.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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)
void initialize_from_source_files(const std::list< std::string > &sources, const optionst &options, language_filest &language_files, symbol_tablet &symbol_table, message_handlert &message_handler)
Populate symbol_table from sources by parsing and type checking via language_files.
void set_up_custom_entry_point(language_filest &language_files, symbol_tablet &symbol_table, const std::function< std::size_t(const irep_idt &)> &unload, const optionst &options, bool try_mode_lookup, message_handlert &message_handler)
Process the "function" option in options to prepare a custom entry point to replace __CPROVER_start.
static bool generate_entry_point_for_function(const optionst &options, symbol_tablet &symbol_table, message_handlert &message_handler)
Generate an entry point that calls a function with the given name, based on the functions language mo...
void update_max_malloc_size(goto_modelt &goto_model, message_handlert &message_handler)
Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed.
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_mode(const irep_idt &mode)
Get the language corresponding to the given 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_goto_binary(const std::string &filename, message_handlert &message_handler)
bool read_objects_and_link(const std::list< std::string > &file_names, goto_modelt &dest, message_handlert &message_handler)
Reads object files and updates the config if any files were read.
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)
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
#define widen_if_needed(s)