Skip to content

Commit 85dccd0

Browse files
committed
Add propertyName for constant args
1 parent dca5df4 commit 85dccd0

3 files changed

Lines changed: 3 additions & 3 deletions

File tree

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ internal fun TsExprResolver.handleArrayAccess(
3131
val arrayRef = array.asExpr(addressSort)
3232

3333
// Check for undefined or null array access.
34-
checkUndefinedOrNullPropertyRead(scope, arrayRef, "[]") ?: return null
34+
checkUndefinedOrNullPropertyRead(scope, arrayRef, propertyName = "[]") ?: return null
3535

3636
// Resolve the index.
3737
val resolvedIndex = resolve(value.index) ?: return null

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -826,7 +826,7 @@ class TsExprResolver(
826826
val obj = resolve(expr.right)?.asExpr(addressSort) ?: return null
827827

828828
// Check for null/undefined access
829-
checkUndefinedOrNullPropertyRead(scope, obj, "<in>") ?: return null
829+
checkUndefinedOrNullPropertyRead(scope, obj, propertyName = "<in>") ?: return null
830830

831831
logger.warn {
832832
"The 'in' operator is supported yet, the result may not be accurate"

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ internal fun TsExprResolver.handleAssignToArrayIndex(
2727
val array = resolvedArray.asExpr(addressSort)
2828

2929
// Check for undefined or null array access.
30-
checkUndefinedOrNullPropertyRead(scope, array, "[]") ?: return null
30+
checkUndefinedOrNullPropertyRead(scope, array, propertyName = "[]") ?: return null
3131

3232
// Resolve the index.
3333
val resolvedIndex = resolve(lhv.index) ?: return null

0 commit comments

Comments
 (0)