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] 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                    |