--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on April 2009 ---
I need to apologize, I just discovered the PO of question. Thank you very much for your hint Christoph ----- Original Message ----- From: "Virgile Prevosto" <virgile.prevosto at cea.fr> To: <frama-c-discuss at lists.gforge.inria.fr> Sent: Monday, April 20, 2009 10:26 AM Subject: Re: [Frama-c-discuss] Predicate call not listed in jessie gui > Hi Christoph, > > Le lun 20 avr 2009 10:11:20 CEST, > "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit : > >> When proving with jessie gui, I do not get any error but the >> predicate-call is neither listed nor does it seem to be proven. >> > > I'm unsure of what you mean exactly: with Frama-C Lithium and why 2.17, > there is a proof obligation related to the post-condition > swapped{...}(...), and it is proved by alt-ergo, Z3 and Simplify. In > fact, there are 5 PO, one for each ensures clause and assigns clause of > the specification (+ 3 more for safety, but this is not related to your > function contract). What is the PO that you expected to find in Why's > output and which is not there? > > Best regards, > -- > Virgile Prevosto > Ing?nieur-Chercheur, CEA, LIST > Laboratoire de S?ret? des Logiciels > +33/0 1 69 08 71 83 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss