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

[Frama-c-discuss] Memory model




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                    |