diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/transformers/JcSingleInstructionTransformer.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/transformers/JcSingleInstructionTransformer.kt index b788672e4e..1f32920656 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/transformers/JcSingleInstructionTransformer.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/transformers/JcSingleInstructionTransformer.kt @@ -99,7 +99,12 @@ class JcSingleInstructionTransformer(originalInstructions: JcInstList) { } } + @OptIn(ExperimentalContracts::class) inline fun MutableList.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 index 18c9ee5318..b1b0c8567e 100644 --- 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 ) }