Hi Lenny,
This looks a bit odd:
+
+ // If the size is zero, there won't be any actual memory access, so
+ // just bind the return value to the destination buffer and return.
+ if (stateZeroSize) {
C.addTransition(stateZeroSize);
+ state = state->BindExpr(CE, destVal);
+ return;
+ }
It looks like 'state' is assigned a new value that is never read.
On Mar 31, 2011, at 9:11 AM, Lenny Maiorani wrote:
> On 03/30/2011 05:34 PM, Lenny Maiorani wrote:
>>> As for the modeling of mempcpy() (and memcpy() for that matter): the
>>> >> behavior is that if NULL is passed as either the src or dst there will
>>> >> be a NULL pointer dereference unless the number of bytes to copy is 0. I
>>> >> am re-working the flow through evalCopyCommon to accurately reflect
>>> >> that.
>> > I'm fine with that coming in with a later patch. I just didn't know what
>> > the plan was. Please feel free to use FIXME comments in the code to
>> > indicate "things to do" in the future.
>> >
>> > If you want to regenerate the patch without tabs (and comments adjusted),
>> > I'll be happy to apply it!
> Attached is a revised patch. The tabs and comments are reformatted.
>
> More importantly, mempcpy() (and memcpy() for that matter) are being properly
> modelled. Meaning, if 0 bytes are to be copied it ignores the inputs. If the
> number of bytes to be copied is >0 then then the dest and src inputs are
> verified to be non-NULL. NULL triggers a bug report. Otherwise it is ensures
> that src and dest do not overlap and the dest buffer is large enough for the
> incoming bytes and triggers a bug report if it is not. Finally, it bind the
> return value (for mempcpy() is the byte after the last byte copied).
>
>
> -Lenny
>
> <mempcpy-checker.diff>_______________________________________________
> cfe-commits mailing list
> [email protected]
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
