CBMC
write_goto_binary.cpp File Reference

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>
+ Include dependency graph for write_goto_binary.cpp:

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...
 

Detailed Description

Write GOTO binaries.

Definition in file write_goto_binary.cpp.

Function Documentation

◆ write_goto_binary() [1/4]

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.

◆ write_goto_binary() [2/4]

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.

◆ write_goto_binary() [3/4]

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.

◆ write_goto_binary() [4/4]

static void write_goto_binary ( std::ostream &  out,
const symbol_table_baset symbol_table,
const goto_functionst goto_functions,
irep_serializationt irepconverter 
)
static

Writes a goto program to disc, using goto binary format.

Definition at line 133 of file write_goto_binary.cpp.

◆ write_goto_functions_binary()

static void write_goto_functions_binary ( std::ostream &  out,
const goto_functionst goto_functions,
irep_serializationt irepconverter 
)
static

Writes the functions to file, but only those with non-empty body.

Definition at line 104 of file write_goto_binary.cpp.

◆ write_instructions_binary()

static void write_instructions_binary ( std::ostream &  out,
irep_serializationt irepconverter,
const std::pair< const irep_idt, goto_functiont > &  fct 
)
static

Definition at line 72 of file write_goto_binary.cpp.

◆ write_symbol_table_binary()

static void write_symbol_table_binary ( std::ostream &  out,
const symbol_table_baset symbol_table,
irep_serializationt irepconverter 
)
static

Writes the symbol table to file.

Definition at line 23 of file write_goto_binary.cpp.