Refine PointerSubChecker: compare the base region instead of the original

region, so that arithmetic within a memory chunk is allowed.

llvm-svn: 86652
This commit is contained in:
Zhongxing Xu 2009-11-10 02:37:53 +00:00
parent 05671ea10a
commit 80bbc6d138
4 changed files with 34 additions and 3 deletions

View File

@ -75,6 +75,8 @@ public:
const MemSpaceRegion *getMemorySpace() const;
const MemRegion *getBaseRegion() const;
const MemRegion *StripCasts() const;
bool hasStackStorage() const;

View File

@ -378,6 +378,24 @@ bool MemRegion::hasGlobalsOrParametersStorage() const {
return false;
}
// getBaseRegion strips away all elements and fields, and get the base region
// of them.
const MemRegion *MemRegion::getBaseRegion() const {
const MemRegion *R = this;
while (true) {
if (const ElementRegion *ER = dyn_cast<ElementRegion>(R)) {
R = ER->getSuperRegion();
continue;
}
if (const FieldRegion *FR = dyn_cast<FieldRegion>(R)) {
R = FR->getSuperRegion();
continue;
}
break;
}
return R;
}
//===----------------------------------------------------------------------===//
// View handling.
//===----------------------------------------------------------------------===//

View File

@ -48,11 +48,17 @@ void PointerSubChecker::PreVisitBinaryOperator(CheckerContext &C,
const MemRegion *LR = LV.getAsRegion();
const MemRegion *RR = RV.getAsRegion();
if (!(LR && RR) || (LR == RR))
if (!(LR && RR))
return;
// We don't reason about SymbolicRegions for now.
if (isa<SymbolicRegion>(LR) || isa<SymbolicRegion>(RR))
const MemRegion *BaseLR = LR->getBaseRegion();
const MemRegion *BaseRR = RR->getBaseRegion();
if (BaseLR == BaseRR)
return;
// Allow arithmetic on different symbolic regions.
if (isa<SymbolicRegion>(BaseLR) || isa<SymbolicRegion>(BaseRR))
return;
if (ExplodedNode *N = C.GenerateNode(B)) {

View File

@ -35,6 +35,11 @@ domain_port (const char *domain_b, const char *domain_e,
void f3() {
int x, y;
int d = &y - &x; // expected-warning{{Subtraction of two pointers that do not point to the same memory chunk may cause incorrect result.}}
int a[10];
int *p = &a[2];
int *q = &a[8];
d = q-p; // no-warning
}
void f4() {