--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on July 2009 ---
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.