[variadic] FRAMAC_SHARE/libc/wchar.h:265: 
  Declaration of variadic function fwprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:267: 
  Declaration of variadic function swprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:269: 
  Declaration of variadic function wprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
  Declaration of variadic function wscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
  Declaration of variadic function fwscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
  Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
  Declaration of variadic function fprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
  Declaration of variadic function fscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
  Declaration of variadic function printf.
[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
  Declaration of variadic function scanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
  Declaration of variadic function snprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
  Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
  Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
  Declaration of variadic function dprintf.
[variadic] tests/known/printf.c:37: 
  Translating call to printf to a call to the specialized version printf_va_1.
[variadic] tests/known/printf.c:38: 
  Translating call to printf to a call to the specialized version printf_va_2.
[variadic] tests/known/printf.c:39: 
  Translating call to printf to a call to the specialized version printf_va_3.
[variadic] tests/known/printf.c:41: 
  Translating call to printf to a call to the specialized version printf_va_4.
[variadic] tests/known/printf.c:42: 
  Translating call to printf to a call to the specialized version printf_va_5.
[variadic] tests/known/printf.c:43: 
  Translating call to printf to a call to the specialized version printf_va_6.
[variadic] tests/known/printf.c:44: 
  Translating call to printf to a call to the specialized version printf_va_7.
[variadic] tests/known/printf.c:45: 
  Translating call to printf to a call to the specialized version printf_va_8.
[variadic] tests/known/printf.c:46: 
  Translating call to printf to a call to the specialized version printf_va_9.
[variadic] tests/known/printf.c:47: 
  Translating call to printf to a call to the specialized version printf_va_10.
[variadic] tests/known/printf.c:48: 
  Translating call to printf to a call to the specialized version printf_va_11.
[variadic] tests/known/printf.c:50: 
  Translating call to printf to a call to the specialized version printf_va_12.
[variadic] tests/known/printf.c:51: 
  Translating call to printf to a call to the specialized version printf_va_13.
[variadic] tests/known/printf.c:52: 
  Translating call to printf to a call to the specialized version printf_va_14.
[variadic] tests/known/printf.c:53: 
  Translating call to printf to a call to the specialized version printf_va_15.
[variadic] tests/known/printf.c:54: 
  Translating call to printf to a call to the specialized version printf_va_16.
[variadic] tests/known/printf.c:55: 
  Translating call to printf to a call to the specialized version printf_va_17.
[variadic] tests/known/printf.c:56: 
  Translating call to printf to a call to the specialized version printf_va_18.
[variadic] tests/known/printf.c:58: 
  Translating call to printf to a call to the specialized version printf_va_19.
[variadic] tests/known/printf.c:59: 
  Translating call to printf to a call to the specialized version printf_va_20.
[variadic] tests/known/printf.c:60: 
  Translating call to printf to a call to the specialized version printf_va_21.
[variadic] tests/known/printf.c:61: 
  Translating call to printf to a call to the specialized version printf_va_22.
[variadic] tests/known/printf.c:63: 
  Translating call to printf to a call to the specialized version printf_va_23.
[variadic] tests/known/printf.c:65: 
  Translating call to printf to a call to the specialized version printf_va_24.
[variadic] tests/known/printf.c:68: 
  Translating call to printf to a call to the specialized version printf_va_25.
[variadic] tests/known/printf.c:69: 
  Translating call to printf to a call to the specialized version printf_va_26.
[variadic] tests/known/printf.c:71: Warning: 
  Flag ' ' and conversion specififer x are not compatibles.
[variadic] tests/known/printf.c:71: 
  Generic translation of call to variadic function.
[variadic] tests/known/printf.c:74: 
  Translating call to printf to a call to the specialized version printf_va_27.
[variadic] tests/known/printf.c:75: 
  Translating call to printf to a call to the specialized version printf_va_28.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function printf_va_1
[eva] using specification for function printf_va_2
[eva] using specification for function printf_va_3
[eva] using specification for function printf_va_4
[eva] using specification for function printf_va_5
[eva] using specification for function printf_va_6
[eva] using specification for function printf_va_7
[eva] using specification for function printf_va_8
[eva] using specification for function printf_va_9
[eva] using specification for function printf_va_10
[eva] using specification for function printf_va_11
[eva] using specification for function printf_va_12
[eva] using specification for function printf_va_13
[eva] using specification for function printf_va_14
[eva] using specification for function printf_va_15
[eva] using specification for function printf_va_16
[eva] using specification for function printf_va_17
[eva] using specification for function printf_va_18
[eva] using specification for function printf_va_19
[eva] using specification for function printf_va_20
[eva] using specification for function printf_va_21
[eva] using specification for function printf_va_22
[eva] using specification for function printf_va_23
[eva] using specification for function printf_va_24
[eva] using specification for function printf_va_25
[eva] using specification for function printf_va_26
[kernel:annot:missing-spec] tests/known/printf.c:71: Warning: 
  Neither code nor specification for function printf, generating default assigns from the prototype
[eva] using specification for function printf
[eva] using specification for function printf_va_27
[eva] using specification for function printf_va_28
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  __fc_initial_stdout.__fc_FILE_id ∈ {1}
                     .__fc_FILE_data ∈
                     {{ garbled mix of &{"Hello world !\n"}
                      (origin: Library function) }}
  string ∈ {{ "Hello world !\n" }}
  wstring ∈ {{ L"Hello world !\n" }}
  c ∈ {52}
  hh ∈ [--..--]
  uhh ∈ {42}
  h ∈ [--..--]
  uh ∈ {42}
  i ∈ [--..--]
  ui ∈ {42}
  l ∈ [--..--]
  ul ∈ {42}
  ll ∈ [--..--]
  ull ∈ {42}
  j ∈ [--..--]
  uj ∈ {42}
  z ∈ [--..--]
  t ∈ [--..--]
  f ∈ {42.}
  L ∈ {42.}
  u64 ∈ {42}
  i8 ∈ {42}
  uleast64 ∈ {42}
  ifast32 ∈ {42}
  hashes[0..3] ∈ {35}
  __retres ∈ {0}
/* Generated by Frama-C */
#include "errno.h"
#include "inttypes.h"
#include "signal.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdint.h"
#include "stdio.c"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "strings.h"
#include "sys/types.h"
#include "time.h"
#include "wchar.h"
/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __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 * __restrict format);

