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

[Ted Kremenek]

On Oct 7, 2008, at 7:05 PM, Zhongxing Xu wrote:

>
> By coincidence, the value of &j may be the same across loop  
> iterations, but that isn't guaranteed to be the case.
>
> I think this is guaranteed to be the case by the C semantics.

That's certainly not the case.  There is no place in the C standard  
that says that.  Using a pointer to an object after the lifetime of  
that object has ended is always undefined behavior.

Consider the case of VLAs:

for (...) {
  if(some_condition) {
   int x[foo()];
   int y[bar()];
   int j = foo();
   if (p) (*p)++;
   p = &y[0];
  }
}

In this example, the location of 'y' on the stack will depend on the  
result of the calls to foo() and bar() respectively.

In practice, the location of 'j' will usually precede in 'x' and 'y',  
but this is an artifact of the implementation, not what is guaranteed  
by the language.

> The thing we should do is: when we exit the true branch (or more  
> generally a scope), we mark all local regions as invalid. Next time  
> we enter the scope, we reget them and mark as valid. This validity  
> property is associated with MemRegions only, has nothing to do with  
> VarDecl and mappings.

A validity property would be useful for all regions, allowing us to  
report accesses to invalid memory.  We should only track the validity  
of regions, however, that are actually referenced, so that we can  
prune this state from the store when possible.