standard-library - put(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 类型的各种对象的模型。