--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on February 2011 ---
Hello Boris, Le mer. 16 f?vr. 2011 16:28:08 CET, "Boris Hollas" <hollas at informatik.htw-dresden.de> a ?crit : > 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. > /*@ 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); > */ This is not related to the labels you pass to equal, but to the argument of the predicate. Remember that a label represent a program state. In the first case, k is a parameter of the predicate, and since ACSL uses call-by-value, its value is independent from the program state in which you evaluate the predicate. In the second case, this->a is not, since you're dereferencing a pointer. In addition, you have two states in your context, represented by the O and H label parameters of doesnt_work. Hence, frama-c does not know if you meant \at(this->a,O) or \at(this->a,H) and asks for more information. It is only when there is only one program state in the context that you can omit the \at, such as in // we only refer to state L /*@ predicate implicit{L}(s_t* this) = equal{L,L}(this->a); */ // we refer implicitely to Here in code annotations or contracts /*@ assert equal{Pre,Here}(this->a); Now, your predicate equal is in fact always true: > /*@ predicate equal{L1,L2}(integer k) = \at(k,L1) == \at(k,L2); > */ as said above, we use a call-by-value semantics for ACSL, and thus k has always the same value, be it in L1 or L2. In particular, all the assertions below are true: int X; //@ requires X == 42; void f(void) { int x = X; X++; /*@ assert equal{Pre,Here}(X); */ // equivalent to /*@ assert equal{Pre, Here}(43); */ /*@ assert \at(X,Pre) == \at(x,Here); */ } I hope this clarifies a little bit the usage of label parameters in ACSL predicate/logic functions. Feel free to ask for more details. Best regards, -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98