Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001601Frama-CPlug-in > wppublic2014-01-13 23:082014-03-13 15:57
Reporterdharma 
Assigned Tocorrenson 
PriorityurgentSeverityblockReproducibilityalways
StatusclosedResolutionfixed 
PlatformUbuntuOSLinuxOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001601: WP Plugin with Alt-Ergo - unable to prove?
DescriptionI'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 */
        }
}
TagsNo tags attached.
Attached Files

- Relationships
related to 0001588closedcorrenson WP ignores some goal 

-  Notes
(0004419)
correnson (manager)
2014-01-16 16:13

By side on effect from 0001588

- Issue History
Date Modified Username Field Change
2014-01-13 23:08 dharma New Issue
2014-01-13 23:08 dharma Status new => assigned
2014-01-13 23:08 dharma Assigned To => correnson
2014-01-16 16:02 correnson Relationship added related to 0001588
2014-01-16 16:13 correnson Note Added: 0004419
2014-01-16 16:13 correnson Status assigned => resolved
2014-01-16 16:13 correnson Resolution open => fixed
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker