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条款（加上伊娃的from条款）。 s和stream的先决条件。在s上添加前提条件很容易; stream的事情比较复杂，因为你需要一个FILE类型的各种对象的模型。