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