Fixed tests

ftsrg · Nov 16, 2023 · badcc43 · badcc43
1 parent 2a9e8c1
commit badcc43
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 6 deletions.
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt
@@ -33,12 +33,12 @@ fun valToAction(xcfa: XCFA, val1: Valuation, val2: Valuation): XcfaAction {
     val val2Map = val2.toMap()
     var i = 0
     val map: MutableMap<XcfaLocation, Int> = HashMap()
-    for (x in xcfa.procedures.first().locs) {
+    for (x in xcfa.procedures.first { it.name == "main" }.locs) {
         map[x] = i++
     }
     return XcfaAction(
         pid = 0,
-        edge = xcfa.procedures.first().edges.first { edge ->
+        edge = xcfa.procedures.first { it.name == "main" }.edges.first { edge ->
             map[edge.source] == (val1Map[val1Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() &&
                 map[edge.target] == (val2Map[val2Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()
         })
@@ -48,7 +48,7 @@ fun valToState(xcfa: XCFA, val1: Valuation): XcfaState<ExplState> {
     val valMap = val1.toMap()
     var i = 0
     val map: MutableMap<Int, XcfaLocation> = HashMap()
-    for (x in xcfa.procedures.first().locs) {
+    for (x in xcfa.procedures.first { it.name == "main" }.locs) {
         map[i++] = x
     }
     return XcfaState(

diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
@@ -65,12 +65,9 @@ class XcfaCliVerifyTest {
                 Arguments.of("/c/litmustest/singlethread/03bitwise.c", null),
                 Arguments.of("/c/litmustest/singlethread/04real.c", null),
                 Arguments.of("/c/litmustest/singlethread/06arrays.c", null),
-                Arguments.of("/c/litmustest/singlethread/07arrayinit.c", null),
-                Arguments.of("/c/litmustest/singlethread/08vararray.c", null),
                 Arguments.of("/c/litmustest/singlethread/13typedef.c", "--domain PRED_CART"),
                 Arguments.of("/c/litmustest/singlethread/14ushort.c", null),
                 Arguments.of("/c/litmustest/singlethread/15addition.c", null),
-                Arguments.of("/c/litmustest/singlethread/16loop.c", null),
                 Arguments.of("/c/litmustest/singlethread/20testinline.c", null),
                 Arguments.of("/c/litmustest/singlethread/21namecollision.c", null),
                 Arguments.of("/c/litmustest/singlethread/22nondet.c", null),