--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on September 2013 ---
? 2013/9/12 18:01, frama-c-discuss-request at lists.gforge.inria.fr ??: > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr > > To subscribe or unsubscribe via the World Wide Web, visit > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > or, via email, send a message with subject or body 'help' to > frama-c-discuss-request at lists.gforge.inria.fr > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > > > Today's Topics: > > 1. Re: Could I disable acsl/rte/wp annotation in value analysis? > or treat all property to be valid in value analysis? (David Yang) > 2. Re: "Re: How to ignore Incompatible declarations without > emitting errors?" (David MENTRE) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Thu, 12 Sep 2013 16:28:59 +0800 > From: David Yang <abiao.yang at gmail.com> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] Could I disable acsl/rte/wp annotation > in value analysis? or treat all property to be valid in value > analysis? > Message-ID: > <CAA1cxujCcK5DHGo2aATV=H5+RTWRnmOO83DSOSmhm+apRF1meQ at mail.gmail.com> > Content-Type: text/plain; charset="windows-1252" > >> On Sun, Sep 8, 2013 at 7:23 PM, David Yang <abiao.yang at gmail.com<http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>> >> wrote: >>> * the code below the line 5 is dead code. I understand that it is because >> *>* the default context-width is 2. So line 5 is out of bound memory >> access. >> *> >>> * But i want to analysis the function by not treat all code to be dead >> code >> *>* and continue the value analysis procedure. >> *> >> This is not possible in Frama-C's value analysis. More precisely, there are >> no values worth continuing the execution with after an undefined behavior, >> such as an out-of-bounds memory access, because ?undefined behavior? means >> that anything is possible. This is discussed as one of the points in this >> article: https://www.dropbox.com/s/el2lidf5v71ogm6/p.pdf >> If you want the value analysis not to treat the code as dead code, tell it >> that variable A points to an array of size at least the value of variable >> size. There are several ways to do that. You may find that the best results >> are obtained with separate analyses for each size. > Dear Pascal, > > Thank you very much for replying me. > I choose to programmatically construct a new function with a new statement > to call that the function by using following api functions. > > Cil.emptyFunction ... > Cil.mkStmt ... > > At the same time I initialized those argument programmatically. > > Best regards. > > David. > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130912/7d3f2afb/attachment-0001.html> > > ------------------------------ > > Message: 2 > Date: Thu, 12 Sep 2013 11:40:50 +0200 > From: David MENTRE <dmentre at linux-france.org> > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> > Subject: Re: [Frama-c-discuss] "Re: How to ignore Incompatible > declarations without emitting errors?" > Message-ID: > <CAC3Lx=ZdRe4pR-ykBJDOoBeb_hj8ztb9Z9HOeXiBWVxgMaxu3Q at mail.gmail.com> > Content-Type: text/plain; charset=ISO-8859-1 > > Hello David, > > 2013/9/12 David Yang <abiao.yang at gmail.com>: >> While I use gcc -C -E -I/$FRAMA_C_PATH/share/frama-c/libc -nostdinc test.c >> >> It failed to pre-process the file. > The "$FRAMA_C_PATH" notation was supposed to mean the location of YOUR > Frama-C setup. ;-) > > In my case this is > "/usr/local/stow/frama-c-Fluorine-20130601/share/frama-c/libc" so I > need to use command: > gcc -C -E -I/usr/local/stow/frama-c-Fluorine-20130601/share/frama-c/libc > -nostdinc test.c > > You need to adapt this to YOUR setting. > > Notice that command "frama-c -print-share-path" can help you find the > relevant path. > > Best regards, > david > > > > ------------------------------ > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > End of Frama-c-discuss Digest, Vol 64, Issue 20 > *********************************************** Thanks very much. Yes, I was using the absolute path. ;-) Thanks for reminding of this issue. I was wondering whether i could pre-processed by using frama-c path without using -nostdinc flag, i.e. using frama-c share library along with including system headers by the following command : gcc -C -E -I/usr/local/share/frama-c/libc -I. test.c Looking forward to your reply. Best regards, David