<br><br><div class="gmail_quote">On Fri, Nov 7, 2008 at 3:39 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="Ih2E3d"><br>
On Nov 6, 2008, at 10:01 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;">
Also I think we should have a clear client for the extent before/when we implement the extent mechanism. One direct client is the array element access checker.<br>
</blockquote>
<br></div>
This can be (potentially) be done in GRExprEngine, just like we handle Null dereferences.<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;">
It should be in the EvalLocation() method to check if the array access is out of bound.<br>
</blockquote>
<br></div>
That or EvalLoad().  An out-of-bounds error occurs on a load or store.<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;">
But not all store manager support this check.<br>
</blockquote>
<br></div>
That's fine.  The default behavior is that all accesses are valid.<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;">
Shall we make a new transfer function to do this check?<br>
</blockquote>
<br></div>
Perhaps, but I think all the logic can be divided between the StoreManager and GRExprEngine.  The StoreManager is responsible for reasoning about what is valid memory, and GRExprEngine handles loads/stores.  </blockquote>
<div><br>This job splitting is OK for me. But does it violates the rule that 'StoreManager does no reasoning'?<br></div><div> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
What would there be left to put in a specific transfer function?<br>
<br>
</blockquote></div><br>