如何证明这个赋值子句？

Question

/*@
  @ requires \valid(p);
  @ assigns \nothing;
*/
void foo(int *p)
{
    int *pb;
    pb = p;
    *pb = 1;
    return;
}

void main(){
    int a = 0;
    foo(&a);
    return;
}

据我了解，函数契约的 assigns 子句仅适用于函数的输入变量。因此，我将 assigns 子句设为空，然后使用 -wp.

获得黄色状态

frama-c -wp test1.c
[kernel] Parsing test1.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assign_part2 : Unknown (Qed:4ms) (51ms)
[wp] Proved goals:    2 / 3
Qed:             2 
Alt-Ergo:        0  (unknown: 1)

如何证明 foo() if assigns \nothing 不起作用？

Answer 1

我不确定您所说的“assigns [...] 仅适用于函数的输入变量”是什么意思。 assigns 子句应该给出在合约的预状态和 post- 状态下分配的所有内存位置的超集（有处理动态（取消）分配的特定子句）和在函数执行期间可能会被修改（或声明合约的声明）。

特别是，你的函数 foo 不能有 assigns \nothing; 子句，因为它修改了 p 指向的位置的值：你必须有类似 assigns *p;，这很容易证明 frama-c -wp.

如何证明这个赋值子句？

How to prove this assign clause?

frama-c