wchar.res.oracle

[variadic] FRAMAC_SHARE/libc/wchar.h:195: 
  Declaration of variadic function fwprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:197: 
  Declaration of variadic function swprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:199: 
  Declaration of variadic function wprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:202: 
  Declaration of variadic function wscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:204: 
  Declaration of variadic function fwscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:206: 
  Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
  Declaration of variadic function fprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
  Declaration of variadic function fscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
  Declaration of variadic function printf.
[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
  Declaration of variadic function scanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
  Declaration of variadic function snprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
  Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
  Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
  Declaration of variadic function dprintf.
[variadic] tests/known/wchar.c:11: 
  Translating call to wprintf to a call to the specialized version wprintf_va_1.
[variadic] tests/known/wchar.c:12: 
  Translating call to wprintf to a call to the specialized version wprintf_va_2.
[variadic] tests/known/wchar.c:13: 
  Translating call to wprintf to a call to the specialized version wprintf_va_3.
[variadic] tests/known/wchar.c:14: 
  Translating call to wprintf to a call to the specialized version wprintf_va_4.
[variadic] tests/known/wchar.c:15: 
  Translating call to wprintf to a call to the specialized version wprintf_va_5.
[variadic] tests/known/wchar.c:16: 
  Translating call to wprintf to a call to the specialized version wprintf_va_6.
[variadic] tests/known/wchar.c:18: 
  Translating call to swprintf to a call to the specialized version swprintf_va_1.
[variadic] tests/known/wchar.c:20: 
  Translating call to wscanf to a call to the specialized version wscanf_va_1.
[variadic] tests/known/wchar.c:21: 
  Translating call to wscanf to a call to the specialized version wscanf_va_2.
[variadic] tests/known/wchar.c:23: 
  Translating call to swscanf to a call to the specialized version swscanf_va_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function wprintf_va_1
[eva] using specification for function wprintf_va_2
[eva] using specification for function wprintf_va_3
[eva] using specification for function wprintf_va_4
[eva] using specification for function wprintf_va_5
[eva] using specification for function wprintf_va_6
[eva] using specification for function swprintf_va_1
[eva] using specification for function wscanf_va_1
[eva] using specification for function wscanf_va_2
[eva] using specification for function swscanf_va_1
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  input[0] ∈ {102}
       [1] ∈ {111}
       [2] ∈ {114}
       [3] ∈ {116}
       [4] ∈ {121}
       [5] ∈ {45}
       [6] ∈ {116}
       [7] ∈ {119}
       [8] ∈ {111}
       [9] ∈ {32}
       [10] ∈ {105}
       [11] ∈ {115}
       [12..255] ∈ {0}
  wstring[0..255] ∈ [--..--] or UNINITIALIZED
  i ∈ [--..--]
  j ∈ [--..--]
  __retres ∈ {0}
  S___fc_stdin[0..1] ∈ [--..--]
  S___fc_stdout[0..1] ∈ [--..--]
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stdio.h"
#include "time.h"
#include "wchar.h"
/*@ requires valid_read_wstring(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 ..))),
            param1, 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 wprintf_va_1(wchar_t const *format, int param0, long param1);

/*@ requires valid_read_wstring(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 ..))),
            param1, 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 wprintf_va_2(wchar_t const *format, int param0, int param1);

/*@ requires valid_read_wstring(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 ..))),
            param4, param3, param2, param1, param0;
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param4, param3, param2, param1, param0;
 */
int wprintf_va_3(wchar_t const *format, int param0, unsigned int param1,
                 unsigned int param2, unsigned int param3,
                 unsigned int param4);

/*@ requires valid_read_wstring(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 ..))),
            param2, param1, param0;
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param2, param1, param0;
 */
int wprintf_va_4(wchar_t const *format, double param0, double param1,
                 double param2);

/*@ requires valid_read_wstring(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 ..))),
            param1, 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 wprintf_va_5(wchar_t const *format, int param0, int param1);

/*@ requires valid_read_wstring(format);
    requires valid_read_wstring(param0);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(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 wprintf_va_6(wchar_t const *format, wchar_t *param0);

/*@ requires
      \valid(ws + (0 .. n - 1)) ∨
      \valid(ws + (0 .. wformat_length(format) - 1));
    requires valid_read_wstring(format);
    requires valid_read_string(param0);
    assigns \result, *(ws + (0 ..));
    assigns \result
      \from (indirect: n), (indirect: *(format + (0 ..))), param1,
            *(param0 + (0 ..));
    assigns *(ws + (0 ..))
      \from (indirect: n), (indirect: *(format + (0 ..))), param1,
            *(param0 + (0 ..));
 */
int swprintf_va_1(wchar_t *ws, size_t n, wchar_t const *format, char *param0,
                  int param1);

/*@ requires valid_read_wstring(format);
    assigns \result, __fc_stdin->__fc_FILE_data, *(param0 + (0 ..));
    assigns \result
      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
            (indirect: *(format + (0 ..)));
    assigns __fc_stdin->__fc_FILE_data
      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
            (indirect: *(format + (0 ..)));
    assigns *(param0 + (0 ..))
      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
            (indirect: *(format + (0 ..)));
 */
int wscanf_va_1(wchar_t const *format, wchar_t *param0);

/*@ requires valid_read_wstring(format);
    requires \valid(param1);
    requires \valid(param0);
    ensures \initialized(param1);
    ensures \initialized(param0);
    assigns \result, __fc_stdin->__fc_FILE_data, *param1, *param0;
    assigns \result
      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
            (indirect: *(format + (0 ..)));
    assigns __fc_stdin->__fc_FILE_data
      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
            (indirect: *(format + (0 ..)));
    assigns *param1
      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
            (indirect: *(format + (0 ..)));
    assigns *param0
      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
            (indirect: *(format + (0 ..)));
 */
int wscanf_va_2(wchar_t const *format, int *param0, int *param1);

/*@ requires valid_read_wstring(str);
    requires valid_read_wstring(format);
    requires \valid(param1);
    ensures \initialized(param1);
    assigns \result, *param1, *(param0 + (0 ..));
    assigns \result
      \from (indirect: *(str + (0 ..))), (indirect: *(format + (0 ..)));
    assigns *param1
      \from (indirect: *(str + (0 ..))), (indirect: *(format + (0 ..)));
    assigns *(param0 + (0 ..))
      \from (indirect: *(str + (0 ..))), (indirect: *(format + (0 ..)));
 */
int swscanf_va_1(wchar_t const *str, wchar_t const *format, wchar_t *param0,
                 int *param1);

int main(void)
{
  int __retres;
  wchar_t wstring[0x100];
  int i;
  int j;
  wchar_t input[0x100] =
    {102, 111, 114, 116, 121, 45, 116, 119, 111, 32, 105, 115, 0};
  wprintf_va_1((wchar_t const *)L"%" "d" " " "%" "l" "d" "\\n" ,42,42L);
  wprintf_va_2((wchar_t const *)L"%" "1" "0" "d" " " "%" "0" "1" "0" "d"
               "\\n" ,42,42);
  wprintf_va_3((wchar_t const *)L"%" "d" " " "%" "x" " " "%" "o" " " "%" "#"
               "x" " " "%" "#" "o" "\\n" ,42,42u,42u,42u,42u);
  wprintf_va_4((wchar_t const *)L"%" "2" "." "1" "f" " " "%" "+" "." "0" "e"
               " " "%" "E" "\\n" ,42.0,42.0,42.0);
  wprintf_va_5((wchar_t const *)L"%" "*" "d" " " "\\n" ,4,2);
  wprintf_va_6((wchar_t const *)L"%" "l" "s" " " "\\n" ,(wchar_t *)L"4" "2" );
  swprintf_va_1(wstring,(unsigned int)0x100,(wchar_t const *)L"%" "s" " " "="
                " " "%" "d" ,(char *)L"4" "2" " " "+" " " "4" "2" ,42 + 42);
  wscanf_va_1((wchar_t const *)L"%" "l" "s" ,wstring);
  wscanf_va_2((wchar_t const *)L"%" "d" " " "%" "d" ,& i,& j);
  swscanf_va_1((wchar_t const *)(input),(wchar_t const *)L"%" "l" "s" " " "%"
               "*" "s" " " "%" "d" ,wstring,& i);
  __retres = 0;
  return __retres;
}