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

  • Subject: [Frama-c-discuss] \at in ACSL assertions
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Mon, 15 Nov 2010 16:38:03 +0100
  • In-reply-to: <1289832872.1984.60.camel@guillaume-laptop>
  • References: <AANLkTimyk_961c8Xk6_U33TAxabBGSeoaRB+EtM-OiBR@mail.gmail.com> <20101115145125.5bad24be@is010235> <4CE13E87.5030807@adacore.com> <2035721159.552419.1289831625935.JavaMail.root@zmbs3.inria.fr> <1289832872.1984.60.camel@guillaume-laptop>
Le lun. 15 nov. 2010 15:54:32 CET,
Guillaume Melquiond <guillaume.melquiond at inria.fr> a ?crit :

> Le lundi 15 novembre 2010 ? 15:33 +0100, Pascal Cuoq a ?crit :
> > On Mon, Nov 15, 2010 at 3:07 PM, Yannick Moy <yannick.moy at adacore.com> wrote:
> > 
> > > Interesting possibility, to designate the last value at some label
> > 
> > I initially thought this would allow to talk imprecisely about
> > execution paths in ACSL, but now that I think about it, I am not sure
> > it is limited to imprecise characterizations of execution paths. Viz:
> > 
> >   for (i=0; i<=5; i++)
> >     {
> >     a:
> >       j=i;
> >     b:
> >       j=i;
> >     }
> >   /*@ assert \at( \at( \at( \at( \at( \at(i, b), a), b), a), b), a) == 2; */
> 
> Unless I'm mistaken, this is equivalent to
> 
> /*@ assert \at(i, b) == 2; */
> 
> since all the other \at operators apply to constant values and are
> therefore ignored.

This tends to be my interpretation too, but my guess is that Pascal has
another semantics in mind: each \at goes back in time (to the last time
the label has been encountered, starting from the current point), so
that the whole expression denotes the value of i the third-to-last time
b has been reached. I'm not sure I agree with using \at as
the (backward) description of an execution path, though. I tend to find
that quite confusing.

> 
> That said, characterizing a label in an inner loop does not seem that
> obvious to me. Virgile explained it should be the last one encountered,
> but why couldn't it be all the labels at once? In other words, the
> logical property would become an invariant of the loop.
> 

But at the point where \at is written, we don't know that the label is
inside a loop or not: in the 'g' example, there is no loop at all, and
as already said, the fact that it is in an inner block is irrelevant as
soon as you have gotos. In addition, \at(i,b) is a term that can be
part of an arbitrary complicated statement (containing others \at as
subterm). What kind of invariant would you infer from that?

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