5

我正在尝试使用 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 仍然有效。我将如何进行？

看来我必须自己建模堆：公理化一些谈论堆的谓词，并使用它们来指定 malloc 和 free，模仿 ACSL 的未实现部分。最简单的方法是什么，以便我可以验证上面的示例？

4

0 回答 0