Merge branch 'fix/andre/libc-locale' into 'master'

[Libc] fix spec of localeconv()

See merge request frama-c/frama-c!2865

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

tests/libc/locale_h.c

+#include <locale.h>
+
+int main() {
+  struct lconv *lc = localeconv();
+  return lc->decimal_point[0];
+}

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)
 {

tests/libc/oracle/locale_h.res.oracle

+[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]