--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on July 2009 ---
Hello, Excepting for the PO related to lemma div1, but Alt-ergo 0.8, Yices, Z3 1.3, CVC3 discharged all the other POs. Command line : frama-c -jessie file.c You can debug what's the matter with GWhy by activating "Proof/Debug mode" menu item and by giving a look to stdout. HTH, Dillon > -----Message d'origine----- > De : frama-c-discuss-bounces at lists.gforge.inria.fr > [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la > part de Hollas Boris (CR/AEY1) > Envoy? : mercredi 29 juillet 2009 09:49 > ? : Frama-C public discussion > Objet : [Frama-c-discuss] Problem with real division > > Hello, > > I tried to verify the code below as an example to our > engineers. R_ges computes the resistance of two resistors in > a parallel circuit. However, even with the help of two > lemmata I provided, none of the proofs obligation can be verified. > > Is there a solution? > > Regards, > Boris > > > /*@ lemma div1 : \forall real x; x > 0 ==> 1.0/x > 0; > lemma add1: \forall real x,y; x > 0 && y > 0 ==> x+y > 0; */ > > /*@ requires R1 > 0 && R2 > 0; > ensures \result > 0; > */ > double R_ges(double R1, double R2) > { > return 1.0/( 1.0/R1 + 1.0/R2 ); > } > > > int main(void) { > double R; > > R = R_ges(100, 200); > return 0; > } > > _______________________________________________ > 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 >