--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on August 2015 ---
Hello Tim, Le 18/08/2015 07:44, Tim Newsham a écrit : > 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? With Value Analysis, you should use both libc.c and builtin.c provided by Frama-C standard library to have proper definition of various C standard library function as C code (better understood by Value analysis). But for some reasons, Frama_C_memcpy() defined in builtin.c does not seem to work properly. You can use a work around by defining FRAMA_C_MEMCPY which uses a C only version. You also need to increase the -slevel parameter for the loop to 8, otherwise Value analysis applies its widening operator and the resulting value could be considered uninitialized. frama-c -val -cpp-extra-args='-DFRAMA_C_MEMCPY' `frama-c -print-share-path`/libc.c `frama-c -print-share-path`/builtin.c -slevel 8 tim-test.c Best regards, david -------------- next part -------------- #include <stdio.h> #include <string.h> int main(void) { unsigned char buf[] = { 0,1,2,3,4,5,6,7 }; unsigned char targ[8]; int i; memcpy(targ, buf, 8); for(i = 0; i < 8; i++) { printf("%d\n", targ[i]); } return 0; }