Merge branch 'feature/andre/libc-ftello-fseeko' into 'master'

[Libc] add specs for ftello/fseeko

See merge request frama-c/frama-c!2366

share/libc/stdio.h

@@ -389,6 +389,15 @@ extern int fgetpos(FILE * restrict stream,
 */
 extern int fseek(FILE *stream, long int offset, int whence);
 
+/*@
+  requires valid_stream: \valid(stream);
+  requires whence_enum: whence == SEEK_SET || whence == SEEK_CUR || whence == SEEK_END;
+  assigns *stream \from *stream, indirect:offset, indirect:whence;
+  assigns \result, __fc_errno \from indirect:*stream, indirect:offset,
+                                    indirect:whence;
+*/
+extern int fseeko(FILE *stream, off_t offset, int whence);
+
 /*@
   requires valid_stream: \valid(stream);
   requires valid_pos: \valid_read(pos);
@@ -397,7 +406,7 @@ extern int fseek(FILE *stream, long int offset, int whence);
 */
 extern int fsetpos(FILE *stream, const fpos_t *pos);
 
-/*@
+/*@ // missing: assigns errno: EBADF, EOVERFLOW, ESPIPE
   requires valid_stream: \valid(stream);
   assigns \result, __fc_errno \from indirect:*stream ;
   ensures success_or_error:
@@ -405,6 +414,14 @@ extern int fsetpos(FILE *stream, const fpos_t *pos);
 */
 extern long int ftell(FILE *stream);
 
+/*@ // missing: assigns errno: EBADF, EOVERFLOW, ESPIPE
+  requires valid_stream: \valid(stream);
+  assigns \result, __fc_errno \from indirect:*stream ;
+  ensures success_or_error:
+    \result == -1 || (\result >= 0 && __fc_errno == \old(__fc_errno));
+*/
+extern off_t ftello(FILE *stream);
+
 /*@
   requires valid_stream: \valid(stream);
   assigns *stream \from \nothing;

src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c

@@ -232,6 +232,11 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
+int __gen_e_acsl_h_short(int s)
+{
+  return s;
+}
+
 int __gen_e_acsl_g_hidden(int x)
 {
   return x;
@@ -379,9 +384,4 @@ int __gen_e_acsl_h_char(int c)
   return c;
 }
 
-int __gen_e_acsl_h_short(int s)
-{
-  return s;
-}
-
 

src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c

@@ -277,6 +277,11 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
+int __gen_e_acsl_h_short(int s)
+{
+  return s;
+}
+
 int __gen_e_acsl_g_hidden(int x)
 {
   return x;
@@ -472,9 +477,4 @@ int __gen_e_acsl_h_char(int c)
   return c;
 }
 
-int __gen_e_acsl_h_short(int s)
-{
-  return s;
-}
-
 

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   Declaration of variadic function dprintf.
 [variadic] tests/erroneous/printf.c:8: Warning: Multiple usage of flag '-'.
 [variadic] tests/erroneous/printf.c:8: Warning: 

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf.c:37: 
   Translating call to printf to a call to the specialized version printf_va_1.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf_garbled_mix.c:8: 
   Variadic builtin Frama_C_show_each_nb_printed left untransformed.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/stdio_print.c:9: Warning: 
   Call to function fprintf with non-static format argument:

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/stdio_scan.c:10: Warning: 
   Call to function fscanf with non-static format argument:

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

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:521: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:538: 
   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.

tests/idct/oracle/ieee_1180_1990.res.oracle

@@ -1938,14 +1938,39 @@
             default behavior
             by Frama-C kernel.
 
+--------------------------------------------------------------------------------
+--- Properties of Function 'fseeko'
+--------------------------------------------------------------------------------
+
+[ Extern  ] Assigns (file share/libc/stdio.h, line 395)
+            assigns *stream, \result, __fc_errno;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 395)
+            assigns *stream
+              \from *stream, (indirect: offset), (indirect: whence);
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 396)
+            assigns \result
+              \from (indirect: *stream), (indirect: offset),
+                    (indirect: whence);
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 396)
+            assigns __fc_errno
+              \from (indirect: *stream), (indirect: offset),
+                    (indirect: whence);
+            Unverifiable but considered Valid.
+[  Valid  ] Default behavior
+            default behavior
+            by Frama-C kernel.
+
 --------------------------------------------------------------------------------
 --- Properties of Function 'fsetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 396)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 405)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 396)
+[ Extern  ] Froms (file share/libc/stdio.h, line 405)
             assigns *stream \from *pos;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1962,13 +1987,36 @@
               \result ≡ -1 ∨
               (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 402)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 411)
             assigns \result, __fc_errno;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 402)
+[ Extern  ] Froms (file share/libc/stdio.h, line 411)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 402)
+[ Extern  ] Froms (file share/libc/stdio.h, line 411)
+            assigns __fc_errno \from (indirect: *stream);
+            Unverifiable but considered Valid.
+[  Valid  ] Default behavior
+            default behavior
+            by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'ftello'
+--------------------------------------------------------------------------------
+
+[ Extern  ] Post-condition 'success_or_error'
+            ensures
+            success_or_error:
+              \result ≡ -1 ∨
+              (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
+            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 419)
+            assigns \result \from (indirect: *stream);
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 419)
             assigns __fc_errno \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1979,10 +2027,10 @@
 --- Properties of Function 'rewind'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 410)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 427)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 410)
+[ Extern  ] Froms (file share/libc/stdio.h, line 427)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1993,10 +2041,10 @@
 --- Properties of Function 'clearerr'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 416)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 433)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 416)
+[ Extern  ] Froms (file share/libc/stdio.h, line 433)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2010,7 +2058,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 422)
+[ Extern  ] Froms (file share/libc/stdio.h, line 439)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2024,7 +2072,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 428)
+[ Extern  ] Froms (file share/libc/stdio.h, line 445)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2035,10 +2083,10 @@
 --- Properties of Function 'flockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 434)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 451)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 434)
+[ Extern  ] Froms (file share/libc/stdio.h, line 451)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2049,10 +2097,10 @@
 --- Properties of Function 'funlockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 440)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 457)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 440)
+[ Extern  ] Froms (file share/libc/stdio.h, line 457)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2063,13 +2111,13 @@
 --- Properties of Function 'ftrylockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 446)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 463)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 446)
+[ Extern  ] Froms (file share/libc/stdio.h, line 463)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 446)
+[ Extern  ] Froms (file share/libc/stdio.h, line 463)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2083,7 +2131,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 452)
+[ Extern  ] Froms (file share/libc/stdio.h, line 469)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2094,10 +2142,10 @@
 --- Properties of Function 'perror'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 458)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 475)
             assigns __fc_stdout;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 458)
+[ Extern  ] Froms (file share/libc/stdio.h, line 475)
             assigns __fc_stdout
               \from __fc_errno, *(s + (0 .. strlen{Old}(s)));
             Unverifiable but considered Valid.
@@ -2109,13 +2157,13 @@
 --- Properties of Function 'getc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 464)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 481)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 464)
+[ Extern  ] Froms (file share/libc/stdio.h, line 481)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 464)
+[ Extern  ] Froms (file share/libc/stdio.h, line 481)
             assigns *stream \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2129,7 +2177,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 486)
             assigns \result \from *__fc_stdin;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2140,13 +2188,13 @@
 --- Properties of Function 'putc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 475)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 492)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 475)
+[ Extern  ] Froms (file share/libc/stdio.h, line 492)
             assigns *stream \from c;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 476)
+[ Extern  ] Froms (file share/libc/stdio.h, line 493)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2157,13 +2205,13 @@
 --- Properties of Function 'putchar_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 481)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 498)
             assigns *__fc_stdout, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 481)
+[ Extern  ] Froms (file share/libc/stdio.h, line 498)
             assigns *__fc_stdout \from c;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 482)
+[ Extern  ] Froms (file share/libc/stdio.h, line 499)
             assigns \result \from (indirect: *__fc_stdout);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2174,10 +2222,10 @@
 --- Properties of Function 'clearerr_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 488)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 505)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 488)
+[ Extern  ] Froms (file share/libc/stdio.h, line 505)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2191,7 +2239,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 494)
+[ Extern  ] Froms (file share/libc/stdio.h, line 511)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2205,7 +2253,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 500)
+[ Extern  ] Froms (file share/libc/stdio.h, line 517)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2219,7 +2267,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 506)
+[ Extern  ] Froms (file share/libc/stdio.h, line 523)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2237,14 +2285,14 @@
               (\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
                is_open_pipe(\result))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 533)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 550)
             assigns \result, __fc_fopen[0 ..];
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 533)
+[ Extern  ] Froms (file share/libc/stdio.h, line 550)
             assigns \result
               \from (indirect: *command), (indirect: *type), __fc_p_fopen;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 535)
+[ Extern  ] Froms (file share/libc/stdio.h, line 552)
             assigns __fc_fopen[0 ..]
               \from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
             Unverifiable but considered Valid.
@@ -2262,7 +2310,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 547)
+[ Extern  ] Froms (file share/libc/stdio.h, line 564)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -4058,9 +4106,9 @@
 --------------------------------------------------------------------------------
 --- Status Report Summary
 --------------------------------------------------------------------------------
-   179 Completely validated
+   181 Completely validated
     16 Locally validated
-   486 Considered valid
+   494 Considered valid
     56 To be validated
-   737 Total
+   747 Total
 --------------------------------------------------------------------------------

tests/libc/oracle/fc_libc.0.res.oracle

@@ -40,7 +40,7 @@
    unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
    wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call); 
   
-  Undefined functions (395)
+  Undefined functions (397)
   =========================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -91,9 +91,9 @@
    flockfile (0 call); floor (0 call); floorf (0 call); floorl (0 call);
    fmod (0 call); fmodf (0 call); fopen (0 call); fork (0 call);
    fputc (0 call); fputs (0 call); fread (0 call); free (1 call);
-   freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
-   ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
-   fwrite (0 call); gai_strerror (0 call); getc (0 call);
+   freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fseeko (0 call);
+   fsetpos (0 call); ftell (0 call); ftello (0 call); ftrylockfile (0 call);
+   funlockfile (0 call); fwrite (0 call); gai_strerror (0 call); getc (0 call);
    getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
    getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
    gethostname (0 call); getitimer (0 call); getopt (0 call);
@@ -181,7 +181,7 @@
   Goto = 89
   Assignment = 438
   Exit point = 82
-  Function = 477
+  Function = 479
   Function call = 89
   Pointer dereferencing = 158
   Cyclomatic complexity = 286

tests/libc/oracle/fc_libc.1.res.oracle

@@ -4811,6 +4811,17 @@ extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos);
  */
 extern int fseek(FILE *stream, long offset, int whence);
 
+/*@ requires valid_stream: \valid(stream);
+    requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+    assigns *stream, \result, __fc_errno;
+    assigns *stream \from *stream, (indirect: offset), (indirect: whence);
+    assigns \result
+      \from (indirect: *stream), (indirect: offset), (indirect: whence);
+    assigns __fc_errno
+      \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ */
+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);
@@ -4830,6 +4841,17 @@ extern int fsetpos(FILE *stream, fpos_t const *pos);
  */
 extern long ftell(FILE *stream);
 
+/*@ requires valid_stream: \valid(stream);
+    ensures
+      success_or_error:
+        \result ≡ -1 ∨
+        (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
+    assigns \result, __fc_errno;
+    assigns \result \from (indirect: *stream);
+    assigns __fc_errno \from (indirect: *stream);
+ */
+extern off_t ftello(FILE *stream);
+
 /*@ requires valid_stream: \valid(stream);
     assigns *stream;
     assigns *stream \from \nothing;