如何证明这个赋值子句，第 2 部分？

Question

我想不出任何想法来证明 foo 的赋值子句。我尝试了 assigns var;，因为 foo() 间接修改了全局 var 变量，但它不起作用。有没有办法从 a() 获取本地 p 变量或位置 return 的 assigns 子句？这是代码：

int var;
//@ assigns \nothing;
int *a(){
    return &var;
}
//@ assigns *p;
void b(int* p){
  *p = 1;
}
//@ assigns \nothing;
void foo(){
   int *p = a();
   b(p);
}
//@ assigns var;
void main(){
    var = 0;
    foo();
    return;
}

frama-c 命令：

frama-c -wp test.c

[kernel] Parsing test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assign_normal_part3 : Unknown (103ms)
[wp] [Alt-Ergo] Goal typed_foo_assign_exit_part3 : Unknown (Qed:4ms) (102ms)
[wp] Proved goals:    8 / 10
  Qed:             8 
  Alt-Ergo:        0  (unknown: 2)

Answer 1

如你所料，foo 确实赋值了一些东西，而assigns \nothing是这个函数的无效子句。正确的子句确实是 assigns var。在 assigns 子句中，您必须列出所有被修改的全局变量，以及所有对调用者来说是本地的并且可以通过正式引用的变量。

现在，为什么带有assigns var的变体证明没有通过呢？好吧，正如所写，在 foo 中，WP 无法猜测 p 指向何处，因为它无法知道它实际上等于 &a。您必须将此信息添加到函数 a 的规范中。通过这个修改，证明是立竿见影的。

完整代码：

int var;

/*@ assigns \nothing;
    ensures \result == &var; */
int *a(){
    return &var;
}

//@ assigns *p;
void b(int* p){
  *p = 1;
}

//@ assigns var;
void foo(){
   int *p = a();
   b(p);
}

//@ assigns var;
void main(){
    var = 0;
    foo();
    return;
}

如何证明这个赋值子句，第 2 部分？

How to prove this assigns clause, part 2?

frama-c