--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on February 2011 ---
On Fri, 2011-02-18 at 13:23 +0100, Virgile Prevosto wrote: > context. That said, the error should be logic label P not found. Could > you give a complete example that reproduce your issue? > Sorry, yes, my original example doesn't makes much sense. The following code verifies, but the specification unchanged{P,H}(\at(&this->a, P)); is quite clumsy. typedef int bool; /*@ predicate unchanged{P,H}(bool* p) = \at(*p, P) <==> \at(*p, H); */ typedef struct { bool a; } S_t; /*@ predicate foo_spec{P,H}(S_t* this) = unchanged{P,H}(\at(&this->a, H)); */ /*@ ensures foo_spec{Pre,Here}(this); */ void foo(S_t* this) { ; } If write &this->a instead of \at(&this->a, H), frama-c complains "no label in the context". In Patrick's example, the pointer is given with an \at: //@ensures bar_spec{Here,Old}(&x) ; Is &x automatically interpreted as \at(&x, Here) in this context? Regards, Boris