Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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
>