如何给出正确的前提条件来证明frama-c中的断言语句？

【问题标题】：How to give the right precondition to prove an assert statemnt in frama-c?如何给出正确的前提条件来证明frama-c中的断言语句？
【发布时间】：2020-10-13 16:10:04
【问题描述】：

我一直在用 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;

上面的断言超时了，函数合约需要修改吗？

【问题讨论】：

标签： proof frama-c preconditions post-conditions

【解决方案1】：

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

自动证明者很少能判断某件事何时是错误，而不是简单地无法证明它。

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

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

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

【讨论】：