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

  • Subject: [Frama-c-discuss] Frama-c: WP issues
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 15 Jan 2014 18:30:57 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7660449A3@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local> <52D6B7B0.4020005@fr.merce.mee.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DD39@Mail1.FCMD.local>, <52D6B9DE.1030402@linux-france.org> <B517F47C2F6D914AA8121201F9EBEE6701C7660449A3@Mail1.FCMD.local>
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;
}