代码之家  ›  专栏  ›  技术社区  ›  Laurent Guillaume

数组指针断言

  •  0
  • Laurent Guillaume  · 技术社区  · 7 年前

    我定义了以下函数,并通过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\u arr==30;”诚然,我不明白。

    谢谢

    2 回复  |  直到 7 年前
        1
  •  0
  •   Anne    7 年前

    仅使用命令行,我发现您的代码中存在一些问题:

    • tmp 循环分配中缺少;
      • 要么添加一个 break then 分公司 seach
      • tmp = 0

    我没有尝试GUI,但您说您的示例是:

    frama-c充分证明了这一点

        2
  •  0
  •   Laurent Guillaume    7 年前

    好的,现在我更正我的代码如下:

    //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;
    
    }
    

    [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)
    

    因此,正如我们预期的那样,断言是“未知”的,如果我们运行frama-c-gui,则项目符号是橙色的。

    安妮,谢谢你的帮助。