35 for(
const auto &symbol_pair : symbol_table.
symbols)
40 const symbolt &sym = symbol_pair.second;
55 flags = (flags << 1) | static_cast<int>(sym.
is_weak);
56 flags = (flags << 1) | static_cast<int>(sym.
is_type);
57 flags = (flags << 1) | static_cast<int>(sym.
is_property);
58 flags = (flags << 1) | static_cast<int>(sym.
is_macro);
59 flags = (flags << 1) | static_cast<int>(sym.
is_exported);
60 flags = (flags << 1) | static_cast<int>(sym.
is_input);
61 flags = (flags << 1) | static_cast<int>(sym.
is_output);
62 flags = (flags << 1) | static_cast<int>(sym.
is_state_var);
63 flags = (flags << 1) | static_cast<int>(sym.
is_parameter);
64 flags = (flags << 1) | static_cast<int>(sym.
is_auxiliary);
65 flags = (flags << 1) | static_cast<int>(
false);
66 flags = (flags << 1) | static_cast<int>(sym.
is_lvalue);
70 flags = (flags << 1) | static_cast<int>(sym.
is_extern);
71 flags = (flags << 1) | static_cast<int>(sym.
is_volatile);
80 if(it->second.body_available())
87 if(fct.second.body_available())
109 for(
const auto &t_it : instruction.
targets)
114 for(
const auto &l_it : instruction.
labels)
147 out << char(0x7f) <<
"GBF";
153 const int current_goto_version = 4;
154 if(version < current_goto_version)
158 else if(version > current_goto_version)
164 out, symbol_table, goto_functions, irepconverter);
169 const std::string &filename,
179 "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?
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool write_goto_binary_v4(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 4.
exprt value
Initial value of symbol.
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.
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.
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)
A collection of 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'.
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
binary irep conversions with hashing
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
void write_string_ref(std::ostream &, const irep_idt &)
Output a string and maintain a reference to it.
source_locationt source_location
The location of the instruction in the source file.
irep_idt base_name
Base (non-scoped) name.
static std::string binary(const constant_exprt &src)
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
goto_functionst goto_functions
GOTO functions.