--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on April 2009 ---
Sure it is correct, and if you add the declaration of i, it is proved correct with Frama-C/Jessie. Even arithmetic overflow checks are OK. What is the point ? - Claude Virgile Prevosto wrote: > 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,