Skip to content

Commit ee7ef44

Browse files
committed
Fix an issue with resolved class
1 parent 49a940e commit ee7ef44

1 file changed

Lines changed: 2 additions & 1 deletion

File tree

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ import org.jacodb.ets.model.EtsBitOrExpr
1515
import org.jacodb.ets.model.EtsBitXorExpr
1616
import org.jacodb.ets.model.EtsBooleanConstant
1717
import org.jacodb.ets.model.EtsCastExpr
18+
import org.jacodb.ets.model.EtsClassSignature
1819
import org.jacodb.ets.model.EtsClassType
1920
import org.jacodb.ets.model.EtsConstant
2021
import org.jacodb.ets.model.EtsDeleteExpr
@@ -632,7 +633,7 @@ class TsExprResolver(
632633
): UExpr<out USort>? = with(ctx) {
633634
val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef
634635
scope.doWithState {
635-
pathConstraints += if (field.type.isResolved()) {
636+
pathConstraints += if (field.enclosingClass != EtsClassSignature.UNKNOWN) {
636637
// If we know an enclosing class of the field,
637638
// we can add a type constraint about the instance type.
638639
// Probably, it's redundant since either both class and field

0 commit comments

Comments
 (0)