Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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