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

[Frama-c-discuss] [PROVENANCE INTERNET] WP, printf



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