Forked from
pub / frama-c
14979 commits behind the upstream repository.
-
Andre Maroneze authoredAndre Maroneze authored
printf.res.oracle 26.52 KiB
[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;
}