diff --git a/share/libc/netdb.h b/share/libc/netdb.h
index 0b09f4b9d9c6acfdfb6909ad4d0ff34a5d35c65b..6e1c25159151f19945ae37a94246b695896a5a68 100644
--- a/share/libc/netdb.h
+++ b/share/libc/netdb.h
@@ -181,7 +181,7 @@ extern struct hostent *gethostbyaddr(const void *, socklen_t, int);
 
 /*@
   allocates \result;
-  assigns \result, *\result \from name[0 .. strlen(name)];
+  assigns *\result \from name[0 .. strlen(name)];
 */
 extern struct hostent *gethostbyname(const char *name);
 
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 9042a4ca36c1efef6bc6f1ec4460e127e8ade2b8..e4c4ca549f14f0f1236df05fb9b70ef151239a36 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -570,7 +570,7 @@ extern int putenv(char *string);
   requires valid_name: valid_read_string(name);
   requires valid_value: valid_read_string(value);
   allocates __fc_env[0..];
-  assigns \result, __fc_env[0..]
+  assigns \result, __fc_env[0..], __fc_errno
     \from __fc_env[0..], indirect:name[0 .. strlen(name)],
     indirect:value[0 .. strlen(value)], indirect:overwrite;
   assigns __fc_env[0..][0..] \from name[0 .. strlen(name)],
diff --git a/share/libc/wchar.h b/share/libc/wchar.h
index 38bcc2d98ccf1815b688fd6c44790c10b47e33c3..89bbba4df2e0a158c99d07b13b969683f51a48ba 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -271,6 +271,8 @@ extern int wcscasecmp(const wchar_t *ws1, const wchar_t *ws2);
   requires valid_wstring: valid_read_wstring(ws);
   allocates \result;
   assigns \result \from indirect:ws[0..wcslen(ws)], indirect:__fc_heap_status;
+  assigns __fc_heap_status \from indirect:ws[0 .. wcslen(ws)],
+                                 __fc_heap_status;
   behavior allocation:
     assumes can_allocate: is_allocable(wcslen(ws));
     assigns __fc_heap_status \from indirect:ws[0 .. wcslen(ws)],
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 8cd873462f24eff47d8b190625670932cc3ff373..6c7da9d862913cc919d2b9a3a57989263d847d38 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -18247,6 +18247,31 @@
             }
           ]
         },
