diff --git a/share/libc/locale.h b/share/libc/locale.h
index 3672e1f5fc3269378016fbf134960d10cf2e93e4..cbe7fec2c6db0439274579f1c2ebe582f344eaa5 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 0000000000000000000000000000000000000000..eaa48e716d5d2ead3d75236bb3fde027cc7a29f1
--- /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 36e9390d1b2681d50ba65bb6ad5c74694fc63512..3c58f77336d9211e32fcf1f042c424df96e53bb7 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 0000000000000000000000000000000000000000..5cbe02120235f81b313b82a50dac7b89b36ad865
--- /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]