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

Le mercredi 29 juillet 2009 ? 16:11 +0200, Hollas Boris (CR/AEY1) a
?crit :
> Can Gappa be used with Jessie so that the code I posted can be verified?

Hum... yes and no. Yes, Gappa can be used with Jessie. No, it won't
verify the code you posted.

However, it will verify the 15 verification conditions [*] that Jessie
generates for the following code:

        #pragma JessieFloatModel(strict)
        
        /*@ requires 0x1p-1000 <= R1 <= 0x1p1000 &&
                     0x1p-1000 <= R2 <= 0x1p1000;
            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;
        }

The lower bounds on R1 and R2 have been added because the first inverse
operations overflow when R1 and R2 are subnormal numbers. The upper
bounds have been added because Jessie is hiding things from Gappa; in
particular, they are needed for proving that the last inverse operation
does not overflow.

Note that all these bounds were arbitrarily chosen; I didn't try to find
the best ones that made the code overflow-free.

Best regards,

Guillaume

[*] Sorry, I'm lying a bit. Your example made me find a small bug in
Gappa. Indeed, Gappa is able to prove all the verification conditions,
but it reports some of them as unproved.

I have now fixed it in CVS. With the next release, Gappa should no
longer say it failed to prove a VC when it did actually prove it. But,
for now, the postcondition will be marked as unknown.