--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on January 2014 ---
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