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/suffix.h>
26 #include <util/tempdir.h>
27 #include <util/unicode.h>
28 #include <util/version.h>
29 
30 #include <ansi-c/ansi_c_language.h>
32 
37 
38 #include <langapi/language_file.h>
39 #include <langapi/mode.h>
40 
42 
43 #define DOTGRAPHSETTINGS "color=black;" \
44  "orientation=portrait;" \
45  "fontsize=20;"\
46  "compound=true;"\
47  "size=\"30,40\";"\
48  "ratio=compress;"
49 
50 // the following are for chdir
51 
52 #if defined(__linux__) || \
53  defined(__FreeBSD_kernel__) || \
54  defined(__GNU__) || \
55  defined(__unix__) || \
56  defined(__CYGWIN__) || \
57  defined(__MACH__)
58 #include <unistd.h>
59 #endif
60 
61 #ifdef _WIN32
62 #include <util/pragma_push.def>
63 #ifdef _MSC_VER
64 #pragma warning(disable:4668)
65  // using #if/#elif on undefined macro
66 #endif
67 #include <direct.h>
68 #include <windows.h>
69 #define chdir _chdir
70 #define popen _popen
71 #define pclose _pclose
72 #include <util/pragma_pop.def>
73 #endif
74 
79 {
81 
83 
84  // Parse command line for source and object file names
85  for(const auto &arg : cmdline.args)
86  if(add_input_file(arg))
87  return true;
88 
89  for(const auto &library : libraries)
90  {
91  if(!find_library(library))
92  // GCC is going to complain if this doesn't exist
93  debug() << "Library not found: " << library << " (ignoring)" << eom;
94  }
95 
96  statistics() << "No. of source files: " << source_files.size() << eom;
97  statistics() << "No. of object files: " << object_files.size() << eom;
98 
99  // Work through the given source files
100 
101  if(source_files.empty() && object_files.empty())
102  {
103  error() << "no input files" << eom;
104  return true;
105  }
106 
107  if(mode==LINK_LIBRARY && !source_files.empty())
108  {
109  error() << "cannot link source files" << eom;
110  return true;
111  }
112 
113  if(mode==PREPROCESS_ONLY && !object_files.empty())
114  {
115  error() << "cannot preprocess object files" << eom;
116  return true;
117  }
118 
119  const unsigned warnings_before=
121 
122  if(!source_files.empty())
123  if(compile())
124  return true;
125 
126  if(mode==LINK_LIBRARY ||
127  mode==COMPILE_LINK ||
129  {
130  if(link())
131  return true;
132  }
133 
134  return
137  warnings_before;
138 }
139 
140 enum class file_typet
141 {
143  UNKNOWN,
144  SOURCE_FILE,
146  THIN_ARCHIVE,
147  GOTO_BINARY,
148  ELF_OBJECT
149 };
150 
151 static file_typet detect_file_type(const std::string &file_name)
152 {
153  // first of all, try to open the file
154  std::ifstream in(file_name);
155  if(!in)
157 
158  const std::string::size_type r = file_name.rfind('.');
159 
160  const std::string ext =
161  r == std::string::npos ? "" : file_name.substr(r + 1, file_name.length());
162 
163  if(
164  ext == "c" || ext == "cc" || ext == "cp" || ext == "cpp" || ext == "CPP" ||
165  ext == "c++" || ext == "C" || ext == "i" || ext == "ii" || ext == "class" ||
166  ext == "jar" || ext == "jsil")
167  {
169  }
170 
171  char hdr[8];
172  in.get(hdr, 8);
173  if((ext == "a" || ext == "o") && strncmp(hdr, "!<thin>", 8) == 0)
175 
176  if(ext == "a")
178 
179  if(is_goto_binary(file_name))
181 
182  if(hdr[0] == 0x7f && memcmp(hdr + 1, "ELF", 3) == 0)
183  return file_typet::ELF_OBJECT;
184 
185  return file_typet::UNKNOWN;
186 }
187 
190 bool compilet::add_input_file(const std::string &file_name)
191 {
192  switch(detect_file_type(file_name))
193  {
195  warning() << "failed to open file `" << file_name
196  << "': " << std::strerror(errno) << eom;
197  return warning_is_fatal; // generously ignore unless -Werror
198 
199  case file_typet::UNKNOWN:
200  // unknown extension, not a goto binary, will silently ignore
201  debug() << "unknown file type in `" << file_name << "'" << eom;
202  return false;
203 
205  // ELF file without goto-cc section, silently ignore
206  debug() << "ELF object without goto-cc section: `" << file_name << "'"
207  << eom;
208  return false;
209 
211  source_files.push_back(file_name);
212  return false;
213 
215  return add_files_from_archive(file_name, false);
216 
218  return add_files_from_archive(file_name, true);
219 
221  object_files.push_back(file_name);
222  return false;
223  }
224 
225  UNREACHABLE;
226 }
227 
231  const std::string &file_name,
232  bool thin_archive)
233 {
234  std::stringstream cmd;
235  FILE *stream;
236 
237  std::string tstr = working_directory;
238 
239  if(!thin_archive)
240  {
241  tstr = get_temporary_directory("goto-cc.XXXXXX");
242 
243  if(tstr=="")
244  {
245  error() << "Cannot create temporary directory" << eom;
246  return true;
247  }
248 
249  tmp_dirs.push_back(tstr);
250  if(chdir(tmp_dirs.back().c_str())!=0)
251  {
252  error() << "Cannot switch to temporary directory" << eom;
253  return true;
254  }
255 
256  // unpack now
257  cmd << "ar x " << concat_dir_file(working_directory, file_name);
258 
259  stream=popen(cmd.str().c_str(), "r");
260  pclose(stream);
261 
262  cmd.clear();
263  cmd.str("");
264  }
265 
266  // add the files from "ar t"
267  cmd << "ar t " << concat_dir_file(working_directory, file_name);
268 
269  stream = popen(cmd.str().c_str(), "r");
270 
271  if(stream != nullptr)
272  {
273  std::string line;
274  int ch; // fgetc returns an int, not char
275  while((ch = fgetc(stream)) != EOF)
276  {
277  if(ch != '\n')
278  {
279  line += static_cast<char>(ch);
280  }
281  else
282  {
283  std::string t = concat_dir_file(tstr, line);
284 
285  if(is_goto_binary(t))
286  object_files.push_back(t);
287  else
288  debug() << "Object file is not a goto binary: " << line << eom;
289 
290  line = "";
291  }
292  }
293 
294  pclose(stream);
295  }
296 
297  if(!thin_archive && chdir(working_directory.c_str()) != 0)
298  error() << "Could not change back to working directory" << eom;
299 
300  return false;
301 }
302 
306 bool compilet::find_library(const std::string &name)
307 {
308  std::string tmp;
309 
310  for(const auto &library_path : library_paths)
311  {
312  #ifdef _WIN32
313  tmp = library_path + "\\lib";
314  #else
315  tmp = library_path + "/lib";
316  #endif
317 
318  std::ifstream in(tmp+name+".a");
319 
320  if(in.is_open())
321  return !add_input_file(tmp+name+".a");
322  else
323  {
324  std::string libname=tmp+name+".so";
325 
326  switch(detect_file_type(libname))
327  {
329  return !add_input_file(libname);
330 
332  warning() << "Warning: Cannot read ELF library " << libname << eom;
333  return warning_is_fatal;
334 
335  default:
336  break;
337  }
338  }
339  }
340 
341  return false;
342 }
343 
347 {
348  // "compile" hitherto uncompiled functions
349  statistics() << "Compiling functions" << eom;
351 
352  // parse object files
353  for(const auto &file_name : object_files)
354  {
356  return true;
357  }
358 
359  // produce entry point?
360 
362  {
363  // new symbols may have been added to a previously linked file
364  // make sure a new entry point is created that contains all
365  // static initializers
367 
371 
372  const bool error = ansi_c_entry_point(
376 
377  if(error)
378  return true;
379 
380  // entry_point may (should) add some more functions.
382  }
383 
385  return true;
386 
388 }
389 
394 {
395  while(!source_files.empty())
396  {
397  std::string file_name=source_files.front();
398  source_files.pop_front();
399 
400  // Visual Studio always prints the name of the file it's doing
401  // onto stdout. The name of the directory is stripped.
402  if(echo_file_name)
403  std::cout << get_base_name(file_name, false) << '\n' << std::flush;
404 
405  bool r=parse_source(file_name); // don't break the program!
406 
407  if(r)
408  {
409  const std::string &debug_outfile=
410  cmdline.get_value("print-rejected-preprocessed-source");
411  if(!debug_outfile.empty())
412  {
413  std::ifstream in(file_name, std::ios::binary);
414  std::ofstream out(debug_outfile, std::ios::binary);
415  out << in.rdbuf();
416  warning() << "Failed sources in " << debug_outfile << eom;
417  }
418 
419  return true; // parser/typecheck error
420  }
421 
423  {
424  // output an object file for every source file
425 
426  // "compile" functions
428 
429  std::string cfn;
430 
431  if(output_file_object=="")
432  {
433  const std::string file_name_with_obj_ext =
434  get_base_name(file_name, true) + "." + object_file_extension;
435 
436  if(!output_directory_object.empty())
437  cfn = concat_dir_file(output_directory_object, file_name_with_obj_ext);
438  else
439  cfn = file_name_with_obj_ext;
440  }
441  else
442  cfn = output_file_object;
443 
444  if(write_object_file(cfn, goto_model))
445  return true;
446 
448  return true;
449 
450  goto_model.clear(); // clean symbol table for next source file.
451  }
452  }
453 
454  return false;
455 }
456 
460  const std::string &file_name,
461  language_filest &language_files)
462 {
463  if(file_name=="-")
464  return parse_stdin();
465 
466  #ifdef _MSC_VER
467  std::ifstream infile(widen(file_name));
468  #else
469  std::ifstream infile(file_name);
470  #endif
471 
472  if(!infile)
473  {
474  error() << "failed to open input file `" << file_name << "'" << eom;
475  return true;
476  }
477 
478  std::unique_ptr<languaget> languagep;
479 
480  // Using '-x', the type of a file can be overridden;
481  // otherwise, it's guessed from the extension.
482 
483  if(override_language!="")
484  {
485  if(override_language=="c++" || override_language=="c++-header")
486  languagep = get_language_from_mode(ID_cpp);
487  else
488  languagep = get_language_from_mode(ID_C);
489  }
490  else
491  languagep=get_language_from_filename(file_name);
492 
493  if(languagep==nullptr)
494  {
495  error() << "failed to figure out type of file `" << file_name << "'" << eom;
496  return true;
497  }
498 
500 
501  language_filet &lf=language_files.add_file(file_name);
502  lf.language=std::move(languagep);
503 
504  if(mode==PREPROCESS_ONLY)
505  {
506  statistics() << "Preprocessing: " << file_name << eom;
507 
508  std::ostream *os = &std::cout;
509  std::ofstream ofs;
510 
511  if(cmdline.isset('o'))
512  {
513  ofs.open(cmdline.get_value('o'));
514  os = &ofs;
515 
516  if(!ofs.is_open())
517  {
518  error() << "failed to open output file `"
519  << cmdline.get_value('o') << "'" << eom;
520  return true;
521  }
522  }
523 
524  lf.language->preprocess(infile, file_name, *os);
525  }
526  else
527  {
528  statistics() << "Parsing: " << file_name << eom;
529 
530  if(lf.language->parse(infile, file_name))
531  {
532  error() << "PARSING ERROR" << eom;
533  return true;
534  }
535  }
536 
537  lf.get_modules();
538  return false;
539 }
540 
544 {
545  ansi_c_languaget language;
546 
548 
549  statistics() << "Parsing: (stdin)" << eom;
550 
551  if(mode==PREPROCESS_ONLY)
552  {
553  std::ostream *os = &std::cout;
554  std::ofstream ofs;
555 
556  if(cmdline.isset('o'))
557  {
558  ofs.open(cmdline.get_value('o'));
559  os = &ofs;
560 
561  if(!ofs.is_open())
562  {
563  error() << "failed to open output file `"
564  << cmdline.get_value('o') << "'" << eom;
565  return true;
566  }
567  }
568 
569  language.preprocess(std::cin, "", *os);
570  }
571  else
572  {
573  if(language.parse(std::cin, ""))
574  {
575  error() << "PARSING ERROR" << eom;
576  return true;
577  }
578  }
579 
580  return false;
581 }
582 
588  const std::string &file_name,
589  const goto_modelt &goto_model)
590 {
591  return write_bin_object_file(file_name, goto_model);
592 }
593 
599  const std::string &file_name,
600  const goto_modelt &goto_model)
601 {
602  statistics() << "Writing binary format object `"
603  << file_name << "'" << eom;
604 
605  // symbols
606  statistics() << "Symbols in table: " << goto_model.symbol_table.symbols.size()
607  << eom;
608 
609  std::ofstream outfile(file_name, std::ios::binary);
610 
611  if(!outfile.is_open())
612  {
613  error() << "Error opening file `" << file_name << "'" << eom;
614  return true;
615  }
616 
617  if(write_goto_binary(outfile, goto_model))
618  return true;
619 
621 
622  statistics() << "Functions: " << goto_model.goto_functions.function_map.size()
623  << "; " << cnt << " have a body." << eom;
624 
625  outfile.close();
626  wrote_object=true;
627 
628  return false;
629 }
630 
633 bool compilet::parse_source(const std::string &file_name)
634 {
635  language_filest language_files;
636  language_files.set_message_handler(get_message_handler());
637 
638  if(parse(file_name, language_files))
639  return true;
640 
641  // we just typecheck one file here
642  if(language_files.typecheck(goto_model.symbol_table))
643  {
644  error() << "CONVERSION ERROR" << eom;
645  return true;
646  }
647 
648  if(language_files.final(goto_model.symbol_table))
649  {
650  error() << "CONVERSION ERROR" << eom;
651  return true;
652  }
653 
654  return false;
655 }
656 
659 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
660  : messaget(mh),
661  ns(goto_model.symbol_table),
662  cmdline(_cmdline),
663  warning_is_fatal(Werror)
664 {
666  echo_file_name=false;
667  wrote_object=false;
669 }
670 
674 {
675  // clean up temp dirs
676 
677  for(const auto &dir : tmp_dirs)
678  delete_directory(dir);
679 }
680 
681 std::size_t
683 {
684  std::size_t count = 0;
685 
686  for(const auto &f : functions.function_map)
687  if(f.second.body_available())
688  count++;
689 
690  return count;
691 }
692 
694 {
695  config.ansi_c.defines.push_back(
696  std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION);
697 }
698 
700 {
701  symbol_table_buildert symbol_table_builder =
703 
704  goto_convert_functionst converter(
705  symbol_table_builder, get_message_handler());
706 
707  // the compilation may add symbols!
708 
710 
711  while(before != symbol_table_builder.symbols.size())
712  {
713  before = symbol_table_builder.symbols.size();
714 
715  typedef std::set<irep_idt> symbols_sett;
716  symbols_sett symbols;
717 
718  for(const auto &named_symbol : symbol_table_builder.symbols)
719  symbols.insert(named_symbol.first);
720 
721  // the symbol table iterators aren't stable
722  for(const auto &symbol : symbols)
723  {
724  symbol_tablet::symbolst::const_iterator s_it =
725  symbol_table_builder.symbols.find(symbol);
726  CHECK_RETURN(s_it != symbol_table_builder.symbols.end());
727 
728  if(
729  s_it->second.is_function() && !s_it->second.is_compiled() &&
730  s_it->second.value.is_not_nil())
731  {
732  debug() << "Compiling " << s_it->first << eom;
733  converter.convert_function(s_it->first, dest.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(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code))
747  continue;
748 
749  bool inserted;
750  std::map<irep_idt, symbolt>::iterator old;
751  std::tie(old, inserted)=written_macros.insert({name, pair.second});
752 
753  if(!inserted && old->second.type!=new_type)
754  {
755  error() << "Incompatible CPROVER macro symbol types:" << eom
756  << old->second.type.pretty() << "(at " << old->second.location
757  << ")" << eom << "and" << eom << new_type.pretty()
758  << "(at " << pair.second.location << ")" << eom;
759  return true;
760  }
761  }
762  return false;
763 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
cmdlinet::args
argst args
Definition: cmdline.h:44
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:121
compilet::wrote_object
bool wrote_object
Definition: compile.h:113
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
compilet::echo_file_name
bool echo_file_name
Definition: compile.h:33
is_goto_binary
bool is_goto_binary(const std::string &filename)
Definition: read_goto_binary.cpp:168
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:35
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
compilet::source_files
std::list< std::string > source_files
Definition: compile.h:46
ansi_c_entry_point.h
goto_modelt::clear
void clear()
Definition: goto_model.h:34
file_typet::GOTO_BINARY
compilet::parse
bool parse(const std::string &filename, language_filest &)
parses a source file (low-level parsing)
Definition: compile.cpp:459
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:230
typet
The type of an expression, extends irept.
Definition: type.h:27
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table)
Definition: language_file.cpp:85
compilet::parse_stdin
bool parse_stdin()
parses a source file (low-level parsing)
Definition: compile.cpp:543
compilet::function_body_count
std::size_t function_body_count(const goto_functionst &) const
Definition: compile.cpp:682
goto_convert_functionst::convert_function
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
Definition: goto_convert_functions.cpp:138
language_filet
Definition: language_file.h:40
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:50
compilet::doit
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:78
compilet::libraries
std::list< std::string > libraries
Definition: compile.h:48
goto_modelt
Definition: goto_model.h:24
mode.h
configt::ansi_c
struct configt::ansi_ct ansi_c
messaget::eom
static eomt eom
Definition: message.h:284
goto_convert.h
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
version.h
tempdir.h
compilet::cmdline
cmdlinet & cmdline
Definition: compile.h:96
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
file_typet::NORMAL_ARCHIVE
write_goto_binary.h
configt
Globally accessible architectural configuration.
Definition: config.h:24
file_typet::FAILED_TO_OPEN_FILE
compilet::COMPILE_LINK
Definition: compile.h:41
compilet::link
bool link()
parses object files and links them
Definition: compile.cpp:346
compilet::written_macros
std::map< irep_idt, symbolt > written_macros
Definition: compile.h:106
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:101
cmdlinet
Definition: cmdline.h:19
compilet::output_file_object
std::string output_file_object
Definition: compile.h:56
goto_functionst::clear
void clear()
Definition: goto_functions.h:70
compilet::object_files
std::list< std::string > object_files
Definition: compile.h:47
messaget::error
mstreamt & error() const
Definition: message.h:386
compilet::add_written_cprover_symbols
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
Definition: compile.cpp:740
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:14
file_typet::UNKNOWN
compilet::working_directory
std::string working_directory
Definition: compile.h:34
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:119
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:110
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
concat_dir_file
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:141
compilet::COMPILE_LINK_EXECUTABLE
Definition: compile.h:42
compilet::compilet
compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
constructor
Definition: compile.cpp:659
compilet::output_file_executable
std::string output_file_executable
Definition: compile.h:53
compilet::mode
enum compilet::@3 mode
goto_convert_functionst
Definition: goto_convert_functions.h:39
compilet::convert_symbols
void convert_symbols(goto_functionst &dest)
Definition: compile.cpp:699
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
compilet::library_paths
std::list< std::string > library_paths
Definition: compile.h:45
compile.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
ansi_c_languaget::preprocess
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Definition: ansi_c_language.cpp:40
language_filest::add_file
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
irept::id
const irep_idt & id() const
Definition: irep.h:259
compilet::object_file_extension
std::string object_file_extension
Definition: compile.h:52
message_handlert
Definition: message.h:24
get_base_name.h
file_typet::ELF_OBJECT
file_typet::SOURCE_FILE
compilet::warning_is_fatal
bool warning_is_fatal
Definition: compile.h:97
compilet::~compilet
~compilet()
cleans up temporary files
Definition: compile.cpp:673
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:46
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:52
file_typet::THIN_ARCHIVE
read_goto_binary.h
compilet::override_language
std::string override_language
Definition: compile.h:35
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:112
compilet::ASSEMBLE_ONLY
Definition: compile.h:39
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:190
compilet::output_directory_object
std::string output_directory_object
Definition: compile.h:56
detect_file_type
static file_typet detect_file_type(const std::string &file_name)
Definition: compile.cpp:151
config
configt config
Definition: config.cpp:24
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:306
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:170
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
compilet::compile
bool compile()
parses source files and writes object files, or keeps the symbols in the symbol_table depending on th...
Definition: compile.cpp:393
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
compilet::parse_source
bool parse_source(const std::string &)
parses a source file
Definition: compile.cpp:633
compilet::write_object_file
bool write_object_file(const std::string &, const goto_modelt &)
writes the goto functions in the function table to a binary format object file.
Definition: compile.cpp:587
compilet::COMPILE_ONLY
Definition: compile.h:38
messaget::M_WARNING
Definition: message.h:160
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
compilet::add_compiler_specific_defines
void add_compiler_specific_defines(class configt &config) const
Definition: compile.cpp:693
ansi_c_language.h
suffix.h
ansi_c_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Definition: ansi_c_language.cpp:52
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
Definition: symbol_table_base.h:27
compilet::write_bin_object_file
bool write_bin_object_file(const std::string &, const goto_modelt &)
writes the goto functions in the function table to a binary format object file.
Definition: compile.cpp:598
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:224
compilet::LINK_LIBRARY
Definition: compile.h:40
read_object_and_link
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
Definition: read_goto_binary.cpp:234
unicode.h
config.h
get_current_working_directory
std::string get_current_working_directory()
Definition: file_util.cpp:48
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
get_temporary_directory
std::string get_temporary_directory(const std::string &name_template)
Definition: tempdir.cpp:38
compilet::tmp_dirs
std::list< std::string > tmp_dirs
Definition: compile.h:49
r
static int8_t r
Definition: irep_hash.h:59
messaget::debug
mstreamt & debug() const
Definition: message.h:416
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
goto_convert_functions.h
static_lifetime_init.h
compilet::PREPROCESS_ONLY
Definition: compile.h:37
write_goto_binary
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
Definition: write_goto_binary.cpp:127
compilet::goto_model
goto_modelt goto_model
Definition: compile.h:30
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
file_typet
file_typet
Definition: compile.cpp:140
symbol_table_builder.h
messaget::warning
mstreamt & warning() const
Definition: message.h:391
delete_directory
void delete_directory(const std::string &path)
deletes all files in 'path' and then the directory itself
Definition: file_util.cpp:100
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
ansi_c_languaget
Definition: ansi_c_language.h:34
message_handlert::get_message_count
std::size_t get_message_count(unsigned level) const
Definition: message.h:51
language_file.h
messaget::statistics
mstreamt & statistics() const
Definition: message.h:406
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
language_filest
Definition: language_file.h:61