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类型的各种对象提供一个模型。