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

Hi!

>I am interested in learning more about the Frama-C tool, and especially 
>about the memory model it implements for C, before I go any further with it.

Thanks for your interest.
There is not a single memory model. Each plug-in is free to define
the hypotheses it needs. The annotation language, ACSL,
is as memory-model-agnostic as we were able to make it.

This has been discussed a bit before in
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-July/000581.html
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-July/000582.html

> Is it a classic "untyped sequence of byte arrays" model or is it anything more involved?

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).

> And more importantly, can it be changed/reimplemented 
> using a plugin or is it fixed in the core?

Each plug-in is free to represent memory as it sees fit,
there is not a single representation imposed (or even
provided) by the core.
What you should consider if you are thinking of starting
a new plug-in is:
1/ How will ACSL properties, that are usually attached
to a point in the analyzed program, translate in your memory
model?
2/ If you plan to interact with existing plug-ins more directly
than through the exchange of ACSL properties, how will you
translate the datatypes exported by the existing plug-in
into your own structures?

The core does not provide ready-made representations for
memory but the value analysis and the dependencies
analysis share the respective datatypes that they use internally.
You can use these if they fit your purpose. They are documented
lightly in the "plug-in development guide", pages 27 and 58.

Regards,

Pascal

-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: non disponible
Type: application/ms-tnef
Taille: 3755 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090526/53c71837/attachment.bin