frama-c - 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);
}

证明者无法证明main没有赋值，这是有道理的，因为main通过函数f赋值给 *p 。但是，我应该如何在 \assigns 子句中说明这一点，因为p是局部变量并且不能在注释中访问。

Answer 1

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

反例

如果new_value定义如下：

int g;

int *new_value(){
  return &g;
}

它满足规范， 的值g在8main 的末尾。

走得更远

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

例如 ：

//@ logic int * R ;
//@ ensures \result == R && \valid(R) ; assigns \nothing ;
extern int *new_value();

//@ assigns *p;
void f(int * p) { … }

//@ assigns *R ;
int main(void) { … }

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