On Nov 7, 2008, at 8:37 AM, Zhongxing Xu wrote:
On Fri, Nov 7, 2008 at 11:40 PM, Ted Kremenek <[EMAIL PROTECTED]>
wrote:
On Nov 7, 2008, at 12:44 AM, Zhongxing Xu wrote:
From what I can tell, an out-of-bounds check has three components:
(1) a location L, which is an offset within a region X
(2) the extent of region X
(3) some logic to determine if the location L is outside the extent
of region X
We need to decide if we currently represent (1) for the interesting
cases that we are initially interested in going after.
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.
Sorry. ;-)
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.
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.
That's right. Wonderful.
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
