diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index c3fa3488a7606152378172963360f8b0c1b467dd..fe7f34f40a97524cb22e1f84377bdc2a7a34d99d 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -371,11 +371,11 @@ extern size_t fwrite(const void * restrict ptr,
FILE * restrict stream);
/*@
+ //missing: assigns errno (EBADF, EOVERFLOW, ESPIPE);
requires valid_stream: \valid(stream);
requires valid_pos: \valid(pos);
- requires initialization:pos: \initialized(pos);
- assigns *pos \from indirect:*stream;
- assigns \result \from indirect:*stream;
+ assigns \result, *pos \from indirect:*stream;
+ ensures initialization:pos: \initialized(pos);
*/
extern int fgetpos(FILE * restrict stream,
fpos_t * restrict pos);
@@ -399,10 +399,13 @@ extern int fseek(FILE *stream, long int offset, int whence);
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;
*/
extern int fsetpos(FILE *stream, const fpos_t *pos);
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index bf32832912efc4f3b07515090655826e888ce94c..42cc5e1f2ad6ba4d0745dbe10560791c5fc5b844 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 d7102dda0aa118a8915a12b3801847c657c4016e..466df2fb14ff799aa664504b31e8c411db639545 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 e75911730236bc2264e15e690bbe63de68d9e92b..18e298855651f28719771d12be1b821e2af2e8ee 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_garbled_mix.c:8:
Variadic builtin Frama_C_show_each_nb_printed left untransformed.
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 4ee27be46611b179b94c9eca126c0a3aed8a46e3..fb8aff5b5010d525860db87b4ed5b932321499ff 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 2c72bbbab0497dc928525540fbe32d744e90c774..d08481ad5e2a4baa0cfdcbf0f7d7aeb3e5e24fad 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 5d41306e7d7770b2f2debc89711360675aa0bdc1..d9fbae7e5f89be7538495e730d7952060a414b09 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 bf4a9d81548e13066cc07874387d684d28e89997..8e0fee8c8c61cb7130dda20c71f83fb974454e16 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 e563ba2f274de6ca32bf4384ba1c876d0d3fed51..84e1b114610bc2fba9c22e3d20992101bebb3551 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 704b3de7532cbbe3b74de18a9b261d8fb1990a4b..2ae6ce88bc32928d31beaa83e61f14f8836b30b7 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 cecc5cc54317c70556a4191b957dfffa35b3ab2b..eff1561846476dc7d311772a7dfd93f670293bda 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 cc3c40be6d63726412cc1680892eec9481895efa..7952572f5ecd71bace98a028b4028ad4f8317874 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 f157c9d36bf492d0950438e324ebd2081d5bfa52..841afb45a4b66b5c672e1ef841727732c4525548 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 585983473b2a34fb414ff248ba31750429cd90cf..5efd248eb0b5ce882b544e4cad53a555fa11a625 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 b85bb1c1d0672bd3a723c7e2b659c56ed8f769c0..05cd9a214e23627b429f80a73c1b52e05f74a1b7 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:538:
+[variadic] FRAMAC_SHARE/libc/stdio.h:541:
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 c3f8b8d2b91ee064a2084b5a3c0cfa2241763c11..ee5c88ae7ff10e6c5521fff4e848a3745f07d258 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1900,15 +1900,18 @@
--- Properties of Function 'fgetpos'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'initialization,pos'
+ ensures initialization: pos: \initialized(\old(pos))
+ Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/stdio.h, line 377)
- assigns *pos, \result;
+ assigns \result, *pos;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/stdio.h, line 377)
- assigns *pos \from (indirect: *stream);
- Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 378)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 377)
+ assigns *pos \from (indirect: *stream);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1967,12 +1970,15 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 405)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 407)
+ assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 405)
+[ Extern ] Froms (file share/libc/stdio.h, line 407)
assigns *stream \from *pos;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 408)
+ assigns \result \from (indirect: *stream), (indirect: *pos);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1987,13 +1993,13 @@
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 411)
+[ Extern ] Assigns (file share/libc/stdio.h, line 414)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 411)
+[ Extern ] Froms (file share/libc/stdio.h, line 414)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 411)
+[ Extern ] Froms (file share/libc/stdio.h, line 414)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2010,13 +2016,13 @@
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 419)
+[ Extern ] Assigns (file share/libc/stdio.h, line 422)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 419)
+[ Extern ] Froms (file share/libc/stdio.h, line 422)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 419)
+[ Extern ] Froms (file share/libc/stdio.h, line 422)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2027,10 +2033,10 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 427)
+[ Extern ] Assigns (file share/libc/stdio.h, line 430)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 427)
+[ Extern ] Froms (file share/libc/stdio.h, line 430)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2041,10 +2047,10 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 433)
+[ Extern ] Assigns (file share/libc/stdio.h, line 436)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 433)
+[ Extern ] Froms (file share/libc/stdio.h, line 436)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2058,7 +2064,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 439)
+[ Extern ] Froms (file share/libc/stdio.h, line 442)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2072,7 +2078,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 445)
+[ Extern ] Froms (file share/libc/stdio.h, line 448)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2083,10 +2089,10 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 451)
+[ Extern ] Assigns (file share/libc/stdio.h, line 454)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 451)
+[ Extern ] Froms (file share/libc/stdio.h, line 454)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2097,10 +2103,10 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 457)
+[ Extern ] Assigns (file share/libc/stdio.h, line 460)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 457)
+[ Extern ] Froms (file share/libc/stdio.h, line 460)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2111,13 +2117,13 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 463)
+[ Extern ] Assigns (file share/libc/stdio.h, line 466)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 463)
+[ Extern ] Froms (file share/libc/stdio.h, line 466)
assigns \result \from \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 463)
+[ Extern ] Froms (file share/libc/stdio.h, line 466)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2131,7 +2137,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 469)
+[ Extern ] Froms (file share/libc/stdio.h, line 472)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2142,10 +2148,10 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 475)
+[ Extern ] Assigns (file share/libc/stdio.h, line 478)
assigns __fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 475)
+[ Extern ] Froms (file share/libc/stdio.h, line 478)
assigns __fc_stdout
\from __fc_errno, *(s + (0 .. strlen{Old}(s)));
Unverifiable but considered Valid.
@@ -2157,13 +2163,13 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 481)
+[ Extern ] Assigns (file share/libc/stdio.h, line 484)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 481)
+[ Extern ] Froms (file share/libc/stdio.h, line 484)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 481)
+[ Extern ] Froms (file share/libc/stdio.h, line 484)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2177,7 +2183,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 486)
+[ Extern ] Froms (file share/libc/stdio.h, line 489)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2188,13 +2194,13 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 492)
+[ Extern ] Assigns (file share/libc/stdio.h, line 495)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 492)
+[ Extern ] Froms (file share/libc/stdio.h, line 495)
assigns *stream \from c;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 493)
+[ Extern ] Froms (file share/libc/stdio.h, line 496)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2205,13 +2211,13 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 498)
+[ Extern ] Assigns (file share/libc/stdio.h, line 501)
assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 498)
+[ Extern ] Froms (file share/libc/stdio.h, line 501)
assigns *__fc_stdout \from c;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 499)
+[ Extern ] Froms (file share/libc/stdio.h, line 502)
assigns \result \from (indirect: *__fc_stdout);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2222,10 +2228,10 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 505)
+[ Extern ] Assigns (file share/libc/stdio.h, line 508)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 505)
+[ Extern ] Froms (file share/libc/stdio.h, line 508)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2239,7 +2245,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 511)
+[ Extern ] Froms (file share/libc/stdio.h, line 514)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2253,7 +2259,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 517)
+[ Extern ] Froms (file share/libc/stdio.h, line 520)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2267,7 +2273,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 523)
+[ Extern ] Froms (file share/libc/stdio.h, line 526)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2285,14 +2291,14 @@
(\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
is_open_pipe(\result))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 550)
+[ Extern ] Assigns (file share/libc/stdio.h, line 553)
assigns \result, __fc_fopen[0 ..];
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 550)
+[ Extern ] Froms (file share/libc/stdio.h, line 553)
assigns \result
\from (indirect: *command), (indirect: *type), __fc_p_fopen;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 552)
+[ Extern ] Froms (file share/libc/stdio.h, line 555)
assigns __fc_fopen[0 ..]
\from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
Unverifiable but considered Valid.
@@ -2310,7 +2316,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 564)
+[ Extern ] Froms (file share/libc/stdio.h, line 567)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3946,7 +3952,7 @@
--------------------------------------------------------------------------------
169 Completely validated
16 Locally validated
- 452 Considered valid
+ 454 Considered valid
56 To be validated
- 693 Total
+ 695 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 981e7bf9215e1c7f30817097018a3be302981db8..36e9390d1b2681d50ba65bb6ad5c74694fc63512 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4713,10 +4713,10 @@ extern size_t fwrite(void const * __restrict ptr, size_t size, size_t nmemb,
/*@ requires valid_stream: \valid(stream);
requires valid_pos: \valid(pos);
- requires initialization: pos: \initialized(pos);
- assigns *pos, \result;
- assigns *pos \from (indirect: *stream);
+ ensures initialization: pos: \initialized(\old(pos));
+ assigns \result, *pos;
assigns \result \from (indirect: *stream);
+ assigns *pos \from (indirect: *stream);
*/
extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos);
@@ -4745,8 +4745,9 @@ 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;
+ assigns *stream, \result;
assigns *stream \from *pos;
+ assigns \result \from (indirect: *stream), (indirect: *pos);
*/
extern int fsetpos(FILE *stream, fpos_t const *pos);
diff --git a/tests/libc/oracle/stdio_h.res.oracle b/tests/libc/oracle/stdio_h.res.oracle
index e839ecd549f19392a27f066d520d13234acee068..3a64229e0e65255d3fede1f6f5d07dd7f5000489 100644
--- a/tests/libc/oracle/stdio_h.res.oracle
+++ b/tests/libc/oracle/stdio_h.res.oracle
@@ -114,6 +114,29 @@
[eva:alarm] tests/libc/stdio_h.c:41: Warning:
function fgets: precondition 'room_s' got status invalid.
[eva] Done for function fgets
+[eva] computing for function fgetpos <- main.
+ Called from tests/libc/stdio_h.c:46.
+[eva] using specification for function fgetpos
+[eva] tests/libc/stdio_h.c:46:
+ function fgetpos: precondition 'valid_stream' got status valid.
+[eva] tests/libc/stdio_h.c:46:
+ function fgetpos: precondition 'valid_pos' got status valid.
+[eva] Done for function fgetpos
+[eva] computing for function fsetpos <- main.
+ Called from tests/libc/stdio_h.c:47.
+[eva] using specification for function fsetpos
+[eva] tests/libc/stdio_h.c:47:
+ function fsetpos: precondition 'valid_stream' got status valid.
+[eva] tests/libc/stdio_h.c:47:
+ function fsetpos: precondition 'valid_pos' got status valid.
+[eva] tests/libc/stdio_h.c:47:
+ function fsetpos: precondition 'initialization,pos' got status valid.
+[eva] Done for function fsetpos
+[eva] computing for function fclose <- main.
+ Called from tests/libc/stdio_h.c:49.
+[eva] tests/libc/stdio_h.c:49:
+ function fclose: precondition 'valid_stream' got status valid.
+[eva] Done for function fclose
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -129,5 +152,7 @@
redirected ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
fgets_buf0[0] ∈ [--..--] or UNINITIALIZED
fgets_res ∈ {{ NULL ; &fgets_buf0[0] }}
+ pos ∈ [--..--] or UNINITIALIZED
+ res_fclose ∈ {-1; 0}
__retres ∈ {0; 1; 2; 3}
S___fc_stdout[0..1] ∈ [--..--]
diff --git a/tests/libc/stdio_h.c b/tests/libc/stdio_h.c
index 1150500b6cb4d2c6c8c8464c279d2ae685777a79..19531ca2e4042e831ad5e57a50d19311687910a3 100644
--- a/tests/libc/stdio_h.c
+++ b/tests/libc/stdio_h.c
@@ -42,5 +42,10 @@ int main() {
//@ assert unreachable: \false;
}
+ fpos_t pos;
+ fgetpos(f, &pos);
+ fsetpos(f, &pos);
+
+ int res_fclose = fclose(f);
return 0;
}
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 1fa05cbf8c666c7af1c93b0cf4bf6425cceeffa2..42a86c5e8f0cac08a72672c4f4908283f3ef6737 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -578,11 +578,13 @@
--- Properties of Function 'fgetpos'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'initialization,pos'
+ Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/stdio.h, line 377)
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/stdio.h, line 377)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 378)
+[ Extern ] Froms (file share/libc/stdio.h, line 377)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -621,9 +623,11 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 405)
+[ Extern ] Assigns (file share/libc/stdio.h, line 407)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 407)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 405)
+[ Extern ] Froms (file share/libc/stdio.h, line 408)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -634,11 +638,11 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 411)
+[ Extern ] Assigns (file share/libc/stdio.h, line 414)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 411)
+[ Extern ] Froms (file share/libc/stdio.h, line 414)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 411)
+[ Extern ] Froms (file share/libc/stdio.h, line 414)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -649,11 +653,11 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 419)
+[ Extern ] Assigns (file share/libc/stdio.h, line 422)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 419)
+[ Extern ] Froms (file share/libc/stdio.h, line 422)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 419)
+[ Extern ] Froms (file share/libc/stdio.h, line 422)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -662,9 +666,9 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 427)
+[ Extern ] Assigns (file share/libc/stdio.h, line 430)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 427)
+[ Extern ] Froms (file share/libc/stdio.h, line 430)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -673,9 +677,9 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 433)
+[ Extern ] Assigns (file share/libc/stdio.h, line 436)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 433)
+[ Extern ] Froms (file share/libc/stdio.h, line 436)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -686,7 +690,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 439)
+[ Extern ] Froms (file share/libc/stdio.h, line 442)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -697,7 +701,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 445)
+[ Extern ] Froms (file share/libc/stdio.h, line 448)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -706,9 +710,9 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 451)
+[ Extern ] Assigns (file share/libc/stdio.h, line 454)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 451)
+[ Extern ] Froms (file share/libc/stdio.h, line 454)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -717,9 +721,9 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 457)
+[ Extern ] Assigns (file share/libc/stdio.h, line 460)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 457)
+[ Extern ] Froms (file share/libc/stdio.h, line 460)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -728,11 +732,11 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 463)
+[ Extern ] Assigns (file share/libc/stdio.h, line 466)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 463)
+[ Extern ] Froms (file share/libc/stdio.h, line 466)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 463)
+[ Extern ] Froms (file share/libc/stdio.h, line 466)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -743,7 +747,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 469)
+[ Extern ] Froms (file share/libc/stdio.h, line 472)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -752,9 +756,9 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 475)
+[ Extern ] Assigns (file share/libc/stdio.h, line 478)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 475)
+[ Extern ] Froms (file share/libc/stdio.h, line 478)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -763,11 +767,11 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 481)
+[ Extern ] Assigns (file share/libc/stdio.h, line 484)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 481)
+[ Extern ] Froms (file share/libc/stdio.h, line 484)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 481)
+[ Extern ] Froms (file share/libc/stdio.h, line 484)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -778,7 +782,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 486)
+[ Extern ] Froms (file share/libc/stdio.h, line 489)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -787,11 +791,11 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 492)
+[ Extern ] Assigns (file share/libc/stdio.h, line 495)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 492)
+[ Extern ] Froms (file share/libc/stdio.h, line 495)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 493)
+[ Extern ] Froms (file share/libc/stdio.h, line 496)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -800,11 +804,11 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 498)
+[ Extern ] Assigns (file share/libc/stdio.h, line 501)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 498)
+[ Extern ] Froms (file share/libc/stdio.h, line 501)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 499)
+[ Extern ] Froms (file share/libc/stdio.h, line 502)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -813,9 +817,9 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 505)
+[ Extern ] Assigns (file share/libc/stdio.h, line 508)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 505)
+[ Extern ] Froms (file share/libc/stdio.h, line 508)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -826,7 +830,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 511)
+[ Extern ] Froms (file share/libc/stdio.h, line 514)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -837,7 +841,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 517)
+[ Extern ] Froms (file share/libc/stdio.h, line 520)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -848,7 +852,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 523)
+[ Extern ] Froms (file share/libc/stdio.h, line 526)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -859,11 +863,11 @@
[ Extern ] Post-condition 'result_error_or_valid_open_pipe'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 550)
+[ Extern ] Assigns (file share/libc/stdio.h, line 553)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 550)
+[ Extern ] Froms (file share/libc/stdio.h, line 553)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 552)
+[ Extern ] Froms (file share/libc/stdio.h, line 555)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -876,7 +880,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 564)
+[ Extern ] Froms (file share/libc/stdio.h, line 567)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -896,7 +900,7 @@
--- Status Report Summary
--------------------------------------------------------------------------------
74 Completely validated
- 206 Considered valid
+ 208 Considered valid
1 To be validated
- 281 Total
+ 283 Total
--------------------------------------------------------------------------------