--- layout: fc_discuss_archives title: Message 19 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



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,