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