@@ -4945,6 +4945,11 @@ void Executor::executeMemoryOperation(ExecutionState &state,
49454945 const ObjectState *os = i->second ;
49464946
49474947 ref<Expr> inBounds = mo->getBoundsCheckPointer (address, bytes);
4948+ if (UseGEPExpr && isGEPExpr (address)) {
4949+ inBounds = AndExpr::create (inBounds, mo->getBoundsCheckPointer (base, 1 ));
4950+ inBounds =
4951+ AndExpr::create (inBounds, mo->getBoundsCheckPointer (base, size));
4952+ }
49484953
49494954 StatePair branches = fork (*unbound, inBounds, true , BranchType::MemOp);
49504955 ExecutionState *bound = branches.first ;
@@ -4993,6 +4998,10 @@ void Executor::executeMemoryOperation(ExecutionState &state,
49934998 unbound = nullptr ;
49944999 } else {
49955000 ref<Expr> baseInObject = mo->getBoundsCheckPointer (base, 1 );
5001+ if (UseGEPExpr && isGEPExpr (address)) {
5002+ baseInObject = OrExpr::create (baseInObject,
5003+ mo->getBoundsCheckPointer (base, size));
5004+ }
49965005 branches = fork (*unbound, baseInObject, true , BranchType::MemOp);
49975006 bound = branches.first ;
49985007 if (bound) {
@@ -5008,7 +5017,6 @@ void Executor::executeMemoryOperation(ExecutionState &state,
50085017 }
50095018 }
50105019
5011-
50125020 if (unbound) {
50135021 StatePair branches =
50145022 fork (*unbound, Expr::createIsZero (base), true , BranchType::MemOp);
@@ -5028,7 +5036,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
50285036 (isa<ReadExpr>(address) || isa<ConcatExpr>(address) ||
50295037 (UseGEPExpr && isGEPExpr (address)))) {
50305038 ObjectPair p =
5031- lazyInstantiateVariable (*unbound, base, target, targetType , size);
5039+ lazyInstantiateVariable (*unbound, base, target, baseTargetType , size);
50325040 assert (p.first && p.second );
50335041
50345042 const MemoryObject *mo = p.first ;
0 commit comments