--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with predicate and location labels



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