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; }
- Follow-Ups:
- [Frama-c-discuss] memcpy / memset question
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] memcpy / memset question
- References:
- [Frama-c-discuss] memcpy / memset question
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] memcpy / memset question
- Prev by Date: [Frama-c-discuss] fopen and null pointers
- Next by Date: [Frama-c-discuss] trouble debugging assertions
- Previous by thread: [Frama-c-discuss] memcpy / memset question
- Next by thread: [Frama-c-discuss] memcpy / memset question
- Index(es):