28 const std::string &filename,
36 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;
81 symbol_table.
add(sym);
86 for(std::size_t i=0; i<count; i++)
91 typedef std::map<goto_programt::targett, std::list<unsigned> > target_mapt;
92 target_mapt target_map;
93 typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
94 rev_target_mapt rev_target_map;
99 for(std::size_t i=0; i<ins_count; i++)
102 goto_programt::instructiont &instruction=*itarget;
109 instruction.guard.make_nil();
112 instruction.target_number = irepconverter.
read_gb_word(in);
113 if(instruction.is_target() &&
114 rev_target_map.insert(
115 rev_target_map.end(),
116 std::make_pair(instruction.target_number, itarget))->second!=itarget)
120 for(std::size_t i=0; i<t_count; i++)
122 target_map[itarget].push_back(irepconverter.
read_gb_word(in));
126 for(std::size_t i=0; i<l_count; i++)
129 instruction.labels.push_back(label);
130 if(label==
"__CPROVER_HIDE")
138 for(target_mapt::iterator tit = target_map.begin();
139 tit!=target_map.end();
144 for(std::list<unsigned>::iterator nit = tit->second.begin();
145 nit!=tit->second.end();
149 rev_target_mapt::const_iterator entry=rev_target_map.find(n);
150 assert(entry!=rev_target_map.end());
151 ins->targets.push_back(entry->second);
171 const std::string &filename,
184 if(hdr[0]==
'G' && hdr[1]==
'B' && hdr[2]==
'F')
191 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
195 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
198 message.
error() <<
"Sorry, but I can't read ELF binary `" 201 message.
error() <<
"Sorry, but I can't read ELF binaries" 208 message.
error() <<
"`" << filename <<
"' is not a goto-binary" 227 "The input was compiled with an old version of " 233 symbol_table, functions,
240 "The input was compiled with an unsupported version of " irep_idt name
The unique identifier.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
irep_idt mode
Language mode.
Goto Programs with Functions.
exprt value
Initial value of symbol.
irep_idt read_string_ref(std::istream &)
reads a string reference from the stream
irep_idt module
Name of module the symbol belongs to.
irep_idt pretty_name
Language-specific display name.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
bool read_bin_goto_object_v3(std::istream &in, const std::string &filename, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler, irep_serializationt &irepconverter)
read goto binary format v3
const irep_idt & id() const
void compute_location_numbers()
void reference_convert(std::istream &, irept &irep)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_function_templatet< goto_programt > goto_functiont
function_mapt function_map
binary irep conversions with hashing
bool read_bin_goto_object(std::istream &in, const std::string &filename, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads a goto binary file back into a symbol and a function table
irep_idt read_gb_string(std::istream &)
reads a string from the stream
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
irep_idt base_name
Base (non-scoped) name.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
static std::size_t read_gb_word(std::istream &)
reads 4 characters and builds a long int from them
instructionst::iterator targett