From dc89269b91c6002a518e3fda7785f4fb409d3441 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 14 May 2024 17:04:29 +0200
Subject: [PATCH] [libc] Initialize vld to avoid warning with macos
---
share/libc/stdio.c | 2 +-
tests/libc/oracle/fc_libc.1.res.oracle | 2 +-
tests/libc/oracle/stdio_c.res.oracle | 2 --
3 files changed, 2 insertions(+), 4 deletions(-)
diff --git a/share/libc/stdio.c b/share/libc/stdio.c
index eda30573e2d..09337ba5dd0 100644
--- a/share/libc/stdio.c
+++ b/share/libc/stdio.c
@@ -431,7 +431,7 @@ int vfscanf(FILE * restrict stream, const char * restrict format, va_list arg) {
case UPPER_L:
// TODO: use Frama_C_long_double_interval when it will be supported
{
- volatile long double vld;
+ volatile long double vld = 0.0;
*va_arg(arg, long double*) = vld;
}
break;
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 3b045dfc981..eba56f1518d 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -7990,8 +7990,8 @@ int vfscanf(FILE * restrict stream, char const * restrict format, va_list arg)
break;
case UPPER_L:
{
- long double volatile vld;
long double *tmp_17;
+ long double volatile vld = (long double)0.0;
tmp_17 = *((long double **)*arg);
arg ++;
*tmp_17 = vld;
diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle
index 18fbf9a277c..e848a868dcf 100644
--- a/tests/libc/oracle/stdio_c.res.oracle
+++ b/tests/libc/oracle/stdio_c.res.oracle
@@ -574,8 +574,6 @@
[eva:alarm] FRAMAC_SHARE/libc/stdio.c:435: Warning:
out of bounds write. assert \valid(tmp_17);
(tmp_17 from vararg)
-[eva:alarm] FRAMAC_SHARE/libc/stdio.c:435: Warning:
- accessing uninitialized left-value. assert \initialized(&vld);
[eva:alarm] FRAMAC_SHARE/libc/stdio.c:435: Warning:
non-finite long double value. assert \is_finite(vld);
[eva:alarm] FRAMAC_SHARE/libc/stdio.c:440: Warning:
--
GitLab