--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on February 2011 ---
Consider the predicates below. The last one gives an error message [kernel] user error: no label in the context. (\at or explicit label missing?) in annotation. What is wrong? /*@ predicate equal{L1,L2}(integer k) = \at(k,L1) == \at(k,L2); */ typedef struct { int a; } s_t; /*@ predicate does_work{O, H}(s_t* this, integer k) = equal{O, H}(k); predicate doesnt_work{O, H}(s_t* this, integer k) = equal{O, H}(this->a); */ Regards, Boris