如何给正确的前提条件来证明frama-c中的断言状态？ 自动证明者很少能分辨出什么东西是 false ，而不是简单地不能证明它使用自动值分析检查某些属性，例如Eva

问题描述

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

上面的声明超时了，是否应该对功能协定进行任何修改？

解决方法

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

自动证明者很少能分辨出什么东西是 false ，而不是简单地不能证明它。

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

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

如果运行Eva（使用-eva），则在程序中将获得 Invalid 属性。您可以使用GUI在程序点（在 Values 选项卡中）检查x的值，您会看到其值为{24}。然后，您可以使用GUI进行回溯，以找到此值的到达时间，例如右键单击x，然后右键单击Dependencies -> Show defs。