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



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

-------------- next part --------------
typedef unsigned char BOOL;
#define TRUE 1
#define FALSE 0

typedef unsigned char uint8;
typedef unsigned short int uint16;
typedef unsigned long  uint32;

uint16 F_MIN_R = 15;  

const uint8 RESP_STATE = 30; 


typedef enum
{
        RESP_MODE,
        SS_A_MODE
}tenumMode;

tenumMode tenumRMode;


BOOL gbCaMStatus;
BOOL gbCaaStatus;
uint8 mnPb;
BOOL mbApLYRange;
float gfApYLineSlope;
float gfApYLineConst;
float gfApRLineSlope;
float gfApRLineConst;
float mfAp;
uint16 almC;
uint16	nApLYL = 0;
uint16	nApLRL = 0;
uint16  Ap_Y_L_Ui = 0;
uint16  Ap_R_L_Ui = 0;
float	fCaValue=0.0;
float   fRrValue = 0.0;
uint16	nCaLYL=0;
uint16	nCaLRL=0;


/*@ 
  @ behavior basic:
  @  assumes fRrValue == 0;
  @  ensures tenumRMode == SS_A_MODE;
  @
*/

void foo()
{

	float	mfNewAp = 0;	
	BOOL	bYAp = FALSE;
	BOOL	bRAp = FALSE;
	BOOL	bApAlmC = FALSE;

	if (fRrValue != 0)
	{
            /* Some code here */ 
	}
	else
	{
		if (mnPb == 1)
		{
			mfAp = RESP_STATE; 
			mnPb = 2; 
		}
		
		tenumRMode = SS_A_MODE;
	}
	//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;

	if ( (mfAp >= F_MIN_R) &&
		 ((gbCaMStatus == TRUE) && (gbCaaStatus == FALSE)) )
	{
		bApAlmC = TRUE;
                almC = 1;
	}
        else
        {
                almC = 0;
        }
	//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
 

	if ( (bApAlmC == TRUE)
		 && (mfAp < nApLYL)
		 && (fCaValue >= nCaLYL) )
	{
		float fmultval = 0;

		fmultval = gfApYLineSlope*fCaValue;

		mfNewAp = fmultval + gfApYLineConst;

		if (mfAp >= mfNewAp)
			bYAp = TRUE;
		else
			bYAp = FALSE;

		Ap_Y_L_Ui = (uint16)mfNewAp;
	}
	//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;


	if ((bApAlmC == TRUE) && (fCaValue > (float)nCaLYL))
	{
		mfNewAp = ((gfApYLineSlope*fCaValue) + gfApYLineConst);
		if (mfNewAp < (float)nApLYL);
                  Ap_Y_L_Ui = (uint16)mfNewAp;
	}

	else if ((bApAlmC == TRUE) && (fCaValue <= (float)nCaLYL))
		Ap_Y_L_Ui = F_MIN_R;	
  
	if ( (bApAlmC == TRUE) && (fCaValue >= nCaLRL) )
	{
		float fmultval = 0;

		fmultval = gfApRLineSlope*fCaValue;

		mfNewAp = fmultval + gfApRLineConst;

             
		if (mfAp >= mfNewAp)
			bRAp = TRUE;
		else
			bRAp = FALSE;

		Ap_R_L_Ui = (uint16)mfNewAp;
	}
        else if ( (bApAlmC == TRUE) && (fCaValue < nCaLRL) )
                Ap_R_L_Ui = F_MIN_R; 
	
	//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
	if ( (mfAp >= nApLYL)
		 || ((bApAlmC == TRUE) && (fCaValue < nCaLYL))
		 || ((bYAp == TRUE)
			 && (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE)  ) )
	{
		mbApLYRange = TRUE;
	}
	else
		mbApLYRange = FALSE;

	//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
	if ( (mfAp >= nApLRL)
		 || ((bApAlmC == TRUE) && (fCaValue < nCaLRL))
		 || ((bRAp == TRUE)
			&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) )  )
	{
	  //@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;

	}

	//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
}