--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on October 2013 ---
[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>