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 
46 
47 #define DOTGRAPHSETTINGS "color=black;" \
48  "orientation=portrait;" \
49  "fontsize=20;"\
50  "compound=true;"\
51  "size=\"30,40\";"\
52  "ratio=compress;"
53 
58 {
60 
62 
63  // Parse command line for source and object file names
64  for(const auto &arg : cmdline.args)
65  if(add_input_file(arg))
66  return true;
67 
68  for(const auto &library : libraries)
69  {
70  if(!find_library(library))
71  // GCC is going to complain if this doesn't exist
72  debug() << "Library not found: " << library << " (ignoring)" << eom;
73  }
74 
75  statistics() << "No. of source files: " << source_files.size() << eom;
76  statistics() << "No. of object files: " << object_files.size() << eom;
77 
78  // Work through the given source files
79 
80  if(source_files.empty() && object_files.empty())
81  {
82  error() << "no input files" << eom;
83  return true;
84  }
85 
86  if(mode==LINK_LIBRARY && !source_files.empty())
87  {
88  error() << "cannot link source files" << eom;
89  return true;
90  }
91 
92  if(mode==PREPROCESS_ONLY && !object_files.empty())
93  {
94  error() << "cannot preprocess object files" << eom;
95  return true;
96  }
97 
98  const unsigned warnings_before=
100 
101  if(!source_files.empty())
102  if(compile())
103  return true;
104 
105  if(mode==LINK_LIBRARY ||
106  mode==COMPILE_LINK ||
108  {
109  if(link())
110  return true;
111  }
112 
113  return
116  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, get_message_handler()))
174  {
176  warning() << "failed to open file '" << file_name
177  << "': " << std::strerror(errno) << 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  debug() << "unknown file type in '" << file_name << "'" << eom;
183  return false;
184 
186  // ELF file without goto-cc section, silently ignore
187  debug() << "ELF object without goto-cc section: '" << file_name << "'"
188  << eom;
189  return false;
190 
192  source_files.push_back(file_name);
193  return false;
194 
196  return add_files_from_archive(file_name, false);
197 
199  return add_files_from_archive(file_name, true);
200 
202  object_files.push_back(file_name);
203  return false;
204  }
205 
206  UNREACHABLE;
207 }
208 
212  const std::string &file_name,
213  bool thin_archive)
214 {
215  std::string tstr = working_directory;
216 
217  if(!thin_archive)
218  {
219  tstr = get_temporary_directory("goto-cc.XXXXXX");
220 
221  tmp_dirs.push_back(tstr);
222  set_current_path(tmp_dirs.back());
223 
224  // unpack now
225  int ret =
226  run("ar", {"ar", "x", concat_dir_file(working_directory, file_name)});
227  if(ret != 0)
228  {
229  error() << "Failed to extract archive " << file_name << 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", "t", concat_dir_file(working_directory, file_name)},
239  "",
240  tmp_file_out(),
241  "");
242  if(ret != 0)
243  {
244  error() << "Failed to list archive " << file_name << eom;
245  return true;
246  }
247 
248  std::ifstream in(tmp_file_out());
249  std::string line;
250 
251  while(!in.fail() && std::getline(in, line))
252  {
253  std::string t = concat_dir_file(tstr, line);
254 
256  object_files.push_back(t);
257  else
258  debug() << "Object file is not a goto binary: " << line << eom;
259  }
260 
261  if(!thin_archive)
263 
264  return false;
265 }
266 
270 bool compilet::find_library(const std::string &name)
271 {
272  std::string library_file_name;
273 
274  for(const auto &library_path : library_paths)
275  {
276  library_file_name = concat_dir_file(library_path, "lib" + name + ".a");
277 
278  std::ifstream in(library_file_name);
279 
280  if(in.is_open())
281  return !add_input_file(library_file_name);
282  else
283  {
284  library_file_name = concat_dir_file(library_path, "lib" + name + ".so");
285 
286  switch(detect_file_type(library_file_name, get_message_handler()))
287  {
289  return !add_input_file(library_file_name);
290 
292  warning() << "Warning: Cannot read ELF library " << library_file_name
293  << eom;
294  return warning_is_fatal;
295 
300  case file_typet::UNKNOWN:
301  break;
302  }
303  }
304  }
305 
306  return false;
307 }
308 
312 {
313  // "compile" hitherto uncompiled functions
314  statistics() << "Compiling functions" << eom;
316 
317  // parse object files
318  for(const auto &file_name : object_files)
319  {
321  return true;
322  }
323 
324  // produce entry point?
325 
327  {
328  // new symbols may have been added to a previously linked file
329  // make sure a new entry point is created that contains all
330  // static initializers
332 
336 
337  const bool error = ansi_c_entry_point(
341 
342  if(error)
343  return true;
344 
345  // entry_point may (should) add some more functions.
347  }
348 
349  if(keep_file_local)
350  {
353  mangler.mangle();
354  }
355 
357  return true;
358 
360 }
361 
366 {
367  while(!source_files.empty())
368  {
369  std::string file_name=source_files.front();
370  source_files.pop_front();
371 
372  // Visual Studio always prints the name of the file it's doing
373  // onto stdout. The name of the directory is stripped.
374  if(echo_file_name)
375  std::cout << get_base_name(file_name, false) << '\n' << std::flush;
376 
377  bool r=parse_source(file_name); // don't break the program!
378 
379  if(r)
380  {
381  const std::string &debug_outfile=
382  cmdline.get_value("print-rejected-preprocessed-source");
383  if(!debug_outfile.empty())
384  {
385  std::ifstream in(file_name, std::ios::binary);
386  std::ofstream out(debug_outfile, std::ios::binary);
387  out << in.rdbuf();
388  warning() << "Failed sources in " << debug_outfile << eom;
389  }
390 
391  return true; // parser/typecheck error
392  }
393 
395  {
396  // output an object file for every source file
397 
398  // "compile" functions
400 
401  std::string cfn;
402 
403  if(output_file_object.empty())
404  {
405  const std::string file_name_with_obj_ext =
406  get_base_name(file_name, true) + "." + object_file_extension;
407 
408  if(!output_directory_object.empty())
409  cfn = concat_dir_file(output_directory_object, file_name_with_obj_ext);
410  else
411  cfn = file_name_with_obj_ext;
412  }
413  else
414  cfn = output_file_object;
415 
416  if(keep_file_local)
417  {
420  mangler.mangle();
421  }
422 
424  return true;
425 
427  return true;
428 
429  goto_model.clear(); // clean symbol table for next source file.
430  }
431  }
432 
433  return false;
434 }
435 
439  const std::string &file_name,
440  language_filest &language_files)
441 {
442  std::unique_ptr<languaget> languagep;
443 
444  // Using '-x', the type of a file can be overridden;
445  // otherwise, it's guessed from the extension.
446 
447  if(!override_language.empty())
448  {
449  if(override_language=="c++" || override_language=="c++-header")
450  languagep = get_language_from_mode(ID_cpp);
451  else
452  languagep = get_language_from_mode(ID_C);
453  }
454  else if(file_name != "-")
455  languagep=get_language_from_filename(file_name);
456 
457  if(languagep==nullptr)
458  {
459  error() << "failed to figure out type of file '" << file_name << "'" << eom;
460  return true;
461  }
462 
464 
465  if(file_name == "-")
466  return parse_stdin(*languagep);
467 
468 #ifdef _MSC_VER
469  std::ifstream infile(widen(file_name));
470 #else
471  std::ifstream infile(file_name);
472 #endif
473 
474  if(!infile)
475  {
476  error() << "failed to open input file '" << file_name << "'" << eom;
477  return true;
478  }
479 
480  language_filet &lf=language_files.add_file(file_name);
481  lf.language=std::move(languagep);
482 
483  if(mode==PREPROCESS_ONLY)
484  {
485  statistics() << "Preprocessing: " << file_name << eom;
486 
487  std::ostream *os = &std::cout;
488  std::ofstream ofs;
489 
490  if(cmdline.isset('o'))
491  {
492  ofs.open(cmdline.get_value('o'));
493  os = &ofs;
494 
495  if(!ofs.is_open())
496  {
497  error() << "failed to open output file '" << cmdline.get_value('o')
498  << "'" << eom;
499  return true;
500  }
501  }
502 
503  lf.language->preprocess(infile, file_name, *os);
504  }
505  else
506  {
507  statistics() << "Parsing: " << file_name << eom;
508 
509  if(lf.language->parse(infile, file_name))
510  {
511  error() << "PARSING ERROR" << eom;
512  return true;
513  }
514  }
515 
516  lf.get_modules();
517  return false;
518 }
519 
524 {
525  statistics() << "Parsing: (stdin)" << eom;
526 
527  if(mode==PREPROCESS_ONLY)
528  {
529  std::ostream *os = &std::cout;
530  std::ofstream ofs;
531 
532  if(cmdline.isset('o'))
533  {
534  ofs.open(cmdline.get_value('o'));
535  os = &ofs;
536 
537  if(!ofs.is_open())
538  {
539  error() << "failed to open output file '" << cmdline.get_value('o')
540  << "'" << eom;
541  return true;
542  }
543  }
544 
545  language.preprocess(std::cin, "", *os);
546  }
547  else
548  {
549  if(language.parse(std::cin, ""))
550  {
551  error() << "PARSING ERROR" << eom;
552  return true;
553  }
554  }
555 
556  return false;
557 }
558 
565  const std::string &file_name,
566  const goto_modelt &src_goto_model)
567 {
569  {
570  status() << "Validating goto model" << eom;
571  src_goto_model.validate();
572  }
573 
574  statistics() << "Writing binary format object '" << file_name << "'" << eom;
575 
576  // symbols
577  statistics() << "Symbols in table: "
578  << src_goto_model.symbol_table.symbols.size() << eom;
579 
580  std::ofstream outfile(file_name, std::ios::binary);
581 
582  if(!outfile.is_open())
583  {
584  error() << "Error opening file '" << file_name << "'" << eom;
585  return true;
586  }
587 
588  if(write_goto_binary(outfile, src_goto_model))
589  return true;
590 
591  const auto cnt = function_body_count(src_goto_model.goto_functions);
592 
593  statistics() << "Functions: "
594  << src_goto_model.goto_functions.function_map.size() << "; "
595  << cnt << " have a body." << eom;
596 
597  outfile.close();
598  wrote_object=true;
599 
600  return false;
601 }
602 
605 bool compilet::parse_source(const std::string &file_name)
606 {
607  language_filest language_files;
608  language_files.set_message_handler(get_message_handler());
609 
610  if(parse(file_name, language_files))
611  return true;
612 
613  // we just typecheck one file here
614  if(language_files.typecheck(goto_model.symbol_table, keep_file_local))
615  {
616  error() << "CONVERSION ERROR" << eom;
617  return true;
618  }
619 
620  if(language_files.final(goto_model.symbol_table))
621  {
622  error() << "CONVERSION ERROR" << eom;
623  return true;
624  }
625 
626  return false;
627 }
628 
631 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
632  : messaget(mh),
633  ns(goto_model.symbol_table),
634  cmdline(_cmdline),
635  warning_is_fatal(Werror),
636  keep_file_local(
637  // function-local is the old name and is still in use, but is misleading
638  cmdline.isset("export-function-local-symbols") ||
639  cmdline.isset("export-file-local-symbols")),
640  file_local_mangle_suffix(
641  cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
642 {
644  echo_file_name=false;
645  wrote_object=false;
647 
648  if(cmdline.isset("export-function-local-symbols"))
649  warning() << "The `--export-function-local-symbols` flag is deprecated. "
650  "Please use `--export-file-local-symbols` instead."
651  << eom;
652 }
653 
657 {
658  // clean up temp dirs
659 
660  for(const auto &dir : tmp_dirs)
661  delete_directory(dir);
662 }
663 
664 std::size_t
666 {
667  std::size_t count = 0;
668 
669  for(const auto &f : functions.function_map)
670  if(f.second.body_available())
671  count++;
672 
673  return count;
674 }
675 
677 {
678  config.ansi_c.defines.push_back(
679  std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION);
680 }
681 
683 {
684  symbol_table_buildert symbol_table_builder =
686 
687  goto_convert_functionst converter(
688  symbol_table_builder, get_message_handler());
689 
690  // the compilation may add symbols!
691 
693 
694  while(before != symbol_table_builder.symbols.size())
695  {
696  before = symbol_table_builder.symbols.size();
697 
698  typedef std::set<irep_idt> symbols_sett;
699  symbols_sett symbols;
700 
701  for(const auto &named_symbol : symbol_table_builder.symbols)
702  symbols.insert(named_symbol.first);
703 
704  // the symbol table iterators aren't stable
705  for(const auto &symbol : symbols)
706  {
707  symbol_tablet::symbolst::const_iterator s_it =
708  symbol_table_builder.symbols.find(symbol);
709  CHECK_RETURN(s_it != symbol_table_builder.symbols.end());
710 
711  if(
712  s_it->second.is_function() && !s_it->second.is_compiled() &&
713  s_it->second.value.is_not_nil())
714  {
715  debug() << "Compiling " << s_it->first << eom;
716  converter.convert_function(s_it->first, dest.function_map[s_it->first]);
717  symbol_table_builder.get_writeable_ref(symbol).set_compiled();
718  }
719  }
720  }
721 }
722 
724 {
725  for(const auto &pair : symbol_table.symbols)
726  {
727  const irep_idt &name=pair.second.name;
728  const typet &new_type=pair.second.type;
729  if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code))
730  continue;
731 
732  bool inserted;
733  std::map<irep_idt, symbolt>::iterator old;
734  std::tie(old, inserted)=written_macros.insert({name, pair.second});
735 
736  if(!inserted && old->second.type!=new_type)
737  {
738  error() << "Incompatible CPROVER macro symbol types:" << eom
739  << old->second.type.pretty() << "(at " << old->second.location
740  << ")" << eom << "and" << eom << new_type.pretty()
741  << "(at " << pair.second.location << ")" << eom;
742  return true;
743  }
744  }
745  return false;
746 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
cmdlinet::args
argst args
Definition: cmdline.h:91
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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:122
tempfile.h
compilet::wrote_object
bool wrote_object
Definition: compile.h:119
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
compilet::echo_file_name
bool echo_file_name
Definition: compile.h:34
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:35
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
compilet::source_files
std::list< std::string > source_files
Definition: compile.h:48
ansi_c_entry_point.h
goto_modelt::clear
void clear()
Definition: goto_model.h:35
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:438
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:211
compilet::parse_stdin
bool parse_stdin(languaget &)
parses a source file (low-level parsing)
Definition: compile.cpp:523
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
Definition: language_file.cpp:85
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
compilet::ASSEMBLE_ONLY
@ ASSEMBLE_ONLY
Definition: compile.h:41
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:25
compilet::function_body_count
std::size_t function_body_count(const goto_functionst &) const
Definition: compile.cpp:665
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:50
compilet::doit
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:57
run
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:49
compilet::libraries
std::list< std::string > libraries
Definition: compile.h:50
goto_modelt
Definition: goto_model.h:26
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
goto_convert.h
Program Transformation.
configt::ansi_c
struct configt::ansi_ct ansi_c
run.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
compilet::LINK_LIBRARY
@ LINK_LIBRARY
Definition: compile.h:42
function_name_manglert
Mangles the names in an entire program and its symbol table.
Definition: name_mangler.h:31
compilet::validate_goto_model
bool validate_goto_model
Definition: compile.h:37
file_typet::NORMAL_ARCHIVE
@ NORMAL_ARCHIVE
write_goto_binary.h
Write GOTO binaries.
file_typet::FAILED_TO_OPEN_FILE
@ FAILED_TO_OPEN_FILE
validate_goto_model.h
compilet::add_compiler_specific_defines
void add_compiler_specific_defines() const
Definition: compile.cpp:676
compilet::link
bool link()
parses object files and links them
Definition: compile.cpp:311
compilet::written_macros
std::map< irep_idt, symbolt > written_macros
Definition: compile.h:112
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:21
CBMC_VERSION
const char * CBMC_VERSION
compilet::output_file_object
std::string output_file_object
Definition: compile.h:58
goto_functionst::clear
void clear()
Definition: goto_functions.h:70
compilet::object_files
std::list< std::string > object_files
Definition: compile.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
compilet::add_written_cprover_symbols
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
Definition: compile.cpp:723
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:15
file_typet::UNKNOWN
@ UNKNOWN
compilet::working_directory
std::string working_directory
Definition: compile.h:35
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:44
compilet::mode
enum compilet::@2 mode
compilet::file_local_mangle_suffix
const std::string file_local_mangle_suffix
String to include in all mangled names.
Definition: compile.h:103
concat_dir_file
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:159
compilet::compilet
compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
constructor
Definition: compile.cpp:631
compilet::output_file_executable
std::string output_file_executable
Definition: compile.h:55
goto_convert_functionst
Definition: goto_convert_functions.h:40
compilet::convert_symbols
void convert_symbols(goto_functionst &dest)
Definition: compile.cpp:682
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
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:47
compile.h
Compile and link source and object files.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
compilet::COMPILE_LINK
@ COMPILE_LINK
Definition: compile.h:43
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:418
compilet::object_file_extension
std::string object_file_extension
Definition: compile.h:54
message_handlert
Definition: message.h:28
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:97
compilet::~compilet
~compilet()
cleans up temporary files
Definition: compile.cpp:656
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:46
compilet::COMPILE_LINK_EXECUTABLE
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:44
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:50
file_typet::THIN_ARCHIVE
@ THIN_ARCHIVE
read_goto_binary.h
Read Goto Programs.
compilet::override_language
std::string override_language
Definition: compile.h:36
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:103
compilet::PREPROCESS_ONLY
@ PREPROCESS_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:171
compilet::output_directory_object
std::string output_directory_object
Definition: compile.h:58
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:270
compilet::keep_file_local
const bool keep_file_local
Whether to keep implementations of file-local symbols.
Definition: compile.h:100
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:180
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
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:365
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
compilet::parse_source
bool parse_source(const std::string &)
parses a source file
Definition: compile.cpp:605
messaget::M_WARNING
@ M_WARNING
Definition: message.h:170
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
suffix.h
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:14
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
compilet::write_bin_object_file
bool write_bin_object_file(const std::string &, const goto_modelt &)
Writes the goto functions of src_goto_model to a binary format object file.
Definition: compile.cpp:564
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:204
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:273
unicode.h
languaget
Definition: language.h:40
is_goto_binary
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Definition: read_goto_binary.cpp:190
detect_file_type
static file_typet detect_file_type(const std::string &file_name, message_handlert &message_handler)
Definition: compile.cpp:130
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:49
get_current_working_directory
std::string get_current_working_directory()
Definition: file_util.cpp:51
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:41
compilet::tmp_dirs
std::list< std::string > tmp_dirs
Definition: compile.h:51
r
static int8_t r
Definition: irep_hash.h:59
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:90
set_current_path
void set_current_path(const std::string &path)
Set working directory.
Definition: file_util.cpp:82
goto_convert_functions.h
Goto Programs with Functions.
static_lifetime_init.h
compilet::goto_model
goto_modelt goto_model
Definition: compile.h:31
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
file_typet
file_typet
Definition: compile.cpp:120
symbol_table_builder.h
compilet::COMPILE_ONLY
@ COMPILE_ONLY
Definition: compile.h:40
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:24
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