--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c: WP issues



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