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

【问题标题】：Assigns clause for local variables in Frama-C在 Frama-C 中为局部变量分配子句
【发布时间】：2014-11-01 00:58:58
【问题描述】：

我正在尝试使用 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 是局部变量，不能在注释中访问。

【问题讨论】：

标签： frama-c

【解决方案1】：

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

反例

如果new_value定义如下：

int g;

int *new_value(){
  return &g;
}

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

走得更远

如果问题是能够在不知道函数 new_value 的行为的情况下对函数 main 进行分配，则可以从逻辑空间访问 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 设置一组指针，而不是唯一的。

【讨论】：

感谢您的回答。使用 wp 插件时，它会中断。现在我正在安装 Jessie 插件，看看它是否有效。你用的是哪一个？
与 Jessie 一起尝试过。我不得不将 R 的声明放入公理块中。之后，我输入错误：未绑定标识符 R。@François，你没有类似的问题吗？你用的是哪个版本的 Jessie？
抱歉，有一些其他的技术问题。引入逻辑 R 的想法适用于 wp。