如何证明此分配条款，第二部分？

Question

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

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