/*@ requires valid_read_string(format);
    requires \valid(param1);
    requires valid_read_string(param0);
    ensures \initialized(param1);
    assigns \result, __fc_stdout->__fc_FILE_data, *param1;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
    assigns *param1
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
int printf_va_2(char const * __restrict format, char *param0, int *param1);

/*@ requires valid_read_string(format);
    requires valid_read_wstring(param0);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
int printf_va_3(char const * __restrict format, wchar_t *param0);

/*@ requires valid_read_string(format);
    requires \valid(param1);
    ensures \initialized(param1);
    assigns \result, __fc_stdout->__fc_FILE_data, *param1;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
    assigns *param1
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_4(char const * __restrict format, int param0,
                signed char *param1);

/*@ requires valid_read_string(format);
    requires \valid(param1);
    ensures \initialized(param1);
    assigns \result, __fc_stdout->__fc_FILE_data, *param1;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
    assigns *param1
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_5(char const * __restrict format, int param0, short *param1);

/*@ requires valid_read_string(format);
    requires \valid(param1);
    ensures \initialized(param1);
    assigns \result, __fc_stdout->__fc_FILE_data, *param1;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
    assigns *param1
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_6(char const * __restrict format, int param0, long *param1);

/*@ requires valid_read_string(format);
    requires \valid(param1);
    ensures \initialized(param1);
    assigns \result, __fc_stdout->__fc_FILE_data, *param1;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
    assigns *param1
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_7(char const * __restrict format, long param0,
                long long *param1);

/*@ requires valid_read_string(format);
    requires \valid(param1);
    ensures \initialized(param1);
    assigns \result, __fc_stdout->__fc_FILE_data, *param1;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
    assigns *param1
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_8(char const * __restrict format, long long param0,
                intmax_t *param1);

/*@ requires valid_read_string(format);
    requires \valid(param1);
    ensures \initialized(param1);
    assigns \result, __fc_stdout->__fc_FILE_data, *param1;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
    assigns *param1
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_9(char const * __restrict format, intmax_t param0,
                size_t *param1);

/*@ requires valid_read_string(format);
    requires \valid(param1);
    ensures \initialized(param1);
    assigns \result, __fc_stdout->__fc_FILE_data, *param1;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
    assigns *param1
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_10(char const * __restrict format, size_t param0,
                 ptrdiff_t *param1);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_11(char const * __restrict format, ptrdiff_t param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_12(char const * __restrict format, unsigned int param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_13(char const * __restrict format, int param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_14(char const * __restrict format, int param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_15(char const * __restrict format, unsigned long param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_16(char const * __restrict format, unsigned long long param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_17(char const * __restrict format, uintmax_t param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param1),
            (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param1, param0;
 */
