From 95cba97e14b0e003a3517e78ca436dcfc179eae5 Mon Sep 17 00:00:00 2001 From: DaniilStepanov Date: Mon, 9 Oct 2023 14:40:58 +0300 Subject: [PATCH] Executor module updated to actual usvm with some improvements and fixes --- .../src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt | 3 ++- usvm-jvm/src/test/kotlin/org/usvm/util/JcTestExecutor.kt | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt index fe0fbe494..6a8d51047 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestInterpreter.kt @@ -52,6 +52,7 @@ import org.usvm.collection.array.UArrayIndexLValue import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collection.field.UFieldLValue import org.usvm.model.UModelBase +import org.usvm.sizeSort import org.usvm.types.first import org.usvm.types.firstOrNull @@ -208,7 +209,7 @@ class JcTestInterpreter( private fun resolveArray(ref: UConcreteHeapRef, heapRef: UHeapRef, type: JcArrayType): Any { val arrayDescriptor = ctx.arrayDescriptorOf(type) - val lengthRef = UArrayLengthLValue(heapRef, arrayDescriptor) + val lengthRef = UArrayLengthLValue(heapRef, arrayDescriptor, ctx.sizeSort) val resolvedLength = resolveLValue(lengthRef, ctx.cp.int) as Int val length = if (resolvedLength in 0..10_000) resolvedLength else 0 // TODO hack diff --git a/usvm-jvm/src/test/kotlin/org/usvm/util/JcTestExecutor.kt b/usvm-jvm/src/test/kotlin/org/usvm/util/JcTestExecutor.kt index 720105b7c..06312bd0f 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/util/JcTestExecutor.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/util/JcTestExecutor.kt @@ -264,7 +264,7 @@ class JcTestExecutor( ref: UConcreteHeapRef, heapRef: UHeapRef, type: JcArrayType ): Pair> { val arrayDescriptor = ctx.arrayDescriptorOf(type) - val lengthRef = UArrayLengthLValue(heapRef, arrayDescriptor) + val lengthRef = UArrayLengthLValue(heapRef, arrayDescriptor, ctx.sizeSort) val resolvedLength = resolveLValue(lengthRef, ctx.cp.int).first as UTestIntExpression // TODO hack val length =