41 #define DOTGRAPHSETTINGS "color=black;" \ 42 "orientation=portrait;" \ 50 #if defined(__linux__) || \ 51 defined(__FreeBSD_kernel__) || \ 53 defined(__unix__) || \ 54 defined(__CYGWIN__) || \ 64 #define pclose _pclose 81 for(std::list<std::string>::const_iterator it =
libraries.begin();
87 debug() <<
"Library not found: " << *it <<
" (ignoring)" <<
eom;
103 error() <<
"cannot link source files" <<
eom;
109 error() <<
"cannot preprocess object files" <<
eom;
113 const unsigned warnings_before=
148 std::ifstream in(file_name);
154 const std::string ext =
155 r == std::string::npos ?
"" : file_name.substr(
r + 1, file_name.length());
158 ext ==
"c" || ext ==
"cc" || ext ==
"cp" || ext ==
"cpp" || ext ==
"CPP" ||
159 ext ==
"c++" || ext ==
"C" || ext ==
"i" || ext ==
"ii" || ext ==
"class" ||
160 ext ==
"jar" || ext ==
"jsil")
167 if((ext ==
"a" || ext ==
"o") && strncmp(hdr,
"!<thin>", 8) == 0)
176 if(hdr[0] == 0x7f && memcmp(hdr + 1,
"ELF", 3) == 0)
189 warning() <<
"failed to open file `" << file_name
190 <<
"': " << std::strerror(errno) <<
eom;
195 debug() <<
"unknown file type in `" << file_name <<
"'" <<
eom;
200 debug() <<
"ELF object without goto-cc section: `" << file_name <<
"'" 225 const std::string &file_name,
228 std::stringstream cmd;
239 error() <<
"Cannot create temporary directory" <<
eom;
244 if(chdir(
tmp_dirs.back().c_str())!=0)
246 error() <<
"Cannot switch to temporary directory" <<
eom;
253 stream=popen(cmd.str().c_str(),
"r");
263 stream = popen(cmd.str().c_str(),
"r");
265 if(stream !=
nullptr)
269 while((ch = fgetc(stream)) != EOF)
273 line +=
static_cast<char>(ch);
282 debug() <<
"Object file is not a goto binary: " << line <<
eom;
292 error() <<
"Could not change back to working directory" <<
eom;
304 for(std::list<std::string>::const_iterator
315 std::ifstream in(tmp+name+
".a");
321 std::string libname=tmp+name+
".so";
329 warning() <<
"Warning: Cannot read ELF library " << libname <<
eom;
396 std::cout <<
get_base_name(file_name,
false) <<
'\n' << std::flush;
402 const std::string &debug_outfile=
404 if(!debug_outfile.empty())
406 std::ifstream in(file_name, std::ios::binary);
407 std::ofstream out(debug_outfile, std::ios::binary);
409 warning() <<
"Failed sources in " << debug_outfile <<
eom;
426 const std::string file_name_with_obj_ext =
432 cfn = file_name_with_obj_ext;
459 std::ifstream infile(
widen(file_name));
461 std::ifstream infile(file_name);
466 error() <<
"failed to open input file `" << file_name <<
"'" <<
eom;
470 std::unique_ptr<languaget> languagep;
485 if(languagep==
nullptr)
487 error() <<
"failed to figure out type of file `" << file_name <<
"'" <<
eom;
500 std::ostream *os = &std::cout;
510 error() <<
"failed to open output file `" 516 lf.
language->preprocess(infile, file_name, *os);
522 if(lf.
language->parse(infile, file_name))
546 std::ostream *os = &std::cout;
556 error() <<
"failed to open output file `" 566 if(language.
parse(std::cin,
""))
582 const std::string &file_name,
594 const std::string &file_name,
598 statistics() <<
"Writing binary format object `" 599 << file_name <<
"'" <<
eom;
605 std::ofstream outfile(file_name, std::ios::binary);
607 if(!outfile.is_open())
609 error() <<
"Error opening file `" << file_name <<
"'" <<
eom;
619 <<
"; " << cnt <<
" have a body." <<
eom;
653 warning_is_fatal(Werror)
667 for(std::list<std::string>::const_iterator it =
tmp_dirs.begin();
677 for(goto_functionst::function_mapt::const_iterator it=
681 if(it->second.body_available())
705 typedef std::set<irep_idt> symbols_sett;
706 symbols_sett symbols;
709 symbols.insert(named_symbol.first);
712 for(symbols_sett::const_iterator
717 symbol_tablet::symbolst::const_iterator s_it=
721 if(s_it->second.type.id()==ID_code &&
722 !s_it->second.is_macro &&
723 !s_it->second.is_type &&
724 s_it->second.value.id()!=
"compiled" &&
725 s_it->second.value.is_not_nil())
727 debug() <<
"Compiling " << s_it->first <<
eom;
739 const irep_idt &name=pair.second.name;
740 const typet &new_type=pair.second.type;
745 std::map<irep_idt, symbolt>::iterator old;
746 std::tie(old, inserted)=
written_macros.insert({name, pair.second});
748 if(!inserted && old->second.type!=new_type)
750 error() <<
"Incompatible CPROVER macro symbol types:" <<
eom 751 << old->second.type.pretty() <<
"(at " << old->second.location
753 <<
"(at " << pair.second.location <<
")" <<
eom;
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
The type of an expression.
symbol_tablet symbol_table
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
struct configt::ansi_ct ansi_c
std::string output_file_executable
compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror)
constructor
const std::string & id2string(const irep_idt &d)
Globally accessible architectural configuration.
virtual void clear() override
static file_typet detect_file_type(const std::string &file_name)
std::wstring widen(const char *s)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
std::list< std::string > tmp_dirs
std::list< std::string > libraries
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::list< std::string > defines
bool is_goto_binary(const std::string &filename)
std::list< std::string > library_paths
language_filest language_files
language_filet & add_file(const std::string &filename)
exprt value
Initial value of symbol.
std::string get_value(char option) const
function_mapt function_map
const cmdlinet & _cmdline
unsignedbv_typet size_type()
bool doit()
reads and source and object files, compiles and links them into goto program objects.
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
static mstreamt & eom(mstreamt &m)
bool parse(std::istream &instream, const std::string &path) override
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
bool write_bin_object_file(const std::string &, const symbol_tablet &, goto_functionst &)
writes the goto functions in the function table to a binary format object file.
std::string get_current_working_directory()
bool parse_stdin()
parses a source file (low-level parsing)
mstreamt & warning() const
std::unique_ptr< languaget > language
const irep_idt & id() const
virtual bool isset(char option) const
bool compile()
parses source files and writes object files, or keeps the symbols in the symbol_table depending on th...
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
bool parse_source(const std::string &)
parses a source file
#define INITIALIZE_FUNCTION
goto_functionst compiled_functions
void delete_directory(const std::string &path)
deletes all files in 'path' and then the directory itself
bool has_prefix(const std::string &s, const std::string &prefix)
virtual void set_message_handler(message_handlert &_message_handler)
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::string working_directory
unsigned function_body_count(const goto_functionst &) const
bool write_object_file(const std::string &, const symbol_tablet &, goto_functionst &)
writes the goto functions in the function table to a binary format object file.
std::map< irep_idt, symbolt > written_macros
Compile and link source and object files.
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.
message_handlert & get_message_handler()
Goto Programs with Functions.
static irep_idt entry_point()
std::string get_temporary_directory(const std::string &name_template)
void convert_symbols(goto_functionst &dest)
const char * CBMC_VERSION
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Base class for all expressions.
std::string object_file_extension
std::list< std::string > source_files
bool has_suffix(const std::string &s, const std::string &suffix)
std::list< std::string > object_files
void remove_file(const std::string &filename)
bool link()
parses object files and links them
void add_compiler_specific_defines(class configt &config) const
std::string output_directory_object
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file
std::string override_language
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
std::string output_file_object
mstreamt & statistics() const
~compilet()
cleans up temporary files
unsigned get_message_count(unsigned level) const