Fix for #582. (#586)

* Fix for #582. * Test for fix.
kframework · Oct 7, 2019 · f4f2406 · f4f2406
1 parent a293965
commit f4f2406
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 0 deletions.
diff --git a/semantics/c/language/translation/elaborator.k b/semantics/c/language/translation/elaborator.k
@@ -27,6 +27,8 @@ module C-ELABORATOR
      rule (.K => K) ~> compoundExp(K:K)
      rule R:KResult ~> compoundExp(K:K)
           => te(compoundExp(K), utype(R))
+     rule toRVal(R:RValue) ~> compoundExp(K:K)
+          => te(compoundExp(K), utype(R))
 
      rule <k> elaborate(K:K) ~> Cont:K => K </k>
           <elab> OldElab:K => .K </elab>

diff --git a/tests/unit-fail-compilation/static-init-comma.c b/tests/unit-fail-compilation/static-init-comma.c
@@ -0,0 +1,5 @@
+int x = (1, 0);
+
+int main() {
+      return x;
+}
diff --git a/tests/unit-fail-compilation/static-init-comma.c.ref b/tests/unit-fail-compilation/static-init-comma.c.ref
@@ -0,0 +1,8 @@
+static-init-comma.c:1:1: error: Non-constant static initializer.
+
+    Constraint violation (CV-TSE3):
+        see C11 section 6.7.9:4 http://rvdoc.org/C11/6.7.9
+        see CERT-C section MSC40-C http://rvdoc.org/CERT-C/MSC40-C
+        see MISRA-C section 8.1:1 http://rvdoc.org/MISRA-C/8.1
+
+Translation failed (kcc_config dumped). To repeat, run this command in directory unit-fail-compilation: