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 <util/cmdline.h>
17 #include <util/config.h>
18 #include <util/get_base_name.h>
19 #include <util/run.h>
21 #include <util/tempdir.h>
22 #include <util/tempfile.h>
23 #include <util/unicode.h>
24 #include <util/version.h>
25 
30 
33 #include <langapi/language.h>
34 #include <langapi/language_file.h>
35 #include <langapi/mode.h>
36 #include <linking/linking.h>
38 
39 #include <cstring>
40 #include <filesystem>
41 #include <fstream>
42 #include <iostream>
43 
44 #define DOTGRAPHSETTINGS "color=black;" \
45  "orientation=portrait;" \
46  "fontsize=20;"\
47  "compound=true;"\
48  "size=\"30,40\";"\
49  "ratio=compress;"
50 
55 {
57 
58  // Parse command line for source and object file names
59  for(const auto &arg : cmdline.args)
60  if(add_input_file(arg))
61  return true;
62 
63  for(const auto &library : libraries)
64  {
65  if(!find_library(library))
66  // GCC is going to complain if this doesn't exist
67  log.debug() << "Library not found: " << library << " (ignoring)"
68  << messaget::eom;
69  }
70 
71  log.statistics() << "No. of source files: " << source_files.size()
72  << messaget::eom;
73  log.statistics() << "No. of object files: " << object_files.size()
74  << messaget::eom;
75 
76  // Work through the given source files
77 
78  if(source_files.empty() && object_files.empty())
79  {
80  log.error() << "no input files" << messaget::eom;
81  return true;
82  }
83 
84  if(mode==LINK_LIBRARY && !source_files.empty())
85  {
86  log.error() << "cannot link source files" << messaget::eom;
87  return true;
88  }
89 
90  if(mode==PREPROCESS_ONLY && !object_files.empty())
91  {
92  log.error() << "cannot preprocess object files" << messaget::eom;
93  return true;
94  }
95 
96  const unsigned warnings_before =
98 
99  auto symbol_table_opt = compile();
100  if(!symbol_table_opt.has_value())
101  return true;
102 
103  if(mode==LINK_LIBRARY ||
104  mode==COMPILE_LINK ||
106  {
107  if(link(*symbol_table_opt))
108  return true;
109  }
110 
112  messaget::M_WARNING) != warnings_before;
113 }
114 
115 enum class file_typet
116 {
118  UNKNOWN,
119  SOURCE_FILE,
121  THIN_ARCHIVE,
122  GOTO_BINARY,
123  ELF_OBJECT
124 };
125 
127  const std::string &file_name,
128  message_handlert &message_handler)
129 {
130  // first of all, try to open the file
131  std::ifstream in(file_name);
132  if(!in)
134 
135  const std::string::size_type r = file_name.rfind('.');
136 
137  const std::string ext =
138  r == std::string::npos ? "" : file_name.substr(r + 1, file_name.length());
139 
140  if(
141  ext == "c" || ext == "cc" || ext == "cp" || ext == "cpp" || ext == "CPP" ||
142  ext == "c++" || ext == "C" || ext == "i" || ext == "ii" || ext == "class" ||
143  ext == "jar")
144  {
146  }
147 
148  char hdr[8];
149  in.get(hdr, 8);
150  if((ext == "a" || ext == "o") && strncmp(hdr, "!<thin>", 8) == 0)
152 
153  if(ext == "a")
155 
156  if(is_goto_binary(file_name, message_handler))
158 
159  if(hdr[0] == 0x7f && memcmp(hdr + 1, "ELF", 3) == 0)
160  return file_typet::ELF_OBJECT;
161 
162  return file_typet::UNKNOWN;
163 }
164 
167 bool compilet::add_input_file(const std::string &file_name)
168 {
169  switch(detect_file_type(file_name, log.get_message_handler()))
170  {
172  log.warning() << "failed to open file '" << file_name
173  << "': " << std::strerror(errno) << messaget::eom;
174  return warning_is_fatal; // generously ignore unless -Werror
175 
176  case file_typet::UNKNOWN:
177  // unknown extension, not a goto binary, will silently ignore
178  log.debug() << "unknown file type in '" << file_name << "'"
179  << messaget::eom;
180  return false;
181 
183  // ELF file without goto-cc section, silently ignore
184  log.debug() << "ELF object without goto-cc section: '" << file_name << "'"
185  << messaget::eom;
186  return false;
187 
189  source_files.push_back(file_name);
190  return false;
191 
193  return add_files_from_archive(file_name, false);
194 
196  return add_files_from_archive(file_name, true);
197 
199  object_files.push_back(file_name);
200  return false;
201  }
202 
203  UNREACHABLE;
204 }
205 
209  const std::string &file_name,
210  bool thin_archive)
211 {
212  std::string tstr = working_directory;
213 
214  if(!thin_archive)
215  {
216  tstr = get_temporary_directory("goto-cc.XXXXXX");
217 
218  tmp_dirs.push_back(tstr);
219  std::filesystem::current_path(tmp_dirs.back());
220 
221  // unpack now
222  int ret = run(
223  "ar",
224  {"ar",
225  "x",
226  std::filesystem::path(working_directory).append(file_name).string()});
227  if(ret != 0)
228  {
229  log.error() << "Failed to extract archive " << file_name << messaget::eom;
230  return true;
231  }
232  }
233 
234  // add the files from "ar t"
235  temporary_filet tmp_file_out("", "");
236  int ret = run(
237  "ar",
238  {"ar",
239  "t",
240  std::filesystem::path(working_directory).append(file_name).string()},
241  "",
242  tmp_file_out(),
243  "");
244  if(ret != 0)
245  {
246  log.error() << "Failed to list archive " << file_name << messaget::eom;
247  return true;
248  }
249 
250  std::ifstream in(tmp_file_out());
251  std::string line;
252 
253  while(!in.fail() && std::getline(in, line))
254  {
255  std::string t = std::filesystem::path(tstr).append(line).string();
256 
258  object_files.push_back(t);
259  else
260  log.debug() << "Object file is not a goto binary: " << line
261  << messaget::eom;
262  }
263 
264  if(!thin_archive)
265  std::filesystem::current_path(working_directory);
266 
267  return false;
268 }
269 
273 bool compilet::find_library(const std::string &name)
274 {
275  std::string library_file_name;
276 
277  for(const auto &library_path : library_paths)
278  {
279  library_file_name =
280  std::filesystem::path(library_path).append("lib" + name + ".a").string();
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 = std::filesystem::path(library_path)
289  .append("lib" + name + ".so")
290  .string();
291 
292  switch(detect_file_type(library_file_name, log.get_message_handler()))
293  {
295  return !add_input_file(library_file_name);
296 
298  log.warning() << "Warning: Cannot read ELF library "
299  << library_file_name << messaget::eom;
300  return warning_is_fatal;
301 
306  case file_typet::UNKNOWN:
307  break;
308  }
309  }
310  }
311 
312  return false;
313 }
314 
317 bool compilet::link(std::optional<symbol_tablet> &&symbol_table)
318 {
319  // "compile" hitherto uncompiled functions
320  log.statistics() << "Compiling functions" << messaget::eom;
321  goto_modelt goto_model;
322  if(symbol_table.has_value())
323  goto_model.symbol_table = std::move(*symbol_table);
324  convert_symbols(goto_model);
325 
326  // parse object files
328  return true;
329 
330  // produce entry point?
331 
333  {
334  // new symbols may have been added to a previously linked file
335  // make sure a new entry point is created that contains all
336  // static initializers
338 
340  goto_model.goto_functions.function_map.erase(
342 
343  const bool error = ansi_c_entry_point(
344  goto_model.symbol_table,
347 
348  if(error)
349  return true;
350 
351  // entry_point may (should) add some more functions.
352  convert_symbols(goto_model);
353  }
354 
355  if(keep_file_local)
356  {
359  mangler.mangle();
360  }
361 
363  return true;
364 
365  return add_written_cprover_symbols(goto_model.symbol_table);
366 }
367 
371 std::optional<symbol_tablet> compilet::compile()
372 {
373  symbol_tablet symbol_table;
374 
375  while(!source_files.empty())
376  {
377  std::string file_name=source_files.front();
378  source_files.pop_front();
379 
380  // Visual Studio always prints the name of the file it's doing
381  // onto stdout. The name of the directory is stripped.
382  if(echo_file_name)
383  std::cout << get_base_name(file_name, false) << '\n' << std::flush;
384 
385  auto file_symbol_table = parse_source(file_name);
386 
387  if(!file_symbol_table.has_value())
388  {
389  const std::string &debug_outfile=
390  cmdline.get_value("print-rejected-preprocessed-source");
391  if(!debug_outfile.empty())
392  {
393  std::ifstream in(file_name, std::ios::binary);
394  std::ofstream out(debug_outfile, std::ios::binary);
395  out << in.rdbuf();
396  log.warning() << "Failed sources in " << debug_outfile << messaget::eom;
397  }
398 
399  return {}; // parser/typecheck error
400  }
401 
403  {
404  // output an object file for every source file
405 
406  // "compile" functions
407  goto_modelt file_goto_model;
408  file_goto_model.symbol_table = std::move(*file_symbol_table);
409  convert_symbols(file_goto_model);
410 
411  std::string cfn;
412 
413  if(output_file_object.empty())
414  {
415  const std::string file_name_with_obj_ext =
416  get_base_name(file_name, true) + "." + object_file_extension;
417 
418  if(!output_directory_object.empty())
419  {
420  cfn = std::filesystem::path(output_directory_object)
421  .append(file_name_with_obj_ext)
422  .string();
423  }
424  else
425  cfn = file_name_with_obj_ext;
426  }
427  else
428  cfn = output_file_object;
429 
430  if(keep_file_local)
431  {
433  log.get_message_handler(), file_goto_model, file_local_mangle_suffix);
434  mangler.mangle();
435  }
436 
437  if(write_bin_object_file(cfn, file_goto_model))
438  return {};
439 
440  if(add_written_cprover_symbols(file_goto_model.symbol_table))
441  return {};
442  }
443  else
444  {
445  if(linking(symbol_table, *file_symbol_table, log.get_message_handler()))
446  {
447  return {};
448  }
449  }
450  }
451 
452  return std::move(symbol_table);
453 }
454 
458  const std::string &file_name,
459  language_filest &language_files)
460 {
461  std::unique_ptr<languaget> languagep;
462 
463  // Using '-x', the type of a file can be overridden;
464  // otherwise, it's guessed from the extension.
465 
466  if(!override_language.empty())
467  {
468  if(override_language=="c++" || override_language=="c++-header")
469  languagep = get_language_from_mode(ID_cpp);
470  else
471  languagep = get_language_from_mode(ID_C);
472  }
473  else if(file_name != "-")
474  languagep=get_language_from_filename(file_name);
475 
476  if(languagep==nullptr)
477  {
478  log.error() << "failed to figure out type of file '" << file_name << "'"
479  << messaget::eom;
480  return true;
481  }
482 
483  if(file_name == "-")
484  return parse_stdin(*languagep);
485 
486  std::ifstream infile(widen_if_needed(file_name));
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, log.get_message_handler());
519  }
520  else
521  {
522  log.statistics() << "Parsing: " << file_name << messaget::eom;
523 
524  if(lf.language->parse(infile, file_name, log.get_message_handler()))
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, log.get_message_handler());
561  }
562  else
563  {
564  if(language.parse(std::cin, "", log.get_message_handler()))
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 
620 std::optional<symbol_tablet>
621 compilet::parse_source(const std::string &file_name)
622 {
623  language_filest language_files;
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(
631  file_symbol_table, keep_file_local, log.get_message_handler()))
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 
647 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
648  : log(mh),
649  cmdline(_cmdline),
650  warning_is_fatal(Werror),
651  keep_file_local(
652  // function-local is the old name and is still in use, but is misleading
653  cmdline.isset("export-function-local-symbols") ||
654  cmdline.isset("export-file-local-symbols")),
655  file_local_mangle_suffix(
656  cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
657 {
659  echo_file_name=false;
660  wrote_object=false;
661  working_directory = std::filesystem::current_path().string();
662 
663  if(cmdline.isset("export-function-local-symbols"))
664  {
665  log.warning()
666  << "The `--export-function-local-symbols` flag is deprecated. "
667  "Please use `--export-file-local-symbols` instead."
668  << messaget::eom;
669  }
670 }
671 
674 {
675  // clean up temp dirs
676 
677  for(const auto &dir : tmp_dirs)
678  std::filesystem::remove_all(dir);
679 }
680 
681 std::size_t compilet::function_body_count(const goto_functionst &functions)
682 {
683  std::size_t count = 0;
684 
685  for(const auto &f : functions.function_map)
686  if(f.second.body_available())
687  count++;
688 
689  return count;
690 }
691 
693 {
694  config.ansi_c.defines.push_back(
695  std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION);
696 }
697 
699 {
700  symbol_table_buildert symbol_table_builder =
702 
703  goto_convert_functionst converter(
704  symbol_table_builder, log.get_message_handler());
705 
706  // the compilation may add symbols!
707 
709 
710  while(before != symbol_table_builder.symbols.size())
711  {
712  before = symbol_table_builder.symbols.size();
713 
714  typedef std::set<irep_idt> symbols_sett;
715  symbols_sett symbols;
716 
717  for(const auto &named_symbol : symbol_table_builder.symbols)
718  symbols.insert(named_symbol.first);
719 
720  // the symbol table iterators aren't stable
721  for(const auto &symbol : symbols)
722  {
723  symbol_tablet::symbolst::const_iterator s_it =
724  symbol_table_builder.symbols.find(symbol);
725  CHECK_RETURN(s_it != symbol_table_builder.symbols.end());
726 
727  if(
728  s_it->second.is_function() && !s_it->second.is_compiled() &&
729  s_it->second.value.is_not_nil())
730  {
731  log.debug() << "Compiling " << s_it->first << messaget::eom;
732  converter.convert_function(
733  s_it->first, goto_model.goto_functions.function_map[s_it->first]);
734  symbol_table_builder.get_writeable_ref(symbol).set_compiled();
735  }
736  }
737  }
738 }
739 
741 {
742  for(const auto &pair : symbol_table.symbols)
743  {
744  const irep_idt &name=pair.second.name;
745  const typet &new_type=pair.second.type;
746  if(!(name.starts_with(CPROVER_PREFIX) && new_type.id() == ID_code))
747  continue;
748 
750  continue;
751 
752  bool inserted;
753  std::map<irep_idt, symbolt>::iterator old;
754  std::tie(old, inserted)=written_macros.insert({name, pair.second});
755 
756  if(!inserted && old->second.type!=new_type)
757  {
758  log.error() << "Incompatible CPROVER macro symbol types:" << '\n'
759  << old->second.type.pretty() << "(at " << old->second.location
760  << ")\n"
761  << "and\n"
762  << new_type.pretty() << "(at " << pair.second.location << ")"
763  << messaget::eom;
764  return true;
765  }
766  }
767  return false;
768 }
bool ansi_c_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
configt config
Definition: config.cpp:25
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:151
@ ASSEMBLE_ONLY
Definition: compile.h:40
@ LINK_LIBRARY
Definition: compile.h:41
@ PREPROCESS_ONLY
Definition: compile.h:38
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:43
@ COMPILE_ONLY
Definition: compile.h:39
@ COMPILE_LINK
Definition: compile.h:42
void add_compiler_specific_defines() const
Definition: compile.cpp:692
std::optional< symbol_tablet > compile()
Parses source files and writes object files, or keeps the symbols in the symbol_table if not compilin...
Definition: compile.cpp:371
cmdlinet & cmdline
Definition: compile.h:111
bool wrote_object
Definition: compile.h:152
bool parse_stdin(languaget &)
parses a source file (low-level parsing)
Definition: compile.cpp:538
bool parse(const std::string &filename, language_filest &)
parses a source file (low-level parsing)
Definition: compile.cpp:457
std::string working_directory
Definition: compile.h:104
std::list< std::string > tmp_dirs
Definition: compile.h:107
bool echo_file_name
Definition: compile.h:35
std::string override_language
Definition: compile.h:105
std::string output_file_object
Definition: compile.h:55
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition: compile.cpp:167
std::list< std::string > libraries
Definition: compile.h:49
std::string output_directory_object
Definition: compile.h:55
std::list< std::string > object_files
Definition: compile.h:48
bool link(std::optional< symbol_tablet > &&symbol_table)
parses object files and links them
Definition: compile.cpp:317
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:54
std::list< std::string > source_files
Definition: compile.h:47
~compilet()
cleans up temporary files
Definition: compile.cpp:673
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
Definition: compile.cpp:740
std::string object_file_extension
Definition: compile.h:51
compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
constructor
Definition: compile.cpp:647
bool validate_goto_model
Definition: compile.h:36
const bool keep_file_local
Whether to keep implementations of file-local symbols.
Definition: compile.h:115
bool warning_is_fatal
Definition: compile.h:112
static std::size_t function_body_count(const goto_functionst &)
Definition: compile.cpp:681
void convert_symbols(goto_modelt &)
Definition: compile.cpp:698
std::map< irep_idt, symbolt > written_macros
Definition: compile.h:145
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:208
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
Definition: compile.cpp:273
enum compilet::@3 mode
messaget log
Definition: compile.h:110
std::optional< symbol_tablet > parse_source(const std::string &)
Parses and type checks a source file located at file_name.
Definition: compile.cpp:621
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
const std::string file_local_mangle_suffix
String to include in all mangled names.
Definition: compile.h:118
std::list< std::string > library_paths
Definition: compile.h:46
std::string output_file_executable
Definition: compile.h:52
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:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition: dstring.h:95
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:105
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irep_idt & id() const
Definition: irep.h:384
language_filet & add_file(const std::string &filename)
Definition: language_file.h:77
bool typecheck(symbol_table_baset &symbol_table, const bool keep_file_local, message_handlert &message_handler)
bool final(symbol_table_baset &symbol_table)
std::unique_ptr< languaget > language
Definition: language_file.h:46
virtual bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler)=0
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &)
Definition: language.h:46
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
@ 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:14
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:120
The type of an expression, extends irept.
Definition: type.h:29
static file_typet detect_file_type(const std::string &file_name, message_handlert &message_handler)
Definition: compile.cpp:126
file_typet
Definition: compile.cpp:116
@ FAILED_TO_OPEN_FILE
Compile and link source and object files.
#define CPROVER_PREFIX
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Goto Programs with Functions.
static int8_t r
Definition: irep_hash.h:60
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:187
Abstract interface to support a programming language.
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &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:1616
ANSI-C Linking.
double log(double x)
Definition: math.c:2776
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
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
Mangle names of file-local functions to make them unique.
#define FILE_LOCAL_PREFIX
Definition: name_mangler.h:16
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.
Read Goto Programs.
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:48
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define INITIALIZE_FUNCTION
int strncmp(const char *s1, const char *s2, size_t n)
Definition: string.c:464
int memcmp(const void *s1, const void *s2, size_t n)
Definition: string.c:923
char * strerror(int errnum)
Definition: string.c:1014
std::list< std::string > defines
Definition: config.h:266
std::string get_temporary_directory(const std::string &name_template)
Definition: tempdir.cpp:29
#define widen_if_needed(s)
Definition: unicode.h:28
#define size_type
Definition: unistd.c:347
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
const char * CBMC_VERSION
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.