1

我一直在用 c 语言编写一些基本程序，以使用 frama-c 工具进行验证。我想知道为什么断言没有在程序中得到证明。提前致谢。

#include <limits.h>

/*@requires \valid(a) && \valid(b) && \separated(a,b);
 assigns \nothing;
 ensures (*a>*b ==> \result == *b) &&
        (*b>=*a ==> \result == *a);
*/

int max_ptr(int* a,int* b){
  return (*a>*b)?*b:*a;
}

extern int h;

//@assigns x;
int main(){
h=42;

 int a=24;
 int b=42;

 //@assert h ==42;
  int x;
  x=max_ptr(&a,&b);

  //@ assert x == 42;
  //@ assert h ==42;

  return 0;
}

所有预定目标均已成功证明，但断言声明除外：

//@ assert x == 42;

上面的断言超时了。函数合约应该有什么修改吗？

4

1 回答 1

1

该断言没有得到证明，因为它不成立。您的max_ptr函数实际上计算两个指向值的最小值，因此x == 24在断言点。

自动证明者很少能分辨出什么时候是假的，而不是根本无法证明它。

如果您使用 WP，它将无法证明断言，但这不会告诉您它是错误的，还是难以证明。一些工具可能有助于找到反例并出现一些错误的状态，但默认情况下 WP 的证明者只会说unknown。

使用自动值分析检查某些属性，例如 Eva

如果你运行 Eva (with -eva)，在你的程序中你会得到一个Invalid属性。您可以使用 GUIx在程序点检查 的值（在“值”选项卡中），您将看到它的值为{24}. 然后，您可以使用 GUI 回溯以找出该值何时到达那里，例如使用右键单击x然后Dependencies -> Show defs。

于 2020-10-13T16:38:15.160 回答