断言上指针阵列

我已经定义下面的函数，其是公由邮资-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;”真的，我不明白。

感谢

来源

2017-09-06 Laurent Guillaume

哪个版本的frama-c？哪些选项？谁说断言是有效的：WP？ – Anne

谢谢您的回复，版本为磷，选项为：frama-c-gui -wp -rte -val ，GUI上的子弹为橙色。这对你来说有足够的信息吗？ –

我会说断言线上的子弹是绿色的，对不起 –

只使用命令行，我看到在你的代码的一些问题：

tmp缺少的循环分配;
您需要：
- 无论是在seach功能的then分支中加入一个break（那么你将返回指针相匹配的第一个元素）
- 或在的开始初始化tmp = 0函数并删除循环中的else分支（然后您将返回最后一次出现的指针）。

我没有尝试的图形用户界面，但它似乎很奇怪，你说你的例子是：

通过邮资-C很好的验证

我建议你使用命令行来开始。

来源

2017-09-07 09:43:47 Anne

谢谢你，同时我得到了和你相同的结论！问题是我在代码的其他地方定义了一些令WP混淆的错误公理，所以一切都被定义为有效。所以现在我要纠正你的建议中的代码并再次尝试，非常感谢你的支持，我会在这里发布最终结果。 –

如果你确定，你可以考虑接受我的答案。谢谢。 – Anne

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

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

}

然后运行：邮资-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)

因此断言是“未知”正如我们预期，如果我们运行邮资-C-GUI子弹为橙色。

所以这工作正常，照顾错误的公理的东西！谢谢安妮的帮助。

来源

2017-09-07 12:51:00

断言上指针阵列

回答

相关问题