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

[Frama-c-discuss] one initialisation of loop invariant is not listed in jessie GUI, this time I am sure



Le lun 20 avr 2009 13:22:00 CEST,
"Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit :

> 
> I would like to know, if 
> loop invariant \forall integer k;   
>    i <= k < length ==> 
>    \at(a[k], Here) == \at(a[k], Pre)&&
>    \at(b[k], Here) == \at(b[k], Pre);
> should be initialized.
> 
> If everything is fine in spite this fact, I would be very happy.

Yes, everything is fine: for the initialization, the resulting proof
obligation is more or less \at(a[k],Pre) == \at(a[k],Pre) (and the same
for b) which is trivially discharged by why itself. If you want to see
all proof obligations, you can use the option -why-opt '-all-vc', but
it is mainly intended for debugging purposes only.

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