puts(NULL) - 为什么 WP+RTE 不抱怨？

Question

考虑一下这个小的 C 文件：

#include <stdio.h>

void f(void) {
    puts(NULL);
}

我正在像这样运行 Frama-C 的 WP 和 RTE 插件：

frama-c-gui puts.c -wp -rte -wp-rte

我希望此代码生成valid_read_string(NULL); 或类似的证明义务，这显然是无法证明的。然而，令我惊讶的是，并没有发生这样的事情。这是标准库的 ACSL 规范的缺陷吗？

Answer 1

基本上是的。您可以在与 Frama-C 捆绑的stdio.h 版本中看到puts 的规范是

/*@ assigns *stream \from s[..]; */
extern int fputs(const char * restrict s,
     FILE * restrict stream);

即最低限度，assigns 子句（加上 Eva 的 from 子句）。 s 和 stream 的先决条件。在s 上添加前提条件很容易； stream 的情况更加复杂，因为您需要为 FILE 类型的各种对象建立模型。