处理Frama-C中的动态分配

Question

我正在尝试使用Frama-C来验证包含动态内存分配的C代码的安全属性.当前版本的ACSL规范语言(1.8)似乎能够表达很多关于动态分配的内存.但是,大部分内容尚未在Frama-C Neon中实现.

假设我们采用以下代码片段:

#include <stdlib.h>

/*@ requires \valid(p) && \valid(q) && \separated(p, q);
  @ ensures \valid(q);
  @*/
void test(char *p, char *q) {
  free(p);
}

int main(void) {
  char *p = (char *) malloc(10);
  char *q = (char *) malloc(10);

  test(p, q);

  return 0;
}

因此,main分配两块内存,并将指针传递给它们进行功能测试.测试释放p指向的块,但不释放q指向的块.假设我想证明在测试结束时,指针q仍然有效.我该怎么办？

似乎我必须自己建模堆:axiomatize一些谓词谈论堆,并使用它们来指定malloc和free,模仿ACSL的未实现部分.最简单的方法是什么,以便我可以验证上面的例子？