--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2015 ---
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>