Review fixes

UnitTestBot · Feb 12, 2024 · 82415bc · 82415bc
1 parent a4baab7
commit 82415bc
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestStateResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestStateResolver.kt
@@ -199,7 +199,7 @@ abstract class JcTestStateResolver<T>(
             model.typeStreamOf(ref)
         } else {
             // allocated object
-            finalStateMemory.typeStreamOf(ref)
+            memory.typeStreamOf(ref)
         }.filterBySupertype(type)
 
         // We filter allocated object type stream, because it could be stored in the input array,

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt
@@ -16,6 +16,7 @@ import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.isTrue
 import org.usvm.machine.JcContext
+import org.usvm.machine.jctx
 import org.usvm.machine.state.JcState
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
@@ -50,8 +51,8 @@ internal class JcStaticFieldsMemoryRegion<Sort : USort>(
 
     override fun read(key: JcStaticFieldLValue<Sort>): UExpr<Sort> {
         val field = key.field
-
-        return fieldValuesByClass[field.enclosingClass]?.get(field) ?: sort.sampleUValue()
+        return fieldValuesByClass[field.enclosingClass]?.get(field)
+            ?: sort.jctx.mkStaticFieldReading(key.memoryRegionId as JcStaticFieldRegionId, field, sort)
     }
 
     override fun write(