0

我正在尝试使用 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 */
        }
}
4

1 回答 1

1

您使用的是哪个版本的 Alt-ergo 和 Frama-C？我使用Frama-C Oxygen-20120901和Alt-Ergo 版本 0.95.2（通过 OPAM 安装）尝试了您的示例，我得到了：

$ frama-c -wp -wp-rte -lib-entry -main foo foo.c -wp-bhv=basic
[kernel] 使用“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] [Alt-Ergo] 目标 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在手工修正语法错误后得到证明。我认为Alt-Ergo v. >= 0.95与Frama-C Oxygen不兼容。顺便说一句，我不知道 OPAM 没有在我的计算机上安装最新版本的 Frama-C（即Fluorine-20130601）

- 问候

于 2014-01-11T13:14:52.307 回答