13#ifndef CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
14#define CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
32class gdb_value_extractort
36 const symbol_table_baset &symbol_table,
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();
55 symbol_tablet get_snapshot_as_symbol_table();
57 using pointer_valuet = gdb_apit::pointer_valuet;
58 using memory_addresst = gdb_apit::memory_addresst;
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);
78 symbol_tablet symbol_table;
81 allocate_objectst allocate_objects;
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);
188 std::optional<std::string>
189 get_malloc_pointee(
const memory_addresst &point,
mp_integer member_size);
194 mp_integer get_type_size(
const typet &type)
const;
200 void analyze_symbol(
const irep_idt &symbol_name);
206 void add_assignment(
const exprt &lhs,
const exprt &value);
214 exprt get_array_value(
217 const source_locationt &location);
228 exprt get_expr_value(
230 const exprt &zero_expr,
231 const source_locationt &location);
238 exprt get_struct_value(
240 const exprt &zero_expr,
241 const source_locationt &location);
248 exprt get_union_value(
250 const exprt &zero_expr,
251 const source_locationt &location);
260 exprt get_pointer_value(
262 const exprt &zero_expr,
263 const source_locationt &location);
272 exprt get_pointer_to_member_value(
274 const pointer_valuet &pointer_value,
275 const source_locationt &location);
284 exprt get_non_char_pointer_value(
286 const pointer_valuet &value,
287 const source_locationt &location);
296 exprt get_pointer_to_function_value(
298 const pointer_valuet &pointer_value,
299 const source_locationt &location);
311 exprt get_char_pointer_value(
313 const memory_addresst &memory_location,
314 const source_locationt &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,
331 const pointer_typet &expected_type);
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Low-level interface to gdb.
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.