Skip to content

Commit

Permalink
Format
Browse files Browse the repository at this point in the history
  • Loading branch information
Lipen committed Feb 28, 2025
1 parent 02c54db commit d5a97eb
Show file tree
Hide file tree
Showing 5 changed files with 10 additions and 13 deletions.
2 changes: 1 addition & 1 deletion usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ package org.usvm.machine

import io.ksmt.sort.KFp64Sort
import io.ksmt.utils.asExpr
import org.jacodb.ets.base.EtsAnyType
import io.ksmt.utils.cast
import org.jacodb.ets.base.EtsAnyType
import org.jacodb.ets.base.EtsBooleanType
import org.jacodb.ets.base.EtsNullType
import org.jacodb.ets.base.EtsNumberType
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,6 @@ import org.usvm.api.allocateArray
import org.usvm.collections.immutable.getOrPut
import org.usvm.isTrue
import org.usvm.machine.TsContext
import org.usvm.machine.interpreter.TsStaticFieldLValue
import org.usvm.machine.interpreter.TsStepScope
import org.usvm.machine.interpreter.isInitialized
import org.usvm.machine.interpreter.markInitialized
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -199,15 +199,15 @@ class TsInterpreter(
it.signature == lhv.field.enclosingClass
} ?: return@doWithState

val instance = scope.calcOnState {
val (updated, result) = staticStorage.getOrPut(clazz, ownership) {
val address = memory.allocConcrete(clazz.type)
// TODO: memory.types.allocate(...)
address
}
staticStorage = updated
result
}
val instance = scope.calcOnState {
val (updated, result) = staticStorage.getOrPut(clazz, ownership) {
val address = memory.allocConcrete(clazz.type)
// TODO: memory.types.allocate(...)
address
}
staticStorage = updated
result
}

// TODO: initialize the static field first
// Note: Since we are assigning to a static field, we can omit its initialization,
Expand Down
1 change: 0 additions & 1 deletion usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ import org.jacodb.ets.base.EtsStmt
import org.jacodb.ets.base.EtsType
import org.jacodb.ets.base.EtsValue
import org.jacodb.ets.model.EtsClass
import org.jacodb.ets.model.EtsClassSignature
import org.jacodb.ets.model.EtsMethod
import org.usvm.PathNode
import org.usvm.UCallStack
Expand Down
1 change: 0 additions & 1 deletion usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
package org.usvm.samples

import org.jacodb.ets.model.EtsScene
import org.jacodb.ets.utils.loadEtsFileAutoConvert
import org.junit.jupiter.api.Test
import org.usvm.api.TsValue
import org.usvm.util.TsMethodTestRunner
Expand Down

0 comments on commit d5a97eb

Please sign in to comment.