Go to the documentation of this file.
50 #define DOTGRAPHSETTINGS "color=black;" \
51 "orientation=portrait;" \
73 log.
debug() <<
"Library not found: " << library <<
" (ignoring)"
102 const unsigned warnings_before =
105 auto symbol_table_opt =
compile();
106 if(!symbol_table_opt.has_value())
113 if(
link(*symbol_table_opt))
133 const std::string &file_name,
137 std::ifstream in(file_name);
143 const std::string ext =
144 r == std::string::npos ?
"" : file_name.substr(
r + 1, file_name.length());
147 ext ==
"c" || ext ==
"cc" || ext ==
"cp" || ext ==
"cpp" || ext ==
"CPP" ||
148 ext ==
"c++" || ext ==
"C" || ext ==
"i" || ext ==
"ii" || ext ==
"class" ||
149 ext ==
"jar" || ext ==
"jsil")
156 if((ext ==
"a" || ext ==
"o") && strncmp(hdr,
"!<thin>", 8) == 0)
165 if(hdr[0] == 0x7f && memcmp(hdr + 1,
"ELF", 3) == 0)
178 log.
warning() <<
"failed to open file '" << file_name
184 log.
debug() <<
"unknown file type in '" << file_name <<
"'"
190 log.
debug() <<
"ELF object without goto-cc section: '" << file_name <<
"'"
215 const std::string &file_name,
251 std::ifstream in(tmp_file_out());
254 while(!in.fail() && std::getline(in, line))
261 log.
debug() <<
"Object file is not a goto binary: " << line
276 std::string library_file_name;
280 library_file_name =
concat_dir_file(library_path,
"lib" + name +
".a");
282 std::ifstream in(library_file_name);
288 library_file_name =
concat_dir_file(library_path,
"lib" + name +
".so");
296 log.
warning() <<
"Warning: Cannot read ELF library "
320 if(symbol_table.has_value())
381 std::cout <<
get_base_name(file_name,
false) <<
'\n' << std::flush;
385 if(!file_symbol_table.has_value())
387 const std::string &debug_outfile=
389 if(!debug_outfile.empty())
406 file_goto_model.
symbol_table = std::move(*file_symbol_table);
413 const std::string file_name_with_obj_ext =
419 cfn = file_name_with_obj_ext;
446 return std::move(symbol_table);
452 const std::string &file_name,
455 std::unique_ptr<languaget> languagep;
467 else if(file_name !=
"-")
470 if(languagep==
nullptr)
472 log.
error() <<
"failed to figure out type of file '" << file_name <<
"'"
483 std::ifstream infile(
widen(file_name));
485 std::ifstream infile(file_name);
490 log.
error() <<
"failed to open input file '" << file_name <<
"'"
502 std::ostream *os = &std::cout;
518 lf.
language->preprocess(infile, file_name, *os);
524 if(lf.
language->parse(infile, file_name))
544 std::ostream *os = &std::cout;
564 if(language.
parse(std::cin,
""))
575 const std::string &file_name,
588 log.
statistics() <<
"Writing binary format object '" << file_name <<
"'"
598 if(!outfile.is_open())
625 if(
parse(file_name, language_files))
636 if(language_files.
final(file_symbol_table))
642 return std::move(file_symbol_table);
649 warning_is_fatal(Werror),
652 cmdline.isset(
"export-function-local-symbols") ||
653 cmdline.isset(
"export-file-local-symbols")),
654 file_local_mangle_suffix(
655 cmdline.isset(
"mangle-suffix") ? cmdline.get_value(
"mangle-suffix") :
"")
665 <<
"The `--export-function-local-symbols` flag is deprecated. "
666 "Please use `--export-file-local-symbols` instead."
682 std::size_t count = 0;
685 if(f.second.body_available())
709 while(before != symbol_table_builder.
symbols.size())
711 before = symbol_table_builder.
symbols.size();
713 typedef std::set<irep_idt> symbols_sett;
714 symbols_sett symbols;
716 for(
const auto &named_symbol : symbol_table_builder.
symbols)
717 symbols.insert(named_symbol.first);
720 for(
const auto &symbol : symbols)
722 symbol_tablet::symbolst::const_iterator s_it =
723 symbol_table_builder.
symbols.find(symbol);
727 s_it->second.is_function() && !s_it->second.is_compiled() &&
728 s_it->second.value.is_not_nil())
741 for(
const auto &pair : symbol_table.
symbols)
743 const irep_idt &name=pair.second.name;
744 const typet &new_type=pair.second.type;
749 std::map<irep_idt, symbolt>::iterator old;
750 std::tie(old, inserted)=
written_macros.insert({name, pair.second});
752 if(!inserted && old->second.type!=new_type)
754 log.
error() <<
"Incompatible CPROVER macro symbol types:" <<
'\n'
755 << old->second.type.pretty() <<
"(at " << old->second.location
758 << new_type.
pretty() <<
"(at " << pair.second.location <<
")"
Class that provides messages with a built-in verbosity 'level'.
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
std::list< std::string > defines
bool linking(symbol_tablet &dest_symbol_table, const symbol_tablet &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
optionalt< symbol_tablet > compile()
Parses source files and writes object files, or keeps the symbols in the symbol_table if not compilin...
virtual bool isset(char option) const
std::list< std::string > source_files
bool parse(const std::string &filename, language_filest &)
parses a source file (low-level parsing)
bool add_files_from_archive(const std::string &file_name, bool thin_archive)
extracts goto binaries from AR archive and add them as input files.
bool parse_stdin(languaget &)
parses a source file (low-level parsing)
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
static bool write_bin_object_file(const std::string &file_name, const goto_modelt &src_goto_model, bool validate_goto_model, message_handlert &message_handler)
Writes the goto functions of src_goto_model to a binary format object file.
mstreamt & status() const
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
bool doit()
reads and source and object files, compiles and links them into goto program objects.
int run(const std::string &what, const std::vector< std::string > &argv)
std::list< std::string > libraries
void mangle()
Mangle all file-local function symbols in the program.
struct configt::ansi_ct ansi_c
function_mapt function_map
Mangles the names in an entire program and its symbol table.
void add_compiler_specific_defines() const
std::map< irep_idt, symbolt > written_macros
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
const char * CBMC_VERSION
std::string output_file_object
std::list< std::string > object_files
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.
bool has_prefix(const std::string &s, const std::string &prefix)
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
std::string working_directory
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const std::string & id2string(const irep_idt &d)
const std::string file_local_mangle_suffix
String to include in all mangled names.
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
@ COMPILE_LINK_EXECUTABLE
compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
constructor
void convert_symbols(goto_modelt &)
std::string output_file_executable
optionalt< symbol_tablet > parse_source(const std::string &)
Parses and type checks a source file located at file_name.
#define INITIALIZE_FUNCTION
std::string get_value(char option) const
virtual bool parse(std::istream &instream, const std::string &path)=0
std::list< std::string > library_paths
virtual void set_message_handler(message_handlert &_message_handler)
language_filet & add_file(const std::string &filename)
const irep_idt & id() const
std::string object_file_extension
~compilet()
cleans up temporary files
std::unique_ptr< languaget > language
std::wstring widen(const char *s)
std::string override_language
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
nonstd::optional< T > optionalt
static std::size_t function_body_count(const goto_functionst &)
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
std::string output_directory_object
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
bool link(optionalt< symbol_tablet > &&symbol_table)
parses object files and links them
const bool keep_file_local
Whether to keep implementations of file-local symbols.
bool final(symbol_table_baset &symbol_table)
A collection of goto functions.
message_handlert & get_message_handler()
goto_functionst goto_functions
GOTO functions.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
static std::string binary(const constant_exprt &src)
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
static file_typet detect_file_type(const std::string &file_name, 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.
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
std::string get_current_working_directory()
std::string get_temporary_directory(const std::string &name_template)
std::list< std::string > tmp_dirs
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void set_current_path(const std::string &path)
Set working directory.
unsignedbv_typet size_type()
mstreamt & warning() const
void delete_directory(const std::string &path)
deletes all files in 'path' and then the directory itself
symbol_tablet symbol_table
Symbol table.
Mangle names of file-local functions to make them unique.
std::size_t get_message_count(unsigned level) const
mstreamt & statistics() const