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

[Frama-c-discuss] Problem with real division



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
>