CBMC
compile.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Compile and link source and object files.
4 
5 Author: CM Wintersteiger
6 
7 Date: June 2006
8 
9 \*******************************************************************/
10 
13 
14 #include "compile.h"
15 
16 #include <cstring>
17 #include <fstream>
18 #include <iostream>
19 
20 #include <util/cmdline.h>
21 #include <util/config.h>
22 #include <util/file_util.h>
23 #include <util/get_base_name.h>
24 #include <util/prefix.h>
25 #include <util/run.h>
27 #include <util/tempdir.h>
28 #include <util/tempfile.h>
29 #include <util/version.h>
30 
31 #ifdef _MSC_VER
32 # include <util/unicode.h>
33 #endif
34 
37 
42 
43 #include <langapi/language.h>
44 #include <langapi/language_file.h>
45 #include <langapi/mode.h>
46 
47 #include <linking/linking.h>
49 
50 #define DOTGRAPHSETTINGS "color=black;" \
51  "orientation=portrait;" \
52  "fontsize=20;"\
53  "compound=true;"\
54  "size=\"30,40\";"\
55  "ratio=compress;"
56 
61 {
63 
64  // Parse command line for source and object file names
65  for(const auto &arg : cmdline.args)
66  if(add_input_file(arg))
67  return true;
68 
69  for(const auto &library : libraries)
70  {
71  if(!find_library(library))
72  // GCC is going to complain if this doesn't exist
73  log.debug() << "Library not found: " << library << " (ignoring)"
74  << messaget::eom;
75  }
76 
77  log.statistics() << "No. of source files: " << source_files.size()
78  << messaget::eom;
79  log.statistics() << "No. of object files: " << object_files.size()
80  << messaget::eom;
81 
82  // Work through the given source files
83 
84  if(source_files.empty() && object_files.empty())
85  {
86  log.error() << "no input files" << messaget::eom;
87  return true;
88  }
89 
90  if(mode==LINK_LIBRARY && !source_files.empty())
91  {
92  log.error() << "cannot link source files" << messaget::eom;
93  return true;
94  }
95 
96  if(mode==PREPROCESS_ONLY && !object_files.empty())
97  {
98  log.error() << "cannot preprocess object files" << messaget::eom;
99  return true;
100  }
101 
102  const unsigned warnings_before =
104 
105  auto symbol_table_opt = compile();
106  if(!symbol_table_opt.has_value())
107  return true;
108 
109  if(mode==LINK_LIBRARY ||
110  mode==COMPILE_LINK ||
112  {
113  if(link(*symbol_table_opt))
114  return true;
115  }
116 
118  messaget::M_WARNING) != warnings_before;
119 }
120 
121 enum class file_typet
122 {
124  UNKNOWN,
125  SOURCE_FILE,
127  THIN_ARCHIVE,
128  GOTO_BINARY,
129  ELF_OBJECT
130 };
131 
133  const std::string &file_name,
134  message_handlert &message_handler)
135 {
136  // first of all, try to open the file
137  std::ifstream in(file_name);
138  if(!in)
140 
141  const std::string::size_type r = file_name.rfind('.');
142 
143  const std::string ext =
144  r == std::string::npos ? "" : file_name.substr(r + 1, file_name.length());
145 
146  if(
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")
150  {
152  }
153 
154  char hdr[8];
155  in.get(hdr, 8);
156  if((ext == "a" || ext == "o") && strncmp(hdr, "!<thin>", 8) == 0)
158 
159  if(ext == "a")
161 
162  if(is_goto_binary(file_name, message_handler))
164 
165  if(hdr[0] == 0x7f && memcmp(hdr + 1, "ELF", 3) == 0)
166  return file_typet::ELF_OBJECT;
167 
168  return file_typet::UNKNOWN;
169 }
170 
173 bool compilet::add_input_file(const std::string &file_name)
174 {
175  switch(detect_file_type(file_name, log.get_message_handler()))
176  {
178  log.warning() << "failed to open file '" << file_name
179  << "': " << std::strerror(errno) << messaget::eom;
180  return warning_is_fatal; // generously ignore unless -Werror
181 
182  case file_typet::UNKNOWN:
183  // unknown extension, not a goto binary, will silently ignore
184  log.debug() << "unknown file type in '" << file_name << "'"
185  << messaget::eom;
186  return false;
187 
189  // ELF file without goto-cc section, silently ignore
190  log.debug() << "ELF object without goto-cc section: '" << file_name << "'"
191  << messaget::eom;
192  return false;
193 
195  source_files.push_back(file_name);
196  return false;
197 
199  return add_files_from_archive(file_name, false);
200 
202  return add_files_from_archive(file_name, true);
203 
205  object_files.push_back(file_name);
206  return false;
207  }
208 
209  UNREACHABLE;
210 }
211 
215  const std::string &file_name,
216  bool thin_archive)
217 {
218  std::string tstr = working_directory;
219 
220  if(!thin_archive)
221  {
222  tstr = get_temporary_directory("goto-cc.XXXXXX");
223 
224  tmp_dirs.push_back(tstr);
225  set_current_path(tmp_dirs.back());
226 
227  // unpack now
228  int ret =
229  run("ar", {"ar", "x", concat_dir_file(working_directory, file_name)});
230  if(ret != 0)
231  {
232  log.error() << "Failed to extract archive " << file_name << messaget::eom;
233  return true;
234  }
235  }
236 
237  // add the files from "ar t"
238  temporary_filet tmp_file_out("", "");
239  int ret = run(
240  "ar",
241  {"ar", "t", concat_dir_file(working_directory, file_name)},
242  "",
243  tmp_file_out(),
244  "");
245  if(ret != 0)
246  {
247  log.error() << "Failed to list archive " << file_name << messaget::eom;
248  return true;
249  }
250 
251  std::ifstream in(tmp_file_out());
252  std::string line;
253 
254  while(!in.fail() && std::getline(in, line))
255  {
256  std::string t = concat_dir_file(tstr, line);
257 
259  object_files.push_back(t);
260  else
261  log.debug() << "Object file is not a goto binary: " << line
262  << messaget::eom;
263  }
264 
265  if(!thin_archive)
267 
268  return false;
269 }
270 
274 bool compilet::find_library(const std::string &name)
275 {
276  std::string library_file_name;
277 
278  for(const auto &library_path : library_paths)
279  {
280  library_file_name = concat_dir_file(library_path, "lib" + name + ".a");
281 
282  std::ifstream in(library_file_name);
283 
284  if(in.is_open())
285  return !add_input_file(library_file_name);
286  else
287  {
288  library_file_name = concat_dir_file(library_path, "lib" + name + ".so");
289 
290  switch(detect_file_type(library_file_name, log.get_message_handler()))
291  {
293  return !add_input_file(library_file_name);
294 
296  log.warning() << "Warning: Cannot read ELF library "
297  << library_file_name << messaget::eom;
298  return warning_is_fatal;
299 
304  case file_typet::UNKNOWN:
305  break;
306  }
307  }
308  }
309 
310  return false;
311 }
312 
316 {
317  // "compile" hitherto uncompiled functions
318  log.statistics() << "Compiling functions" << messaget::eom;
319  goto_modelt goto_model;
320  if(symbol_table.has_value())
321  goto_model.symbol_table = std::move(*symbol_table);
322  convert_symbols(goto_model);
323 
324  // parse object files
326  return true;
327 
328  // produce entry point?
329 
331  {
332  // new symbols may have been added to a previously linked file
333  // make sure a new entry point is created that contains all
334  // static initializers
336 
338  goto_model.goto_functions.function_map.erase(
340 
341  const bool error = ansi_c_entry_point(
342  goto_model.symbol_table,
345 
346  if(error)
347  return true;
348 
349  // entry_point may (should) add some more functions.
350  convert_symbols(goto_model);
351  }
352 
353  if(keep_file_local)
354  {
357  mangler.mangle();
358  }
359 
361  return true;
362 
363  return add_written_cprover_symbols(goto_model.symbol_table);
364 }
365 
370 {
371  symbol_tablet symbol_table;
372 
373  while(!source_files.empty())
374  {
375  std::string file_name=source_files.front();
376  source_files.pop_front();
377 
378  // Visual Studio always prints the name of the file it's doing
379  // onto stdout. The name of the directory is stripped.
380  if(echo_file_name)
381  std::cout << get_base_name(file_name, false) << '\n' << std::flush;
382 
383  auto file_symbol_table = parse_source(file_name);
384 
385  if(!file_symbol_table.has_value())
386  {
387  const std::string &debug_outfile=
388  cmdline.get_value("print-rejected-preprocessed-source");
389  if(!debug_outfile.empty())
390  {
391  std::ifstream in(file_name, std::ios::binary);
392  std::ofstream out(debug_outfile, std::ios::binary);
393  out << in.rdbuf();
394  log.warning() << "Failed sources in " << debug_outfile << messaget::eom;
395  }
396 
397  return {}; // parser/typecheck error
398  }
399 
401  {
402  // output an object file for every source file
403 
404  // "compile" functions
405  goto_modelt file_goto_model;
406  file_goto_model.symbol_table = std::move(*file_symbol_table);
407  convert_symbols(file_goto_model);
408 
409  std::string cfn;
410 
411  if(output_file_object.empty())
412  {
413  const std::string file_name_with_obj_ext =
414  get_base_name(file_name, true) + "." + object_file_extension;
415 
416  if(!output_directory_object.empty())
417  cfn = concat_dir_file(output_directory_object, file_name_with_obj_ext);
418  else
419  cfn = file_name_with_obj_ext;
420  }
421  else
422  cfn = output_file_object;
423 
424  if(keep_file_local)
425  {
427  log.get_message_handler(), file_goto_model, file_local_mangle_suffix);
428  mangler.mangle();
429  }
430 
431  if(write_bin_object_file(cfn, file_goto_model))
432  return {};
433 
434  if(add_written_cprover_symbols(file_goto_model.symbol_table))
435  return {};
436  }
437  else
438  {
439  if(linking(symbol_table, *file_symbol_table, log.get_message_handler()))
440  {
441  return {};
442  }
443  }
444  }
445 
446  return std::move(symbol_table);
447 }
448 
452  const std::string &file_name,
453  language_filest &language_files)
454 {
455  std::unique_ptr<languaget> languagep;
456 
457  // Using '-x', the type of a file can be overridden;
458  // otherwise, it's guessed from the extension.
459 
460  if(!override_language.empty())
461  {
462  if(override_language=="c++" || override_language=="c++-header")
463  languagep = get_language_from_mode(ID_cpp);
464  else
465  languagep = get_language_from_mode(ID_C);
466  }
467  else if(file_name != "-")
468  languagep=get_language_from_filename(file_name);
469 
470  if(languagep==nullptr)
471  {
472  log.error() << "failed to figure out type of file '" << file_name << "'"
473  << messaget::eom;
474  return true;
475  }
476 
478 
479  if(file_name == "-")
480  return parse_stdin(*languagep);
481 
482 #ifdef _MSC_VER
483  std::ifstream infile(widen(file_name));
484 #else
485  std::ifstream infile(file_name);
486 #endif
487 
488  if(!infile)
489  {
490  log.error() << "failed to open input file '" << file_name << "'"
491  << messaget::eom;
492  return true;
493  }
494 
495  language_filet &lf=language_files.add_file(file_name);
496  lf.language=std::move(languagep);
497 
498  if(mode==PREPROCESS_ONLY)
499  {
500  log.statistics() << "Preprocessing: " << file_name << messaget::eom;
501 
502  std::ostream *os = &std::cout;
503  std::ofstream ofs;
504 
505  if(cmdline.isset('o'))
506  {
507  ofs.open(cmdline.get_value('o'));
508  os = &ofs;
509 
510  if(!ofs.is_open())
511  {
512  log.error() << "failed to open output file '" << cmdline.get_value('o')
513  << "'" << messaget::eom;
514  return true;
515  }
516  }
517 
518  lf.language->preprocess(infile, file_name, *os);
519  }
520  else
521  {
522  log.statistics() << "Parsing: " << file_name << messaget::eom;
523 
524  if(lf.language->parse(infile, file_name))
525  {
526  log.error() << "PARSING ERROR" << messaget::eom;
527  return true;
528  }
529  }
530 
531  lf.get_modules();
532  return false;
533 }
534 
539 {
540  log.statistics() << "Parsing: (stdin)" << messaget::eom;
541 
542  if(mode==PREPROCESS_ONLY)
543  {
544  std::ostream *os = &std::cout;
545  std::ofstream ofs;
546 
547  if(cmdline.isset('o'))
548  {
549  ofs.open(cmdline.get_value('o'));
550  os = &ofs;
551 
552  if(!ofs.is_open())
553  {
554  log.error() << "failed to open output file '" << cmdline.get_value('o')
555  << "'" << messaget::eom;
556  return true;
557  }
558  }
559 
560  language.preprocess(std::cin, "", *os);
561  }
562  else
563  {
564  if(language.parse(std::cin, ""))
565  {
566  log.error() << "PARSING ERROR" << messaget::eom;
567  return true;
568  }
569  }
570 
571  return false;
572 }
573 
575  const std::string &file_name,
576  const goto_modelt &src_goto_model,
577  bool validate_goto_model,
578  message_handlert &message_handler)
579 {
580  messaget log(message_handler);
581 
583  {
584  log.status() << "Validating goto model" << messaget::eom;
585  src_goto_model.validate();
586  }
587 
588  log.statistics() << "Writing binary format object '" << file_name << "'"
589  << messaget::eom;
590 
591  // symbols
592  log.statistics() << "Symbols in table: "
593  << src_goto_model.symbol_table.symbols.size()
594  << messaget::eom;
595 
596  std::ofstream outfile(file_name, std::ios::binary);
597 
598  if(!outfile.is_open())
599  {
600  log.error() << "Error opening file '" << file_name << "'" << messaget::eom;
601  return true;
602  }
603 
604  if(write_goto_binary(outfile, src_goto_model))
605  return true;
606 
607  const auto cnt = function_body_count(src_goto_model.goto_functions);
608 
609  log.statistics() << "Functions: "
610  << src_goto_model.goto_functions.function_map.size() << "; "
611  << cnt << " have a body." << messaget::eom;
612 
613  outfile.close();
614 
615  return false;
616 }
617 
621 {
622  language_filest language_files;
623  language_files.set_message_handler(log.get_message_handler());
624 
625  if(parse(file_name, language_files))
626  return {};
627 
628  // we just typecheck one file here
629  symbol_tablet file_symbol_table;
630  if(language_files.typecheck(file_symbol_table, keep_file_local))
631  {
632  log.error() << "CONVERSION ERROR" << messaget::eom;
633  return {};
634  }
635 
636  if(language_files.final(file_symbol_table))
637  {
638  log.error() << "CONVERSION ERROR" << messaget::eom;
639  return {};
640  }
641 
642  return std::move(file_symbol_table);
643 }
644 
646 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
647  : log(mh),
648  cmdline(_cmdline),
649  warning_is_fatal(Werror),
650  keep_file_local(
651  // function-local is the old name and is still in use, but is misleading
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") : "")
656 {
658  echo_file_name=false;
659  wrote_object=false;
661 
662  if(cmdline.isset("export-function-local-symbols"))
663  {
664  log.warning()
665  << "The `--export-function-local-symbols` flag is deprecated. "
666  "Please use `--export-file-local-symbols` instead."
667  << messaget::eom;
668  }
669 }
670 
673 {
674  // clean up temp dirs
675 
676  for(const auto &dir : tmp_dirs)
677  delete_directory(dir);
678 }
679 
680 std::size_t compilet::function_body_count(const goto_functionst &functions)
681 {
682  std::size_t count = 0;
683 
684  for(const auto &f : functions.function_map)
685  if(f.second.body_available())
686  count++;
687 
688  return count;
689 }
690 
692 {
693  config.ansi_c.defines.push_back(
694  std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION);
695 }
696 
698 {
699  symbol_table_buildert symbol_table_builder =
701 
702  goto_convert_functionst converter(
703  symbol_table_builder, log.get_message_handler());
704 
705  // the compilation may add symbols!
706 
708 
709  while(before != symbol_table_builder.symbols.size())
710  {
711  before = symbol_table_builder.symbols.size();
712 
713  typedef std::set<irep_idt> symbols_sett;
714  symbols_sett symbols;
715 
716  for(const auto &named_symbol : symbol_table_builder.symbols)
717  symbols.insert(named_symbol.first);
718 
719  // the symbol table iterators aren't stable
720  for(const auto &symbol : symbols)
721  {
722  symbol_tablet::symbolst::const_iterator s_it =
723  symbol_table_builder.symbols.find(symbol);
724  CHECK_RETURN(s_it != symbol_table_builder.symbols.end());
725 
726  if(
727  s_it->second.is_function() && !s_it->second.is_compiled() &&
728  s_it->second.value.is_not_nil())
729  {
730  log.debug() << "Compiling " << s_it->first << messaget::eom;
731  converter.convert_function(
732  s_it->first, goto_model.goto_functions.function_map[s_it->first]);
733  symbol_table_builder.get_writeable_ref(symbol).set_compiled();
734  }
735  }
736  }
737 }
738 
740 {
741  for(const auto &pair : symbol_table.symbols)
742  {
743  const irep_idt &name=pair.second.name;
744  const typet &new_type=pair.second.type;
745  if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code))
746  continue;
747 
748  bool inserted;
749  std::map<irep_idt, symbolt>::iterator old;
750  std::tie(old, inserted)=written_macros.insert({name, pair.second});
751 
752  if(!inserted && old->second.type!=new_type)
753  {
754  log.error() << "Incompatible CPROVER macro symbol types:" << '\n'
755  << old->second.type.pretty() << "(at " << old->second.location
756  << ")\n"
757  << "and\n"
758  << new_type.pretty() << "(at " << pair.second.location << ")"
759  << messaget::eom;
760  return true;
761  }
762  }
763  return false;
764 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
cmdlinet::args
argst args
Definition: cmdline.h:145
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
get_base_name
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Definition: get_base_name.cpp:16
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:250
tempfile.h
compilet::wrote_object
bool wrote_object
Definition: compile.h:151
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
compilet::echo_file_name
bool echo_file_name
Definition: compile.h:34
linking
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...
Definition: linking.cpp:1475
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:33
compilet::compile
optionalt< symbol_tablet > compile()
Parses source files and writes object files, or keeps the symbols in the symbol_table if not compilin...
Definition: compile.cpp:369
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:30
compilet::source_files
std::list< std::string > source_files
Definition: compile.h:46
ansi_c_entry_point.h
file_typet::GOTO_BINARY
@ GOTO_BINARY
compilet::parse
bool parse(const std::string &filename, language_filest &)
parses a source file (low-level parsing)
Definition: compile.cpp:451
file_util.h
compilet::add_files_from_archive
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.
Definition: compile.cpp:214
compilet::parse_stdin
bool parse_stdin(languaget &)
parses a source file (low-level parsing)
Definition: compile.cpp:538
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
typet
The type of an expression, extends irept.
Definition: type.h:28
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
Definition: language_file.cpp:83
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
compilet::write_bin_object_file
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.
Definition: compile.cpp:574
messaget::status
mstreamt & status() const
Definition: message.h:414
write_goto_binary
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.
Definition: write_goto_binary.cpp:24
goto_convert_functionst::convert_function
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
Definition: goto_convert_functions.cpp:142
prefix.h
language_filet
Definition: language_file.h:41
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
compilet::doit
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:60
run
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:48
compilet::libraries
std::list< std::string > libraries
Definition: compile.h:48
goto_modelt
Definition: goto_model.h:25
mode.h
messaget::eom
static eomt eom
Definition: message.h:297
function_name_manglert::mangle
void mangle()
Mangle all file-local function symbols in the program.
Definition: name_mangler.h:49
configt::ansi_c
struct configt::ansi_ct ansi_c
run.h
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
version.h
tempdir.h
compilet::cmdline
cmdlinet & cmdline
Definition: compile.h:110
function_name_manglert
Mangles the names in an entire program and its symbol table.
Definition: name_mangler.h:30
compilet::validate_goto_model
bool validate_goto_model
Definition: compile.h:35
file_typet::NORMAL_ARCHIVE
@ NORMAL_ARCHIVE
write_goto_binary.h
file_typet::FAILED_TO_OPEN_FILE
@ FAILED_TO_OPEN_FILE
compilet::COMPILE_LINK
@ COMPILE_LINK
Definition: compile.h:41
compilet::add_compiler_specific_defines
void add_compiler_specific_defines() const
Definition: compile.cpp:691
compilet::written_macros
std::map< irep_idt, symbolt > written_macros
Definition: compile.h:144
get_language_from_filename
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Definition: mode.cpp:102
cmdlinet
Definition: cmdline.h:20
CBMC_VERSION
const char * CBMC_VERSION
compilet::output_file_object
std::string output_file_object
Definition: compile.h:54
compilet::mode
enum compilet::@3 mode
compilet::object_files
std::list< std::string > object_files
Definition: compile.h:47
c_object_factory_parameters.h
messaget::error
mstreamt & error() const
Definition: message.h:399
read_objects_and_link
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.
Definition: read_goto_binary.cpp:291
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
compilet::add_written_cprover_symbols
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
Definition: compile.cpp:739
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:14
file_typet::UNKNOWN
@ UNKNOWN
compilet::working_directory
std::string working_directory
Definition: compile.h:103
symbolt::set_compiled
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
Definition: symbol.h:114
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
compilet::file_local_mangle_suffix
const std::string file_local_mangle_suffix
String to include in all mangled names.
Definition: compile.h:117
concat_dir_file
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:159
compilet::COMPILE_LINK_EXECUTABLE
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:42
compilet::compilet
compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
constructor
Definition: compile.cpp:646
compilet::convert_symbols
void convert_symbols(goto_modelt &)
Definition: compile.cpp:697
compilet::output_file_executable
std::string output_file_executable
Definition: compile.h:51
compilet::parse_source
optionalt< symbol_tablet > parse_source(const std::string &)
Parses and type checks a source file located at file_name.
Definition: compile.cpp:620
goto_convert_functionst
Definition: goto_convert_functions.h:40
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:48
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
compilet::library_paths
std::list< std::string > library_paths
Definition: compile.h:45
compile.h
language.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
linking.h
language_filest::add_file
language_filet & add_file(const std::string &filename)
Definition: language_file.h:77
irept::id
const irep_idt & id() const
Definition: irep.h:396
compilet::object_file_extension
std::string object_file_extension
Definition: compile.h:50
message_handlert
Definition: message.h:27
get_base_name.h
file_typet::ELF_OBJECT
@ ELF_OBJECT
file_typet::SOURCE_FILE
@ SOURCE_FILE
compilet::warning_is_fatal
bool warning_is_fatal
Definition: compile.h:111
compilet::~compilet
~compilet()
cleans up temporary files
Definition: compile.cpp:672
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:47
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:48
file_typet::THIN_ARCHIVE
@ THIN_ARCHIVE
read_goto_binary.h
compilet::override_language
std::string override_language
Definition: compile.h:104
symbol_table_baset::remove
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Definition: symbol_table_base.cpp:27
ansi_c_entry_point
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Definition: ansi_c_entry_point.cpp:106
compilet::ASSEMBLE_ONLY
@ ASSEMBLE_ONLY
Definition: compile.h:39
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
compilet::log
messaget log
Definition: compile.h:109
compilet::function_body_count
static std::size_t function_body_count(const goto_functionst &)
Definition: compile.cpp:680
compilet::add_input_file
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition: compile.cpp:173
compilet::output_directory_object
std::string output_directory_object
Definition: compile.h:54
config
configt config
Definition: config.cpp:25
compilet::find_library
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
Definition: compile.cpp:274
compilet::link
bool link(optionalt< symbol_tablet > &&symbol_table)
parses object files and links them
Definition: compile.cpp:315
compilet::keep_file_local
const bool keep_file_local
Whether to keep implementations of file-local symbols.
Definition: compile.h:114
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:178
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
compilet::COMPILE_ONLY
@ COMPILE_ONLY
Definition: compile.h:38
messaget::M_WARNING
@ M_WARNING
Definition: message.h:170
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
cmdline.h
symbol_table_buildert::wrap
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
Definition: symbol_table_builder.h:42
symbol_table_buildert
Author: Diffblue Ltd.
Definition: symbol_table_builder.h:13
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:189
validate_goto_model
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
Definition: validate_goto_model.cpp:130
compilet::LINK_LIBRARY
@ LINK_LIBRARY
Definition: compile.h:40
unicode.h
languaget
Definition: language.h:37
is_goto_binary
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Definition: read_goto_binary.cpp:192
detect_file_type
static file_typet detect_file_type(const std::string &file_name, message_handlert &message_handler)
Definition: compile.cpp:132
config.h
goto_modelt::validate
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.
Definition: goto_model.h:98
languaget::preprocess
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:47
get_current_working_directory
std::string get_current_working_directory()
Definition: file_util.cpp:51
get_temporary_directory
std::string get_temporary_directory(const std::string &name_template)
Definition: tempdir.cpp:42
compilet::tmp_dirs
std::list< std::string > tmp_dirs
Definition: compile.h:106
r
static int8_t r
Definition: irep_hash.h:60
messaget::debug
mstreamt & debug() const
Definition: message.h:429
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
set_current_path
void set_current_path(const std::string &path)
Set working directory.
Definition: file_util.cpp:82
goto_convert_functions.h
static_lifetime_init.h
compilet::PREPROCESS_ONLY
@ PREPROCESS_ONLY
Definition: compile.h:37
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:68
file_typet
file_typet
Definition: compile.cpp:121
symbol_table_builder.h
messaget::warning
mstreamt & warning() const
Definition: message.h:404
delete_directory
void delete_directory(const std::string &path)
deletes all files in 'path' and then the directory itself
Definition: file_util.cpp:118
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
name_mangler.h
Mangle names of file-local functions to make them unique.
temporary_filet
Definition: tempfile.h:23
message_handlert::get_message_count
std::size_t get_message_count(unsigned level) const
Definition: message.h:56
language_file.h
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
language_filest
Definition: language_file.h:62