WP Plugin with Alt-Ergo - unable to prove?

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

---

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

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

Description :

I'm trying to test WP plugin with Alt-Ergo on a fairly complex function. Unfortunately, I am not able to figure out what's wrong with the "basic" behavior given below.

This behavior should be true because there is no other place tenumRMode is updated except the first conditional statement's else section.

The weird thing is that if I comment some lines arbitrarily (after the first if-else block) I always get "valid" from Alt-ergo.

Any comments? The below code might be lengthy, but the behavior is easy to verify manually because the variables mentioned in the behavior are never updated after the first if-else block.

I also discussed with a alt-ergo developer, see http://stackoverflow.com/questions/21036098/wp-plugin-with-alt-ergo-unable-to-prove

Steps To Reproduce :

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

$ frama-c -wp -wp-rte -wp-bhv=basic foo.c -wp-out t -lib-entry -main foo -wp-model ref -wp-timeout=50 -wp-fct=foo -wp-out t [kernel] preprocessing with "gcc -C -E -I. foo.c" [wp] Running WP plugin... [rte] annotating function foo [wp] Collecting axiomatic usage [wp] Collecting variable usage [wp] 1 goal scheduled [wp] [Alt-Ergo] Goal typed_ref_foo_basic_post : Unknown (Qed:20ms)

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; BOOL mbApLRange; 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;
    }

    if ( (mfAp >= F_MIN_R) &&
             ((gbCaMStatus == TRUE) && (gbCaaStatus == FALSE)) )
    {
            bApAlmC = TRUE;
            almC = 1;
    }
    else
    {
          almC = 0;
    }


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


    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;

    if ( (mfAp >= nApLYL)
             || ((bApAlmC == TRUE) && (fCaValue < nCaLYL))
             || ((bYAp == TRUE)
                     && (gbCaMStatus == TRUE)  && (gbCaaStatus == FALSE)  ) )
    {
            mbApLYRange = TRUE;
    }
    else
            mbApLYRange = FALSE;

    if ( (mfAp >= nApLRL)
             || ((bApAlmC == TRUE) && (fCaValue < nCaLRL))
             || ((bRAp == TRUE)
                    && (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) )  )
    {
        /* Some code here */
    }

}