<br><br><div class="gmail_quote">On Fri, Nov 7, 2008 at 11:40 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 7, 2008, at 12:44 AM, 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;">
>From what I can tell, an out-of-bounds check has three components:<br>
<br>
(1) a location L, which is an offset within a region X<br>
(2) the extent of region X<br>
(3) some logic to determine if the location L is outside the extent of region X<br>
<br>
We need to decide if we currently represent (1) for the interesting cases that we are initially interested in going after.<br>
<br>
I have some difficulty to understand this sentence. I think a we will just get a location MemRegionVal with a out-of-bound ElementRegion, returned by getLValue(). And nobody is aware of its illegality at that time.<br>
</blockquote>
<br></div>
Sorry.  ;-)<br>
<br>
I meant can we represent all "locations" (using SVals) for the cases that would be most interesting for array bounds checking?  At this point I think the answer is no, since we don't have a location that represents a "base" + "offset", where the base is a location (i.e., a MemRegion) and offset is an index off of that base.  Currently we drop all pointer arithmetic operations on the floor, so we haven't had to reason about such things yet.<br>

</blockquote></div><br>I think we have. That is an ElementRegion with a symbolic SVal as its index. Because all 'base'+'offset' boils down to an array element.<br>