13#ifndef CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
14#define CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
41 const std::vector<std::string> &args);
96 std::map<memory_addresst, exprt>
values;
173 std::vector<memory_scopet>::iterator
234 const exprt &zero_expr,
244 const exprt &zero_expr,
254 const exprt &zero_expr,
266 const exprt &zero_expr,
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
Interface for running and querying GDB.
bool run_gdb_to_breakpoint(const std::string &breakpoint)
Run gdb to the given breakpoint.
void create_gdb_process()
Create a new gdb process for analysing the binary indicated by the first element in args
void run_gdb_from_core(const std::string &corefile)
Run gdb with the given core file.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The type of an expression, extends irept.
Low-level interface to gdb.
API to expression classes for Pointers.
Memory address imbued with the explicit boolean data indicating if the address is null or not.
Data associated with the value of a pointer, i.e.