scanf.1.res.oracle 4.35 KiB
[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:550:
Declaration of variadic function dprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] scanf.c:12:
Translating call to scanf to a call to the specialized version scanf_va_1.
[variadic] scanf.c:15:
Translating call to scanf to a call to the specialized version scanf_va_2.
[variadic] scanf.c:23:
Translating call to scanf to a call to the specialized version scanf_va_3.
[eva] Analyzing a complete application starting at main
[eva] using specification for function scanf_va_1
[eva] using specification for function scanf_va_2
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
c[0] ∈ [--..--]
[1..9] ∈ [--..--] or UNINITIALIZED
i ∈ [--..--]
wc ∈ [--..--]
__retres ∈ {0}
S___fc_stdin[0..1] ∈ [--..--]
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdint.h"
#include "stdio.h"
/*@ requires \valid(param1);
requires \valid(param2);
requires valid_read_string(format);
ensures \initialized(param1);
ensures \initialized(param2);
assigns \result, __fc_stdin->__fc_FILE_data, *param2, *param1,
*(param0 + (0 ..));
assigns \result
\from (indirect: __fc_stdin->__fc_FILE_id),
(indirect: __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 *param2
\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 + (0 ..))
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * restrict format, char *param0, char *param1,
int *param2);
/*@ requires \valid(param0);
requires valid_read_string(format);