13#ifndef CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
14#define CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
32class gdb_value_extractort
37 const std::vector<std::string> &args);
43 void analyze_symbols(
const std::list<std::string> &symbols);
47 std::string get_snapshot_as_c_code();
60 void create_gdb_process()
62 gdb_api.create_gdb_process();
64 bool run_gdb_to_breakpoint(
const std::string &breakpoint)
66 return gdb_api.run_gdb_to_breakpoint(breakpoint);
68 void run_gdb_from_core(
const std::string &corefile)
70 gdb_api.run_gdb_from_core(corefile);
84 std::map<exprt, exprt> assignments;
88 std::map<exprt, memory_addresst> outstanding_assignments;
92 std::map<memory_addresst, exprt> values;
104 size_t address2size_t(
const memory_addresst &point)
const;
109 bool check_containment(
const size_t &point_int)
const
111 return point_int >= begin_int && (begin_int + byte_size) > point_int;
116 const memory_addresst &begin,
123 bool contains(
const memory_addresst &point)
const
125 return check_containment(address2size_t(point));
133 distance(
const memory_addresst &point,
mp_integer member_size)
const;
151 std::vector<memory_scopet> dynamically_allocated;
154 std::map<irep_idt, pointer_valuet> memory_map;
156 bool has_known_memory_location(
const irep_idt &
id)
const
158 return memory_map.count(
id) != 0;
164 std::vector<memory_scopet>::iterator find_dynamic_allocation(
irep_idt name);
169 std::vector<memory_scopet>::iterator
170 find_dynamic_allocation(
const memory_addresst &point);
189 get_malloc_pointee(
const memory_addresst &point,
mp_integer member_size);
200 void analyze_symbol(
const irep_idt &symbol_name);
206 void add_assignment(
const exprt &lhs,
const exprt &value);
214 exprt get_array_value(
228 exprt get_expr_value(
230 const exprt &zero_expr,
238 exprt get_struct_value(
240 const exprt &zero_expr,
248 exprt get_union_value(
250 const exprt &zero_expr,
260 exprt get_pointer_value(
262 const exprt &zero_expr,
272 exprt get_pointer_to_member_value(
274 const pointer_valuet &pointer_value,
284 exprt get_non_char_pointer_value(
286 const pointer_valuet &value,
296 exprt get_pointer_to_function_value(
298 const pointer_valuet &pointer_value,
311 exprt get_char_pointer_value(
313 const memory_addresst &memory_location,
317 void process_outstanding_assignments();
322 std::string get_gdb_value(
const exprt &expr);
329 bool points_to_member(
330 pointer_valuet &pointer_value,
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.
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 symbol table base class interface.
The type of an expression, extends irept.
Low-level interface to gdb.
nonstd::optional< T > optionalt
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
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.