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] about volatile variable in value analysis plugin and "Volatile" plugin

Dear Pascal,

Thank you very much for your suggestion and solution.


On 15 October 2013 18:11, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:

> Hello,
>
> On Tue, Oct 15, 2013 at 12:12 PM, David Yang <abiao.yang at gmail.com> wrote:
>
>> The interpret function is the function in eval.c file of gawk-3.0.2
>> software system.
>>
>
> According to the NEWS file in gawk, ?Uses volatile declaration if STDC > 0
> to avoid problems due to longjmp.?
>
> The bad news is that it would be an enormous amount of work to correctly
> and precisely model longjmp so that you can analyze a gawk program that
> uses it.
>
> The good news is that since you are not going to model longjmp anyway, you
> can effectively ignore the volatile qualifier in the source files of gawk.
> Adding the option -Dvolatile= to the pre-processor's command-line options
> should do it.
>

Yeah, I only want to get the pdg of these functions.  So delete those
volatiles is good suggestion.


> Without the ?volatile? qualifier, those pointers that are inputs of the
> analysis' entry point have variables generated for them to point to
> according to -context-width and similar options.
>
> The pointer arguments for functions that are not the entry point of the
> analysis will behave as you would expect.
>

Not the entry point? I am sorry i don't understand it exactly. What do you
mean? not using the -lib-entry option?

Thanks again.
Best regards,

David
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131015/daf72886/attachment.html>