WP内存模型在Frama-C中做出的实施假设

Question

有没有办法执行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内存模型，则此功能会验证，因为它假定分离。但是，即使使用Typed内存模型，我仍然可以验证main。使用命令行选项-wp-warn-memory-model，消息警告您内存模型所需的假设。是否可以执行这些假设，例如，将它们添加为assign_many？

Answer 1

我恐怕这是不可能的（即，不复制生成的规范到新的c文件中并重新分析整个来源：警告的文字似乎会照顾好表示为有效的ACSL合同）。

在WP插件的API中稍微挖掘，可以看出，分隔假设在插件的MemoryContext模块中处理，该模块使用其自己的自定义数据类型来表示它们（相对于一个来自内核中定义的标准AST的ACSL谓词。

可以编写一些代码，以获取给定功能给定模型生成的条款，并生成一组ACSL谓词，然后可以将其添加为此功能的requires子句（即复制的程序化等效词 - 上面提到的帕斯特），但这意味着对Frama-C API有一定的了解。