--- layout: fc_discuss_archives title: Message 43 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



Hi,

I just got an email that this issue is fixed. I'm very curious to try but do not know where to pull the source code of the updated version?

Any comments, please?

Thanks,
Dharma

-----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