Added missing c elements

ftsrg · Jul 25, 2023 · 57aae56 · 57aae56
1 parent 7d3d9bc
commit 57aae56
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 2 deletions.
diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt
@@ -365,7 +365,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo
         val breakLoc = param.breakLoc
         val continueLoc = param.continueLoc
         val returnLoc = param.returnLoc
-        return statement.accept(this, ParamPack(builder, lastLoc, breakLoc, continueLoc, returnLoc))
+        return statement.statement.accept(this, ParamPack(builder, lastLoc, breakLoc, continueLoc, returnLoc))
     }
 
     override fun visit(statement: CCompound, param: ParamPack): XcfaLocation {
@@ -417,7 +417,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo
         val breakLoc = param.breakLoc
         val continueLoc = param.continueLoc
         val returnLoc = param.returnLoc
-        return statement.accept(this, ParamPack(builder, lastLoc, breakLoc, continueLoc, returnLoc))
+        return statement.statement.accept(this, ParamPack(builder, lastLoc, breakLoc, continueLoc, returnLoc))
     }
 
     override fun visit(statement: CDoWhile, param: ParamPack): XcfaLocation {

diff --git a/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt
@@ -57,6 +57,7 @@ class TestFrontendXcfaBuilder {
                 arrayOf("/20testinline.c"),
                 arrayOf("/21namecollision.c"),
                 arrayOf("/22nondet.c"),
+                arrayOf("/23exotic.c"),
             )
         }
     }

diff --git a/subprojects/xcfa/c2xcfa/src/test/resources/23exotic.c b/subprojects/xcfa/c2xcfa/src/test/resources/23exotic.c
@@ -0,0 +1,20 @@
+extern unsigned int __VERIFIER_nondet_uint();
+int main() {
+    int i = 0;
+    do{
+        unsigned int add = __VERIFIER_nondet_uint();
+        switch(add) {
+            case 0:
+                break;
+            case 1:
+                i += add;
+                break;
+            default:
+                i += 1;
+                break;
+        }
+        if ( i == 5) continue;
+        if ( i == 11) break;
+    } while(i < 10);
+    if(i < 10) reach_error();
+}