diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index c33a599cc6a5be7e989d98a9fb6268d50fe6d072..f17604ecd8bd63fd5c60dcbc78ba3f881fbe0de7 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 cf2ce359ad051f41fb7a8144456c48f3ba162a7f..10dd20d3d4aab0753980a088b7cfaeb2eb638a95 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -10,21 +10,21 @@
Declaration of variadic function fwscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 25e8c3610196c5963f1c9e911eb1e8f829319bfe..6f4e577c033a7b540636a76393835e057996ec18 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
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 96287d6d468ea3815206a73c3e4595685e794299..c521f9b6e1df5649fb3d1df3c55f30a9bc595ee9 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
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 1830a1983da84f82418e69a71b2efb0c3d288aea..3d1a8179fdb9d308a4045d06d249fe7dc092aa80 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
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 5e1783c24206b61b139ddbdf83738a710f416f66..2e05f03059b0019feafc95d8b72ee55ae04dbca6 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
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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.
@@ -410,21 +410,21 @@ int main(void)
}
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 c17cd35b1db426762475e22683b67d5642322df7..1e9108fb2f45ec63c4be5fcfb26e2e7a6c307b14 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 dc4f5f5056b7a506d36065e972d4bae7f15b2bed..c1dca1139d60fde19acc48315f97e092799d84b4 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 01d07d14edca771660ecc911e471607621e0a323..0759f0aaf693ad80a837dd9f5a15ba4f3c0089aa 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 b5123404c1c521e1cdb3c842124c7f6be08fdacc..38179fb9489837b05fc033be954e08bb89a9670f 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 f6082cc06eddc1ec8fd7e81cbb3d66be38349fad..425efedf60e4b4453903454646cdd7ca5a1b7ea3 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 7d4b64672ebf65221f4cbcffeca8202eceb82b9f..a5c8be576800630f398bec54d44bd2ee5adb3a70 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 ff34f6beb5cfd87e523c1f71f5c2e697af1685eb..18c89dfdb6652e57d476d864d13aa28d45058338 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -10,21 +10,21 @@
Declaration of variadic function fwscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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 ad8320c3cca852be30d2b0ff8fe5a13e1a3e0a98..abfecedc1a5423f82d3105c738944ddd50d89c6a 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -10,21 +10,21 @@
Declaration of variadic function fwscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:205:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:210:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:439:
+[variadic] FRAMAC_SHARE/libc/stdio.h:519:
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/builtins/oracle/linked_list.0.res.oracle b/tests/builtins/oracle/linked_list.0.res.oracle
index a720cea4364ad8be5ec34cc894fc4c0c6c6b63a0..7edb0dc61aa38f4ca9fa5dd58d0b5404bc3a30ec 100644
--- a/tests/builtins/oracle/linked_list.0.res.oracle
+++ b/tests/builtins/oracle/linked_list.0.res.oracle
@@ -15,6 +15,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -55,6 +57,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -91,6 +95,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -130,6 +136,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -168,6 +176,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -210,6 +220,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -250,6 +262,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -294,6 +308,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -336,6 +352,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -382,6 +400,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -426,6 +446,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -474,6 +496,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -765,6 +789,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -1058,6 +1084,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index 67b3d10651f9e9d8f7d950db2f0cc401ee64c0bf..58a095a29ca9923f3349863a3f663a973737095e 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -15,6 +15,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -55,6 +57,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -91,6 +95,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -130,6 +136,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -168,6 +176,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -210,6 +220,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -250,6 +262,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -294,6 +308,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -336,6 +352,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -382,6 +400,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -427,6 +447,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -476,6 +498,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -519,6 +543,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -560,6 +586,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
diff --git a/tests/builtins/oracle/linked_list.2.res.oracle b/tests/builtins/oracle/linked_list.2.res.oracle
index 4687366532f8f130442769db11f45930b3d4ec6e..b893ef1a658089db5f2be138b4391460dc1624ea 100644
--- a/tests/builtins/oracle/linked_list.2.res.oracle
+++ b/tests/builtins/oracle/linked_list.2.res.oracle
@@ -15,6 +15,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -55,6 +57,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -90,6 +94,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -129,6 +135,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -167,6 +175,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -209,6 +219,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -249,6 +261,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -293,6 +307,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -335,6 +351,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -381,6 +399,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -425,6 +445,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -473,6 +495,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -519,6 +543,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -569,6 +595,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -617,6 +645,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -669,6 +699,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -719,6 +751,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -773,6 +807,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -825,6 +861,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -881,6 +919,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 7dff010c2ccf5ba38a23b37e5d80e80143973836..81abf155c213717183c80821298706fa0fe68aae 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1276,9 +1276,16 @@
--- Properties of Function 'remove'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'result_ok_or_error'
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 76)
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename))));
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1287,9 +1294,17 @@
--- Properties of Function 'rename'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'result_ok_or_error'
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 85)
+ assigns \result
+ \from (indirect: *(old_name + (0 .. strlen{Old}(old_name)))),
+ (indirect: *(new_name + (0 .. strlen{Old}(new_name))));
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1307,7 +1322,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 80)
+[ Extern ] Froms (file share/libc/stdio.h, line 95)
assigns \result \from __fc_p_fopen;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1318,14 +1333,26 @@
--- Properties of Function 'tmpnam'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 87)
- assigns \result, *(s + (..));
+[ Extern ] Post-condition 'result_string_or_null'
+ ensures
+ result_string_or_null:
+ \result ≡ \null ∨ \result ≡ \old(s) ∨
+ \result ≡ __fc_p_tmpnam
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 108)
+ assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)),
+ \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 108)
+ assigns *(__fc_p_tmpnam + (0 .. 2048))
+ \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 87)
- assigns \result \from *(s + (..));
+[ Extern ] Froms (file share/libc/stdio.h, line 110)
+ assigns *(s + (0 .. 2048))
+ \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 88)
- assigns *(s + (..)) \from \nothing;
+[ Extern ] Froms (file share/libc/stdio.h, line 111)
+ assigns \result \from s, __fc_p_tmpnam;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1341,8 +1368,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 95)
- assigns \result \from stream, stream->__fc_FILE_id;
+[ Extern ] Froms (file share/libc/stdio.h, line 120)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1355,15 +1382,47 @@
[ Extern ] Post-condition 'result_zero_or_EOF'
ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1
Unverifiable but considered Valid.
-[ Extern ] Assigns nothing
- assigns \nothing;
+[ Extern ] Assigns (file share/libc/stdio.h, line 129)
+ assigns \result, *stream, __fc_fopen[0 .. 16 - 1];
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'flush_all' (file share/libc/stdio.h, line 135)
+ assigns __fc_fopen[0 .. 16 - 1], \result;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'flush_stream' (file share/libc/stdio.h, line 140)
+ assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 103)
- assigns \result \from stream, stream->__fc_FILE_id;
+[ Extern ] Froms (file share/libc/stdio.h, line 129)
+ assigns \result \from (indirect: *stream);
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 130)
+ assigns *stream
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 130)
+ assigns __fc_fopen[0 .. 16 - 1]
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_all' (file share/libc/stdio.h, line 135)
+ assigns __fc_fopen[0 .. 16 - 1] \from __fc_fopen[0 .. 16 - 1];
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_all' (file share/libc/stdio.h, line 137)
+ assigns \result \from (indirect: __fc_fopen[0 .. 16 - 1]);
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_stream' (file share/libc/stdio.h, line 140)
+ assigns *stream \from *stream;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_stream' (file share/libc/stdio.h, line 141)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'flush_all'
+ behavior flush_all
+ by Frama-C kernel.
+[ Valid ] Behavior 'flush_stream'
+ behavior flush_stream
+ by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'fopen'
@@ -1378,10 +1437,11 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 112)
+[ Extern ] Froms (file share/libc/stdio.h, line 150)
assigns \result
- \from (indirect: *(filename + (..))),
- (indirect: *(mode + (..))), __fc_p_fopen;
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))),
+ __fc_p_fopen;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1397,17 +1457,19 @@
\result ≡ \null ∨
\subset(\result, &__fc_fopen[0 .. 16 - 1])
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 121)
+[ Extern ] Assigns (file share/libc/stdio.h, line 160)
assigns \result, __fc_fopen[fd];
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 121)
+[ Extern ] Froms (file share/libc/stdio.h, line 160)
assigns \result
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ \from (indirect: fd),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))),
(indirect: __fc_fopen[fd]), __fc_p_fopen;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 121)
+[ Extern ] Froms (file share/libc/stdio.h, line 160)
assigns __fc_fopen[fd]
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ \from (indirect: fd),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))),
(indirect: __fc_fopen[fd]), __fc_p_fopen;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1426,16 +1488,16 @@
[ Extern ] Post-condition 'stream_opened'
ensures stream_opened: *\old(stream) ∈ __fc_fopen[0 .. 16 - 1]
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 132)
+[ Extern ] Assigns (file share/libc/stdio.h, line 172)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 132)
+[ Extern ] Froms (file share/libc/stdio.h, line 172)
assigns \result
\from (indirect: *(filename + (..))),
(indirect: *(mode + (..))), __fc_p_fopen,
(indirect: stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 134)
+[ Extern ] Froms (file share/libc/stdio.h, line 174)
assigns *stream
\from (indirect: *(filename + (..))),
(indirect: *(mode + (..))), __fc_p_fopen,
@@ -1449,10 +1511,10 @@
--- Properties of Function 'setbuf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 145)
+[ Extern ] Assigns (file share/libc/stdio.h, line 185)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 145)
+[ Extern ] Froms (file share/libc/stdio.h, line 185)
assigns *stream \from buf;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1463,10 +1525,10 @@
--- Properties of Function 'setvbuf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 149)
+[ Extern ] Assigns (file share/libc/stdio.h, line 189)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 149)
+[ Extern ] Froms (file share/libc/stdio.h, line 189)
assigns *stream \from buf, mode, size;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1477,10 +1539,10 @@
--- Properties of Function 'vfprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 178)
+[ Extern ] Assigns (file share/libc/stdio.h, line 218)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 178)
+[ Extern ] Froms (file share/libc/stdio.h, line 218)
assigns *stream \from *(format + (..)), arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1491,10 +1553,10 @@
--- Properties of Function 'vfscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 183)
+[ Extern ] Assigns (file share/libc/stdio.h, line 223)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 183)
+[ Extern ] Froms (file share/libc/stdio.h, line 223)
assigns *stream \from *(format + (..)), *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1505,10 +1567,10 @@
--- Properties of Function 'vprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 189)
+[ Extern ] Assigns (file share/libc/stdio.h, line 229)
assigns *__fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 189)
+[ Extern ] Froms (file share/libc/stdio.h, line 229)
assigns *__fc_stdout \from arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1519,10 +1581,10 @@
--- Properties of Function 'vscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 193)
+[ Extern ] Assigns (file share/libc/stdio.h, line 233)
assigns *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 193)
+[ Extern ] Froms (file share/libc/stdio.h, line 233)
assigns *__fc_stdin \from *(format + (..));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1533,10 +1595,10 @@
--- Properties of Function 'vsnprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 198)
+[ Extern ] Assigns (file share/libc/stdio.h, line 238)
assigns *(s + (0 .. n - 1));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 198)
+[ Extern ] Froms (file share/libc/stdio.h, line 238)
assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1547,10 +1609,10 @@
--- Properties of Function 'vsprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 204)
+[ Extern ] Assigns (file share/libc/stdio.h, line 244)
assigns *(s + (0 ..));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 204)
+[ Extern ] Froms (file share/libc/stdio.h, line 244)
assigns *(s + (0 ..)) \from *(format + (..)), arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1565,13 +1627,13 @@
ensures
result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 217)
+[ Extern ] Assigns (file share/libc/stdio.h, line 257)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 217)
+[ Extern ] Froms (file share/libc/stdio.h, line 257)
assigns *stream \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 218)
+[ Extern ] Froms (file share/libc/stdio.h, line 258)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1596,14 +1658,14 @@
terminated_string_on_success:
\result ≢ \null ⇒ valid_string(\old(s))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 226)
+[ Extern ] Assigns (file share/libc/stdio.h, line 266)
assigns *(s + (0 .. size - 1)), \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 226)
+[ Extern ] Froms (file share/libc/stdio.h, line 266)
assigns *(s + (0 .. size - 1))
\from (indirect: size), (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 227)
+[ Extern ] Froms (file share/libc/stdio.h, line 267)
assigns \result \from s, (indirect: size), (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1614,8 +1676,14 @@
--- Properties of Function 'fputc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 238)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 280)
+ assigns *stream, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 280)
+ assigns *stream \from c, *stream;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 281)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1625,11 +1693,16 @@
--- Properties of Function 'fputs'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 241)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 287)
+ assigns *stream, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 287)
+ assigns *stream \from *(s + (0 .. strlen{Old}(s)));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 241)
- assigns *stream \from *(s + (..));
+[ Extern ] Froms (file share/libc/stdio.h, line 288)
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1639,13 +1712,13 @@
--- Properties of Function 'getc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 245)
+[ Extern ] Assigns (file share/libc/stdio.h, line 295)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 245)
+[ Extern ] Froms (file share/libc/stdio.h, line 295)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 245)
+[ Extern ] Froms (file share/libc/stdio.h, line 295)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1656,12 +1729,15 @@
--- Properties of Function 'getchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns nothing
- assigns \nothing;
+[ Extern ] Assigns (file share/libc/stdio.h, line 300)
+ assigns \result, *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 248)
+[ Extern ] Froms (file share/libc/stdio.h, line 300)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 300)
+ assigns *__fc_stdin \from *__fc_stdin;
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1674,16 +1750,16 @@
ensures
result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 260)
+[ Extern ] Assigns (file share/libc/stdio.h, line 313)
assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 260)
+[ Extern ] Froms (file share/libc/stdio.h, line 313)
assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 261)
+[ Extern ] Froms (file share/libc/stdio.h, line 314)
assigns \result \from s, *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 262)
+[ Extern ] Froms (file share/libc/stdio.h, line 315)
assigns *__fc_stdin \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1694,12 +1770,15 @@
--- Properties of Function 'putc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 269)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 322)
+ assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 269)
+[ Extern ] Froms (file share/libc/stdio.h, line 322)
assigns *stream \from c;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 323)
+ assigns \result \from (indirect: *stream);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1708,12 +1787,15 @@
--- Properties of Function 'putchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 273)
- assigns *__fc_stdout;
+[ Extern ] Assigns (file share/libc/stdio.h, line 328)
+ assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 273)
+[ Extern ] Froms (file share/libc/stdio.h, line 328)
assigns *__fc_stdout \from c;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 329)
+ assigns \result \from (indirect: *__fc_stdout);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1722,11 +1804,16 @@
--- Properties of Function 'puts'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 276)
- assigns *__fc_stdout;
+[ Extern ] Assigns (file share/libc/stdio.h, line 335)
+ assigns *__fc_stdout, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 335)
+ assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s)));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 276)
- assigns *__fc_stdout \from *(s + (..));
+[ Extern ] Froms (file share/libc/stdio.h, line 336)
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: *__fc_stdout);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1736,11 +1823,18 @@
--- Properties of Function 'ungetc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 281)
- assigns *stream;
+[ Extern ] Post-condition 'result_ok_or_error'
+ ensures
+ result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 281)
- assigns *stream \from c;
+[ Extern ] Assigns (file share/libc/stdio.h, line 342)
+ assigns *stream, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 342)
+ assigns *stream \from (indirect: c);
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 343)
+ assigns \result \from (indirect: c), (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1759,15 +1853,15 @@
\initialized((char *)\old(ptr) +
(0 .. \result * \old(size) - 1))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 288)
+[ Extern ] Assigns (file share/libc/stdio.h, line 351)
assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 288)
+[ Extern ] Froms (file share/libc/stdio.h, line 351)
assigns *((char *)ptr + (0 .. nmemb * size - 1))
- \from size, nmemb, *stream;
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 289)
- assigns \result \from size, *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 353)
+ assigns \result \from size, (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1780,14 +1874,16 @@
[ Extern ] Post-condition 'size_written'
ensures size_written: \result ≤ \old(nmemb)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 301)
+[ Extern ] Assigns (file share/libc/stdio.h, line 364)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 301)
- assigns *stream \from *((char *)ptr + (0 .. nmemb * size - 1));
+[ Extern ] Froms (file share/libc/stdio.h, line 364)
+ assigns *stream
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 301)
- assigns \result \from *((char *)ptr + (0 .. nmemb * size - 1));
+[ Extern ] Froms (file share/libc/stdio.h, line 364)
+ assigns \result
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1797,11 +1893,14 @@
--- Properties of Function 'fgetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 309)
- assigns *pos;
+[ Extern ] Assigns (file share/libc/stdio.h, line 375)
+ assigns *pos, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 309)
- assigns *pos \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 375)
+ assigns *pos \from (indirect: *stream);
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 376)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1811,19 +1910,19 @@
--- Properties of Function 'fseek'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 316)
+[ Extern ] Assigns (file share/libc/stdio.h, line 384)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 316)
+[ Extern ] Froms (file share/libc/stdio.h, line 384)
assigns *stream
\from *stream, (indirect: offset), (indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 317)
+[ Extern ] Froms (file share/libc/stdio.h, line 385)
assigns \result
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 317)
+[ Extern ] Froms (file share/libc/stdio.h, line 385)
assigns __fc_errno
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
@@ -1836,10 +1935,10 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 322)
+[ Extern ] Assigns (file share/libc/stdio.h, line 394)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 322)
+[ Extern ] Froms (file share/libc/stdio.h, line 394)
assigns *stream \from *pos;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1856,13 +1955,13 @@
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 327)
+[ Extern ] Assigns (file share/libc/stdio.h, line 400)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 327)
+[ Extern ] Froms (file share/libc/stdio.h, line 400)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 327)
+[ Extern ] Froms (file share/libc/stdio.h, line 400)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1873,10 +1972,10 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 335)
+[ Extern ] Assigns (file share/libc/stdio.h, line 408)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 335)
+[ Extern ] Froms (file share/libc/stdio.h, line 408)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1887,10 +1986,10 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 341)
+[ Extern ] Assigns (file share/libc/stdio.h, line 414)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 341)
+[ Extern ] Froms (file share/libc/stdio.h, line 414)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1904,8 +2003,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 347)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 420)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1918,8 +2017,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 353)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 426)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1929,10 +2028,10 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 359)
+[ Extern ] Assigns (file share/libc/stdio.h, line 432)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 359)
+[ Extern ] Froms (file share/libc/stdio.h, line 432)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1943,10 +2042,10 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 365)
+[ Extern ] Assigns (file share/libc/stdio.h, line 438)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 365)
+[ Extern ] Froms (file share/libc/stdio.h, line 438)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1957,13 +2056,13 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 371)
+[ Extern ] Assigns (file share/libc/stdio.h, line 444)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 371)
+[ Extern ] Froms (file share/libc/stdio.h, line 444)
assigns \result \from \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 371)
+[ Extern ] Froms (file share/libc/stdio.h, line 444)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1977,8 +2076,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 377)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 450)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1988,11 +2087,12 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 383)
+[ Extern ] Assigns (file share/libc/stdio.h, line 456)
assigns __fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 383)
- assigns __fc_stdout \from __fc_errno, *(s + (..));
+[ Extern ] Froms (file share/libc/stdio.h, line 456)
+ assigns __fc_stdout
+ \from __fc_errno, *(s + (0 .. strlen{Old}(s)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -2002,13 +2102,13 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 389)
+[ Extern ] Assigns (file share/libc/stdio.h, line 462)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 389)
+[ Extern ] Froms (file share/libc/stdio.h, line 462)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 389)
+[ Extern ] Froms (file share/libc/stdio.h, line 462)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2022,7 +2122,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 392)
+[ Extern ] Froms (file share/libc/stdio.h, line 467)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2033,12 +2133,15 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 397)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 473)
+ assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 397)
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
assigns *stream \from c;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 474)
+ assigns \result \from (indirect: *stream);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -2047,12 +2150,15 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 401)
- assigns *__fc_stdout;
+[ Extern ] Assigns (file share/libc/stdio.h, line 479)
+ assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 401)
+[ Extern ] Froms (file share/libc/stdio.h, line 479)
assigns *__fc_stdout \from c;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 480)
+ assigns \result \from (indirect: *__fc_stdout);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -2061,10 +2167,10 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 406)
+[ Extern ] Assigns (file share/libc/stdio.h, line 486)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 406)
+[ Extern ] Froms (file share/libc/stdio.h, line 486)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2078,8 +2184,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 412)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 492)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -2092,8 +2198,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 418)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 498)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -2106,8 +2212,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 424)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 504)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -2124,14 +2230,14 @@
(\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
is_open_pipe(\result))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 451)
+[ Extern ] Assigns (file share/libc/stdio.h, line 531)
assigns \result, __fc_fopen[0 ..];
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 451)
+[ Extern ] Froms (file share/libc/stdio.h, line 531)
assigns \result
\from (indirect: *command), (indirect: *type), __fc_p_fopen;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 453)
+[ Extern ] Froms (file share/libc/stdio.h, line 533)
assigns __fc_fopen[0 ..]
\from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
Unverifiable but considered Valid.
@@ -2149,7 +2255,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 465)
+[ Extern ] Froms (file share/libc/stdio.h, line 545)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3939,9 +4045,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 177 Completely validated
+ 179 Completely validated
16 Locally validated
- 457 Considered valid
+ 483 Considered valid
56 To be validated
- 706 Total
+ 734 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index e8cb83c5ada4c1850d6cd7cd3708da2ec16145dc..8554a5a2d796a49cecbaea8e86f5ded905a0e92f 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -172,7 +172,7 @@
==============
Sloc = 1083
Decision point = 204
- Global variables = 68
+ Global variables = 70
If = 195
Loop = 43
Goto = 89
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index e843f8502134755dde99808dfc93fa8e50c26db5..75d29b2cadc0be606bab5e65630a62f26e2c2310 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4467,10 +4467,22 @@ FILE *__fc_stdin;
FILE *__fc_stdout;
-/*@ assigns \nothing; */
+/*@ requires valid_filename: valid_read_string(filename);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename))));
+ */
extern int remove(char const *filename);
-/*@ assigns \nothing; */
+/*@ requires valid_old_name: valid_read_string(old_name);
+ requires valid_new_name: valid_read_string(new_name);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result
+ \from (indirect: *(old_name + (0 .. strlen{Old}(old_name)))),
+ (indirect: *(new_name + (0 .. strlen{Old}(new_name))));
+ */
extern int rename(char const *old_name, char const *new_name);
FILE __fc_fopen[16];
@@ -4483,23 +4495,52 @@ FILE * const __fc_p_fopen = __fc_fopen;
*/
extern FILE *tmpfile(void);
-/*@ assigns \result, *(s + (..));
- assigns \result \from *(s + (..));
- assigns *(s + (..)) \from \nothing;
+char __fc_tmpnam[2048];
+char * const __fc_p_tmpnam = __fc_tmpnam;
+/*@ requires valid_s_or_null: s ≡ \null ∨ \valid(s + (0 .. 2048));
+ ensures
+ result_string_or_null:
+ \result ≡ \null ∨ \result ≡ \old(s) ∨
+ \result ≡ __fc_p_tmpnam;
+ assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)), \result;
+ assigns *(__fc_p_tmpnam + (0 .. 2048))
+ \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
+ assigns *(s + (0 .. 2048))
+ \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
+ assigns \result \from s, __fc_p_tmpnam;
*/
extern char *tmpnam(char *s);
/*@ requires valid_stream: \valid(stream);
ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
- assigns \result \from stream, stream->__fc_FILE_id;
+ assigns \result \from (indirect: *stream);
*/
extern int fclose(FILE *stream);
/*@ requires null_or_valid_stream: stream ≡ \null ∨ \valid_read(stream);
ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result;
- assigns \result \from stream, stream->__fc_FILE_id;
+ assigns \result, *stream, __fc_fopen[0 .. 16 - 1];
+ assigns \result \from (indirect: *stream);
+ assigns *stream
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+ assigns __fc_fopen[0 .. 16 - 1]
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+
+ behavior flush_all:
+ assumes all_streams: stream ≡ \null;
+ assigns __fc_fopen[0 .. 16 - 1], \result;
+ assigns __fc_fopen[0 .. 16 - 1] \from __fc_fopen[0 .. 16 - 1];
+ assigns \result \from (indirect: __fc_fopen[0 .. 16 - 1]);
+
+ behavior flush_stream:
+ assumes single_stream: stream ≢ \null;
+ assigns *stream, \result;
+ assigns *stream \from *stream;
+ assigns \result \from (indirect: *stream);
+
+ complete behaviors flush_stream, flush_all;
+ disjoint behaviors flush_stream, flush_all;
*/
extern int fflush(FILE *stream);
@@ -4510,8 +4551,8 @@ extern int fflush(FILE *stream);
\result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
assigns \result;
assigns \result
- \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
- __fc_p_fopen;
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen;
*/
extern FILE *fopen(char const * __restrict filename,
char const * __restrict mode);
@@ -4522,10 +4563,10 @@ extern FILE *fopen(char const * __restrict filename,
\result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
assigns \result, __fc_fopen[fd];
assigns \result
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))),
(indirect: __fc_fopen[fd]), __fc_p_fopen;
assigns __fc_fopen[fd]
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))),
(indirect: __fc_fopen[fd]), __fc_p_fopen;
*/
extern FILE *fdopen(int fd, char const *mode);
@@ -4617,21 +4658,32 @@ extern int fgetc(FILE *stream);
*/
extern char *fgets(char * __restrict s, int size, FILE * __restrict stream);
-/*@ assigns *stream; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream, \result;
+ assigns *stream \from c, *stream;
+ assigns \result \from (indirect: *stream);
+ */
extern int fputc(int c, FILE *stream);
-/*@ assigns *stream;
- assigns *stream \from *(s + (..)); */
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns *stream, \result;
+ assigns *stream \from *(s + (0 .. strlen{Old}(s)));
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: *stream);
+ */
extern int fputs(char const * __restrict s, FILE * __restrict stream);
-/*@ assigns \result, *stream;
+/*@ requires valid_stream: \valid(stream);
+ assigns \result, *stream;
assigns \result \from *stream;
assigns *stream \from *stream;
*/
extern int getc(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *__fc_stdin; */
+/*@ assigns \result, *__fc_stdin;
+ assigns \result \from *__fc_stdin;
+ assigns *__fc_stdin \from *__fc_stdin;
+ */
extern int getchar(void);
/*@ axiomatic GetsLength {
@@ -4651,22 +4703,32 @@ extern int getchar(void);
extern char *gets(char *s);
/*@ requires valid_stream: \valid(stream);
- assigns *stream;
+ assigns *stream, \result;
assigns *stream \from c;
+ assigns \result \from (indirect: *stream);
*/
extern int putc(int c, FILE *stream);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from c; */
+/*@ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from c;
+ assigns \result \from (indirect: *__fc_stdout);
+ */
extern int putchar(int c);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(s + (..)); */
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s)));
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: *__fc_stdout);
+ */
extern int puts(char const *s);
/*@ requires valid_stream: \valid(stream);
- assigns *stream;
- assigns *stream \from c;
+ ensures result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1;
+ assigns *stream, \result;
+ assigns *stream \from (indirect: c);
+ assigns \result \from (indirect: c), (indirect: *stream);
*/
extern int ungetc(int c, FILE *stream);
@@ -4678,8 +4740,8 @@ extern int ungetc(int c, FILE *stream);
\initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
assigns *((char *)ptr + (0 .. nmemb * size - 1))
- \from size, nmemb, *stream;
- assigns \result \from size, *stream;
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns \result \from size, (indirect: *stream);
*/
extern size_t fread(void * __restrict ptr, size_t size, size_t nmemb,
FILE * __restrict stream);
@@ -4689,14 +4751,21 @@ extern size_t fread(void * __restrict ptr, size_t size, size_t nmemb,
requires valid_stream: \valid(stream);
ensures size_written: \result ≤ \old(nmemb);
assigns *stream, \result;
- assigns *stream \from *((char *)ptr + (0 .. nmemb * size - 1));
- assigns \result \from *((char *)ptr + (0 .. nmemb * size - 1));
+ assigns *stream
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
+ assigns \result
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
*/
extern size_t fwrite(void const * __restrict ptr, size_t size, size_t nmemb,
FILE * __restrict stream);
-/*@ assigns *pos;
- assigns *pos \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+ requires valid_pos: \valid(pos);
+ requires initialization: pos: \initialized(pos);
+ assigns *pos, \result;
+ assigns *pos \from (indirect: *stream);
+ assigns \result \from (indirect: *stream);
+ */
extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos);
/*@ requires valid_stream: \valid(stream);
@@ -4710,8 +4779,12 @@ extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos);
*/
extern int fseek(FILE *stream, long offset, int whence);
-/*@ assigns *stream;
- assigns *stream \from *pos; */
+/*@ requires valid_stream: \valid(stream);
+ requires valid_pos: \valid_read(pos);
+ requires initialization: pos: \initialized(pos);
+ assigns *stream;
+ assigns *stream \from *pos;
+ */
extern int fsetpos(FILE *stream, fpos_t const *pos);
/*@ requires valid_stream: \valid(stream);
@@ -4739,13 +4812,13 @@ extern void clearerr(FILE *stream);
/*@ requires valid_stream: \valid(stream);
assigns \result;
- assigns \result \from *stream;
+ assigns \result \from (indirect: *stream);
*/
extern int feof(FILE *stream);
/*@ requires valid_stream: \valid(stream);
assigns \result;
- assigns \result \from *stream;
+ assigns \result \from (indirect: *stream);
*/
extern int fileno(FILE *stream);
@@ -4770,13 +4843,13 @@ extern int ftrylockfile(FILE *stream);
/*@ requires valid_stream: \valid(stream);
assigns \result;
- assigns \result \from *stream;
+ assigns \result \from (indirect: *stream);
*/
extern int ferror(FILE *stream);
/*@ requires valid_string_s: valid_read_string(s);
assigns __fc_stdout;
- assigns __fc_stdout \from __fc_errno, *(s + (..));
+ assigns __fc_stdout \from __fc_errno, *(s + (0 .. strlen{Old}(s)));
*/
extern void perror(char const *s);
@@ -4792,13 +4865,16 @@ extern int getc_unlocked(FILE *stream);
extern int getchar_unlocked(void);
/*@ requires valid_stream: \valid(stream);
- assigns *stream;
+ assigns *stream, \result;
assigns *stream \from c;
+ assigns \result \from (indirect: *stream);
*/
extern int putc_unlocked(int c, FILE *stream);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from c; */
+/*@ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from c;
+ assigns \result \from (indirect: *__fc_stdout);
+ */
extern int putchar_unlocked(int c);
/*@ requires valid_stream: \valid(stream);
@@ -4809,19 +4885,19 @@ extern void clearerr_unlocked(FILE *stream);
/*@ requires valid_stream: \valid(stream);
assigns \result;
- assigns \result \from *stream;
+ assigns \result \from (indirect: *stream);
*/
extern int feof_unlocked(FILE *stream);
/*@ requires valid_stream: \valid(stream);
assigns \result;
- assigns \result \from *stream;
+ assigns \result \from (indirect: *stream);
*/
extern int ferror_unlocked(FILE *stream);
/*@ requires valid_stream: \valid(stream);
assigns \result;
- assigns \result \from *stream;
+ assigns \result \from (indirect: *stream);
*/
extern int fileno_unlocked(FILE *stream);
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index eca3c4a7d227c3204cc015581c99570d60fa0430..24cfd8d35b1ec774597df2d92db5dcd32f240b4b 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -53,7 +53,7 @@
==============
Sloc = 17
Decision point = 0
- Global variables = 15
+ Global variables = 17
If = 0
Loop = 0
Goto = 0
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 9c9da490751c46d4be61d72f0e1ecfdbdb85258d..849833c6393789831788f9412892bbd911f1de18 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -43,6 +43,7 @@
cpt ∈ {0; 1; 2; 3; 4}
tmp ∈ [-2147483648..4]
__retres ∈ {1}
+ S___fc_stdin[0..1] ∈ [--..--]
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Global Properties
@@ -151,8 +152,12 @@
--- Properties of Function 'remove'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'result_ok_or_error'
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 76)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -160,8 +165,12 @@
--- Properties of Function 'rename'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'result_ok_or_error'
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 85)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -173,7 +182,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 80)
+[ Extern ] Froms (file share/libc/stdio.h, line 95)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -182,11 +191,15 @@
--- Properties of Function 'tmpnam'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 87)
+[ Extern ] Post-condition 'result_string_or_null'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 108)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 108)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 87)
+[ Extern ] Froms (file share/libc/stdio.h, line 110)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 88)
+[ Extern ] Froms (file share/libc/stdio.h, line 111)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -199,7 +212,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 95)
+[ Extern ] Froms (file share/libc/stdio.h, line 120)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -210,12 +223,32 @@
[ Extern ] Post-condition 'result_zero_or_EOF'
Unverifiable but considered Valid.
-[ Extern ] Assigns nothing
+[ Extern ] Assigns (file share/libc/stdio.h, line 129)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'flush_all' (file share/libc/stdio.h, line 135)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'flush_stream' (file share/libc/stdio.h, line 140)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 129)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 130)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 130)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 103)
+[ Extern ] Froms for 'flush_all' (file share/libc/stdio.h, line 135)
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_all' (file share/libc/stdio.h, line 137)
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_stream' (file share/libc/stdio.h, line 140)
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_stream' (file share/libc/stdio.h, line 141)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'flush_all'
+ by Frama-C kernel.
+[ Valid ] Behavior 'flush_stream'
+ by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'fopen'
@@ -225,7 +258,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 112)
+[ Extern ] Froms (file share/libc/stdio.h, line 150)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -236,11 +269,11 @@
[ Extern ] Post-condition 'result_null_or_valid_fd'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 121)
+[ Extern ] Assigns (file share/libc/stdio.h, line 160)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 121)
+[ Extern ] Froms (file share/libc/stdio.h, line 160)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 121)
+[ Extern ] Froms (file share/libc/stdio.h, line 160)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -253,11 +286,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'stream_opened'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 132)
+[ Extern ] Assigns (file share/libc/stdio.h, line 172)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 132)
+[ Extern ] Froms (file share/libc/stdio.h, line 172)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 134)
+[ Extern ] Froms (file share/libc/stdio.h, line 174)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -266,9 +299,9 @@
--- Properties of Function 'setbuf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 145)
+[ Extern ] Assigns (file share/libc/stdio.h, line 185)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 145)
+[ Extern ] Froms (file share/libc/stdio.h, line 185)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -277,9 +310,9 @@
--- Properties of Function 'setvbuf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 149)
+[ Extern ] Assigns (file share/libc/stdio.h, line 189)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 149)
+[ Extern ] Froms (file share/libc/stdio.h, line 189)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -288,9 +321,9 @@
--- Properties of Function 'vfprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 178)
+[ Extern ] Assigns (file share/libc/stdio.h, line 218)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 178)
+[ Extern ] Froms (file share/libc/stdio.h, line 218)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -299,9 +332,9 @@
--- Properties of Function 'vfscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 183)
+[ Extern ] Assigns (file share/libc/stdio.h, line 223)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 183)
+[ Extern ] Froms (file share/libc/stdio.h, line 223)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -310,9 +343,9 @@
--- Properties of Function 'vprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 189)
+[ Extern ] Assigns (file share/libc/stdio.h, line 229)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 189)
+[ Extern ] Froms (file share/libc/stdio.h, line 229)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -321,9 +354,9 @@
--- Properties of Function 'vscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 193)
+[ Extern ] Assigns (file share/libc/stdio.h, line 233)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 193)
+[ Extern ] Froms (file share/libc/stdio.h, line 233)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -332,9 +365,9 @@
--- Properties of Function 'vsnprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 198)
+[ Extern ] Assigns (file share/libc/stdio.h, line 238)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 198)
+[ Extern ] Froms (file share/libc/stdio.h, line 238)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -343,9 +376,9 @@
--- Properties of Function 'vsprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 204)
+[ Extern ] Assigns (file share/libc/stdio.h, line 244)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 204)
+[ Extern ] Froms (file share/libc/stdio.h, line 244)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -356,11 +389,11 @@
[ Extern ] Post-condition 'result_uchar_or_eof'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 217)
+[ Extern ] Assigns (file share/libc/stdio.h, line 257)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 217)
+[ Extern ] Froms (file share/libc/stdio.h, line 257)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 218)
+[ Extern ] Froms (file share/libc/stdio.h, line 258)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -375,11 +408,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'terminated_string_on_success'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 226)
+[ Extern ] Assigns (file share/libc/stdio.h, line 266)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 226)
+[ Extern ] Froms (file share/libc/stdio.h, line 266)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 227)
+[ Extern ] Froms (file share/libc/stdio.h, line 267)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -388,7 +421,11 @@
--- Properties of Function 'fputc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 238)
+[ Extern ] Assigns (file share/libc/stdio.h, line 280)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 280)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 281)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -397,9 +434,11 @@
--- Properties of Function 'fputs'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 241)
+[ Extern ] Assigns (file share/libc/stdio.h, line 287)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 241)
+[ Extern ] Froms (file share/libc/stdio.h, line 287)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 288)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -408,11 +447,11 @@
--- Properties of Function 'getc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 245)
+[ Extern ] Assigns (file share/libc/stdio.h, line 295)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 245)
+[ Extern ] Froms (file share/libc/stdio.h, line 295)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 245)
+[ Extern ] Froms (file share/libc/stdio.h, line 295)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -421,9 +460,11 @@
--- Properties of Function 'getchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns nothing
+[ Extern ] Assigns (file share/libc/stdio.h, line 300)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 300)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 248)
+[ Extern ] Froms (file share/libc/stdio.h, line 300)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -434,13 +475,13 @@
[ Extern ] Post-condition 'result_null_or_same'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 260)
+[ Extern ] Assigns (file share/libc/stdio.h, line 313)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 260)
+[ Extern ] Froms (file share/libc/stdio.h, line 313)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 261)
+[ Extern ] Froms (file share/libc/stdio.h, line 314)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 262)
+[ Extern ] Froms (file share/libc/stdio.h, line 315)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -449,9 +490,11 @@
--- Properties of Function 'putc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 269)
+[ Extern ] Assigns (file share/libc/stdio.h, line 322)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 322)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 269)
+[ Extern ] Froms (file share/libc/stdio.h, line 323)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -460,9 +503,11 @@
--- Properties of Function 'putchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 273)
+[ Extern ] Assigns (file share/libc/stdio.h, line 328)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 328)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 273)
+[ Extern ] Froms (file share/libc/stdio.h, line 329)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -471,9 +516,11 @@
--- Properties of Function 'puts'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 276)
+[ Extern ] Assigns (file share/libc/stdio.h, line 335)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 335)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 276)
+[ Extern ] Froms (file share/libc/stdio.h, line 336)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -482,9 +529,13 @@
--- Properties of Function 'ungetc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 281)
+[ Extern ] Post-condition 'result_ok_or_error'
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 281)
+[ Extern ] Assigns (file share/libc/stdio.h, line 342)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 342)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 343)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -497,11 +548,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'initialization'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 288)
+[ Extern ] Assigns (file share/libc/stdio.h, line 351)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 288)
+[ Extern ] Froms (file share/libc/stdio.h, line 351)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 289)
+[ Extern ] Froms (file share/libc/stdio.h, line 353)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -512,11 +563,11 @@
[ Extern ] Post-condition 'size_written'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 301)
+[ Extern ] Assigns (file share/libc/stdio.h, line 364)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 301)
+[ Extern ] Froms (file share/libc/stdio.h, line 364)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 301)
+[ Extern ] Froms (file share/libc/stdio.h, line 364)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -525,9 +576,11 @@
--- Properties of Function 'fgetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 309)
+[ Extern ] Assigns (file share/libc/stdio.h, line 375)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 375)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 309)
+[ Extern ] Froms (file share/libc/stdio.h, line 376)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -536,13 +589,13 @@
--- Properties of Function 'fseek'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 316)
+[ Extern ] Assigns (file share/libc/stdio.h, line 384)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 316)
+[ Extern ] Froms (file share/libc/stdio.h, line 384)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 317)
+[ Extern ] Froms (file share/libc/stdio.h, line 385)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 317)
+[ Extern ] Froms (file share/libc/stdio.h, line 385)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -551,9 +604,9 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 322)
+[ Extern ] Assigns (file share/libc/stdio.h, line 394)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 322)
+[ Extern ] Froms (file share/libc/stdio.h, line 394)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -564,11 +617,11 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 327)
+[ Extern ] Assigns (file share/libc/stdio.h, line 400)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 327)
+[ Extern ] Froms (file share/libc/stdio.h, line 400)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 327)
+[ Extern ] Froms (file share/libc/stdio.h, line 400)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -577,9 +630,9 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 335)
+[ Extern ] Assigns (file share/libc/stdio.h, line 408)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 335)
+[ Extern ] Froms (file share/libc/stdio.h, line 408)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -588,9 +641,9 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 341)
+[ Extern ] Assigns (file share/libc/stdio.h, line 414)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 341)
+[ Extern ] Froms (file share/libc/stdio.h, line 414)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -601,7 +654,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 347)
+[ Extern ] Froms (file share/libc/stdio.h, line 420)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -612,7 +665,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 353)
+[ Extern ] Froms (file share/libc/stdio.h, line 426)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -621,9 +674,9 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 359)
+[ Extern ] Assigns (file share/libc/stdio.h, line 432)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 359)
+[ Extern ] Froms (file share/libc/stdio.h, line 432)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -632,9 +685,9 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 365)
+[ Extern ] Assigns (file share/libc/stdio.h, line 438)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 365)
+[ Extern ] Froms (file share/libc/stdio.h, line 438)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -643,11 +696,11 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 371)
+[ Extern ] Assigns (file share/libc/stdio.h, line 444)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 371)
+[ Extern ] Froms (file share/libc/stdio.h, line 444)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 371)
+[ Extern ] Froms (file share/libc/stdio.h, line 444)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -658,7 +711,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 377)
+[ Extern ] Froms (file share/libc/stdio.h, line 450)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -667,9 +720,9 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 383)
+[ Extern ] Assigns (file share/libc/stdio.h, line 456)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 383)
+[ Extern ] Froms (file share/libc/stdio.h, line 456)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -678,11 +731,11 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 389)
+[ Extern ] Assigns (file share/libc/stdio.h, line 462)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 389)
+[ Extern ] Froms (file share/libc/stdio.h, line 462)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 389)
+[ Extern ] Froms (file share/libc/stdio.h, line 462)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -693,7 +746,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 392)
+[ Extern ] Froms (file share/libc/stdio.h, line 467)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -702,9 +755,11 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 397)
+[ Extern ] Assigns (file share/libc/stdio.h, line 473)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 473)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 397)
+[ Extern ] Froms (file share/libc/stdio.h, line 474)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -713,9 +768,11 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 401)
+[ Extern ] Assigns (file share/libc/stdio.h, line 479)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 479)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 401)
+[ Extern ] Froms (file share/libc/stdio.h, line 480)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -724,9 +781,9 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 406)
+[ Extern ] Assigns (file share/libc/stdio.h, line 486)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 406)
+[ Extern ] Froms (file share/libc/stdio.h, line 486)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -737,7 +794,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 412)
+[ Extern ] Froms (file share/libc/stdio.h, line 492)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -748,7 +805,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 418)
+[ Extern ] Froms (file share/libc/stdio.h, line 498)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -759,7 +816,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 424)
+[ Extern ] Froms (file share/libc/stdio.h, line 504)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -770,11 +827,11 @@
[ Extern ] Post-condition 'result_error_or_valid_open_pipe'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 451)
+[ Extern ] Assigns (file share/libc/stdio.h, line 531)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 451)
+[ Extern ] Froms (file share/libc/stdio.h, line 531)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 453)
+[ Extern ] Froms (file share/libc/stdio.h, line 533)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -787,7 +844,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 465)
+[ Extern ] Froms (file share/libc/stdio.h, line 545)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -806,8 +863,8 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 70 Completely validated
- 171 Considered valid
+ 72 Completely validated
+ 197 Considered valid
1 To be validated
- 242 Total
+ 270 Total
--------------------------------------------------------------------------------