Executor module updated to actual usvm with some improvements and fixes

UnitTestBot · Oct 9, 2023 · 95cba97 · 95cba97
1 parent aad21bb
commit 95cba97
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 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
@@ -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
@@ -264,7 +264,7 @@ class JcTestExecutor(
             ref: UConcreteHeapRef, heapRef: UHeapRef, type: JcArrayType
         ): Pair<UTestExpression, List<UTestInst>> {
             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 =