34 for(
const auto &symbol_pair : symbol_table.
symbols)
39 const symbolt &sym = symbol_pair.second;
54 flags = (flags << 1) | static_cast<int>(sym.
is_weak);
55 flags = (flags << 1) | static_cast<int>(sym.
is_type);
56 flags = (flags << 1) | static_cast<int>(sym.
is_property);
57 flags = (flags << 1) | static_cast<int>(sym.
is_macro);
58 flags = (flags << 1) | static_cast<int>(sym.
is_exported);
59 flags = (flags << 1) | static_cast<int>(sym.
is_input);
60 flags = (flags << 1) | static_cast<int>(sym.
is_output);
61 flags = (flags << 1) | static_cast<int>(sym.
is_state_var);
62 flags = (flags << 1) | static_cast<int>(sym.
is_parameter);
63 flags = (flags << 1) | static_cast<int>(sym.
is_auxiliary);
64 flags = (flags << 1) | static_cast<int>(
false);
65 flags = (flags << 1) | static_cast<int>(sym.
is_lvalue);
69 flags = (flags << 1) | static_cast<int>(sym.
is_extern);
70 flags = (flags << 1) | static_cast<int>(sym.
is_volatile);
80 if(gf_entry.second.body_available())
88 if(fct.second.body_available())
96 for(
const auto &instruction : fct.second.body.instructions)
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";
168 const std::string &filename,
177 message.
error() <<
"Failed to open '" << filename <<
"'";
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 ...
void write_string_ref(std::ostream &, const irep_idt &)
Output a string and maintain a reference to it.
const irept & reference_convert(std::istream &)
Class that provides messages with a built-in verbosity 'level'.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
irep_idt base_name
Base (non-scoped) name.
irep_idt module
Name of module the symbol belongs to.
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
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 std::string binary(const constant_exprt &src)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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