Anonymous | Login | Signup for a new account | 2019-02-19 23:22 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | 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 | ||||||
Platform | OS | OS Version | |||||||
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; } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | ![]() | ||||||||
![]() |
|
(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 ! |
![]() |
|||
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 - 2019 MantisBT Team |