--- layout: fc_discuss_archives title: Message 77 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis: treating locations at absolute addresses as volatile?



Hello all,

some of you may use Frama-C's value analysis, and some of those
may use the option -absolute-valid-range.
In pure theory this option should be considered as a Frama-C option
and not just as a value analysis option, but this particular option
is only taken into account by the value analysis and the plug-ins
that depend directly on it. It specifies that a range of absolute
addresses in memory should be considered as valid.

Currently, when this option is used, the value analysis considers
that the locations in question are ordinary locations. Would anyone
object if the behavior in the next version was to consider that
they are, from the point of view of the value analysis,
assimilated to volatile locations: what is read from them
is any integer and not necessarily what was previously
written there by the program?

The modelization of volatile locations in Frama-C will ultimately
change anyway, but I am talking about the next version here,
not about the far future.

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090422/242ba657/attachment.htm