--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on February 2011 ---
On Mon, 2011-02-21 at 10:27 +0100, Virgile Prevosto wrote: Le ven. 18 f?vr. 2011 15:28:58 CET, > "Boris Hollas" <hollas at informatik.htw-dresden.de> a ?crit : > > > > > The following code verifies, but the specification > > unchanged{P,H}(\at(&this->a, P)); is quite clumsy. > > > > OK, I see your point now. You're right, &this->a does not necessitate a > memory state: it's merely a matter of adding the offset of field 'a' to > 'this'. In fact, I guess that it can be argued that taking the address > of any left value does not require a memory state: this address won't > change for the lifetime of the variable. > However, if predicates indeed use call-by value semantics, shouldn't frama-c interpret &this->a as a value that does not depend on a memory state, hence a label wouldn't be necessary? -- Regards, Boris