Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] memcpy / memset question

  • Subject: [Frama-c-discuss] memcpy / memset question
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 18 Aug 2015 10:47:53 +0200
  • In-reply-to: <CAGSRWbjiKXeX75=hvAE+16Lr4ikb-eHQLab9m1bYRmUM+9qdBA@mail.gmail.com>
  • References: <CAGSRWbjiKXeX75=hvAE+16Lr4ikb-eHQLab9m1bYRmUM+9qdBA@mail.gmail.com>
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;
}