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