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

[Frama-c-discuss] WP, printf



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>