--- layout: fc_discuss_archives title: Message 128 from Frama-C-discuss on October 2008 ---
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