时间戳

首页 > 解决方案 > puts(NULL) - 为什么 WP+RTE 不抱怨？

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

问题描述

考虑这个小 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 规范的缺陷吗？

标签： standard-libraryframa-c

解决方案

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

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

即最低限度，一个assigns子句（加上fromEva 的一个子句）。s和的前提条件stream。添加前提条件s很容易；事情更复杂，stream因为你需要一个模型来处理各种类型的对象FILE。

推荐阅读