diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt index 4620d25aa..c2e715c59 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt @@ -663,7 +663,7 @@ class TSSimpleValueResolver( } override fun visit(value: EtsNullConstant): UExpr = with(ctx) { - scope.calcOnState { mkTSNullValue() } + mkTSNullValue() } override fun visit(value: EtsUndefinedConstant): UExpr = with(ctx) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt index 2f0abfd7e..45746651c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt @@ -186,6 +186,7 @@ sealed interface TSBinaryOperator { ) ) + scope.assert(lhsType.fpTypeExpr or lhsType.boolTypeExpr) // TODO: support objects } @@ -206,6 +207,7 @@ sealed interface TSBinaryOperator { ) ) + scope.assert(lhsType.fpTypeExpr or lhsType.boolTypeExpr) // TODO: support objects } @@ -218,6 +220,7 @@ sealed interface TSBinaryOperator { ) ) + scope.assert(lhsType.refTypeExpr) // TODO: support objects } @@ -250,6 +253,7 @@ sealed interface TSBinaryOperator { ) ) + scope.assert(rhsType.fpTypeExpr or rhsType.boolTypeExpr) // TODO: support objects } @@ -270,6 +274,7 @@ sealed interface TSBinaryOperator { ) ) + scope.assert(rhsType.fpTypeExpr or rhsType.boolTypeExpr) // TODO: support objects } @@ -282,6 +287,7 @@ sealed interface TSBinaryOperator { ) ) + scope.assert(rhsType.refTypeExpr) // TODO: support objects } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt index 844962406..cfb3d4d01 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt @@ -2,10 +2,10 @@ package org.usvm.samples import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.RepeatedTest import org.usvm.api.TSObject import org.usvm.util.TSMethodTestRunner import org.usvm.util.getResourcePath -import kotlin.test.Test class Null : TSMethodTestRunner() { @@ -16,7 +16,7 @@ class Null : TSMethodTestRunner() { EtsScene(listOf(file)) } - @Test + @RepeatedTest(20) fun testIsNull() { val method = getMethod("Null", "isNull") discoverProperties(