@@ -1249,6 +1249,8 @@ class Traverser(
12491249 ): ObjectValue {
12501250 touchAddress(addr)
12511251
1252+ val nullEqualityConstraint = mkEq(addr, nullObjectAddr)
1253+
12521254 if (mockInfoGenerator != null ) {
12531255 val mockInfo = mockInfoGenerator.generate(addr)
12541256
@@ -1260,8 +1262,11 @@ class Traverser(
12601262 queuedSymbolicStateUpdates + = MemoryUpdate (mockInfos = persistentListOf(MockInfoEnriched (mockInfo)))
12611263
12621264 // 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()
12651270
12661271 return mockedObject
12671272 }
@@ -1286,8 +1291,10 @@ class Traverser(
12861291 typeStoragePossiblyWithOverriddenTypes
12871292 }
12881293
1294+ val typeHardConstraint = typeRegistry.typeConstraint(addr, typeStorage).all().asHardConstraint()
1295+
12891296 wrapper(type, addr)?.let {
1290- queuedSymbolicStateUpdates + = typeRegistry.typeConstraint(addr, typeStorage).all().asHardConstraint()
1297+ queuedSymbolicStateUpdates + = typeHardConstraint
12911298 return it
12921299 }
12931300
@@ -1303,8 +1310,11 @@ class Traverser(
13031310 queuedSymbolicStateUpdates + = MemoryUpdate (mockInfos = persistentListOf(MockInfoEnriched (mockInfo)))
13041311
13051312 // 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()
13081318
13091319 return mockedObject
13101320 }
@@ -1313,9 +1323,10 @@ class Traverser(
13131323 // We should create an object with typeStorage of all possible real types and concrete implementation
13141324 // Otherwise we'd have either a wrong type in the resolver, or missing method like 'preconditionCheck'.
13151325 val concreteImplementation = wrapperToClass[type]?.first()?.let { wrapper(it, addr) }?.concrete
1326+ val isMockConstraint = mkEq(typeRegistry.isMock(addr), UtFalse )
13161327
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()
13191330
13201331 return ObjectValue (typeStorage, addr, concreteImplementation)
13211332 }
0 commit comments