cprover
write_goto_binary.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Write GOTO binaries
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
13 #define CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
14 
15 #define GOTO_BINARY_VERSION 3
16 
17 #include <iosfwd>
18 #include <string>
19 
20 #include "goto_functions.h"
21 
22 class symbol_tablet;
23 class goto_functionst;
24 class message_handlert;
25 
27  std::ostream &out,
28  const symbol_tablet &symbol_table,
29  const goto_functionst &goto_functions,
30  int version=GOTO_BINARY_VERSION);
31 
33  const std::string &filename,
34  const symbol_tablet &lsymbol_table,
35  const goto_functionst &goto_functions,
36  message_handlert &message_handler);
37 
38 #endif // CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
Goto Programs with Functions.
#define GOTO_BINARY_VERSION
The symbol table.
Definition: symbol_table.h:52
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, int version=3)
Writes a goto program to disc.