const MemSpaceRegion *getMemorySpace() const;
+ const MemRegion *getBaseRegion() const;
+
const MemRegion *StripCasts() const;
bool hasStackStorage() 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.
//===----------------------------------------------------------------------===//
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)) {
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() {