[cfe-commits] static analysis: multiple VarRegions per VarDecl?

[Ted Kremenek]

On Oct 6, 2008, at 11:49 PM, Zhongxing Xu wrote:

> Could you show me an example where the same VarDecl should bind to  
> different region during one analysis path?

Hopefully here is a better example to illustrate the point I was  
trying to make.

Consider:

int *p = 0;

for (...) {
   if(some_condition) {
    int j = foo();
    if (p) (*p)++;
    p = &j;
  }
}

This is a very contrived example, but the point is that the variable  
'j' goes out of scope at the end of the true block for  
if(some_condition), but 'p' still refers to the VarRegion for  
'j'  (which at that point is invalid).

Upon entry to if(some_condition) on a subsequent iteration of the  
loop, what should we do?  If we have one VarRegion for 'j', then the  
expression '(*p)++' will appear valid, even though it really refers to  
the 'j' on a previous loop iteration.  By coincidence, the value of &j  
may be the same across loop iterations, but that isn't guaranteed to  
be the case.  This is also poor programming, since 'p' refers to  
garbage as soon as the compound statement for if(some_condition)  
finishes.

There are potentially other solution than having multiple VarRegions.   
We could potentially fix up all the old bindings to &j after j goes  
out of scope to point to an invalid region.  This seems a little  
cumbersome, and it also causes us to lose some information that can be  
cumbersome to recover. (i.e., the region 'p' points to is now invalid,  
but what region did it point to originally?)

The only reason I'm bringing this up now is not that we have to  
implement flexible bindings for VarDecl* -> VarRegions right now (if  
that indeed is what we decide to do), but that the interface for  
getLVal(VarDecl*) and getRegion(VarDecl*) that is exposed in  
GRStateManager and StoreManager probably should take some extra  
parameters (e.g., const GRState*) to provide some context in case the  
StoreManager/RegionManager wishes to allow flexible bindings.