+        {
+          "ruleId": "user-spec",
+          "kind": "pass",
+          "level": "none",
+          "message": {
+            "text": "from clause of term __fc_errno in function setenv."
+          },
+          "locations": [
+            {
+              "physicalLocation": {
+                "artifactLocation": {
+                  "uri": "libc/stdlib.h",
+                  "uriBaseId": "FRAMAC_SHARE"
+                },
+                "region": {
+                  "startLine": 573,
+                  "startColumn": 34,
+                  "endLine": 573,
+                  "endColumn": 44,
+                  "byteLength": 10
+                }
+              }
+            }
+          ]
+        },
         {
           "ruleId": "user-spec",
           "kind": "pass",
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 2dc413e1c2b0772f552ddf056279124588bb262e..00a916d66f04b9e80fda0b2e932f9c9f0f0f693a 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:292: 
-  Declaration of variadic function fwprintf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:294: 
-  Declaration of variadic function swprintf.
+  Declaration of variadic function fwprintf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:296: 
+  Declaration of variadic function swprintf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:298: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:299: 
-  Declaration of variadic function wscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:301: 
-  Declaration of variadic function fwscanf.
+  Declaration of variadic function wscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:303: 
+  Declaration of variadic function fwscanf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:305: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index a7437bfcd7ce641e866f72a40da2ed7e4e0e0516..dc5aa4bc442e933bfd48886bf346e8db86cd04ff 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:292: 
-  Declaration of variadic function fwprintf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:294: 
-  Declaration of variadic function swprintf.
+  Declaration of variadic function fwprintf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:296: 
+  Declaration of variadic function swprintf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:298: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:299: 
-  Declaration of variadic function wscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:301: 
-  Declaration of variadic function fwscanf.
+  Declaration of variadic function wscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:303: 
+  Declaration of variadic function fwscanf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:305: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
@@ -35,7 +35,7 @@
 [eva] Analyzing a complete application starting at main
 [eva] using specification for function wmemset
 [eva] using specification for function swprintf_va_1
-[eva] FRAMAC_SHARE/libc/wchar.h:294: 
+[eva] FRAMAC_SHARE/libc/wchar.h:296: 
   Cannot evaluate range bound wformat_length(format) - 1
   (unsupported ACSL construct: logic function wformat_length). Approximating
 [eva:alarm] swprintf.c:12: Warning: 
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index e0192389ab09f034d7cf9800f641395f7a80ed42..e845bbf02f0ea226aabc42339cdb937ebb3eadc2 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:292: 
-  Declaration of variadic function fwprintf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:294: 
-  Declaration of variadic function swprintf.
+  Declaration of variadic function fwprintf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:296: 
+  Declaration of variadic function swprintf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:298: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:299: 
-  Declaration of variadic function wscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:301: 
-  Declaration of variadic function fwscanf.
+  Declaration of variadic function wscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:303: 
+  Declaration of variadic function fwscanf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:305: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6f3dc88e2dfd03c476cf941de0ad06f557a5eef9..bb27675e27a7b75dc2a8b46d57fdec09c8682c90 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5254,8 +5254,7 @@ static int res_search(char const *dname, int rec_class, int type,
   return tmp;
 }
 
-/*@ assigns \result, *\result;
-    assigns \result \from *(name + (0 .. strlen{Old}(name)));
+/*@ assigns *\result;
     assigns *\result \from *(name + (0 .. strlen{Old}(name)));
     allocates \result;
  */
@@ -8346,7 +8345,7 @@ int putenv(char *string)
 /*@ requires valid_name: valid_read_string(name);
     requires valid_value: valid_read_string(value);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
-    assigns \result, __fc_env[0 ..], *(__fc_env[0 ..] + (0 ..));
+    assigns \result, __fc_env[0 ..], __fc_errno, *(__fc_env[0 ..] + (0 ..));
     assigns \result
       \from __fc_env[0 ..], (indirect: *(name + (0 .. strlen{Old}(name)))),
             (indirect: *(value + (0 .. strlen{Old}(value)))),
@@ -8355,6 +8354,10 @@ int putenv(char *string)
       \from __fc_env[0 ..], (indirect: *(name + (0 .. strlen{Old}(name)))),
             (indirect: *(value + (0 .. strlen{Old}(value)))),
             (indirect: overwrite);
+    assigns __fc_errno
+      \from __fc_env[0 ..], (indirect: *(name + (0 .. strlen{Old}(name)))),
+            (indirect: *(value + (0 .. strlen{Old}(value)))),
+            (indirect: overwrite);
     assigns *(__fc_env[0 ..] + (0 ..))
       \from *(name + (0 .. strlen{Old}(name))),
             *(value + (0 .. strlen{Old}(value))), (indirect: __fc_env[0 ..]),
@@ -10245,10 +10248,12 @@ wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n)
 }
 
 /*@ requires valid_wstring: valid_read_wstring(ws);
-    assigns \result;
+    assigns \result, __fc_heap_status;
     assigns \result
       \from (indirect: *(ws + (0 .. wcslen{Old}(ws)))),
             (indirect: __fc_heap_status);
+    assigns __fc_heap_status
+      \from (indirect: *(ws + (0 .. wcslen{Old}(ws)))), __fc_heap_status;
     allocates \result;
     
     behavior allocation:
diff --git a/tests/libc/oracle/stdlib_h.0.res.oracle b/tests/libc/oracle/stdlib_h.0.res.oracle
index 4c93198f82653a64bf2d38e2f1fb872e5678b7d0..1cc7c46da275314b800ce751b73538b533351c96 100644
--- a/tests/libc/oracle/stdlib_h.0.res.oracle
+++ b/tests/libc/oracle/stdlib_h.0.res.oracle
@@ -424,6 +424,9 @@
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
+  __fc_errno ∈
+            {{ garbled mix of &{S_0___fc_env; S_1___fc_env}
+             (origin: Library function {stdlib_h.c:131}) }}
   __fc_random48_init ∈ {1}
   __fc_random48_counter[0..2] ∈ [--..--]
   __fc_env[0..4095] ∈
diff --git a/tests/libc/oracle/stdlib_h.1.res.oracle b/tests/libc/oracle/stdlib_h.1.res.oracle
index 9f36d6f4d130ae722c6a13da7173db39e027e22e..51a15bb613a6ef5a89578c5d4cdcb03753f2684d 100644
--- a/tests/libc/oracle/stdlib_h.1.res.oracle
+++ b/tests/libc/oracle/stdlib_h.1.res.oracle
@@ -424,6 +424,9 @@
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
+  __fc_errno ∈
+            {{ garbled mix of &{S_0___fc_env; S_1___fc_env}
+             (origin: Library function {stdlib_h.c:131}) }}
   __fc_random48_init ∈ {1}
   __fc_random48_counter[0..2] ∈ [--..--]
   __fc_env[0..4095] ∈
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index b11bedc26e32b1bd658d42c38a85bc2ad45daa82..8abb7517100080b86d59d184223110565f997c34 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -209,6 +209,7 @@
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
+  __fc_heap_status ∈ [--..--]
   fd ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
   buf[0..28] ∈ [--..--] or UNINITIALIZED
      [29] ∈ UNINITIALIZED