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

[Zhongxing Xu]

On Thu, Oct 9, 2008 at 1:08 AM, Ted Kremenek <kremenek at apple.com> wrote:

>
> 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.


Now I see your point. Thank you.


>
>
> 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.
>
>
Yeah, these details should be considered when we do the implementation.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20081009/3778321f/attachment.html>