--- layout: fc_discuss_archives title: Message 66 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



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