Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001622Frama-CPlug-in > wppublic2014-01-20 20:472014-03-13 15:57
Reporterdharma 
Assigned Tocorrenson 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001622: WP: This term has type real but is expected to have type int
DescriptionHi,

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 ReproduceThe 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;
}
TagsNo tags attached.
Attached Files? file icon foo_Why3_ide.why [^] (2,737 bytes) 2014-01-20 20:47

- Relationships

-  Notes
(0004432)
dharma (reporter)
2014-01-22 02:17
edited on: 2014-01-22 02:34

I tried to debug this error. Found that the type casting seems to be a problem when using wp-proof=z3


float a = 0.0;
float b = 1.5;

int main()
{
  a = (int)b;

  return 0;
}

frama-c -wp -wp-rte cast.c -wp-proof=z3

(0004440)
correnson (manager)
2014-01-24 14:12

In development version, WP no more generates any goal for file foo.c (we introduced more simplifications on real constants).
The bug on negative integer constants for Why-3 is also fixed, such that cast.c also works (with cvc4).
Thanks for all reports !

- Issue History
Date Modified Username Field Change
2014-01-20 20:47 dharma New Issue
2014-01-20 20:47 dharma Status new => assigned
2014-01-20 20:47 dharma Assigned To => correnson
2014-01-20 20:47 dharma File Added: foo_Why3_ide.why
2014-01-22 02:17 dharma Note Added: 0004432
2014-01-22 02:34 dharma Note Edited: 0004432 View Revisions
2014-01-24 14:12 correnson Note Added: 0004440
2014-01-24 14:15 correnson Status assigned => resolved
2014-01-24 14:15 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