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