--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on April 2018 ---
What is happening here is that the Variadic plug-in (enabled by default) is converting your call to printf into a specialized version, printf_va_1, and generating a specification for the function call. You can see it by running `frama-c -print hello.c`: /* Generated by Frama-C */ #include "errno.h" #include "stdarg.h" #include "stddef.h" #include "stdio.h" /*@ requires valid_read_string(format);    assigns \result, __fc_stdout->__fc_FILE_data;    assigns \result      \from (indirect: __fc_stdout->__fc_FILE_id),            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));    assigns __fc_stdout->__fc_FILE_data      \from (indirect: __fc_stdout->__fc_FILE_id),            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));  */ int printf_va_1(char const *format); int main(void) {  int __retres;  printf_va_1("Hello, world.\n");  __retres = 0;  return __retres; } Since printf is variadic, each call has a different number and type of arguments, so the specifications must be made on a per-call basis, hence why they are done by Variadic and not directly via Frama-C's libc. The precondition is thus "valid_read_string(format)", in other words: is the format string given to printf an actual string? I will let someone else comment on how to discharge the generated PO (sorry, I don't use WP very often), but note that you can also disable Variadic via option `-variadic-no-translation`. However, if you disable it without giving a specification to printf, Frama-C will warn you: hello.c:2:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype On 18/04/18 11:08, Stephen Siegel wrote: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Researcher/Engineer CEA/LIST Software Reliability and Security Laboratory -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180418/561c1a0f/attachment.bin>