<div dir="ltr"><br><br><div class="gmail_quote">On Thu, Oct 9, 2008 at 1:08 AM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="Ih2E3d"><br>
On Oct 7, 2008, at 7:05 PM, Zhongxing Xu wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
By coincidence, the value of &j may be the same across loop iterations, but that isn't guaranteed to be the case.<br>
<br>
I think this is guaranteed to be the case by the C semantics.<br>
</blockquote>
<br></div>
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.<br>
<br>
Consider the case of VLAs:<br>
<br>
for (...) {<br>
 if(some_condition) {<br>
  int x[foo()];<br>
  int y[bar()];<div class="Ih2E3d"><br>
  int j = foo();<br>
  if (p) (*p)++;<br></div>
  p = &y[0];<br>
 }<br>
}<br>
<br>
In this example, the location of 'y' on the stack will depend on the result of the calls to foo() and bar() respectively.</blockquote><div><br>Now I see your point. Thank you.<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
<br>
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.<div class="Ih2E3d"><br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
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.<br>

</blockquote>
<br></div>
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.<br>

<br>
</blockquote></div><br>Yeah, these details should be considered when we do the implementation.<br></div>