[cfe-commits] [PATCH] review request: mempcpy() checker implementation for Static Analyzer

[Ted Kremenek]

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
> cfe-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits