Go to the documentation of this file.
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 <<
"'";
Class that provides messages with a built-in verbosity 'level'.
source_locationt source_location
The location of the instruction in the source file.
void reference_convert(std::istream &, irept &irep)
typet type
Type of symbol.
goto_program_instruction_typet type
What kind of instruction?
irep_idt base_name
Base (non-scoped) name.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
targetst targets
The list of successor instructions.
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.
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
irep_idt mode
Language mode.
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.
A collection of goto functions.
exprt value
Initial value of symbol.
unsigned target_number
A number to identify branch targets.
goto_functionst goto_functions
GOTO functions.
irep_idt function
The function this instruction belongs to.
source_locationt location
Source code location of definition of symbol.
exprt guard
Guard for gotos, assume, assert.
static std::string binary(const constant_exprt &src)
#define forall_goto_functions(it, functions)
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
irep_idt module
Name of module the symbol belongs to.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.
irep_idt name
The unique identifier.
#define forall_goto_program_instructions(it, program)
void write_string_ref(std::ostream &, const irep_idt &)
Output a string and maintain a reference to it.