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 locations

Hi,

>
> I think this would be really neat and probably not too difficult to
> implement knowing the different structs involved.


Being myself quick to push in the language things that do not belong there,
I think your idea is one of these! Probably you could implement a set of
macros that do almost what you want, except of course you would have to
specify in the macro definition the exact set of fields represented. Then,
these macros may be themselves generated from the source by appropriate
scripts ...

Also, in the above annotation on function_3, I would be curious to know the
> exact meaning, for ACSL and Frama-C of the following annotations (according
> to the current design):
> - assigns arg                   // does it mean changes the address of arg,
> of just the o_* and the addresses of arg->s_1 and arg->s_2, or some other
> signification?


It means nothing in fact. It is neither a memory location not a global
variable, so it does not mean anything, and it is ignored by the Jessie
plugin. Maybe a warning could be emitted.

>
> - assigns *arg                 // same question


The location pointed-to by pointer [arg] in the pre-state is the only one
assigned.

>
> - assigns arg->s_1        // same question


The field s_1  pointed-to by pointer [arg] in the pre-state is the only one
assigned.

>
> - assigns &(arg->s_1)  // same question


does not mean anything, but leads to a less precise translation.

>
> - assigns arg->s_2        // same question


like arg->s_1

>
> - assigns *(arg->s_2)    // same question


The location pointed to by the field s_2 pointed-to by pointer [arg] in the
pre-state is the only one assigned.

The semantics of assigns is different from all other predicates and
constructs dealing with pointers. While predicates and \valid and \separated
deal with pointers and sets of pointers, assigns clauses deal with locations
pointed-to, which may be a bit awkward. But the reverse option would be
awkard too, needing a lot of address-of operators ...

HTH,
-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081031/88370e16/attachment.html