使用Alt-Ergo的WP插件-无法证明？

Question

我正在尝试用Alt-Ergo在一个相当复杂的函数上测试WP插件。不幸的是，我不能弄清楚下面给出的“基本”行为有什么问题。

这种行为应该是真的，因为除了第一个条件语句的else部分之外，没有其他地方可以更新tenumRMode。

奇怪的是，如果我随意注释一些行，我总是会从Alt-ergo得到“有效”。

有什么意见吗？

/*@ behavior basic:
      @  assumes fRrValue == 0;
      @  ensures tenumRMode == SS_A_MODE;
      @
    */


[formal_verification]$ 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 */
        }
}

Answer 1

您使用的是Alt-ergo和Frama-C的哪些版本？我尝试使用Frama-C OPAM 20120901和Alt-Ergo版本0.95.2 (通过OPAM安装)来测试您的示例，我得到了：

$frama c -wp -wp-rte -lib-entry -main foo foo.c -wp-bhv=basic

用"gcc -C -E -I.foo.c“进行内核预处理

wp正在运行WP插件...

wp收集公理用法

foo.c:51:wp警告:未找到get_strategies行为

foo.c:51:wp警告:未找到get_strategies行为

rte注释函数foo

wp 1目标计划

wp目标store_foo_basic_post :未知

当我直接尝试Alt-Ergo (v.0.95.2)时，我得到：

$ alt-ergo store_foo_basic_post_po_ergo.why

文件"store_foo_basic_post_po_ergo.why"，第1220行，字符22-24:语法错误

在手工修复语法错误后，对VC进行了验证。我认为Frama Alt-Ergo v.Frama 0.95与Frama-C Oxygen不兼容。顺便说一句，我不知道为什么奥帕姆没有在我的电脑上安装Frama-C的最新版本(即Fluorine-20130601)

--问候