--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] "\at(var, Pre)" before a loop



Hello,

Le jeu 02 avr 2009 18:14:51 CEST,
"PAREAUD, Thomas" <Thomas.PAREAUD at astrium.eads.net> a ?crit :

> I have a qestion regarding the value of \at(var, Pre) before a loop.
> In the following example, is the value of \at(pString, Pre) in the loop
> invariant annotations before the loop has a constant value during all
> iterations and is equal to the value of the pString original argument?
> In other words, is this loop invariant correct?
> 

\at(expr,Pre) always denotes the value of expr in the pre-state of the
function (i.e. when the function is entered). Assuming there's no
overflow or invalid pointer access, the loop invariant is correct.

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 71 83