@@ -84,14 +84,14 @@ class SampleExprResolver(
84
84
fun resolveStruct (expr : StructExpr ): UHeapRef ? = with (ctx) {
85
85
when (expr) {
86
86
is StructCreation -> {
87
- val ref = scope.calcOnState { memory.alloc(expr.type) } ? : return null
87
+ val ref = scope.calcOnState { memory.alloc(expr.type) }
88
88
89
89
for ((field, fieldExpr) in expr.fields) {
90
90
val sort = typeToSort(field.type)
91
91
val fieldRef = UFieldLValue (sort, ref, field)
92
92
val fieldUExpr = resolveExpr(fieldExpr) ? : return null
93
93
94
- scope.doWithState { memory.write(fieldRef, fieldUExpr) } ? : return null
94
+ scope.doWithState { memory.write(fieldRef, fieldUExpr) }
95
95
}
96
96
97
97
ref
@@ -110,15 +110,15 @@ class SampleExprResolver(
110
110
val size = resolveInt(expr.size) ? : return null
111
111
checkArrayLength(size, expr.values.size) ? : return null
112
112
113
- val ref = scope.calcOnState { memory.malloc(expr.type, size) } ? : return null
113
+ val ref = scope.calcOnState { memory.malloc(expr.type, size) }
114
114
115
115
val cellSort = typeToSort(expr.type.elementType)
116
116
117
117
val values = expr.values.map { resolveExpr(it) ? : return null }
118
118
values.forEachIndexed { index, kExpr ->
119
119
val lvalue = UArrayIndexLValue (cellSort, ref, mkBv(index), expr.type)
120
120
121
- scope.doWithState { memory.write(lvalue, kExpr) } ? : return null
121
+ scope.doWithState { memory.write(lvalue, kExpr) }
122
122
}
123
123
124
124
// TODO: memset is not implemented
@@ -140,7 +140,7 @@ class SampleExprResolver(
140
140
val ref = resolveArray(expr.array) ? : return null
141
141
checkNullPointer(ref) ? : return null
142
142
val lengthRef = UArrayLengthLValue (ref, expr.array.type)
143
- val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) } ? : return null
143
+ val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
144
144
checkHardMaxArrayLength(length) ? : return null
145
145
scope.assert (mkBvSignedLessOrEqualExpr(mkBv(0 ), length)) ? : return null
146
146
length
@@ -300,7 +300,7 @@ class SampleExprResolver(
300
300
301
301
val idx = resolveInt(index) ? : return null
302
302
val lengthRef = UArrayLengthLValue (arrayRef, array.type)
303
- val length = scope.calcOnState { memory.read(lengthRef).asExpr(ctx.sizeSort) } ? : return null
303
+ val length = scope.calcOnState { memory.read(lengthRef).asExpr(ctx.sizeSort) }
304
304
305
305
checkHardMaxArrayLength(length) ? : return null
306
306
0 commit comments