--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on April 2018 ---
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