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



Hello David,

2013/10/11 David Yang <abiao.yang at gmail.com>:
> Value analysis plugin seems not to support "volatile" variables. While i use
> value analysis plugin to analysis a function has volatile variables, many
> dead code is reported.

Hmm, the reported dead code is probably an indirect effect of the use
of volatile. As far as I know, "volatile" is supported in Frama-C
Fluorine and tells Frama-C: "a new value can be read each time this
variable is accessed, do not rely on previous analysis for this
variable".

Would you have a minimal example that reproduces the issue?

Best regards,
david