--- layout: fc_discuss_archives title: Message 56 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 Boris,

Many thanks for such detailed information.

In the function "interpret", it has this pointer: Node *volatile tree,
which you said it's a volatile pointer.
I mistake the "volatile Node* tree;" for the volatile pointer .

The interpret function is the function in eval.c file of gawk-3.0.2
software system.

Thanks again.

-david


On 15 October 2013 09:34, Boris Yakobowski <boris at yakobowski.org> wrote:

> Hi,
>
> I was about to give you the same answer as David Mentr?: the support
> of volatile variables in Value is quite good. Unfortunately, your code
> invokes one of the few cases that cannot be handled automatically.
>
> More precisely, your function 'interpret' uses a volatile pointer to a
> node (_not_ a pointer to a volatile node). Abstract interpreters have
> no perfect way to automatically model such a pointer. Using Top (or
> something equivalent) means that any write '*p = ...' would destroy
> any precise information about the entire memory; and all the other
> choices are potentially unsound. Values chooses to model such volatile
> pointers as [..-..], which is good for embedded code -- that accesses
> memory-mapped devices. In your example, this modelization is
> incorrect. The Volatile plugin would allow you to specify, using an
> user-supplied function, what happens when such a volatile pointer is
> read.
>
> On Mon, Oct 14, 2013 at 10:58 AM, David Yang <abiao.yang at gmail.com> wrote:
> > Dear David,
> >
> > Thank you for replying me.
> >
> > On 14 October 2013 08:38, David MENTRE <dmentre at linux-france.org> wrote:
> >>
> >> Would you have a minimal example that reproduces the issue?
> >>
> >
> > Attachment please find the example of the function using volatile
> variables.
> >
> > the command I used for analysis this function is:
> >
> > frama-c -lib-entry -main interpret  test.c -val -context-depth 0
> >
> >
> > Thanks again.
> >
> > -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
>
>
>
> --
> Boris
>
> _______________________________________________
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131015/1cece4e6/attachment.html>