--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on April 2009 ---
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