<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Nov 7, 2008, at 8:37 AM, Zhongxing Xu wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><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></blockquote></div><br><div>That's right. Wonderful.</div></body></html>