--- layout: fc_discuss_archives title: Message 18 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



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;
}