--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on April 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP, printf



Just wondering how you deal with programs that do simple I/O, when using Frama-C+WP.
For example:

basie:simple siegel$ cat hello.c

#include <stdio.h>
int main() {
  printf("Hello, world.\n");
}

basie:simple siegel$ frama-c -wp hello.c
[kernel] Parsing hello.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_main_call_printf_va_1_pre : Timeout (Qed:1ms) (10s)
[wp] Proved goals:    0 / 1
    Alt-Ergo:        0  (interrupted: 1)
basie:simple siegel$


Questions: what is the pre-condition for printf?  How do I discharge the generated proof obligation?

Thanks,
Steve