数组指针断言

Question

我定义了以下函数，frama-c 很好地证明了这一点：

//ensures array <= \result < array+length && *\result == element;
/*@
  requires 0 < length;
  requires \valid_read(array + (0 .. length-1));

  assigns  \nothing;

  behavior in:
    assumes \exists int off ; 0 <= off < length && array[off] == element;
    ensures *\result == element;

  behavior notin:
    assumes \forall int off ; 0 <= off < length ==> array[off] != element;
    ensures \result == 0;

  disjoint behaviors;
  complete behaviors;
*/
int* search(int* array, int length, int element){
   int *tmp;
  /*@
    loop invariant 0 <= i <= length;
    loop invariant \forall int j; 0 <= j < i ==> array[j] != element;
    loop assigns i;
    loop variant length-i;
  */ 
  for(int i = 0; i < length; i++)
  {
    if(array[i] == element) 
    {
        tmp = &array[i];
        //@ assert *tmp==element;
    }
    else
    {
        tmp = 0;    
    }
  }
  return tmp;
}

我在以下主要条目中使用它：

int main(){
  int arr[5]={1,2,3,4,5};
  int *p_arr;

  p_arr = search(arr,5,4);
  //@ assert *p_arr==30;

  return 0
}

我想知道为什么 frama-c 给出断言“//@ assert *p_arr==30;”是真的，没看懂

谢谢

Answer 1

仅使用命令行，我在您的代码中发现了一些问题：

tmp 在循环赋值中丢失；
您需要：
- 在seach函数的then分支中添加一个break （然后你会 return 匹配第一个元素的指针）
- 或者在函数的开头初始化 tmp = 0 并删除循环中的 else 分支（然后你会 return 最后一次出现的指针）。

我没试过图形用户界面，但你说你的例子是这样的似乎很奇怪：

well proved by frama-c

我建议您首先使用命令行。

Answer 2

好的，现在我更正我的代码如下：

//ensures array <= \result < array+length && *\result == element;
/*@
  requires 0 < length;
  requires \valid_read(array + (0 .. length-1));

  assigns  \nothing;

  behavior in:
    assumes \exists int off ; 0 <= off < length && array[off] == element;
    ensures *\result == element;

  behavior notin:
    assumes \forall int off ; 0 <= off < length ==> array[off] != element;
    ensures \result == 0;

  disjoint behaviors;
  complete behaviors;
*/
int* search(int* array, int length, int element){

  /*@
    loop invariant 0 <= i <= length;
    loop invariant \forall int j; 0 <= j < i ==> array[j] != element;
    loop assigns i;
    loop variant length-i;
  */ 
  for(int i = 0; i < length ; i++)
  {
    if(array[i] == element) 
    {
        return &array[i];
    }
  }
  return 0;
}

并添加以下断言：

int main()
{
    int arr[5] = {1,2,3,4,5};
    int *ptr;

    ptr = search(arr,5,3);
    //@ assert *ptr==3;

}

然后运行: frama-c -wp -rte myfile.c 得到结果:

[wp] Proved goals:   65 / 65
     Qed:            35  (1.00ms-6ms-24ms)
     Alt-Ergo:       30  (16ms-30ms-94ms) (132)

如果我设置另一个断言：

int main()
    {
        int arr[5] = {1,2,3,4,5};
        int *ptr;

        ptr = search(arr,5,3);
        //@ assert *ptr==5;

    }

然后我得到输出：

[wp] [Alt-Ergo] Goal typed_main_assert_2 : Timeout (Qed:4ms) (10s)
[wp] Proved goals:   64 / 65
     Qed:            35  (1.00ms-4ms-10ms)
     Alt-Ergo:       29  (16ms-28ms-109ms) (132) (interrupted: 1)

所以断言是 "unknown" 正如我们预期的那样，如果我们运行 frama-c-gui 项目符号是橙色的。

所以这很好用，注意错误的公理化内容！谢谢安妮的帮助。

数组指针断言

Assertion on pointer to array

frama-c