--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] \at in ACSL assertions



Le lun. 15 nov. 2010 17:10:41 CET,
Guillaume Melquiond <guillaume.melquiond at inria.fr> a ?crit :

> As a matter of fact, that's exactly the current ACSL interpretation. The
> annotation above is syntactic sugar for
> 
> Here42:
> //@ assert \at(x,Here42) > \at(y,Here42);
> 
> and it precisely states that for any program state at label Here42, the
> value of variable x in that state is greater than the value of variable
> y in that state.

Well, if we are taking your interpretation literally, I think that
the assert means rather 'any value that x can have in state Here42 is
greater than any value that y can have in state Here42' which is not
the same thing (assuming we got there at least twice of course) as
fixing an arbitrary state Here42 and evaluating x and y in the same
state

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