int printf_va_18(char const * __restrict format, size_t param0,
                 ptrdiff_t param1);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_19(char const * __restrict format, unsigned long long param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_20(char const * __restrict format, int param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_21(char const * __restrict format, unsigned long long param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_22(char const * __restrict format, int param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param1),
            (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param1, param0;
 */
int printf_va_23(char const * __restrict format, double param0,
                 long double param1);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_24(char const * __restrict format, int param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param0;
 */
int printf_va_25(char const * __restrict format, void *param0);

/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param3),
            (indirect: param2), (indirect: param1), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param3, param2, param1, param0;
 */
int printf_va_26(char const * __restrict format, int param0, int param1,
                 int param2, unsigned int param3);

/*@ requires valid_read_string(format);
    requires valid_read_nstring(param1, param0);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: *(param1 + (0 ..))),
            (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param1 + (0 ..)), param0;
 */
int printf_va_27(char const * __restrict format, int param0, char *param1);

/*@ requires valid_read_string(format);
    requires valid_read_nstring(param0, 4);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param0 + (0 ..));
 */
int printf_va_28(char const * __restrict format, char *param0);

int main(void)
{
  int __retres;
  signed char hh;
  short h;
  int i;
  long l;
  long long ll;
  intmax_t j;
  size_t z;
  ptrdiff_t t;
  char *string = (char *)"Hello world !\n";
  wchar_t *wstring = (wchar_t *)L"H" "e" "l" "l" "o" " " "w" "o" "r" "l" "d"
    " " "!" "\\n" ;
  char c = (char)'4';
  unsigned char uhh = (unsigned char)42;
  unsigned short uh = (unsigned short)42;
  unsigned int ui = (unsigned int)42;
  unsigned long ul = (unsigned long)42;
  unsigned long long ull = (unsigned long long)42;
  uintmax_t uj = (unsigned long long)42;
  double f = (double)42.0f;
  long double L = 42.0l;
  uint64_t u64 = (unsigned long long)42ul;
  int8_t i8 = (signed char)42;
  uint_least64_t uleast64 = (unsigned long long)42u;
  int_fast32_t ifast32 = 42;
  printf_va_1("Hello world !\n");
  printf_va_2("%s%n",string,& i);
  printf_va_3("%ls",wstring);
  printf_va_4("%d %hhn",i,& hh);
  printf_va_5("%hhi %hn",(int)hh,& h);
  printf_va_6("%hd %ln",(int)h,& l);
  printf_va_7("%li %lln",l,& ll);
  printf_va_8("%lld %jn",ll,& j);
  printf_va_9("%jd %zn",j,& z);
  printf_va_10("%zd %tn",z,& t);
  printf_va_11("%td\n",t);
  printf_va_12("%u ",ui);
  printf_va_13("%hho ",(int)uhh);
  printf_va_14("%hx ",(int)uh);
  printf_va_15("%lX ",ul);
  printf_va_16("%llu ",ull);
  printf_va_17("%jo ",uj);
  printf_va_18("%zx %tX\n",z,t);
  printf_va_19("%llu",u64);
  printf_va_20("%hhi",(int)i8);
  printf_va_21("%llx",uleast64);
  printf_va_22("%d",ifast32);
  printf_va_23("%f %Le\n",f,L);
  printf_va_24("%c\n",(int)c);
  printf_va_25("%p ",(void *)string);
  printf_va_26("%d %*.*u\n",1,- (-1),2,ui);
  {
    unsigned int __va_arg0 = ui;
    char *__va_arg1 = string;
    int __va_arg2 = 42;
    void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
    printf("Hello %- 0+#20.10lx %% %s world %d !",
           (void * const *)(__va_args));
  }
  char hashes[4] = {(char)'#', (char)'#', (char)'#', (char)'#'};
  printf_va_27("%.*s",4,hashes);
  printf_va_28("%.4s",hashes);
  __retres = 0;
  return __retres;
}