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