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



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