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())
107 for(
const auto &t_it : instruction.
targets)
112 for(
const auto &l_it : instruction.
labels)
145 out << char(0x7f) <<
"GBF";
165 const std::string &filename,
174 message.error() <<
"Failed to open '" << filename <<
"'";
Class that provides messages with a built-in verbosity 'level'.
#define GOTO_BINARY_VERSION
binary irep conversions with hashing
source_locationt source_location
The location of the instruction in the source file.
typet type
Type of symbol.
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.
goto_program_instruction_typet type
What kind of instruction?
const irept & reference_convert(std::istream &)
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.
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
irep_idt mode
Language mode.
const std::string & id2string(const irep_idt &d)
codet code
Do not read or modify directly – use get_X() instead.
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.
source_locationt location
Source code location of definition of symbol.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
static std::string binary(const constant_exprt &src)
#define forall_goto_functions(it, functions)
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.