File tree Expand file tree Collapse file tree 3 files changed +14
-6
lines changed
main/kotlin/org/usvm/machine/expr
test/kotlin/org/usvm/util
usvm-util/src/main/kotlin/org/usvm/test/util/checkers Expand file tree Collapse file tree 3 files changed +14
-6
lines changed Original file line number Diff line number Diff line change @@ -878,7 +878,7 @@ class TsExprResolver(
878
878
val fakeType = instanceRef.getFakeType(scope)
879
879
880
880
// If we want to get length from a fake object, we assume that it is an array.
881
- scope.assert ( fakeType.refTypeExpr)
881
+ scope.doWithState { pathConstraints + = fakeType.refTypeExpr }
882
882
883
883
val refLValue = getIntermediateRefLValue(instanceRef.address)
884
884
val obj = scope.calcOnState { memory.read(refLValue) }
@@ -973,6 +973,12 @@ class TsExprResolver(
973
973
}
974
974
975
975
override fun visit (expr : EtsNewArrayExpr ): UExpr <out USort >? = with (ctx) {
976
+ val arrayType = expr.type
977
+
978
+ require(arrayType is EtsArrayType ) {
979
+ " Expected EtsArrayType in newArrayExpr, but got ${arrayType::class .simpleName} "
980
+ }
981
+
976
982
scope.calcOnState {
977
983
val size = resolve(expr.size) ? : return @calcOnState null
978
984
@@ -1003,8 +1009,6 @@ class TsExprResolver(
1003
1009
blockOnFalseState = allocateException(EtsStringType ) // TODO incorrect exception type
1004
1010
)
1005
1011
1006
- val arrayType = expr.type as EtsArrayType
1007
-
1008
1012
if (arrayType.elementType is EtsArrayType ) {
1009
1013
TODO (" Multidimensional arrays are not supported yet, https://github.com/UnitTestBot/usvm/issues/287" )
1010
1014
}
Original file line number Diff line number Diff line change @@ -109,7 +109,9 @@ class TsTestResolver {
109
109
resolvedLValuesToFakeObjects + = arrayIndexLValue to fakeObject
110
110
}
111
111
112
- else -> error(" Unexpected lValue type: ${lValue::class .java.name} " )
112
+ else -> {
113
+ error(" Unexpected lValue type: ${lValue::class .java.name} " )
114
+ }
113
115
}
114
116
}
115
117
}
@@ -265,7 +267,9 @@ open class TsTestStateResolver(
265
267
resolveExpr(fakeObject.extractRef(finalStateMemory))
266
268
}
267
269
268
- else -> error(" Unsupported fake object type: $fakeType " )
270
+ else -> {
271
+ error(" Unsupported fake object type: $fakeType " )
272
+ }
269
273
}
270
274
}
271
275
Original file line number Diff line number Diff line change @@ -22,7 +22,7 @@ val ignoreNumberOfAnalysisResults = AnalysisResultsNumberMatcher(
22
22
23
23
val noResultsExpected = AnalysisResultsNumberMatcher (
24
24
description = " No executions expected" ,
25
- matcherFailedMessage = { it -> " Expected no analysis results, but $it executions were found" }
25
+ matcherFailedMessage = { " Expected no analysis results, but $it executions were found" }
26
26
) { it == 0 }
27
27
28
28
class AnalysisResultsNumberMatcher (
You can’t perform that action at this time.
0 commit comments