diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 054d583873..9c260c84d0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -30,6 +30,7 @@ import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsValue +import org.jacodb.ets.model.EtsVoidType import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort @@ -167,6 +168,7 @@ class TsContext( is EtsStringType -> addressSort is EtsNullType -> addressSort is EtsUndefinedType -> addressSort + is EtsVoidType -> addressSort is EtsUnionType -> unresolvedSort is EtsIntersectionType -> { val memberSorts = type.types.map(::typeToSort) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/VoidAssignment.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/VoidAssignment.kt new file mode 100644 index 0000000000..922edac6ad --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/VoidAssignment.kt @@ -0,0 +1,23 @@ +package org.usvm.samples.lang + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import org.usvm.test.util.checkers.eq as exactly + +class VoidAssignment : TsMethodTestRunner() { + override val scene: EtsScene = loadScene("/samples/lang/VoidAssignment.ts") + + @Test + fun `assigned void call returns undefined after its mutation`() { + val method = getMethod("assignmentResult") + + checkMatches( + method = method, + analysisResultNumberMatches = exactly(1), + { result -> result eq 1 }, + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/lang/VoidAssignment.ts b/usvm-ts/src/test/resources/samples/lang/VoidAssignment.ts new file mode 100644 index 0000000000..26107ae476 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/VoidAssignment.ts @@ -0,0 +1,22 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class VoidMutation { + value: number = 0; + + change(): void { + this.value = 7; + } +} + +class VoidAssignment { + assignmentResult(): number { + const instance = new VoidMutation(); + const result = instance.change(); + const observation = { result, value: instance.value }; + if (observation.result === undefined && observation.value === 7) { + return 1; + } + return 0; + } +}