From 82415bc087d395866869728bdec8bfbf93e8a213 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Mon, 12 Feb 2024 13:05:47 +0300 Subject: [PATCH] Review fixes --- .../src/main/kotlin/org/usvm/api/util/JcTestStateResolver.kt | 2 +- .../usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt | 5 +++-- 2 files changed, 4 insertions(+), 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 index 5ffeaf487..9f8119642 100644 --- 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( 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 index 767af47f3..0affe1c0d 100644 --- 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( override fun read(key: JcStaticFieldLValue): UExpr { 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(