Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Value analysis: treating locations at absolute addresses as volatile?
  • From: Pascal.CUOQ at cea.fr (Pascal Cuoq)
  • Date: Wed, 22 Apr 2009 16:20:20 +0200
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