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 */
}
}