如何证明这个赋值子句,第 2 部分?
How to prove this assigns clause, part 2?
我想不出任何想法来证明 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)
如你所料,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;
}
我想不出任何想法来证明 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)
如你所料,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;
}