--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] memcpy / memset question



Hi,
    I am analyzing some code that uses memcpy and memset
from <string.h>.  I notice that the frama libc came with implementations
for these that had their own annotations.  However, when doing
value analysis it doesn't seem to be working as I expected.
I'm using the attached test.c and when I analyze it, I get:

test.c:12:[kernel] warning: accessing uninitialized left-value: assert
\initialized(&targ[i]);

which indicates that the analyzer did not notice that memcpy
is initializing all of targ[0..n-1] when doing memcpy(targ, src, n).
Is there an easy way to force this in the analysis?

I see virtually the same thing happening with memset as well.

-- 
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150817/269cf023/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.c
Type: text/x-csrc
Size: 254 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150817/269cf023/attachment-0001.c>