@@ -367,6 +367,45 @@ static std::string strip_first_field_from_suffix(
367
367
return suffix.substr (field.length () + 1 );
368
368
}
369
369
370
+ const value_sett::entryt *value_sett::get_entry_for_symbol (
371
+ const irep_idt identifier,
372
+ const typet &expr_type,
373
+ const std::string &suffix) const
374
+ {
375
+ // We only deal with pointers, integers, arrays and structs
376
+ if (
377
+ expr_type.id () != ID_pointer && expr_type.id () != ID_signedbv &&
378
+ expr_type.id () != ID_unsignedbv && expr_type.id () != ID_struct &&
379
+ expr_type.id () != ID_union && expr_type.id () != ID_array)
380
+ {
381
+ return nullptr ;
382
+ }
383
+
384
+ // look it up
385
+ const value_sett::entryt *entry = find_entry (id2string (identifier) + suffix);
386
+
387
+ // try first component name as suffix if not yet found
388
+ if (!entry && (expr_type.id () == ID_struct || expr_type.id () == ID_union))
389
+ {
390
+ const struct_union_typet &struct_union_type =
391
+ to_struct_union_type (expr_type);
392
+
393
+ const irep_idt &first_component_name =
394
+ struct_union_type.components ().front ().get_name ();
395
+
396
+ entry = find_entry (
397
+ id2string (identifier) + " ." + id2string (first_component_name) + suffix);
398
+ }
399
+
400
+ if (!entry)
401
+ {
402
+ // not found? try without suffix
403
+ entry = find_entry (identifier);
404
+ }
405
+
406
+ return entry;
407
+ }
408
+
370
409
void value_sett::get_value_set_rec (
371
410
const exprt &expr,
372
411
object_mapt &dest,
@@ -414,45 +453,17 @@ void value_sett::get_value_set_rec(
414
453
}
415
454
else if (expr.id ()==ID_symbol)
416
455
{
417
- irep_idt identifier=to_symbol_expr (expr).get_identifier ();
456
+ const entryt *entry = get_entry_for_symbol (
457
+ to_symbol_expr (expr).get_identifier (), expr_type, suffix);
418
458
419
- // is it a pointer, integer, array or struct?
420
- if (expr_type.id ()==ID_pointer ||
421
- expr_type.id ()==ID_signedbv ||
422
- expr_type.id ()==ID_unsignedbv ||
423
- expr_type.id ()==ID_struct ||
424
- expr_type.id ()==ID_union ||
425
- expr_type.id ()==ID_array)
459
+ if (entry)
426
460
{
427
- // look it up
428
- const entryt *entry =
429
- find_entry (id2string (identifier) + suffix);
430
-
431
- // try first component name as suffix if not yet found
432
- if (!entry && (expr_type.id () == ID_struct || expr_type.id () == ID_union))
433
- {
434
- const struct_union_typet &struct_union_type=
435
- to_struct_union_type (expr_type);
436
-
437
- const irep_idt &first_component_name =
438
- struct_union_type.components ().front ().get_name ();
439
-
440
- entry = find_entry (
441
- id2string (identifier) + " ." + id2string (first_component_name) +
442
- suffix);
443
- }
444
-
445
- // not found? try without suffix
446
- if (!entry)
447
- entry = find_entry (identifier);
448
-
449
- if (entry)
450
- make_union (dest, entry->object_map );
451
- else
452
- insert (dest, exprt (ID_unknown, original_type));
461
+ make_union (dest, entry->object_map );
453
462
}
454
463
else
464
+ {
455
465
insert (dest, exprt (ID_unknown, original_type));
466
+ }
456
467
}
457
468
else if (expr.id ()==ID_if)
458
469
{
0 commit comments