在Frama-C中为局部变量分配子句

Question

我正在尝试使用frama-c验证以下代码

/*@ ensures \result != \null; 
  @ assigns \nothing;
  @*/
extern int *new_value();

//@ assigns *p;
void f(int* p){
  *p = 8;
}
//@ assigns \nothing;
int main(void){
 int *p = new_value(); 
 f(p);
}

证明者无法证明主要指定\没有,这是有道理的,因为主要通过函数f分配给*p .但是,我应该如何在\ assigns子句中声明,因为p是局部变量,并且无法在注释中访问.

Answer 1

确实assigns nothing是假的。该变量p是局部变量，但效果是在*p任意指针上完成的。

\n\n

反例

\n\n

如果new_value定义如下：

\n\n

int g;\n\nint *new_value(){\n  return &g;\n}\n

\n\n

它满足规范，并且 的值g位于8main 的末尾。

\n\n

为了走得更远

\n\n

如果问题是能够在不了解函数行为的情况下对函数 main 进行赋值，则可以从逻辑空间访问new_value结果：new_value

\n\n

例如 ：

\n\n

//@ logic int * R ;\n//@ ensures \\result == R && \\valid(R) ; assigns \\nothing ;\nextern int *new_value();\n\n//@ assigns *p;\nvoid f(int * p) { \xe2\x80\xa6 }\n\n//@ assigns *R ;\nint main(void) { \xe2\x80\xa6 }\n

\n\n

更通用的解决方案是为 R 提供一组指针，而不是唯一的指针。

\n