From 548d249aa00f9c76d2db76696b56215f143b5bb4 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 30 Sep 2020 12:22:36 +0200
Subject: [PATCH] [Libc] fix specs of fgetpos and fsetpos
---
share/libc/stdio.h | 9 +-
.../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 | 106 +++++++++---------
tests/libc/oracle/fc_libc.1.res.oracle | 9 +-
tests/libc/oracle/stdio_h.res.oracle | 25 +++++
tests/libc/stdio_h.c | 5 +
tests/rte/oracle/value_rte.res.oracle | 96 ++++++++--------
20 files changed, 162 insertions(+), 118 deletions(-)
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index c3fa3488a76..fe7f34f40a9 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 bf32832912e..42cc5e1f2ad 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 d7102dda0aa..466df2fb14f 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 e7591173023..18e29885565 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 4ee27be4661..fb8aff5b501 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 2c72bbbab04..d08481ad5e2 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 5d41306e7d7..d9fbae7e5f8 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 bf4a9d81548..8e0fee8c8c6 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 e563ba2f274..84e1b114610 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 704b3de7532..2ae6ce88bc3 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 cecc5cc5431..eff15618464 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 cc3c40be6d6..7952572f5ec 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 f157c9d36bf..841afb45a4b 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 585983473b2..5efd248eb0b 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 b85bb1c1d06..05cd9a214e2 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 c3f8b8d2b91..ee5c88ae7ff 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 981e7bf9215..36e9390d1b2 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 e839ecd549f..3a64229e0e6 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 1150500b6cb..19531ca2e40 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 1fa05cbf8c6..42a86c5e8f0 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
--------------------------------------------------------------------------------
--
GitLab