30 for(std::size_t i=0; i<count; i++)
50 sym.is_weak = (flags &(1 << 16))!=0;
51 sym.is_type = (flags &(1 << 15))!=0;
52 sym.is_property = (flags &(1 << 14))!=0;
53 sym.is_macro = (flags &(1 << 13))!=0;
54 sym.is_exported = (flags &(1 << 12))!=0;
55 sym.is_input = (flags &(1 << 11))!=0;
56 sym.is_output = (flags &(1 << 10))!=0;
57 sym.is_state_var = (flags &(1 << 9))!=0;
58 sym.is_parameter = (flags &(1 << 8))!=0;
59 sym.is_auxiliary = (flags &(1 << 7))!=0;
61 sym.is_lvalue = (flags &(1 << 5))!=0;
62 sym.is_static_lifetime = (flags &(1 << 4))!=0;
63 sym.is_thread_local = (flags &(1 << 3))!=0;
64 sym.is_file_local = (flags &(1 << 2))!=0;
65 sym.is_extern = (flags &(1 << 1))!=0;
66 sym.is_volatile = (flags &1)!=0;
115 target_mapt target_map;
140 if(instruction.is_target() &&
143 std::make_pair(instruction.target_number,
itarget))->second!=
itarget)
147 for(std::size_t i=0; i<
t_count; i++)
153 for(std::size_t i=0; i<
l_count; i++)
156 instruction.labels.push_back(label);
167 for(target_mapt::iterator
tit = target_map.begin();
168 tit!=target_map.end();
173 for(std::list<unsigned>::iterator
nit =
tit->second.begin();
181 "something from the target map should also be in the reverse target "
183 ins->targets.push_back(entry->second);
214 const std::string &filename,
222 hdr[0] =
static_cast<char>(in.get());
223 hdr[1] =
static_cast<char>(in.get());
224 hdr[2] =
static_cast<char>(in.get());
226 if(
hdr[0] ==
'G' &&
hdr[1] ==
'B' &&
hdr[2] ==
'F')
232 hdr[3] =
static_cast<char>(in.get());
233 if(
hdr[0] == 0x7f &&
hdr[1] ==
'G' &&
hdr[2] ==
'B' &&
hdr[3] ==
'F')
237 else if(
hdr[0] == 0x7f &&
hdr[1] ==
'E' &&
hdr[2] ==
'L' &&
hdr[3] ==
'F')
239 if(!filename.empty())
240 message.
error() <<
"Sorry, but I can't read ELF binary '" << filename
243 message.
error() <<
"Sorry, but I can't read ELF binaries"
250 message.
error() <<
"'" << filename <<
"' is not a goto-binary"
263 message.
error() <<
"The input was compiled with an old version of "
264 "goto-cc; please recompile"
275 message.
error() <<
"The input was compiled with an unsupported version of "
276 "goto-cc; please recompile"
static exprt guard(const exprt::operandst &guards, exprt cond)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
instructionst::iterator targett
Class that provides messages with a built-in verbosity 'level'.
The symbol table base class interface.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The type of an expression, extends irept.
Goto Programs with Functions.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
binary irep conversions with hashing
static void copy_parameter_identifiers(const symbol_table_baset &symbol_table, goto_functionst &functions)
The serialised form of the goto-model currently includes the parameter identifiers in the symbol tabl...
static void read_bin_goto_object(std::istream &in, symbol_table_baset &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
static void read_bin_functions_object(std::istream &in, goto_functionst &functions, irep_serializationt &irepconverter)
static void read_bin_symbol_table_object(std::istream &in, symbol_table_baset &symbol_table, irep_serializationt &irepconverter)
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
A total order over targett and const_targett.
#define GOTO_BINARY_VERSION