在 Frama-C 中处理动态分配-解网

问：

我正在尝试使用 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 的未实现部分。最简单的方法是什么，以便我可以验证上面的例子？

malloc 动态分配 frama-c

我无法列出注释室中不起作用的所有内容，但我注意到您的函数没有子句，如果您的函数有子句，则该子句不会表示在调用后不再有效，原因与函数在其后置条件中没有相同，这并不意味着在执行函数后不再有效。assignsassignsassignsptest\valid(&a)&a

1赞 Filip Nikšić 10/22/2014

明白了。是的，我认为这将是主要问题。但在我看来，我可以定义一个新的谓词，比如 MyValid，并在任何地方使用它，而不是内置的谓词。从本质上讲，我将有一个与内置模型完全分离的内存模型，并且只能谈论动态分配的内存。

0赞 Pascal Cuoq 10/22/2014

是的，这可以工作。

答： 暂无答案

上一个：将（x）malloc 与预分配池一起使用

下一个：如何解读malloc_info

在 Frama-C 中处理动态分配

Handling dynamic allocation in Frama-C

评论