33 for(
const auto &symbol_pair : symbol_table.
symbols)
38 const symbolt &sym = symbol_pair.second;
53 flags = (flags << 1) | static_cast<int>(sym.
is_weak);
54 flags = (flags << 1) | static_cast<int>(sym.
is_type);
55 flags = (flags << 1) | static_cast<int>(sym.
is_property);
56 flags = (flags << 1) | static_cast<int>(sym.
is_macro);
57 flags = (flags << 1) | static_cast<int>(sym.
is_exported);
58 flags = (flags << 1) | static_cast<int>(sym.
is_input);
59 flags = (flags << 1) | static_cast<int>(sym.
is_output);
60 flags = (flags << 1) | static_cast<int>(sym.
is_state_var);
61 flags = (flags << 1) | static_cast<int>(sym.
is_parameter);
62 flags = (flags << 1) | static_cast<int>(sym.
is_auxiliary);
63 flags = (flags << 1) | static_cast<int>(
false);
64 flags = (flags << 1) | static_cast<int>(sym.
is_lvalue);
68 flags = (flags << 1) | static_cast<int>(sym.
is_extern);
69 flags = (flags << 1) | static_cast<int>(sym.
is_volatile);
78 if(it->second.body_available())
85 if(fct.second.body_available())
107 for(
const auto &t_it : instruction.
targets)
112 for(
const auto &l_it : instruction.
labels)
145 out << char(0x7f) <<
"GBF";
154 throw "version 1 no longer supported";
157 throw "version 2 no longer supported";
161 out, symbol_table, goto_functions, irepconverter);
164 throw "unknown goto binary version";
172 const std::string &filename,
176 std::ofstream out(filename, std::ios::binary);
182 "Failed to open `" << filename <<
"'";
exprt guard
Guard for gotos, assume, assert.
irep_idt function
The function this instruction belongs to.
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
irep_idt mode
Language mode.
goto_program_instruction_typet type
What kind of instruction?
exprt value
Initial value of symbol.
void write_gb_word(std::ostream &out, std::size_t u)
outputs 4 characters for a long, most-significant byte first
irep_idt module
Name of module the symbol belongs to.
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
targetst targets
The list of successor instructions.
This class represents an instruction in the GOTO intermediate representation.
unsigned target_number
A number to identify branch targets.
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
void reference_convert(std::istream &, irept &irep)
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
binary irep conversions with hashing
bool write_goto_binary_v3(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 ver 2.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
void write_string_ref(std::ostream &, const irep_idt &)
outputs the string reference
source_locationt source_location
The location of the instruction in the source file.
irep_idt base_name
Base (non-scoped) name.
goto_programt coverage_criteriont message_handlert & message_handler
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
goto_functionst goto_functions
GOTO functions.