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

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001622

Frama-C

Plug-in > wp

public

2014-01-20 20:47

2014-03-13 15:57

Reporter

dharma

Assigned To

correnson

Priority

high

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Product Version

Frama-C Fluorine-20130601

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

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

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

Notes
~0004432 dharma (reporter) 2014-01-22 02:17 Last edited: 2014-01-22 02:34 View 2 revisions	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 !

Date Modified	Username	Field	Change
Issue History
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

Relationships