CBMC
|
Write GOTO binaries. More...
#include "write_goto_binary.h"
#include <fstream>
#include <util/exception_utils.h>
#include <util/irep_serialization.h>
#include <util/message.h>
#include <goto-programs/goto_model.h>
Go to the source code of this file.
Functions | |
static void | write_symbol_table_binary (std::ostream &out, const symbol_table_baset &symbol_table, irep_serializationt &irepconverter) |
Writes the symbol table to file. More... | |
static void | write_instructions_binary (std::ostream &out, irep_serializationt &irepconverter, const std::pair< const irep_idt, goto_functiont > &fct) |
static void | write_goto_functions_binary (std::ostream &out, const goto_functionst &goto_functions, irep_serializationt &irepconverter) |
Writes the functions to file, but only those with non-empty body. More... | |
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. More... | |
bool | write_goto_binary (std::ostream &out, const goto_modelt &goto_model, int version) |
Writes a goto program to disc. More... | |
bool | write_goto_binary (std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, int version) |
Writes a goto program to disc. More... | |
bool | write_goto_binary (const std::string &filename, const goto_modelt &goto_model, message_handlert &message_handler) |
Writes a goto program to disc. More... | |
Write GOTO binaries.
Definition in file write_goto_binary.cpp.
bool write_goto_binary | ( | const std::string & | filename, |
const goto_modelt & | goto_model, | ||
message_handlert & | message_handler | ||
) |
Writes a goto program to disc.
Definition at line 187 of file write_goto_binary.cpp.
bool write_goto_binary | ( | std::ostream & | out, |
const goto_modelt & | goto_model, | ||
int | version | ||
) |
Writes a goto program to disc.
Definition at line 144 of file write_goto_binary.cpp.
bool write_goto_binary | ( | std::ostream & | out, |
const symbol_table_baset & | symbol_table, | ||
const goto_functionst & | goto_functions, | ||
int | version | ||
) |
Writes a goto program to disc.
Definition at line 157 of file write_goto_binary.cpp.
|
static |
Writes a goto program to disc, using goto binary format.
Definition at line 133 of file write_goto_binary.cpp.
|
static |
Writes the functions to file, but only those with non-empty body.
Definition at line 104 of file write_goto_binary.cpp.
|
static |
Definition at line 72 of file write_goto_binary.cpp.
|
static |
Writes the symbol table to file.
Definition at line 23 of file write_goto_binary.cpp.