--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2018 ---
Actually, WP is not (yet) able to discharge proof obligations related to string-validity as provided by the Frama-C standard library. You shall provide your own stubs for printf and alike if you wants to use WP on such programs. L. > Le 18 avr. 2018 à 13:59, Andre Maroneze <Andre.OLIVEIRAMARONEZE at cea.fr> a écrit : > > 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss