Test fixes

UnitTestBot · Dec 20, 2024 · 703b36c · 703b36c
1 parent a5aed8f
commit 703b36c
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 4 deletions.
diff --git a/...c/main/kotlin/org/usvm/machine/interpreter/transformers/JcSingleInstructionTransformer.kt b/...c/main/kotlin/org/usvm/machine/interpreter/transformers/JcSingleInstructionTransformer.kt
@@ -99,7 +99,12 @@ class JcSingleInstructionTransformer(originalInstructions: JcInstList<JcInst>) {
         }
     }
 
+    @OptIn(ExperimentalContracts::class)
     inline fun MutableList<JcInst>.addInstruction(origin: JcInstLocation, body: (JcInstLocation) -> JcInst) {
+        contract {
+            callsInPlace(body, InvocationKind.EXACTLY_ONCE)
+        }
+
         val index = size
         val newLocation = JcInstLocationImpl(origin.method, index, origin.lineNumber)
         val instruction = body(newLocation)

diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/collections/QueueUsagesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/collections/QueueUsagesTest.kt
@@ -90,8 +90,8 @@ class QueueUsagesTest : JavaMethodTestRunner() {
             eq(4),
             { _, q, r -> q == null && r == 0 },
             { _, q, r -> q is LinkedList<*> && r == 1 },
-            { _, q, r -> q is ArrayDeque<*> && r == 2 },
-            { _, q, r -> q !is LinkedList<*> && q !is ArrayDeque<*> && r == 3 }
+            { _, q, r -> q is java.util.ArrayDeque<*> && r == 2 },
+            { _, q, r -> q !is LinkedList<*> && q !is java.util.ArrayDeque<*> && r == 3 }
         )
     }
 
@@ -102,8 +102,8 @@ class QueueUsagesTest : JavaMethodTestRunner() {
             eq(4),
             { _, q, r -> q == null && r == 0 },
             { _, q, r -> q is LinkedList<*> && r == 1 },
-            { _, q, r -> q is ArrayDeque<*> && r == 2 },
-            { _, q, r -> q !is LinkedList<*> && q !is ArrayDeque<*> && r == 3 } // this is uncovered
+            { _, q, r -> q is java.util.ArrayDeque<*> && r == 2 },
+            { _, q, r -> q !is LinkedList<*> && q !is java.util.ArrayDeque<*> && r == 3 } // this is uncovered
         )
     }