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