retain union/struct tag type during initialization

Daniel Kroening · Daniel Kroening · commit 8e6ed7d23551 · 2018-09-19T21:38:21.000+01:00
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
@@ -291,17 +291,23 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   }
   else if(type_id==ID_struct_tag)
   {
-    return
-      expr_initializer_rec(
-        ns.follow_tag(to_struct_tag_type(type)),
-        source_location);
+    exprt result = expr_initializer_rec(
+      ns.follow_tag(to_struct_tag_type(type)), source_location);
+
+    // use the tag type
+    result.type() = type;
+
+    return result;
   }
   else if(type_id==ID_union_tag)
   {
-    return
-      expr_initializer_rec(
-        ns.follow_tag(to_union_tag_type(type)),
-        source_location);
+    exprt result = expr_initializer_rec(
+      ns.follow_tag(to_union_tag_type(type)), source_location);
+
+    // use the tag type
+    result.type() = type;
+
+    return result;
   }
   else if(type_id==ID_string)
   {

Original file line number	Diff line number	Diff line change
`@@ -291,17 +291,23 @@ exprt expr_initializert<nondet>::expr_initializer_rec(`
`291`	`291`	`}`
`292`	`292`	`else if(type_id==ID_struct_tag)`
`293`	`293`	`{`
`294`		`- return`
`295`		`- expr_initializer_rec(`
`296`		`- ns.follow_tag(to_struct_tag_type(type)),`
`297`		`- source_location);`
	`294`	`+ exprt result = expr_initializer_rec(`
	`295`	`+ ns.follow_tag(to_struct_tag_type(type)), source_location);`
	`296`	`+`
	`297`	`+ // use the tag type`
	`298`	`+ result.type() = type;`
	`299`	`+`
	`300`	`+ return result;`
`298`	`301`	`}`
`299`	`302`	`else if(type_id==ID_union_tag)`
`300`	`303`	`{`
`301`		`- return`
`302`		`- expr_initializer_rec(`
`303`		`- ns.follow_tag(to_union_tag_type(type)),`
`304`		`- source_location);`
	`304`	`+ exprt result = expr_initializer_rec(`
	`305`	`+ ns.follow_tag(to_union_tag_type(type)), source_location);`
	`306`	`+`
	`307`	`+ // use the tag type`
	`308`	`+ result.type() = type;`
	`309`	`+`
	`310`	`+ return result;`
`305`	`311`	`}`
`306`	`312`	`else if(type_id==ID_string)`
`307`	`313`	`{`