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