ставит (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

В основном да. В версии stdio.h, поставляемой в комплекте с Frama-C, вы можете видеть, что спецификацией для puts является

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

т.е. абсолютный минимум, предложение assigns (плюс предложение from для Eva). Предпосылки на s и stream. Добавить предварительное условие для s было бы легко; вещи более сложны для stream, так как вам нужна модель для различных объектов типа FILE.