--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on February 2011 ---
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.This would void that your next question: > Is &x automatically interpreted as \at(&x, Here) in this context? Yes. In code annotation, when a memory state is needed to evaluate e but not explicitely provided, it is interpreted as \at(e,Here). Best regards, -- E tutto per oggi, a la prossima volta. Virgile