88 if(
fct.second.body_available())
96 for(
const auto &instruction :
fct.second.body.instructions)
99 irepconverter.reference_convert(instruction.source_location(), out);
102 const auto condition =
103 instruction.has_condition() ? instruction.condition() :
true_exprt();
110 for(
const auto &
t_it : instruction.targets)
115 for(
const auto &
l_it : instruction.labels)
148 out <<
char(0x7f) <<
"GBF";
156 "version " + std::to_string(version) +
" no longer supported",
160 "unknown goto binary version " + std::to_string(version),
168 const std::string &filename,
172 std::ofstream out(filename, std::ios::binary);
177 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'.
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
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
#define GOTO_BINARY_VERSION