@@ -294,18 +294,60 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
294
294
symbol_exprt dummy (" tmp" , expr.type ());
295
295
code_blockt assignments;
296
296
297
+ const auto zero_expr = zero_initializer (target_type, location, ns);
298
+ CHECK_RETURN (zero_expr);
299
+
300
+ // Check if pointer was dynamically allocated (via malloc). If so we will
301
+ // replace the pointee with a static array filled with values stored at the
302
+ // expected positions. Since the allocated size is over-approximation we may
303
+ // end up querying pass the allocated bounds and building larger array with
304
+ // meaningless values.
305
+ size_t allocated_size =
306
+ gdb_api.query_malloc_size (c_converter.convert (expr));
307
+ // get the sizeof(target_type) and thus the number of elements
308
+ const auto target_size_bits = pointer_offset_bits (target_type, ns);
309
+ CHECK_RETURN (target_size_bits.has_value ());
310
+ const auto number_of_elements = allocated_size / (*target_size_bits / 8 );
311
+ if (number_of_elements > 1 )
312
+ {
313
+ array_exprt::operandst elements;
314
+ // build the operands by querying for an index expression
315
+ for (size_t i = 0 ; i < number_of_elements; i++)
316
+ {
317
+ const auto sub_expr_value = get_expr_value (
318
+ index_exprt{expr, from_integer (i, index_type ())},
319
+ *zero_expr,
320
+ location);
321
+ elements.push_back (sub_expr_value);
322
+ }
323
+ CHECK_RETURN (elements.size () == number_of_elements);
324
+
325
+ // knowing the number of elements we can build the type
326
+ const typet target_array_type =
327
+ array_typet{target_type, from_integer (elements.size (), index_type ())};
328
+
329
+ array_exprt new_array{elements, to_array_type (target_array_type)};
330
+
331
+ // allocate a new symbol for the temporary static array
332
+ symbol_exprt array_dummy (" tmp" , pointer_type (target_array_type));
333
+ const auto array_symbol =
334
+ allocate_objects.allocate_automatic_local_object (
335
+ assignments, array_dummy, target_array_type);
336
+
337
+ // add assignment of value to newly created symbol
338
+ add_assignment (array_symbol, new_array);
339
+ values[memory_location] = array_symbol;
340
+ return array_symbol;
341
+ }
342
+
297
343
const symbol_exprt new_symbol =
298
344
to_symbol_expr (allocate_objects.allocate_automatic_local_object (
299
345
assignments, dummy, target_type));
300
346
301
347
dereference_exprt dereference_expr (expr);
302
348
303
- const auto zero_expr = zero_initializer (target_type, location, ns);
304
- CHECK_RETURN (zero_expr);
305
-
306
349
const exprt target_expr =
307
350
get_expr_value (dereference_expr, *zero_expr, location);
308
-
309
351
// add assignment of value to newly created symbol
310
352
add_assignment (new_symbol, target_expr);
311
353
0 commit comments