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] \at in ACSL assertions

Hello,

Le lun. 15 nov. 2010 13:24:19 CET,
Pascal Cuoq <pascal.cuoq at gmail.com> a ?crit :

> a- should the commented functions main and f be parsable by the
> front-end? Currently, they can't be parsed with either Boron or the
> development version. The error message is similar to "u.c:14:[kernel]
> user error: logic label `cond' not found in annotation"

No, they shouldn't, at least for now. The ACSL manual
(section 2.4.3) explicitely says that the label mentioned in an \at()
expression cannot be in an inner block.

[disclaimer: what follows is my personal understanding of what the
current ACSL says (or would say, supposing that we allow arbitrary
labels in \at)]

> b- if they were parsable, should the assertion in each function be provable?

yes for main: the value of j the last time we reach odd before
evaluating the assert is indeed 3. \at(...,cond) does not play any
role here, it is subsumed by the inner \at, 

no for f: then is not reached when c==0, \at(i-d,then) has no defined
value. Basically, we can't say much more than \at(i-d,then) ==
\at(i-d,then).

//@ assert \at(c,Pre) != 0 ==> \at(i-d, then) == 0; 
would be true, though.

> 
> c- should the assertion in parsable function g be provable?

no (same reason as for g above).

> #if 0
> int main(void)
> {
>   int i, j;
>   for (i=0; i<=4; i++)
>     {
>       j=i;
>     cond:
>       if (i%2)
> 	{
> 	odd:
> 	  j=1;
> 	}
>     }
>   /*@ assert \at( \at(j, odd), cond) == 3; */
>   return 0;
> }
> 
> int f(int c, int d)
> {
>   int i, j;
>   if (c)
>     i=d;
>   if (c)
>     {
>     then:
>       j=1;
>     }
>   /*@ assert \at(i-d, then) == 0; */
>   return 0;
> }
> #endif
> 
> 
> int g(int c, int d)
> {
>   int i, j;
>   if (c) goto next1;
>     i=d;
>  next1:
>     if (c) goto next2;
>  then:
>     j=1;
>  next2:
>   /*@ assert \at(i-d, then) == 0; */
>   return 0;
> }


-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98