@@ -1249,6 +1249,8 @@ class Traverser(
1249
1249
): ObjectValue {
1250
1250
touchAddress(addr)
1251
1251
1252
+ val nullEqualityConstraint = mkEq(addr, nullObjectAddr)
1253
+
1252
1254
if (mockInfoGenerator != null ) {
1253
1255
val mockInfo = mockInfoGenerator.generate(addr)
1254
1256
@@ -1260,8 +1262,11 @@ class Traverser(
1260
1262
queuedSymbolicStateUpdates + = MemoryUpdate (mockInfos = persistentListOf(MockInfoEnriched (mockInfo)))
1261
1263
1262
1264
// add typeConstraint for mocked object. It's a declared type of the object.
1263
- queuedSymbolicStateUpdates + = typeRegistry.typeConstraint(addr, mockedObject.typeStorage).all().asHardConstraint()
1264
- queuedSymbolicStateUpdates + = mkEq(typeRegistry.isMock(mockedObject.addr), UtTrue ).asHardConstraint()
1265
+ val typeConstraint = typeRegistry.typeConstraint(addr, mockedObject.typeStorage).all()
1266
+ val isMockConstraint = mkEq(typeRegistry.isMock(mockedObject.addr), UtTrue )
1267
+
1268
+ queuedSymbolicStateUpdates + = typeConstraint.asHardConstraint()
1269
+ queuedSymbolicStateUpdates + = mkOr(isMockConstraint, nullEqualityConstraint).asHardConstraint()
1265
1270
1266
1271
return mockedObject
1267
1272
}
@@ -1286,8 +1291,10 @@ class Traverser(
1286
1291
typeStoragePossiblyWithOverriddenTypes
1287
1292
}
1288
1293
1294
+ val typeHardConstraint = typeRegistry.typeConstraint(addr, typeStorage).all().asHardConstraint()
1295
+
1289
1296
wrapper(type, addr)?.let {
1290
- queuedSymbolicStateUpdates + = typeRegistry.typeConstraint(addr, typeStorage).all().asHardConstraint()
1297
+ queuedSymbolicStateUpdates + = typeHardConstraint
1291
1298
return it
1292
1299
}
1293
1300
@@ -1303,8 +1310,11 @@ class Traverser(
1303
1310
queuedSymbolicStateUpdates + = MemoryUpdate (mockInfos = persistentListOf(MockInfoEnriched (mockInfo)))
1304
1311
1305
1312
// add typeConstraint for mocked object. It's a declared type of the object.
1306
- queuedSymbolicStateUpdates + = typeRegistry.typeConstraint(addr, mockedObject.typeStorage).all().asHardConstraint()
1307
- queuedSymbolicStateUpdates + = mkEq(typeRegistry.isMock(mockedObject.addr), UtTrue ).asHardConstraint()
1313
+ val typeConstraint = typeRegistry.typeConstraint(addr, mockedObject.typeStorage).all()
1314
+ val isMockConstraint = mkEq(typeRegistry.isMock(mockedObject.addr), UtTrue )
1315
+
1316
+ queuedSymbolicStateUpdates + = typeConstraint.asHardConstraint()
1317
+ queuedSymbolicStateUpdates + = mkOr(isMockConstraint, nullEqualityConstraint).asHardConstraint()
1308
1318
1309
1319
return mockedObject
1310
1320
}
@@ -1313,9 +1323,10 @@ class Traverser(
1313
1323
// We should create an object with typeStorage of all possible real types and concrete implementation
1314
1324
// Otherwise we'd have either a wrong type in the resolver, or missing method like 'preconditionCheck'.
1315
1325
val concreteImplementation = wrapperToClass[type]?.first()?.let { wrapper(it, addr) }?.concrete
1326
+ val isMockConstraint = mkEq(typeRegistry.isMock(addr), UtFalse )
1316
1327
1317
- queuedSymbolicStateUpdates + = typeRegistry.typeConstraint(addr, typeStorage).all().asHardConstraint()
1318
- queuedSymbolicStateUpdates + = mkEq(typeRegistry.isMock(addr), UtFalse ).asHardConstraint()
1328
+ queuedSymbolicStateUpdates + = typeHardConstraint
1329
+ queuedSymbolicStateUpdates + = mkOr(isMockConstraint, nullEqualityConstraint ).asHardConstraint()
1319
1330
1320
1331
return ObjectValue (typeStorage, addr, concreteImplementation)
1321
1332
}
0 commit comments