Go to the documentation of this file.
35 for(std::size_t i=0; i<count; i++)
55 sym.
is_weak = (flags &(1 << 16))!=0;
56 sym.
is_type = (flags &(1 << 15))!=0;
58 sym.
is_macro = (flags &(1 << 13))!=0;
60 sym.
is_input = (flags &(1 << 11))!=0;
79 entry.first->second.type = code_type;
80 entry.first->second.set_parameter_identifiers(code_type);
83 symbol_table.
add(sym);
88 for(std::size_t fct_index = 0; fct_index < count; ++fct_index)
93 typedef std::map<goto_programt::targett, std::list<unsigned> > target_mapt;
94 target_mapt target_map;
95 typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
96 rev_target_mapt rev_target_map;
101 for(std::size_t ins_index = 0; ins_index < ins_count; ++ins_index)
116 rev_target_map.insert(
117 rev_target_map.end(),
118 std::make_pair(instruction.
target_number, itarget))->second!=itarget)
122 for(std::size_t i=0; i<t_count; i++)
124 target_map[itarget].push_back(irepconverter.
read_gb_word(in));
128 for(std::size_t i=0; i<l_count; i++)
131 instruction.
labels.push_back(label);
140 for(target_mapt::iterator tit = target_map.begin();
141 tit!=target_map.end();
146 for(std::list<unsigned>::iterator nit = tit->second.begin();
147 nit!=tit->second.end();
151 rev_target_mapt::const_iterator entry=rev_target_map.find(n);
153 entry != rev_target_map.end(),
154 "something from the target map should also be in the reverse target "
156 ins->targets.push_back(entry->second);
167 #if GOTO_BINARY_VERSION > 5
168 #error This code should be removed
184 const std::string &filename,
193 hdr[0]=
static_cast<char>(in.get());
194 hdr[1]=
static_cast<char>(in.get());
195 hdr[2]=
static_cast<char>(in.get());
197 if(hdr[0]==
'G' && hdr[1]==
'B' && hdr[2]==
'F')
203 hdr[3]=
static_cast<char>(in.get());
204 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
208 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
210 if(!filename.empty())
211 message.error() <<
"Sorry, but I can't read ELF binary '" << filename
214 message.error() <<
"Sorry, but I can't read ELF binaries"
221 message.error() <<
"'" << filename <<
"' is not a goto-binary"
238 "The input was compiled with an old version of "
249 "The input was compiled with an unsupported version of "
Class that provides messages with a built-in verbosity 'level'.
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define GOTO_BINARY_VERSION
binary irep conversions with hashing
source_locationt source_location
The location of the instruction in the source file.
static bool read_bin_goto_object(std::istream &in, symbol_tablet &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
irep_idt read_gb_string(std::istream &)
reads a string from the stream
The type of an expression, extends irept.
typet type
Type of symbol.
goto_program_instruction_typet type
What kind of instruction?
const irept & reference_convert(std::istream &)
void compute_location_numbers()
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
static std::size_t read_gb_word(std::istream &)
Interpret a stream of byte as a 7-bit encoded unsigned number.
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.
void set_hidden()
Mark a symbol for internal use.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
irep_idt mode
Language mode.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
codet code
Do not read or modify directly – use get_X() instead.
const irep_idt & id() const
A goto function, consisting of function type (see type), function body (see body),...
goto_program_instruction_typet
The type of an instruction in a GOTO program.
::goto_functiont goto_functiont
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
A collection of goto functions.
exprt value
Initial value of symbol.
unsigned target_number
A number to identify branch targets.
source_locationt location
Source code location of definition of symbol.
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
Goto Programs with Functions.
irep_idt read_string_ref(std::istream &)
Read a string reference from the stream.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
irep_idt module
Name of module the symbol belongs to.
This class represents an instruction in the GOTO intermediate representation.
bool is_target() const
Is this node a branch target?
irep_idt name
The unique identifier.
instructionst::iterator targett
Data structure for representing an arbitrary statement in a program.