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

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