CBMC
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 5
16 
17 #include <iosfwd>
18 #include <string>
19 
20 class goto_functionst;
21 class goto_modelt;
22 class message_handlert;
23 class symbol_tablet;
24 
25 bool write_goto_binary(
26  std::ostream &out,
27  const goto_modelt &,
28  int version=GOTO_BINARY_VERSION);
29 
30 bool write_goto_binary(
31  std::ostream &out,
32  const symbol_tablet &,
33  const goto_functionst &,
34  int version=GOTO_BINARY_VERSION);
35 
36 bool write_goto_binary(
37  const std::string &filename,
38  const goto_modelt &,
39  message_handlert &);
40 
41 #endif // CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
GOTO_BINARY_VERSION
#define GOTO_BINARY_VERSION
Definition: write_goto_binary.h:15
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
write_goto_binary
bool write_goto_binary(std::ostream &out, const goto_modelt &, int version=5)
Writes a goto program to disc.
Definition: write_goto_binary.cpp:128
goto_modelt
Definition: goto_model.h:25
message_handlert
Definition: message.h:27
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24