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] Frama-c: WP issues
- Subject: [Frama-c-discuss] Frama-c: WP issues
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- Date: Wed, 15 Jan 2014 13:12:06 -0500
- In-reply-to: <52D6C5D1.2060905@linux-france.org>
- References: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local> <52D6B7B0.4020005@fr.merce.mee.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DD39@Mail1.FCMD.local>, <52D6B9DE.1030402@linux-france.org> <B517F47C2F6D914AA8121201F9EBEE6701C7660449A3@Mail1.FCMD.local> <52D6C5D1.2060905@linux-france.org>
Thanks for inserting asserts in different points. Fully agree that this problem is somewhat subtle. I'm really interested in using WP. I hope a WP specialist will help me... -----Original Message----- From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of David MENTRE Sent: Wednesday, January 15, 2014 12:31 PM To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] Frama-c: WP issues Hello Dharmalingam, Le 15/01/2014 17:45, Dharmalingam Ganesan a ?crit : > I tried your suggestion adding asserts but no luck. I attach the C code for your reference. Sorry, my assertion was incorrect. It should have been "assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;". In attached foo.c, I have added above annotation at various points in the code. It is proved everywhere except for the last block: """ if ( (mfAp >= nApLRL) || ((bApAlmC == TRUE) && (fCaValue < nCaLRL)) || ((bRAp == TRUE) && (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) ) { } """ If this code block is commented out, then your contract is proved. I don't know why. It seems pretty innocuous regarding your property to me. Any WP specialist having an idea? Best regards, david
- References:
- [Frama-c-discuss] Frama-c: WP issues
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Frama-c: WP issues
- From: d.mentre at fr.merce.mee.com (David MENTRE)
- [Frama-c-discuss] Frama-c: WP issues
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Frama-c: WP issues
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Frama-c: WP issues
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Frama-c: WP issues
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Frama-c: WP issues
- Prev by Date: [Frama-c-discuss] Frama-c: WP issues
- Next by Date: [Frama-c-discuss] Can i specify/proove a function to be "just called"?
- Previous by thread: [Frama-c-discuss] Frama-c: WP issues
- Next by thread: [Frama-c-discuss] Frama-c: WP issues
- Index(es):