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

Thanks for the reply. This is what I expected to read, and will happily 
start fiddling with Frama-c.

I have been using Microsoft Research's VCC so far but we recently hit 
serious limitations in it, and I felt like trying something else out 
without throwing all the previous work away (including work that relies 
quite heavily on their typed memory model with pointer cast support). It 
also seems that Frama-c's plugin architecture would be good for our 
rather specific purpose verification problems, as opposed to having to 
give annotations that are not relevant to our goals.

I will keep you informed of anything I implement, and you will probably 
get more questions from me in the future :)

Cheers,
Francois Dupressoir

CUOQ Pascal wrote:
>
> 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
>