时间戳

首页 > 解决方案 > 如何证明这个 assigns 子句，第 2 部分？

frama-c - 如何证明这个 assigns 子句，第 2 部分？

问题描述

我想不出任何想法来foo证明 's assigns 子句。我试过了assigns var;，因为foo()间接修改了全局var变量，但它不起作用。有没有办法获取局部变量或位置返回的assigns子句？这是代码： pa()

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)

标签： frama-c

解决方案

正如您所猜到的，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;
}

推荐阅读