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