<br><br><div class="gmail_quote">On Tue, Mar 10, 2009 at 2:09 PM, 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="im"><br>
On Mar 9, 2009, at 10:48 PM, Zhongxing Xu wrote:<br>
<br>
</div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Hi Ted,<br>
<br><div class="im">
We don't have any casts for this example. So why would p and q point to different region?<br>
<br>
typedef struct s* MyPointer;<br>
<br>
struct s* foo();<br>
<br>
void bar() {<br>
  MyPointer p = foo();<br>
  struct s* q = p;<br>
}<br>
</div></blockquote>
<br>
<br>
That's a fair point.  There are no casts in this example.  That doesn't mean, however, that we don't have to reason about them when they are present.  Put another way, I'm not convinced it isn't a problem.<br>

<br>
For example, considered the following contrived example:<br>
<br>
  struct s* p = ...<br>
  p->f = 5;<br>
<br>
  void* r = p;<br>
  MyPointer *q = r;<br>
  if (q->f == 5)<br>
    // do something<br>
<br>
  if (q == p)<br>
    // do something<br>
<br>
While contrived, we should be able to readily determine that q->f is indeed 5 at the first branch as well as the fact that q == p at the second branch.  We have a variety of hacks in place to handle some of these cases; it would be nice if there was just a clear, consistent model of what different kinds of region views mean and how they should be interpreted.<br>

<br>
The point of having a clear model for region views and their semantics that handles all cases consistently (and inductively) means that the corner cases just get naturally handled without us having to specifically consider them.</blockquote>
<div><br>I see your point. But how can we recognize which casts are semantic changes and which are sugar typed?<br>I doubt there is a consistent rule for this.<br></div></div><br>