--- layout: fc_discuss_archives title: Message 55 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



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