File tree Expand file tree Collapse file tree
main/kotlin/org/usvm/machine Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -9,7 +9,6 @@ import org.jacodb.ets.model.EtsNumberType
99import org.jacodb.ets.model.EtsRefType
1010import org.jacodb.ets.model.EtsScene
1111import org.jacodb.ets.model.EtsType
12- import org.jacodb.ets.model.EtsUnclearRefType
1312import org.jacodb.ets.model.EtsUndefinedType
1413import org.jacodb.ets.model.EtsUnionType
1514import org.jacodb.ets.model.EtsUnknownType
@@ -30,7 +29,6 @@ import org.usvm.machine.expr.TsUnresolvedSort
3029import org.usvm.machine.interpreter.TsStepScope
3130import org.usvm.machine.types.FakeType
3231import org.usvm.types.UTypeStream
33- import org.usvm.types.single
3432import org.usvm.util.mkFieldLValue
3533import kotlin.contracts.ExperimentalContracts
3634import kotlin.contracts.contract
Original file line number Diff line number Diff line change @@ -12,7 +12,6 @@ import org.usvm.machine.TsContext
1212import org.usvm.machine.interpreter.TsStepScope
1313import org.usvm.machine.types.ExprWithTypeConstraint
1414import org.usvm.machine.types.FakeType
15- import org.usvm.types.single
1615import org.usvm.util.boolToFp
1716
1817fun TsContext.mkTruthyExpr (
Original file line number Diff line number Diff line change @@ -97,7 +97,6 @@ import org.usvm.machine.types.FakeType
9797import org.usvm.machine.types.mkFakeValue
9898import org.usvm.memory.ULValue
9999import org.usvm.sizeSort
100- import org.usvm.types.single
101100import org.usvm.util.mkArrayIndexLValue
102101import org.usvm.util.mkArrayLengthLValue
103102import org.usvm.util.mkFieldLValue
Original file line number Diff line number Diff line change @@ -17,7 +17,6 @@ import org.usvm.machine.interpreter.TsStepScope
1717import org.usvm.machine.types.ExprWithTypeConstraint
1818import org.usvm.machine.types.FakeType
1919import org.usvm.machine.types.iteWriteIntoFakeObject
20- import org.usvm.types.single
2120import org.usvm.util.boolToFp
2221
2322sealed interface TsBinaryOperator {
Original file line number Diff line number Diff line change @@ -13,7 +13,6 @@ import org.usvm.UConcreteHeapRef
1313import org.usvm.USort
1414import org.usvm.UState
1515import org.usvm.api.targets.TsTarget
16- import org.usvm.collections.immutable.getOrPut
1716import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
1817import org.usvm.collections.immutable.internal.MutabilityOwnership
1918import org.usvm.collections.immutable.persistentHashMapOf
Original file line number Diff line number Diff line change @@ -15,7 +15,6 @@ import org.usvm.machine.TsContext
1515import org.usvm.machine.interpreter.TsStepScope
1616import org.usvm.machine.state.TsState
1717import org.usvm.memory.ULValue
18- import org.usvm.types.single
1918
2019fun TsContext.mkFakeValue (
2120 scope : TsStepScope ,
Original file line number Diff line number Diff line change @@ -15,7 +15,6 @@ import org.jacodb.ets.model.EtsMethodImpl
1515import org.jacodb.ets.model.EtsMethodParameter
1616import org.jacodb.ets.model.EtsMethodSignature
1717import org.jacodb.ets.model.EtsNumberType
18- import org.jacodb.ets.model.EtsParameterRef
1918import org.jacodb.ets.model.EtsScene
2019import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME
2120import org.jacodb.ets.utils.toEtsBlockCfg
Original file line number Diff line number Diff line change @@ -33,7 +33,6 @@ import org.usvm.api.TsValue
3333import org.usvm.isTrue
3434import org.usvm.machine.TsContext
3535import org.usvm.machine.expr.TsUnresolvedSort
36- import org.usvm.machine.expr.extractBool
3736import org.usvm.machine.expr.extractDouble
3837import org.usvm.machine.state.TsMethodResult
3938import org.usvm.machine.state.TsState
@@ -43,8 +42,6 @@ import org.usvm.memory.UReadOnlyMemory
4342import org.usvm.memory.URegisterStackLValue
4443import org.usvm.mkSizeExpr
4544import org.usvm.model.UModelBase
46- import org.usvm.types.first
47- import org.usvm.types.single
4845
4946class TsTestResolver {
5047 fun resolve (method : EtsMethod , state : TsState ): TsTest = with (state.ctx) {
You can’t perform that action at this time.
0 commit comments