frama-c - WP 插件：Alt-Ergo 语法错误

Question

对于下面的 C 函数，我从 Alt-Ergo 收到最新版本的 Frama-c 的语法错误。

frama-c -wp -wp-rte -lib-entry  RoundNearestFive.c   -wp-out temp -wp-model="nat, real"

我不确定这个生成的行有什么问题：

 ...
      let r_0 = dat_0 / 5.0e0 : real in   /* syntax error here */
    ...

正在分析的 C 函数

typedef unsigned short int uint16;


/*@
  @ requires 0<=dat<= 300;
*/
uint16 RoundNearestFive(float dat)
{
    uint16 result= 0;
    float fra = 0;

    result = (uint16)(dat/5);

    fra = dat - (float)result*5; // fractional part of the input

    if (fra < 2.5)
        result = (uint16) (dat-fra);
    else
        result = (uint16) (dat+(5-fra));

        return result;
}

Answer 1

我在下面的公式上尝试了 Alt-Ergo（版本 0.95.2 和主干），但没有出现语法错误。您使用的是旧版本的 Alt-Ergo 吗？或者语法错误可能在其他地方。

--

逻辑 dat_0：真实

目标 g: let r_0 = dat_0 / 5.0e0 : real in (* 这里有语法错误 *) false

Answer 2

WP 用户手册明确指出不支持 0.95 之前的 Alt-Ergo 版本（参见第 21 页）。