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] "Re: How to ignore Incompatible declarations without, emitting errors?" (David MENTRE)

  • Subject: [Frama-c-discuss] "Re: How to ignore Incompatible declarations without, emitting errors?" (David MENTRE)
  • From: abiao.yang at gmail.com (David)
  • Date: Thu, 12 Sep 2013 18:30:38 +0800
  • In-reply-to: <mailman.29.1378980073.12435.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.29.1378980073.12435.frama-c-discuss@lists.gforge.inria.fr>
? 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