WP: This term has type real but is expected to have type int

ID0001622: This issue was created automatically from Mantis Issue 1622. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001622	Frama-C	Plug-in > wp	public	2014-01-20	2014-03-13

Reporter	dharma	Assigned To	correnson	Resolution	fixed
Priority	high	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Fluorine-20130601	Target Version	-	Fixed in Version	Frama-C Neon-20140301

Description :

Hi,

I'm not sure "This term has type real but is expected to have type int" when using WP with Z3 (Z3 version 4.3.1).

Please note that I do not have this error when I used alt-ergo (0.95.2).

$ frama-c -wp-proof=z3 -wp -wp-rte foo.c -wp-fct=foo -wp-bhv=basic -wp-out=t -pp-annot

[kernel] preprocessing with "gcc -C -E -I. -dD foo.c" [wp] Running WP plugin... [rte] annotating function foo [wp] Collecting axiomatic usage [wp] 1 goal scheduled

--- Why3 (stderr) :

File "t/typed/foo_Why3_ide.why", line 60, characters 14-17: This term has type real but is expected to have type int

[wp] [Z3] Goal typed_foo_basic_post : Failed Error: Why3 exits with status [1]

Steps To Reproduce :

The generated why file is attached for your reference. foo.c is given below.

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;

}

Attachments

• foo_Why3_ide.why