diff --git a/share/libc/__fc_machdep.h b/share/libc/__fc_machdep.h
index 0f896073b29e71b5ab81eae8e7069dff0b7ee7b8..6af1bbe7c382e329b9a0add976dda89b1e1feb4a 100644
--- a/share/libc/__fc_machdep.h
+++ b/share/libc/__fc_machdep.h
@@ -637,6 +637,145 @@
#ifndef _M_X64
# define _M_X64 1
#endif
+
+/* errno.h */
+#define __FC_EPERM 1
+#define __FC_ENOENT 2
+#define __FC_ESRCH 3
+#define __FC_EINTR 4
+#define __FC_EIO 5
+#define __FC_ENXIO 6
+#define __FC_E2BIG 7
+#define __FC_ENOEXEC 8
+#define __FC_EBADF 9
+#define __FC_ECHILD 10
+#define __FC_EAGAIN 11
+#define __FC_ENOMEM 12
+#define __FC_EACCES 13
+#define __FC_EFAULT 14
+//NOT IN MSVC: #define __FC_ENOTBLK
+#define __FC_EBUSY 16
+#define __FC_EEXIST 17
+#define __FC_EXDEV 18
+#define __FC_ENODEV 19
+#define __FC_ENOTDIR 20
+#define __FC_EISDIR 21
+#define __FC_EINVAL 22
+#define __FC_ENFILE 23
+#define __FC_EMFILE 24
+#define __FC_ENOTTY 25
+#define __FC_ETXTBSY 139
+#define __FC_EFBIG 27
+#define __FC_ENOSPC 28
+#define __FC_ESPIPE 29
+#define __FC_EROFS 30
+#define __FC_EMLINK 31
+#define __FC_EPIPE 32
+#define __FC_EDOM 33
+#define __FC_ERANGE 34
+#define __FC_EDEADLK 36
+#define __FC_ENAMETOOLONG 38
+#define __FC_ENOLCK 39
+#define __FC_ENOSYS 40
+#define __FC_ENOTEMPTY 41
+#define __FC_ELOOP 114
+#define __FC_EWOULDBLOCK 140
+#define __FC_ENOMSG 122
+#define __FC_EIDRM 111
+//NOT IN MSVC: #define __FC_ECHRNG
+//NOT IN MSVC: #define __FC_EL2NSYNC
+//NOT IN MSVC: #define __FC_EL3HLT
+//NOT IN MSVC: #define __FC_EL3RST
+//NOT IN MSVC: #define __FC_ELNRNG
+//NOT IN MSVC: #define __FC_EUNATCH
+//NOT IN MSVC: #define __FC_ENOCSI
+//NOT IN MSVC: #define __FC_EL2HLT
+//NOT IN MSVC: #define __FC_EBADE
+//NOT IN MSVC: #define __FC_EBADR
+//NOT IN MSVC: #define __FC_EXFULL
+//NOT IN MSVC: #define __FC_ENOANO
+//NOT IN MSVC: #define __FC_EBADRQC
+//NOT IN MSVC: #define __FC_EBADSLT
+#define __FC_EDEADLOCK 36
+//NOT IN MSVC: #define __FC_EBFONT
+#define __FC_ENOSTR 125
+#define __FC_ENODATA 120
+#define __FC_ETIME 137
+#define __FC_ENOSR 124
+//NOT IN MSVC: #define __FC_ENONET
+//NOT IN MSVC: #define __FC_ENOPKG
+//NOT IN MSVC: #define __FC_EREMOTE
+#define __FC_ENOLINK 121
+//NOT IN MSVC: #define __FC_EADV
+//NOT IN MSVC: #define __FC_ESRMNT
+//NOT IN MSVC: #define __FC_ECOMM
+#define __FC_EPROTO 134
+//NOT IN MSVC: #define __FC_EMULTIHOP
+//NOT IN MSVC: #define __FC_EDOTDOT
+#define __FC_EBADMSG 104
+#define __FC_EOVERFLOW 132
+//NOT IN MSVC: #define __FC_ENOTUNIQ
+//NOT IN MSVC: #define __FC_EBADFD
+//NOT IN MSVC: #define __FC_EREMCHG
+//NOT IN MSVC: #define __FC_ELIBACC
+//NOT IN MSVC: #define __FC_ELIBBAD
+//NOT IN MSVC: #define __FC_ELIBSCN
+//NOT IN MSVC: #define __FC_ELIBMAX
+//NOT IN MSVC: #define __FC_ELIBEXEC
+#define __FC_EILSEQ 42
+//NOT IN MSVC: #define __FC_ERESTART
+//NOT IN MSVC: #define __FC_ESTRPIPE
+//NOT IN MSVC: #define __FC_EUSERS
+#define __FC_ENOTSOCK 128
+#define __FC_EDESTADDRREQ 109
+#define __FC_EMSGSIZE 115
+#define __FC_EPROTOTYPE 136
+#define __FC_ENOPROTOOPT 123
+#define __FC_EPROTONOSUPPORT 135
+//NOT IN MSVC: #define __FC_ESOCKTNOSUPPORT
+#define __FC_ENOTSUP 129
+#define __FC_EOPNOTSUPP 130
+//NOT IN MSVC: #define __FC_EPFNOSUPPORT
+#define __FC_EAFNOSUPPORT 102
+#define __FC_EADDRINUSE 100
+#define __FC_EADDRNOTAVAIL 101
+#define __FC_ENETDOWN 116
+#define __FC_ENETUNREACH 118
+#define __FC_ENETRESET 117
+#define __FC_ECONNABORTED 106
+#define __FC_ECONNRESET 108
+#define __FC_ENOBUFS 119
+#define __FC_EISCONN 113
+#define __FC_ENOTCONN 126
+//NOT IN MSVC: #define __FC_ESHUTDOWN
+//NOT IN MSVC: #define __FC_ETOOMANYREFS
+#define __FC_ETIMEDOUT 138
+#define __FC_ECONNREFUSED 107
+//NOT IN MSVC: #define __FC_EHOSTDOWN
+#define __FC_EHOSTUNREACH 110
+#define __FC_EALREADY 103
+#define __FC_EINPROGRESS 112
+//NOT IN MSVC: #define __FC_ESTALE
+//NOT IN MSVC: #define __FC_EUCLEAN
+//NOT IN MSVC: #define __FC_ENOTNAM
+//NOT IN MSVC: #define __FC_ENAVAIL
+//NOT IN MSVC: #define __FC_EISNAM
+//NOT IN MSVC: #define __FC_EREMOTEIO
+//NOT IN MSVC: #define __FC_EDQUOT
+//NOT IN MSVC: #define __FC_ENOMEDIUM
+//NOT IN MSVC: #define __FC_EMEDIUMTYPE
+#define __FC_ECANCELED 105
+//NOT IN MSVC: #define __FC_ENOKEY
+//NOT IN MSVC: #define __FC_EKEYEXPIRED
+//NOT IN MSVC: #define __FC_EKEYREVOKED
+//NOT IN MSVC: #define __FC_EKEYREJECTED
+#define __FC_EOWNERDEAD 133
+#define __FC_ENOTRECOVERABLE 127
+//NOT IN MSVC: #define __FC_ERFKILL
+//NOT IN MSVC: #define __FC_EHWPOISON
+
+
+
// End of MSVC_X86_64
#else
#error Must define __FC_MACHDEP_<M>, where <M> is one of the \
diff --git a/share/libc/errno.h b/share/libc/errno.h
index 392f8226d8da65085f6a69045c9d027edb7bbb64..7193ba6629a28728f3a6af86bbadf2369f7b0757 100644
--- a/share/libc/errno.h
+++ b/share/libc/errno.h
@@ -83,7 +83,7 @@ __PUSH_FC_STDLIB
#define ELIBBAD __FC_ELIBBAD
#define ELIBMAX __FC_ELIBMAX
#define ELIBSCN __FC_ELIBSCN
-#define ELIBEXEC __FC_ELIBEXEC
+#define ELIBEXEC __FC_ELIBEXEC
#define ELOOP __FC_ELOOP
#define EMEDIUMTYPE __FC_EMEDIUMTYPE
#define EMFILE __FC_EMFILE
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index 69e8f869721672cd0ab6f6981a012fa561257cc3..93a5829898c63cfe07face63d45209f21d0fa60c 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -386,6 +386,8 @@ extern int fgetpos(FILE * restrict stream,
assigns *stream \from *stream, indirect:offset, indirect:whence;
assigns \result, __fc_errno \from indirect:*stream, indirect:offset,
indirect:whence;
+ ensures errno_set: __fc_errno \in {EAGAIN, EBADF, EFBIG, EINTR, EINVAL, EIO,
+ ENOSPC, EOVERFLOW, EPIPE, ESPIPE, ENXIO};
*/
extern int fseek(FILE *stream, long int offset, int whence);
@@ -395,17 +397,20 @@ extern int fseek(FILE *stream, long int offset, int whence);
assigns *stream \from *stream, indirect:offset, indirect:whence;
assigns \result, __fc_errno \from indirect:*stream, indirect:offset,
indirect:whence;
+ ensures errno_set: __fc_errno \in {EAGAIN, EBADF, EFBIG, EINTR, EINVAL, EIO,
+ ENOSPC, EOVERFLOW, EPIPE, ESPIPE, ENXIO};
*/
extern int fseeko(FILE *stream, off_t offset, int whence);
/*@
- //missing: assigns errno (EAGAIN, EBADF, EFBIG, EINTR, EIO, ENOSPC, EPIPE,
- // ESPIPE, ENXIO);
requires valid_stream: \valid(stream);
requires valid_pos: \valid_read(pos);
requires initialization:pos: \initialized(pos);
assigns *stream \from *pos;
assigns \result \from indirect:*stream, indirect:*pos;
+ assigns __fc_errno \from __fc_errno, indirect:*stream, indirect:*pos;
+ ensures errno_set: __fc_errno \in {EAGAIN, EBADF, EFBIG, EINTR, EIO,
+ ENOSPC, EPIPE, ESPIPE, ENXIO};
*/
extern int fsetpos(FILE *stream, const fpos_t *pos);
@@ -414,6 +419,7 @@ extern int fsetpos(FILE *stream, const fpos_t *pos);
assigns \result, __fc_errno \from indirect:*stream ;
ensures success_or_error:
\result == -1 || (\result >= 0 && __fc_errno == \old(__fc_errno));
+ ensures errno_set: __fc_errno \in {EBADF, EOVERFLOW, ESPIPE};
*/
extern long int ftell(FILE *stream);
@@ -422,6 +428,7 @@ extern long int ftell(FILE *stream);
assigns \result, __fc_errno \from indirect:*stream ;
ensures success_or_error:
\result == -1 || (\result >= 0 && __fc_errno == \old(__fc_errno));
+ ensures errno_set: __fc_errno \in {EBADF, EOVERFLOW, ESPIPE};
*/
extern off_t ftello(FILE *stream);
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index 42cc5e1f2ad6ba4d0745dbe10560791c5fc5b844..c4e0b6755536fe283e3d06bf066e2af31afa11cf 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/erroneous/printf.c:8: Warning: Multiple usage of flag '-'.
[variadic] tests/erroneous/printf.c:8: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 591d9eb02fe97ba608a2aec6af1a5cce8506d1d4..6a3b0b88b1d319fa010db5e21bd79015aaf7b9fd 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -24,7 +24,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
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.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 3a0595dbf02893ae29e58d09e7b6644f86c71cc1..f4a8692821de3ba3ec72efdcd68c48facd4f7cff 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_garbled_mix.c:7:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index f41ebdd476a827f6d6784ace54e6ef74b1aedad6..02785d8ff3d6251f2f7f1ccd575e7861d9c50f33 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_arity.c:8:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
index 90f907e7b0fb2a779cea9537aa86efa62de964da..94e8f171ee2275f1b2d002cceb36e9505b5182d9 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_pointers.c:14:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index cdc57a22aae9b2a20b0cb946f1fb42a61b0d731f..96262a87b67497376f5f1d83f8f81dee8e406a59 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
@@ -424,7 +424,7 @@ int main(void)
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
index 3eecc8a2862f226537cd1f8d4fbcf28bb26045ec..f32b5df9f60c07f1d819cf06e896492469def5d7 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf.c:7:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
index 3ea7bd6ac928f0b44b731d893844d951dd39fa5c..972e7931d57597e331d370f502670e38def9a140 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf_loop.c:6:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
index 2eb005e42169333d18e8000e2ae995dd6c778dad..84a91e7152af473882c844d54525e9abeff70d4b 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf_wrong.c:8:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index aeb7aa1c440e7559662cabfd91c8936f7eeda554..3f928d34658aa98eea01088a65b1b8d542829b8d 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/snprintf.c:12:
Translating call to snprintf to a call to the specialized version snprintf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index 1c6cbba330cc7157847d0047429c8f06bf4f487a..d1eefe22d5db925f19fa564f707af18bab3f19e7 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/stdio_print.c:9: Warning:
Call to function fprintf with non-static format argument:
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index e9425f50afe0efde098eff7834483a9d71281e48..673cafd33f94eae29f7fae8d958841effcdd4a08 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/stdio_scan.c:10: Warning:
Call to function fscanf with non-static format argument:
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 8205df96d4a61e8c2a4eae55f86162b07d38e555..ceed1ffebc170828b83e370b702f66362998b732 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -24,7 +24,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/swprintf.c:12:
Translating call to swprintf to a call to the specialized version swprintf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index d04b2860030418ce2dc78f032a869e8c57636e53..c9a23135ec5ecfdbf3841c0c247f8bce2df6ac11 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -24,7 +24,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
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.
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 9f23868dd0dccaa94f1142abf3a7e6a05ee5b172..2596ed249ede591884191af9e518229af9617054 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1920,6 +1920,11 @@
--- Properties of Function 'fseek'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'errno_set'
+ ensures
+ errno_set:
+ __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6}
+ Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/stdio.h, line 386)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
@@ -1945,19 +1950,24 @@
--- Properties of Function 'fseeko'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 395)
+[ Extern ] Post-condition 'errno_set'
+ ensures
+ errno_set:
+ __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6}
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 397)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 395)
+[ Extern ] Froms (file share/libc/stdio.h, line 397)
assigns *stream
\from *stream, (indirect: offset), (indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 396)
+[ Extern ] Froms (file share/libc/stdio.h, line 398)
assigns \result
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 396)
+[ Extern ] Froms (file share/libc/stdio.h, line 398)
assigns __fc_errno
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
@@ -1970,15 +1980,23 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 407)
- assigns *stream, \result;
+[ Extern ] Post-condition 'errno_set'
+ ensures
+ errno_set: __fc_errno ∈ {11, 9, 27, 4, 5, 28, 32, 29, 6}
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 409)
+ assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 407)
+[ Extern ] Froms (file share/libc/stdio.h, line 409)
assigns *stream \from *pos;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 408)
+[ Extern ] Froms (file share/libc/stdio.h, line 410)
assigns \result \from (indirect: *stream), (indirect: *pos);
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 411)
+ assigns __fc_errno
+ \from __fc_errno, (indirect: *stream), (indirect: *pos);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1993,13 +2011,16 @@
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 414)
+[ Extern ] Post-condition 'errno_set'
+ ensures errno_set: __fc_errno ∈ {9, 75, 29}
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 419)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 414)
+[ Extern ] Froms (file share/libc/stdio.h, line 419)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 414)
+[ Extern ] Froms (file share/libc/stdio.h, line 419)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2016,13 +2037,16 @@
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 422)
+[ Extern ] Post-condition 'errno_set'
+ ensures errno_set: __fc_errno ∈ {9, 75, 29}
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 428)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2033,10 +2057,10 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 430)
+[ Extern ] Assigns (file share/libc/stdio.h, line 437)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 430)
+[ Extern ] Froms (file share/libc/stdio.h, line 437)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2047,10 +2071,10 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 436)
+[ Extern ] Assigns (file share/libc/stdio.h, line 443)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 436)
+[ Extern ] Froms (file share/libc/stdio.h, line 443)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2064,7 +2088,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 442)
+[ Extern ] Froms (file share/libc/stdio.h, line 449)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2078,7 +2102,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 448)
+[ Extern ] Froms (file share/libc/stdio.h, line 455)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2089,10 +2113,10 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 454)
+[ Extern ] Assigns (file share/libc/stdio.h, line 461)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 454)
+[ Extern ] Froms (file share/libc/stdio.h, line 461)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2103,10 +2127,10 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 460)
+[ Extern ] Assigns (file share/libc/stdio.h, line 467)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 460)
+[ Extern ] Froms (file share/libc/stdio.h, line 467)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2117,13 +2141,13 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 466)
+[ Extern ] Assigns (file share/libc/stdio.h, line 473)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 466)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
assigns \result \from \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 466)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2137,7 +2161,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 472)
+[ Extern ] Froms (file share/libc/stdio.h, line 479)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2148,10 +2172,10 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 478)
+[ Extern ] Assigns (file share/libc/stdio.h, line 485)
assigns __fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 478)
+[ Extern ] Froms (file share/libc/stdio.h, line 485)
assigns __fc_stdout
\from __fc_errno, *(s + (0 .. strlen{Old}(s)));
Unverifiable but considered Valid.
@@ -2163,13 +2187,13 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 484)
+[ Extern ] Assigns (file share/libc/stdio.h, line 491)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 484)
+[ Extern ] Froms (file share/libc/stdio.h, line 491)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 484)
+[ Extern ] Froms (file share/libc/stdio.h, line 491)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2183,7 +2207,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 489)
+[ Extern ] Froms (file share/libc/stdio.h, line 496)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2194,13 +2218,13 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 495)
+[ Extern ] Assigns (file share/libc/stdio.h, line 502)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 495)
+[ Extern ] Froms (file share/libc/stdio.h, line 502)
assigns *stream \from c;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 496)
+[ Extern ] Froms (file share/libc/stdio.h, line 503)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2211,13 +2235,13 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 501)
+[ Extern ] Assigns (file share/libc/stdio.h, line 508)
assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 501)
+[ Extern ] Froms (file share/libc/stdio.h, line 508)
assigns *__fc_stdout \from c;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 502)
+[ Extern ] Froms (file share/libc/stdio.h, line 509)
assigns \result \from (indirect: *__fc_stdout);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2228,10 +2252,10 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 508)
+[ Extern ] Assigns (file share/libc/stdio.h, line 515)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 508)
+[ Extern ] Froms (file share/libc/stdio.h, line 515)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2245,7 +2269,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 514)
+[ Extern ] Froms (file share/libc/stdio.h, line 521)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2259,7 +2283,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 520)
+[ Extern ] Froms (file share/libc/stdio.h, line 527)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2273,7 +2297,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 526)
+[ Extern ] Froms (file share/libc/stdio.h, line 533)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2291,14 +2315,14 @@
(\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
is_open_pipe(\result))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 553)
+[ Extern ] Assigns (file share/libc/stdio.h, line 560)
assigns \result, __fc_fopen[0 ..];
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 553)
+[ Extern ] Froms (file share/libc/stdio.h, line 560)
assigns \result
\from (indirect: *command), (indirect: *type), __fc_p_fopen;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 555)
+[ Extern ] Froms (file share/libc/stdio.h, line 562)
assigns __fc_fopen[0 ..]
\from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
Unverifiable but considered Valid.
@@ -2316,7 +2340,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 567)
+[ Extern ] Froms (file share/libc/stdio.h, line 574)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4263,7 +4287,7 @@
--------------------------------------------------------------------------------
184 Completely validated
16 Locally validated
- 528 Considered valid
+ 534 Considered valid
56 To be validated
- 784 Total
+ 790 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index c99ba102c79368d6a0891069a36e52ff359cfd10..d091867259e5fe0c5544af9c413708fb01cea5bc 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4945,6 +4945,8 @@ extern int fgetpos(FILE * restrict stream, fpos_t * restrict pos);
/*@ requires valid_stream: \valid(stream);
requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+ ensures
+ errno_set: __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6};
assigns *stream, \result, __fc_errno;
assigns *stream \from *stream, (indirect: offset), (indirect: whence);
assigns \result
@@ -4956,6 +4958,8 @@ extern int fseek(FILE *stream, long offset, int whence);
/*@ requires valid_stream: \valid(stream);
requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+ ensures
+ errno_set: __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6};
assigns *stream, \result, __fc_errno;
assigns *stream \from *stream, (indirect: offset), (indirect: whence);
assigns \result
@@ -4968,9 +4972,12 @@ extern int fseeko(FILE *stream, off_t offset, int whence);
/*@ requires valid_stream: \valid(stream);
requires valid_pos: \valid_read(pos);
requires initialization: pos: \initialized(pos);
- assigns *stream, \result;
+ ensures errno_set: __fc_errno ∈ {11, 9, 27, 4, 5, 28, 32, 29, 6};
+ assigns *stream, \result, __fc_errno;
assigns *stream \from *pos;
assigns \result \from (indirect: *stream), (indirect: *pos);
+ assigns __fc_errno
+ \from __fc_errno, (indirect: *stream), (indirect: *pos);
*/
extern int fsetpos(FILE *stream, fpos_t const *pos);
@@ -4979,6 +4986,7 @@ extern int fsetpos(FILE *stream, fpos_t const *pos);
success_or_error:
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
+ ensures errno_set: __fc_errno ∈ {9, 75, 29};
assigns \result, __fc_errno;
assigns \result \from (indirect: *stream);
assigns __fc_errno \from (indirect: *stream);
@@ -4990,6 +4998,7 @@ extern long ftell(FILE *stream);
success_or_error:
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
+ ensures errno_set: __fc_errno ∈ {9, 75, 29};
assigns \result, __fc_errno;
assigns \result \from (indirect: *stream);
assigns __fc_errno \from (indirect: *stream);
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 70d52622e9915aa69db43a5d579cedd29410a89f..83a5a5c7b2168e4db1cd0fdb406364b51427d35b 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -593,6 +593,8 @@
--- Properties of Function 'fseek'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'errno_set'
+ Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/stdio.h, line 386)
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/stdio.h, line 386)
@@ -608,13 +610,15 @@
--- Properties of Function 'fseeko'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 395)
+[ Extern ] Post-condition 'errno_set'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 397)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 395)
+[ Extern ] Froms (file share/libc/stdio.h, line 397)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 396)
+[ Extern ] Froms (file share/libc/stdio.h, line 398)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 396)
+[ Extern ] Froms (file share/libc/stdio.h, line 398)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -623,11 +627,15 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 407)
+[ Extern ] Post-condition 'errno_set'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 409)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 409)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 407)
+[ Extern ] Froms (file share/libc/stdio.h, line 410)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 408)
+[ Extern ] Froms (file share/libc/stdio.h, line 411)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -638,11 +646,13 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 414)
+[ Extern ] Post-condition 'errno_set'
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 414)
+[ Extern ] Assigns (file share/libc/stdio.h, line 419)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 414)
+[ Extern ] Froms (file share/libc/stdio.h, line 419)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 419)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -653,11 +663,13 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 422)
+[ Extern ] Post-condition 'errno_set'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 428)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -666,9 +678,9 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 430)
+[ Extern ] Assigns (file share/libc/stdio.h, line 437)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 430)
+[ Extern ] Froms (file share/libc/stdio.h, line 437)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -677,9 +689,9 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 436)
+[ Extern ] Assigns (file share/libc/stdio.h, line 443)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 436)
+[ Extern ] Froms (file share/libc/stdio.h, line 443)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -690,7 +702,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 442)
+[ Extern ] Froms (file share/libc/stdio.h, line 449)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -701,7 +713,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 448)
+[ Extern ] Froms (file share/libc/stdio.h, line 455)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -710,9 +722,9 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 454)
+[ Extern ] Assigns (file share/libc/stdio.h, line 461)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 454)
+[ Extern ] Froms (file share/libc/stdio.h, line 461)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -721,9 +733,9 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 460)
+[ Extern ] Assigns (file share/libc/stdio.h, line 467)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 460)
+[ Extern ] Froms (file share/libc/stdio.h, line 467)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -732,11 +744,11 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 466)
+[ Extern ] Assigns (file share/libc/stdio.h, line 473)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 466)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 466)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -747,7 +759,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 472)
+[ Extern ] Froms (file share/libc/stdio.h, line 479)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -756,9 +768,9 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 478)
+[ Extern ] Assigns (file share/libc/stdio.h, line 485)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 478)
+[ Extern ] Froms (file share/libc/stdio.h, line 485)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -767,11 +779,11 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 484)
+[ Extern ] Assigns (file share/libc/stdio.h, line 491)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 484)
+[ Extern ] Froms (file share/libc/stdio.h, line 491)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 484)
+[ Extern ] Froms (file share/libc/stdio.h, line 491)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -782,7 +794,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 489)
+[ Extern ] Froms (file share/libc/stdio.h, line 496)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -791,11 +803,11 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 495)
+[ Extern ] Assigns (file share/libc/stdio.h, line 502)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 495)
+[ Extern ] Froms (file share/libc/stdio.h, line 502)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 496)
+[ Extern ] Froms (file share/libc/stdio.h, line 503)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -804,11 +816,11 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 501)
+[ Extern ] Assigns (file share/libc/stdio.h, line 508)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 501)
+[ Extern ] Froms (file share/libc/stdio.h, line 508)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 502)
+[ Extern ] Froms (file share/libc/stdio.h, line 509)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -817,9 +829,9 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 508)
+[ Extern ] Assigns (file share/libc/stdio.h, line 515)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 508)
+[ Extern ] Froms (file share/libc/stdio.h, line 515)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -830,7 +842,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 514)
+[ Extern ] Froms (file share/libc/stdio.h, line 521)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -841,7 +853,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 520)
+[ Extern ] Froms (file share/libc/stdio.h, line 527)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -852,7 +864,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 526)
+[ Extern ] Froms (file share/libc/stdio.h, line 533)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -863,11 +875,11 @@
[ Extern ] Post-condition 'result_error_or_valid_open_pipe'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 553)
+[ Extern ] Assigns (file share/libc/stdio.h, line 560)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 553)
+[ Extern ] Froms (file share/libc/stdio.h, line 560)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 555)
+[ Extern ] Froms (file share/libc/stdio.h, line 562)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -880,7 +892,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 567)
+[ Extern ] Froms (file share/libc/stdio.h, line 574)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -900,7 +912,7 @@
--- Status Report Summary
--------------------------------------------------------------------------------
74 Completely validated
- 208 Considered valid
+ 214 Considered valid
1 To be validated
- 283 Total
+ 289 Total
--------------------------------------------------------------------------------