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

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.

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.

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