From f93dc3a8d82e8c1c5e12d6525d7a20c2bbfde127 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 30 Aug 2019 17:58:44 +0200
Subject: [PATCH] [Libc] add specs for ftello/fseeko
---
share/libc/stdio.h | 19 ++-
.../tests/arith/oracle_ci/gen_functions.c | 10 +-
.../tests/gmp-only/oracle_ci/gen_functions.c | 10 +-
.../tests/erroneous/oracle/printf.res.oracle | 2 +-
.../tests/known/oracle/printf.res.oracle | 2 +-
.../oracle/printf_garbled_mix.res.oracle | 2 +-
.../oracle/printf_wrong_arity.res.oracle | 2 +-
.../oracle/printf_wrong_pointers.res.oracle | 2 +-
.../oracle/printf_wrong_types.res.oracle | 4 +-
.../tests/known/oracle/scanf.res.oracle | 2 +-
.../tests/known/oracle/scanf_loop.res.oracle | 2 +-
.../tests/known/oracle/scanf_wrong.res.oracle | 2 +-
.../tests/known/oracle/snprintf.res.oracle | 2 +-
.../tests/known/oracle/stdio_print.res.oracle | 2 +-
.../tests/known/oracle/stdio_scan.res.oracle | 2 +-
.../tests/known/oracle/swprintf.res.oracle | 2 +-
.../tests/known/oracle/wchar.res.oracle | 2 +-
tests/idct/oracle/ieee_1180_1990.res.oracle | 134 ++++++++++++------
tests/libc/oracle/fc_libc.0.res.oracle | 10 +-
tests/libc/oracle/fc_libc.1.res.oracle | 22 +++
tests/libc/oracle/stdio_h.res.oracle | 56 +++++---
tests/libc/stdio_h.c | 3 +
tests/metrics/oracle/libc.1.res.oracle | 34 ++---
tests/rte/oracle/value_rte.res.oracle | 116 +++++++++------
24 files changed, 293 insertions(+), 151 deletions(-)
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index c0dd5448ba9..c3fa3488a76 100644
--- a/share/libc/stdio.h
+++ b/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;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index 457ff5d2aa2..42381d641e8 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/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;
-}
-
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index f7f9708c3cc..2bdf4cd9f28 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/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;
-}
-
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index ebb217fac02..bf32832912e 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: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:
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index f04b44a2b44..d7102dda0aa 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: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.
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 545c7824113..e7591173023 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: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.
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 d7f8115fec3..4ee27be4661 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: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.
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 48af02448ee..2c72bbbab04 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: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.
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 b720645e934..5d41306e7d7 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: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.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
index cd8ae9652f3..bf4a9d81548 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: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.
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 db959e60948..e563ba2f274 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: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.
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 b468aea8aca..704b3de7532 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: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.
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index 2b2dd3e7684..cecc5cc5431 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: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.
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 0cacefc0330..cc3c40be6d6 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: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:
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 671f5bf3f35..f157c9d36bf 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: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:
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 79025ff0d26..585983473b2 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: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.
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index 0e93065e23f..b85bb1c1d06 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: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.
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 73d8292ef2d..6019d52b697 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/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
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 413b1aee0f0..f0d8a56d9da 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/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
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 34abdcbb6ed..c4e0a539a60 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/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;
diff --git a/tests/libc/oracle/stdio_h.res.oracle b/tests/libc/oracle/stdio_h.res.oracle
index 8262aa6c408..e839ecd549f 100644
--- a/tests/libc/oracle/stdio_h.res.oracle
+++ b/tests/libc/oracle/stdio_h.res.oracle
@@ -51,47 +51,67 @@
[eva] tests/libc/stdio_h.c:25:
function fseek: precondition 'whence_enum' got status valid.
[eva] Done for function fseek
-[eva] computing for function fclose <- main.
+[eva] computing for function fseeko <- main.
Called from tests/libc/stdio_h.c:26.
-[eva] using specification for function fclose
+[eva] using specification for function fseeko
+[eva] tests/libc/stdio_h.c:26:
+ function fseeko: precondition 'valid_stream' got status valid.
[eva] tests/libc/stdio_h.c:26:
+ function fseeko: precondition 'whence_enum' got status valid.
+[eva] Done for function fseeko
+[eva] computing for function ftell <- main.
+ Called from tests/libc/stdio_h.c:27.
+[eva] using specification for function ftell
+[eva] tests/libc/stdio_h.c:27:
+ function ftell: precondition 'valid_stream' got status valid.
+[eva] Done for function ftell
+[eva] computing for function ftello <- main.
+ Called from tests/libc/stdio_h.c:28.
+[eva] using specification for function ftello
+[eva] tests/libc/stdio_h.c:28:
+ function ftello: precondition 'valid_stream' got status valid.
+[eva] Done for function ftello
+[eva] computing for function fclose <- main.
+ Called from tests/libc/stdio_h.c:29.
+[eva] using specification for function fclose
+[eva] tests/libc/stdio_h.c:29:
function fclose: precondition 'valid_stream' got status valid.
[eva] Done for function fclose
[eva] computing for function freopen <- main.
- Called from tests/libc/stdio_h.c:28.
+ Called from tests/libc/stdio_h.c:31.
[eva] using specification for function freopen
-[eva] tests/libc/stdio_h.c:28:
+[eva] tests/libc/stdio_h.c:31:
function freopen: precondition 'valid_filename' got status valid.
-[eva] tests/libc/stdio_h.c:28:
+[eva] tests/libc/stdio_h.c:31:
function freopen: precondition 'valid_mode' got status valid.
-[eva:alarm] tests/libc/stdio_h.c:28: Warning:
+[eva:alarm] tests/libc/stdio_h.c:31: Warning:
function freopen: precondition 'valid_stream' got status unknown.
[eva] Done for function freopen
[eva] computing for function printf_va_1 <- main.
- Called from tests/libc/stdio_h.c:30.
+ Called from tests/libc/stdio_h.c:33.
[eva] using specification for function printf_va_1
-[eva] tests/libc/stdio_h.c:30:
+[eva] tests/libc/stdio_h.c:33:
function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] computing for function fclose <- main.
- Called from tests/libc/stdio_h.c:31.
-[eva] tests/libc/stdio_h.c:31:
+ Called from tests/libc/stdio_h.c:34.
+[eva] tests/libc/stdio_h.c:34:
function fclose: precondition 'valid_stream' got status valid.
[eva] Done for function fclose
[eva] computing for function fgets <- main.
- Called from tests/libc/stdio_h.c:34.
+ Called from tests/libc/stdio_h.c:37.
[eva] using specification for function fgets
-[eva] tests/libc/stdio_h.c:34:
+[eva] tests/libc/stdio_h.c:37:
function fgets: precondition 'valid_stream' got status valid.
-[eva] tests/libc/stdio_h.c:34:
+[eva] tests/libc/stdio_h.c:37:
function fgets: precondition 'room_s' got status valid.
[eva] Done for function fgets
-[eva:alarm] tests/libc/stdio_h.c:36: Warning: check got status unknown.
+[eva:alarm] tests/libc/stdio_h.c:39: Warning: check got status unknown.
[eva] computing for function fgets <- main.
- Called from tests/libc/stdio_h.c:38.
-[eva] tests/libc/stdio_h.c:38:
+ Called from tests/libc/stdio_h.c:41.
+[eva] tests/libc/stdio_h.c:41:
function fgets: precondition 'valid_stream' got status valid.
-[eva:alarm] tests/libc/stdio_h.c:38: Warning:
+[eva:alarm] tests/libc/stdio_h.c:41: Warning:
function fgets: precondition 'room_s' got status invalid.
[eva] Done for function fgets
[eva] Recording results for main
@@ -104,6 +124,8 @@
f ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
r ∈ [--..--]
tmp_2 ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
+ told ∈ [-1..2147483647]
+ toldo ∈ [-1..2147483647]
redirected ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
fgets_buf0[0] ∈ [--..--] or UNINITIALIZED
fgets_res ∈ {{ NULL ; &fgets_buf0[0] }}
diff --git a/tests/libc/stdio_h.c b/tests/libc/stdio_h.c
index a1d6f3fa161..1150500b6cb 100644
--- a/tests/libc/stdio_h.c
+++ b/tests/libc/stdio_h.c
@@ -23,6 +23,9 @@ int main() {
FILE *tmp = tmpfile();
if (!tmp) return 2;
fseek(tmp, 0L, SEEK_SET);
+ fseeko(tmp, 0, SEEK_SET);
+ long told = ftell(tmp);
+ off_t toldo = ftello(tmp);
fclose(tmp);
FILE *redirected = freopen("/tmp/mytmp.txt", "w+", stdout);
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index 24cfd8d35b1..b00598fd71a 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -4,7 +4,7 @@
bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call);
getopt (1 call); main (0 call);
- Undefined functions (120)
+ Undefined functions (122)
=========================
_exit (0 call); access (0 call); chdir (0 call); chown (0 call);
chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
@@ -15,20 +15,20 @@
fflush (0 call); fgetc (0 call); fgetpos (0 call); fgets (0 call);
fileno (0 call); fileno_unlocked (0 call); flockfile (0 call);
fopen (0 call); fork (0 call); fputc (0 call); fputs (0 call);
- fread (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
- ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
- fwrite (0 call); getc (0 call); getc_unlocked (0 call); getchar (1 call);
- getchar_unlocked (0 call); getcwd (0 call); getegid (0 call);
- geteuid (0 call); getgid (0 call); gethostname (0 call);
- getopt_long (0 call); getopt_long_only (0 call); getpgid (0 call);
- getpgrp (0 call); getpid (0 call); getppid (0 call); getresgid (0 call);
- getresuid (0 call); gets (0 call); getsid (0 call); getuid (0 call);
- isalnum (0 call); isalpha (1 call); isascii (0 call); isatty (0 call);
- isblank (1 call); iscntrl (0 call); isdigit (0 call); isgraph (0 call);
- islower (0 call); isprint (0 call); ispunct (0 call); isspace (0 call);
- isupper (0 call); isxdigit (0 call); lseek (0 call); pathconf (0 call);
- pclose (0 call); perror (0 call); pipe (0 call); popen (0 call);
- putc (0 call); putc_unlocked (0 call); putchar (0 call);
+ fread (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); getc (0 call);
+ getc_unlocked (0 call); getchar (1 call); getchar_unlocked (0 call);
+ getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
+ gethostname (0 call); getopt_long (0 call); getopt_long_only (0 call);
+ getpgid (0 call); getpgrp (0 call); getpid (0 call); getppid (0 call);
+ getresgid (0 call); getresuid (0 call); gets (0 call); getsid (0 call);
+ getuid (0 call); isalnum (0 call); isalpha (1 call); isascii (0 call);
+ isatty (0 call); isblank (1 call); iscntrl (0 call); isdigit (0 call);
+ isgraph (0 call); islower (0 call); isprint (0 call); ispunct (0 call);
+ isspace (0 call); isupper (0 call); isxdigit (0 call); lseek (0 call);
+ pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
+ popen (0 call); putc (0 call); putc_unlocked (0 call); putchar (0 call);
putchar_unlocked (0 call); puts (0 call); read (0 call); remove (0 call);
rename (0 call); rewind (0 call); setbuf (0 call); setegid (0 call);
seteuid (0 call); setgid (0 call); sethostname (0 call); setpgid (0 call);
@@ -59,7 +59,7 @@
Goto = 0
Assignment = 8
Exit point = 6
- Function = 126
+ Function = 128
Function call = 7
Pointer dereferencing = 1
Cyclomatic complexity = 6
@@ -87,7 +87,7 @@
----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 7 (out of 126)
+ Syntactically reachable functions = 7 (out of 128)
Semantically reached functions = 7
Coverage estimation = 100.0%
[metrics] References to non-analyzed functions
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 2cf4947a7f1..1fa05cbf8c6 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -603,13 +603,28 @@
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'fsetpos'
+--- Properties of Function 'fseeko'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 396)
+[ Extern ] Assigns (file share/libc/stdio.h, line 395)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 395)
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/stdio.h, line 396)
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 396)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'fsetpos'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns (file share/libc/stdio.h, line 405)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 405)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -619,11 +634,26 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 402)
+[ Extern ] Assigns (file share/libc/stdio.h, line 411)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 402)
+[ Extern ] Froms (file share/libc/stdio.h, line 411)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 402)
+[ Extern ] Froms (file share/libc/stdio.h, line 411)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'ftello'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'success_or_error'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 419)
+ Unverifiable but considered Valid.
+[ 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.
@@ -632,9 +662,9 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 410)
+[ Extern ] Assigns (file share/libc/stdio.h, line 427)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 410)
+[ Extern ] Froms (file share/libc/stdio.h, line 427)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -643,9 +673,9 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 416)
+[ Extern ] Assigns (file share/libc/stdio.h, line 433)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 416)
+[ Extern ] Froms (file share/libc/stdio.h, line 433)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -656,7 +686,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 439)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -667,7 +697,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 428)
+[ Extern ] Froms (file share/libc/stdio.h, line 445)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -676,9 +706,9 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 434)
+[ Extern ] Assigns (file share/libc/stdio.h, line 451)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 434)
+[ Extern ] Froms (file share/libc/stdio.h, line 451)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -687,9 +717,9 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 440)
+[ Extern ] Assigns (file share/libc/stdio.h, line 457)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 440)
+[ Extern ] Froms (file share/libc/stdio.h, line 457)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -698,11 +728,11 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 446)
+[ Extern ] Assigns (file share/libc/stdio.h, line 463)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 446)
+[ Extern ] Froms (file share/libc/stdio.h, line 463)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 446)
+[ Extern ] Froms (file share/libc/stdio.h, line 463)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -713,7 +743,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 452)
+[ Extern ] Froms (file share/libc/stdio.h, line 469)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -722,9 +752,9 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 458)
+[ Extern ] Assigns (file share/libc/stdio.h, line 475)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 458)
+[ Extern ] Froms (file share/libc/stdio.h, line 475)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -733,11 +763,11 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 464)
+[ Extern ] Assigns (file share/libc/stdio.h, line 481)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 464)
+[ Extern ] Froms (file share/libc/stdio.h, line 481)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 464)
+[ Extern ] Froms (file share/libc/stdio.h, line 481)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -748,7 +778,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 486)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -757,11 +787,11 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 475)
+[ Extern ] Assigns (file share/libc/stdio.h, line 492)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 475)
+[ Extern ] Froms (file share/libc/stdio.h, line 492)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 476)
+[ Extern ] Froms (file share/libc/stdio.h, line 493)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -770,11 +800,11 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 481)
+[ Extern ] Assigns (file share/libc/stdio.h, line 498)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 481)
+[ Extern ] Froms (file share/libc/stdio.h, line 498)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 482)
+[ Extern ] Froms (file share/libc/stdio.h, line 499)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -783,9 +813,9 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 488)
+[ Extern ] Assigns (file share/libc/stdio.h, line 505)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 488)
+[ Extern ] Froms (file share/libc/stdio.h, line 505)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -796,7 +826,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 494)
+[ Extern ] Froms (file share/libc/stdio.h, line 511)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -807,7 +837,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 500)
+[ Extern ] Froms (file share/libc/stdio.h, line 517)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -818,7 +848,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 506)
+[ Extern ] Froms (file share/libc/stdio.h, line 523)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -829,11 +859,11 @@
[ Extern ] Post-condition 'result_error_or_valid_open_pipe'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 533)
+[ Extern ] Assigns (file share/libc/stdio.h, line 550)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 533)
+[ Extern ] Froms (file share/libc/stdio.h, line 550)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 535)
+[ Extern ] Froms (file share/libc/stdio.h, line 552)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -846,7 +876,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 547)
+[ Extern ] Froms (file share/libc/stdio.h, line 564)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -865,8 +895,8 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 72 Completely validated
- 198 Considered valid
+ 74 Completely validated
+ 206 Considered valid
1 To be validated
- 271 Total
+ 281 Total
--------------------------------------------------------------------------------
--
GitLab