--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] "Re: How to ignore Incompatible declarations without, emitting errors?" (David MENTRE)



? 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