@@ -418,6 +418,10 @@ exprt symbol_analyzert::get_expr_value(
418
418
419
419
return get_pointer_value (expr, zero_expr, location);
420
420
}
421
+ else if (type.id () == ID_union_tag)
422
+ {
423
+ return get_union_value (expr, zero_expr, location);
424
+ }
421
425
else
422
426
{
423
427
throw analysis_exceptiont (" unexpected expression:\n " + expr.pretty ());
@@ -459,6 +463,39 @@ exprt symbol_analyzert::get_struct_value(
459
463
return new_expr;
460
464
}
461
465
466
+ exprt symbol_analyzert::get_union_value (
467
+ const exprt &expr,
468
+ const exprt &zero_expr,
469
+ const source_locationt &location)
470
+ {
471
+ PRECONDITION (zero_expr.id () == ID_union);
472
+
473
+ PRECONDITION (expr.type ().id () == ID_union_tag);
474
+ PRECONDITION (expr.type () == zero_expr.type ());
475
+
476
+ exprt new_expr (zero_expr);
477
+
478
+ const union_tag_typet &union_tag_type = to_union_tag_type (expr.type ());
479
+ const union_typet union_type = ns.follow_tag (union_tag_type);
480
+
481
+ for (size_t i = 0 ; i < new_expr.operands ().size (); ++i)
482
+ {
483
+ const union_typet::componentt &component = union_type.components ()[i];
484
+
485
+ if (component.get_is_padding ())
486
+ {
487
+ continue ;
488
+ }
489
+
490
+ exprt &operand = new_expr.operands ()[i];
491
+ member_exprt member_expr (expr, component);
492
+
493
+ operand = get_expr_value (member_expr, operand, location);
494
+ }
495
+
496
+ return new_expr;
497
+ }
498
+
462
499
void symbol_analyzert::process_outstanding_assignments ()
463
500
{
464
501
for (const auto &pair : outstanding_assignments)
0 commit comments