在 Frama-C 中强制执行 WP 内存模型所做的假设答案

【问题标题】：Enforce assumptions made by WP memory model in Frama-C在 Frama-C 中强制执行 WP 内存模型所做的假设
【发布时间】：2019-03-13 01:50:25
【问题描述】：

有没有办法强制执行 WP 内存模型所做的假设？

考虑使用 Frama-C 验证以下两个函数：

/*@ requires \valid(a) && \valid(b);
  @ ensures A: *a == 1;
  @ ensures B: *b == 2;
  @ assigns *a, *b;
  @*/
void assign_many(int *a, int *b)
{
  *a = 1;
  *b = 2;
}


int main() {
  int a = 42;
  assign_many(&a, &a);
  //@ assert a == 1;
  //@ assert a == 2;
  return 0;
}

函数assign_many 在一般情况下无法验证，因为这两个参数可以别名（如main 所示）。但是，如果您选择Hoare+ref 内存模型，则此函数会进行验证，因为它假定分离。但我仍然可以验证main，即使使用Typed 内存模型。使用命令行选项-wp-warn-memory-model，一条消息会警告您内存模型需要哪些假设。是否可以强制执行这些假设，例如，将它们作为前提条件添加到assign_many？

【问题讨论】：

标签： frama-c

【解决方案1】：

恐怕这是不可能直接实现的（即，无需将生成的规范复制粘贴到新的 C 文件中并重新分析整个源代码：警告文本似乎将其表达为有效的 ACSL 合同） .

稍微挖掘一下Wp插件的API，可以看出分离假设是在插件的MemoryContext模块中处理的，它使用自己自定义的数据类型来表示它们（相反到内核中定义的标准 AST 的 ACSL 谓词）。

可以编写一些代码，将给定模型为给定函数生成的子句生成一组 ACSL 谓词，然后可以将这些谓词添加为该函数的 requires 子句（即上面提到的复制和粘贴），但这意味着对 Frama-C API 有一定的了解。

【讨论】：