Enums were treated as their underlying type while reading.

kframework · Apr 6, 2017 · ea0aeb2 · ea0aeb2
1 parent 91161bd
commit ea0aeb2
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 1 deletion.
diff --git a/semantics/cpp14/language/common/memory/reading.k b/semantics/cpp14/language/common/memory/reading.k
@@ -52,6 +52,8 @@ module CPP-MEMORY-READING
      rule interpret(prv(0, Tr::Trace, T:CPPNullPtrTType)) => prv(nullptrVal, Tr, T)
      rule interpret(prv(0, Tr::Trace, T:CPPPointerType)) => prv(NullPointer, Tr, T)
 
-     rule interpret(prv(I:Int, Tr::Trace, T:CPPEnumType)) => #fun(prv(I::Int, Tr::Trace, (T => T)))(interpret(prv(I, Tr, underlyingType(T))))
+     syntax PRVal ::= interpretEnum(PRVal, CPPEnumType)
+     rule interpret(prv(I:Int, Tr::Trace, T:CPPEnumType)) => interpretEnum(interpret(prv(I, Tr, underlyingType(T))), T)
+     rule interpretEnum(prv(I:Int, Tr::Trace, T:CPPIntegerType), E:CPPEnumType) => prv(I, Tr, E)
 
 endmodule
diff --git a/tests/unit-pass/enum-copy-initialize.C b/tests/unit-pass/enum-copy-initialize.C
@@ -0,0 +1,10 @@
+enum class E { Val = 7 };
+enum F { F_Val = 8 };
+
+int main() {
+	E e1 = E::Val;
+	E e2 = e1;
+
+	F f1 = F_Val;
+	F f2 = f1;
+}