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



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