We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 31ff087 commit 64a374eCopy full SHA for 64a374e
usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
@@ -249,7 +249,7 @@ fun TsContext.checkReadingInRange(
249
)
250
}
251
252
-fun TsContext.checkLengthBounds(
+fun TsContext.ensureLengthBounds(
253
scope: TsStepScope,
254
length: UExpr<TsSizeSort>,
255
maxLength: Int,
usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
@@ -59,7 +59,7 @@ fun TsContext.readArrayLength(
59
60
61
// Check that the length is within the allowed bounds.
62
- checkLengthBounds(scope, length, maxArraySize) ?: return null
+ ensureLengthBounds(scope, length, maxArraySize) ?: return null
63
64
// Convert the length to fp64.
65
return mkBvToFpExpr(
0 commit comments