From e92445583d7197473a0fa5254cbaa2e39fec4c6f Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 16 Jun 2021 15:47:56 +0200
Subject: [PATCH] [Libc] add specific errno codes in a few function
specifications
---
share/libc/stdio.h | 11 +-
.../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 | 126 +++++++++++-------
tests/libc/oracle/fc_libc.1.res.oracle | 11 +-
tests/rte/oracle/value_rte.res.oracle | 112 +++++++++-------
18 files changed, 171 insertions(+), 119 deletions(-)
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index 69e8f869721..93a5829898c 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -386,6 +386,8 @@ extern int fgetpos(FILE * restrict stream,
assigns *stream \from *stream, indirect:offset, indirect:whence;
assigns \result, __fc_errno \from indirect:*stream, indirect:offset,
indirect:whence;
+ ensures errno_set: __fc_errno \in {EAGAIN, EBADF, EFBIG, EINTR, EINVAL, EIO,
+ ENOSPC, EOVERFLOW, EPIPE, ESPIPE, ENXIO};
*/
extern int fseek(FILE *stream, long int offset, int whence);
@@ -395,17 +397,20 @@ extern int fseek(FILE *stream, long int offset, int whence);
assigns *stream \from *stream, indirect:offset, indirect:whence;
assigns \result, __fc_errno \from indirect:*stream, indirect:offset,
indirect:whence;
+ ensures errno_set: __fc_errno \in {EAGAIN, EBADF, EFBIG, EINTR, EINVAL, EIO,
+ ENOSPC, EOVERFLOW, EPIPE, ESPIPE, ENXIO};
*/
extern int fseeko(FILE *stream, off_t offset, int whence);
/*@
- //missing: assigns errno (EAGAIN, EBADF, EFBIG, EINTR, EIO, ENOSPC, EPIPE,
- // ESPIPE, ENXIO);
requires valid_stream: \valid(stream);
requires valid_pos: \valid_read(pos);
requires initialization:pos: \initialized(pos);
assigns *stream \from *pos;
assigns \result \from indirect:*stream, indirect:*pos;
+ assigns __fc_errno \from __fc_errno, indirect:*stream, indirect:*pos;
+ ensures errno_set: __fc_errno \in {EAGAIN, EBADF, EFBIG, EINTR, EIO,
+ ENOSPC, EPIPE, ESPIPE, ENXIO};
*/
extern int fsetpos(FILE *stream, const fpos_t *pos);
@@ -414,6 +419,7 @@ extern int fsetpos(FILE *stream, const fpos_t *pos);
assigns \result, __fc_errno \from indirect:*stream ;
ensures success_or_error:
\result == -1 || (\result >= 0 && __fc_errno == \old(__fc_errno));
+ ensures errno_set: __fc_errno \in {EBADF, EOVERFLOW, ESPIPE};
*/
extern long int ftell(FILE *stream);
@@ -422,6 +428,7 @@ extern long int ftell(FILE *stream);
assigns \result, __fc_errno \from indirect:*stream ;
ensures success_or_error:
\result == -1 || (\result >= 0 && __fc_errno == \old(__fc_errno));
+ ensures errno_set: __fc_errno \in {EBADF, EOVERFLOW, ESPIPE};
*/
extern off_t ftello(FILE *stream);
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index 42cc5e1f2ad..c4e0b675553 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/erroneous/printf.c:8: Warning: Multiple usage of flag '-'.
[variadic] tests/erroneous/printf.c:8: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 591d9eb02fe..6a3b0b88b1d 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -24,7 +24,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf.c:37:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 3a0595dbf02..f4a8692821d 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_garbled_mix.c:7:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index f41ebdd476a..02785d8ff3d 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_arity.c:8:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
index 90f907e7b0f..94e8f171ee2 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_pointers.c:14:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index cdc57a22aae..96262a87b67 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
@@ -424,7 +424,7 @@ int main(void)
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
index 3eecc8a2862..f32b5df9f60 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf.c:7:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
index 3ea7bd6ac92..972e7931d57 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf_loop.c:6:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
index 2eb005e4216..84a91e7152a 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf_wrong.c:8:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index aeb7aa1c440..3f928d34658 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/snprintf.c:12:
Translating call to snprintf to a call to the specialized version snprintf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index 1c6cbba330c..d1eefe22d5d 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/stdio_print.c:9: Warning:
Call to function fprintf with non-static format argument:
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index e9425f50afe..673cafd33f9 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -12,7 +12,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/stdio_scan.c:10: Warning:
Call to function fscanf with non-static format argument:
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 8205df96d4a..ceed1ffebc1 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -24,7 +24,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/swprintf.c:12:
Translating call to swprintf to a call to the specialized version swprintf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index d04b2860030..c9a23135ec5 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -24,7 +24,7 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:541:
+[variadic] FRAMAC_SHARE/libc/stdio.h:548:
Declaration of variadic function dprintf.
[variadic] tests/known/wchar.c:11:
Translating call to wprintf to a call to the specialized version wprintf_va_1.
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 9f23868dd0d..2596ed249ed 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1920,6 +1920,11 @@
--- Properties of Function 'fseek'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'errno_set'
+ ensures
+ errno_set:
+ __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6}
+ Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/stdio.h, line 386)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
@@ -1945,19 +1950,24 @@
--- Properties of Function 'fseeko'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 395)
+[ Extern ] Post-condition 'errno_set'
+ ensures
+ errno_set:
+ __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6}
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 397)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 395)
+[ Extern ] Froms (file share/libc/stdio.h, line 397)
assigns *stream
\from *stream, (indirect: offset), (indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 396)
+[ Extern ] Froms (file share/libc/stdio.h, line 398)
assigns \result
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 396)
+[ Extern ] Froms (file share/libc/stdio.h, line 398)
assigns __fc_errno
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
@@ -1970,15 +1980,23 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 407)
- assigns *stream, \result;
+[ Extern ] Post-condition 'errno_set'
+ ensures
+ errno_set: __fc_errno ∈ {11, 9, 27, 4, 5, 28, 32, 29, 6}
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 409)
+ assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 407)
+[ Extern ] Froms (file share/libc/stdio.h, line 409)
assigns *stream \from *pos;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 408)
+[ Extern ] Froms (file share/libc/stdio.h, line 410)
assigns \result \from (indirect: *stream), (indirect: *pos);
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 411)
+ assigns __fc_errno
+ \from __fc_errno, (indirect: *stream), (indirect: *pos);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1993,13 +2011,16 @@
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 414)
+[ Extern ] Post-condition 'errno_set'
+ ensures errno_set: __fc_errno ∈ {9, 75, 29}
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 419)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 414)
+[ Extern ] Froms (file share/libc/stdio.h, line 419)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 414)
+[ Extern ] Froms (file share/libc/stdio.h, line 419)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2016,13 +2037,16 @@
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 422)
+[ Extern ] Post-condition 'errno_set'
+ ensures errno_set: __fc_errno ∈ {9, 75, 29}
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 428)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2033,10 +2057,10 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 430)
+[ Extern ] Assigns (file share/libc/stdio.h, line 437)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 430)
+[ Extern ] Froms (file share/libc/stdio.h, line 437)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2047,10 +2071,10 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 436)
+[ Extern ] Assigns (file share/libc/stdio.h, line 443)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 436)
+[ Extern ] Froms (file share/libc/stdio.h, line 443)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2064,7 +2088,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 442)
+[ Extern ] Froms (file share/libc/stdio.h, line 449)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2078,7 +2102,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 448)
+[ Extern ] Froms (file share/libc/stdio.h, line 455)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2089,10 +2113,10 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 454)
+[ Extern ] Assigns (file share/libc/stdio.h, line 461)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 454)
+[ Extern ] Froms (file share/libc/stdio.h, line 461)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2103,10 +2127,10 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 460)
+[ Extern ] Assigns (file share/libc/stdio.h, line 467)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 460)
+[ Extern ] Froms (file share/libc/stdio.h, line 467)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2117,13 +2141,13 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 466)
+[ Extern ] Assigns (file share/libc/stdio.h, line 473)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 466)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
assigns \result \from \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 466)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2137,7 +2161,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 472)
+[ Extern ] Froms (file share/libc/stdio.h, line 479)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2148,10 +2172,10 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 478)
+[ Extern ] Assigns (file share/libc/stdio.h, line 485)
assigns __fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 478)
+[ Extern ] Froms (file share/libc/stdio.h, line 485)
assigns __fc_stdout
\from __fc_errno, *(s + (0 .. strlen{Old}(s)));
Unverifiable but considered Valid.
@@ -2163,13 +2187,13 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 484)
+[ Extern ] Assigns (file share/libc/stdio.h, line 491)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 484)
+[ Extern ] Froms (file share/libc/stdio.h, line 491)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 484)
+[ Extern ] Froms (file share/libc/stdio.h, line 491)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2183,7 +2207,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 489)
+[ Extern ] Froms (file share/libc/stdio.h, line 496)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2194,13 +2218,13 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 495)
+[ Extern ] Assigns (file share/libc/stdio.h, line 502)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 495)
+[ Extern ] Froms (file share/libc/stdio.h, line 502)
assigns *stream \from c;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 496)
+[ Extern ] Froms (file share/libc/stdio.h, line 503)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2211,13 +2235,13 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 501)
+[ Extern ] Assigns (file share/libc/stdio.h, line 508)
assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 501)
+[ Extern ] Froms (file share/libc/stdio.h, line 508)
assigns *__fc_stdout \from c;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 502)
+[ Extern ] Froms (file share/libc/stdio.h, line 509)
assigns \result \from (indirect: *__fc_stdout);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2228,10 +2252,10 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 508)
+[ Extern ] Assigns (file share/libc/stdio.h, line 515)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 508)
+[ Extern ] Froms (file share/libc/stdio.h, line 515)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2245,7 +2269,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 514)
+[ Extern ] Froms (file share/libc/stdio.h, line 521)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2259,7 +2283,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 520)
+[ Extern ] Froms (file share/libc/stdio.h, line 527)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2273,7 +2297,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 526)
+[ Extern ] Froms (file share/libc/stdio.h, line 533)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2291,14 +2315,14 @@
(\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
is_open_pipe(\result))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 553)
+[ Extern ] Assigns (file share/libc/stdio.h, line 560)
assigns \result, __fc_fopen[0 ..];
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 553)
+[ Extern ] Froms (file share/libc/stdio.h, line 560)
assigns \result
\from (indirect: *command), (indirect: *type), __fc_p_fopen;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 555)
+[ Extern ] Froms (file share/libc/stdio.h, line 562)
assigns __fc_fopen[0 ..]
\from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
Unverifiable but considered Valid.
@@ -2316,7 +2340,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 567)
+[ Extern ] Froms (file share/libc/stdio.h, line 574)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4263,7 +4287,7 @@
--------------------------------------------------------------------------------
184 Completely validated
16 Locally validated
- 528 Considered valid
+ 534 Considered valid
56 To be validated
- 784 Total
+ 790 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index c99ba102c79..d091867259e 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4945,6 +4945,8 @@ extern int fgetpos(FILE * restrict stream, fpos_t * restrict pos);
/*@ requires valid_stream: \valid(stream);
requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+ ensures
+ errno_set: __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6};
assigns *stream, \result, __fc_errno;
assigns *stream \from *stream, (indirect: offset), (indirect: whence);
assigns \result
@@ -4956,6 +4958,8 @@ extern int fseek(FILE *stream, long offset, int whence);
/*@ requires valid_stream: \valid(stream);
requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+ ensures
+ errno_set: __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6};
assigns *stream, \result, __fc_errno;
assigns *stream \from *stream, (indirect: offset), (indirect: whence);
assigns \result
@@ -4968,9 +4972,12 @@ extern int fseeko(FILE *stream, off_t offset, int whence);
/*@ requires valid_stream: \valid(stream);
requires valid_pos: \valid_read(pos);
requires initialization: pos: \initialized(pos);
- assigns *stream, \result;
+ ensures errno_set: __fc_errno ∈ {11, 9, 27, 4, 5, 28, 32, 29, 6};
+ assigns *stream, \result, __fc_errno;
assigns *stream \from *pos;
assigns \result \from (indirect: *stream), (indirect: *pos);
+ assigns __fc_errno
+ \from __fc_errno, (indirect: *stream), (indirect: *pos);
*/
extern int fsetpos(FILE *stream, fpos_t const *pos);
@@ -4979,6 +4986,7 @@ extern int fsetpos(FILE *stream, fpos_t const *pos);
success_or_error:
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
+ ensures errno_set: __fc_errno ∈ {9, 75, 29};
assigns \result, __fc_errno;
assigns \result \from (indirect: *stream);
assigns __fc_errno \from (indirect: *stream);
@@ -4990,6 +4998,7 @@ extern long ftell(FILE *stream);
success_or_error:
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
+ ensures errno_set: __fc_errno ∈ {9, 75, 29};
assigns \result, __fc_errno;
assigns \result \from (indirect: *stream);
assigns __fc_errno \from (indirect: *stream);
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 70d52622e99..83a5a5c7b21 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -593,6 +593,8 @@
--- Properties of Function 'fseek'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'errno_set'
+ Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/stdio.h, line 386)
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/stdio.h, line 386)
@@ -608,13 +610,15 @@
--- Properties of Function 'fseeko'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 395)
+[ Extern ] Post-condition 'errno_set'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 397)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 395)
+[ Extern ] Froms (file share/libc/stdio.h, line 397)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 396)
+[ Extern ] Froms (file share/libc/stdio.h, line 398)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 396)
+[ Extern ] Froms (file share/libc/stdio.h, line 398)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -623,11 +627,15 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 407)
+[ Extern ] Post-condition 'errno_set'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 409)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 409)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 407)
+[ Extern ] Froms (file share/libc/stdio.h, line 410)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 408)
+[ Extern ] Froms (file share/libc/stdio.h, line 411)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -638,11 +646,13 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 414)
+[ Extern ] Post-condition 'errno_set'
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 414)
+[ Extern ] Assigns (file share/libc/stdio.h, line 419)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 414)
+[ Extern ] Froms (file share/libc/stdio.h, line 419)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 419)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -653,11 +663,13 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 422)
+[ Extern ] Post-condition 'errno_set'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 428)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 422)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -666,9 +678,9 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 430)
+[ Extern ] Assigns (file share/libc/stdio.h, line 437)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 430)
+[ Extern ] Froms (file share/libc/stdio.h, line 437)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -677,9 +689,9 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 436)
+[ Extern ] Assigns (file share/libc/stdio.h, line 443)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 436)
+[ Extern ] Froms (file share/libc/stdio.h, line 443)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -690,7 +702,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 442)
+[ Extern ] Froms (file share/libc/stdio.h, line 449)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -701,7 +713,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 448)
+[ Extern ] Froms (file share/libc/stdio.h, line 455)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -710,9 +722,9 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 454)
+[ Extern ] Assigns (file share/libc/stdio.h, line 461)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 454)
+[ Extern ] Froms (file share/libc/stdio.h, line 461)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -721,9 +733,9 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 460)
+[ Extern ] Assigns (file share/libc/stdio.h, line 467)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 460)
+[ Extern ] Froms (file share/libc/stdio.h, line 467)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -732,11 +744,11 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 466)
+[ Extern ] Assigns (file share/libc/stdio.h, line 473)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 466)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 466)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -747,7 +759,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 472)
+[ Extern ] Froms (file share/libc/stdio.h, line 479)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -756,9 +768,9 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 478)
+[ Extern ] Assigns (file share/libc/stdio.h, line 485)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 478)
+[ Extern ] Froms (file share/libc/stdio.h, line 485)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -767,11 +779,11 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 484)
+[ Extern ] Assigns (file share/libc/stdio.h, line 491)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 484)
+[ Extern ] Froms (file share/libc/stdio.h, line 491)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 484)
+[ Extern ] Froms (file share/libc/stdio.h, line 491)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -782,7 +794,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 489)
+[ Extern ] Froms (file share/libc/stdio.h, line 496)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -791,11 +803,11 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 495)
+[ Extern ] Assigns (file share/libc/stdio.h, line 502)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 495)
+[ Extern ] Froms (file share/libc/stdio.h, line 502)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 496)
+[ Extern ] Froms (file share/libc/stdio.h, line 503)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -804,11 +816,11 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 501)
+[ Extern ] Assigns (file share/libc/stdio.h, line 508)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 501)
+[ Extern ] Froms (file share/libc/stdio.h, line 508)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 502)
+[ Extern ] Froms (file share/libc/stdio.h, line 509)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -817,9 +829,9 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 508)
+[ Extern ] Assigns (file share/libc/stdio.h, line 515)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 508)
+[ Extern ] Froms (file share/libc/stdio.h, line 515)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -830,7 +842,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 514)
+[ Extern ] Froms (file share/libc/stdio.h, line 521)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -841,7 +853,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 520)
+[ Extern ] Froms (file share/libc/stdio.h, line 527)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -852,7 +864,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 526)
+[ Extern ] Froms (file share/libc/stdio.h, line 533)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -863,11 +875,11 @@
[ Extern ] Post-condition 'result_error_or_valid_open_pipe'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 553)
+[ Extern ] Assigns (file share/libc/stdio.h, line 560)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 553)
+[ Extern ] Froms (file share/libc/stdio.h, line 560)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 555)
+[ Extern ] Froms (file share/libc/stdio.h, line 562)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -880,7 +892,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 567)
+[ Extern ] Froms (file share/libc/stdio.h, line 574)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -900,7 +912,7 @@
--- Status Report Summary
--------------------------------------------------------------------------------
74 Completely validated
- 208 Considered valid
+ 214 Considered valid
1 To be validated
- 283 Total
+ 289 Total
--------------------------------------------------------------------------------
--
GitLab