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
- Subject: [Frama-c-discuss] Problem with real division
- From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
- Date: Wed, 29 Jul 2009 17:21:29 +0200
- In-reply-to: <FC0686BB6178BC43B9DC035287A11A720DBB0336D8@SI-MBX12.de.bosch.com>
- References: <FC0686BB6178BC43B9DC035287A11A720DBAFF54A0@SI-MBX12.de.bosch.com> <BAB2FD70-AC55-477D-B475-62C7D7F9B75B@cea.fr> <FC0686BB6178BC43B9DC035287A11A720DBB0336D8@SI-MBX12.de.bosch.com>
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.
- References:
- [Frama-c-discuss] Problem with real division
- From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
- [Frama-c-discuss] Problem with real division
- From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
- [Frama-c-discuss] Problem with real division
- From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
- [Frama-c-discuss] Problem with real division
- Prev by Date: [Frama-c-discuss] Problem with real division
- Next by Date: [Frama-c-discuss] Oracles of Jessie tests in source distributions
- Previous by thread: [Frama-c-discuss] Problem with real division
- Next by thread: [Frama-c-discuss] Problem with real division
- Index(es):