expr_initializert: fix type of enum constants

Daniel Kroening · thk123 · commit 6f38516a8503 · 2019-01-23T10:50:36.000Z
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
@@ -270,10 +270,13 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   }
   else if(type_id==ID_c_enum_tag)
   {
-    return
-      expr_initializer_rec(
-        ns.follow_tag(to_c_enum_tag_type(type)),
-        source_location);
+    exprt result = expr_initializer_rec(
+      ns.follow_tag(to_c_enum_tag_type(type)), source_location);
+
+    // use the tag type
+    result.type() = type;
+
+    return result;
   }
   else if(type_id==ID_struct_tag)
   {

Original file line number	Diff line number	Diff line change
`@@ -270,10 +270,13 @@ exprt expr_initializert<nondet>::expr_initializer_rec(`
`270`	`270`	`}`
`271`	`271`	`else if(type_id==ID_c_enum_tag)`
`272`	`272`	`{`
`273`		`- return`
`274`		`- expr_initializer_rec(`
`275`		`- ns.follow_tag(to_c_enum_tag_type(type)),`
`276`		`- source_location);`
	`273`	`+ exprt result = expr_initializer_rec(`
	`274`	`+ ns.follow_tag(to_c_enum_tag_type(type)), source_location);`
	`275`	`+`
	`276`	`+ // use the tag type`
	`277`	`+ result.type() = type;`
	`278`	`+`
	`279`	`+ return result;`
`277`	`280`	`}`
`278`	`281`	`else if(type_id==ID_struct_tag)`
`279`	`282`	`{`