From 69e7a2509970a1dfb929e6a100730f9b42f40cb1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 30 Sep 2020 10:26:10 +0200
Subject: [PATCH] [Libc] fix spec of localeconv()

---
 share/libc/locale.h                    |  5 +++--
 tests/libc/locale_h.c                  |  6 ++++++
 tests/libc/oracle/fc_libc.1.res.oracle |  3 ++-
 tests/libc/oracle/locale_h.res.oracle  | 20 ++++++++++++++++++++
 4 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 tests/libc/locale_h.c
 create mode 100644 tests/libc/oracle/locale_h.res.oracle

diff --git a/share/libc/locale.h b/share/libc/locale.h
index 3672e1f5fc3..cbe7fec2c6d 100644
--- a/share/libc/locale.h
+++ b/share/libc/locale.h
@@ -143,9 +143,10 @@ extern char*__fc_locale_names[512];
 */
 extern char *setlocale(int category, const char *locale);
 
-/*@ assigns \nothing;
+/*@
+  assigns \result \from __fc_locale;
   ensures result_current_locale: \result == __fc_locale;
- */
+*/
 extern struct lconv *localeconv(void);
 
 __END_DECLS
diff --git a/tests/libc/locale_h.c b/tests/libc/locale_h.c
new file mode 100644
index 00000000000..eaa48e716d5
--- /dev/null
+++ b/tests/libc/locale_h.c
@@ -0,0 +1,6 @@
+#include <locale.h>
+
+int main() {
+  struct lconv *lc = localeconv();
+  return lc->decimal_point[0];
+}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 36e9390d1b2..3c58f77336d 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2767,7 +2767,8 @@ char *setlocale(int category, char const *locale)
 }
 
 /*@ ensures result_current_locale: \result ≡ __fc_locale;
-    assigns \nothing;
+    assigns \result;
+    assigns \result \from __fc_locale;
  */
 struct lconv *localeconv(void)
 {
diff --git a/tests/libc/oracle/locale_h.res.oracle b/tests/libc/oracle/locale_h.res.oracle
new file mode 100644
index 00000000000..5cbe0212023
--- /dev/null
+++ b/tests/libc/oracle/locale_h.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/libc/locale_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] computing for function localeconv <- main.
+  Called from tests/libc/locale_h.c:4.
+[eva] using specification for function localeconv
+[eva] Done for function localeconv
+[eva:alarm] tests/libc/locale_h.c:5: Warning: 
+  out of bounds read. assert \valid_read(&lc->decimal_point);
+[eva:alarm] tests/libc/locale_h.c:5: Warning: 
+  out of bounds read. assert \valid_read(lc->decimal_point + 0);
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  lc ∈ {{ &S___fc_locale[0] }}
+  __retres ∈ [-128..127]
-- 
GitLab