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