--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on May 2009 ---
CUOQ Pascal wrote: > If by "untyped sequence of byte arrays" you mean one untyped byte > array for each "base address", base addresses being among other things > string literals and variables, this is quite exactly the memory model of the > value analysis plug-in. A weakest precondition plug-in such as Jessie > may have a more abstract view of memory, in order to obtain > separation hypotheses between pointers of different > types for free (at the cost of not handling some kinds of > pointer casts). Regarding documentation of memory models in jessie, I recommend http://www.lri.fr/~marche/moy09phd.pdf the "default" memory model is typed, which allows to assume separation properties which are handy in general, but does not allow pointer casts. When pointer casts occurs, it tries to switch to a more complicated memory model. See document above. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |