75 const std::pair<const irep_idt, goto_functiont> &
fct)
79 for(
const auto &instruction :
fct.second.body.instructions)
82 irepconverter.reference_convert(instruction.source_location(), out);
85 const auto condition =
86 instruction.has_condition() ? instruction.condition() :
true_exprt();
93 for(
const auto &
t_it : instruction.targets)
98 for(
const auto &
l_it : instruction.labels)
112 if(
gf_entry.second.body_available())
120 if(!
fct.second.body_available())
164 out <<
char(0x7f) <<
"GBF";
173 "version " + std::to_string(version) +
" no longer supported",
179 "unknown goto binary version " + std::to_string(version),
188 const std::string &filename,
192 std::ofstream out(filename, std::ios::binary);
197 message.
error() <<
"Failed to open '" << filename <<
"'";
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The Boolean constant true.
const std::string & id2string(const irep_idt &d)
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
void write_gb_word(std::ostream &out, std::size_t u)
Write 7 bits of u each time, least-significant byte first, until we have zero.
binary irep conversions with hashing
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.
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.
static void write_symbol_table_binary(std::ostream &out, const symbol_table_baset &symbol_table, irep_serializationt &irepconverter)
Writes the symbol table to file.
#define GOTO_BINARY_VERSION