diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 1c516ccb5a5dc1104fa6fe51530fbee23629a3e8..dc131429c407a4a5441add4281e8b64389693445 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -416,7 +416,7 @@ extern long int jrand48 (unsigned short xsubi[3]);
   complete behaviors;
   disjoint behaviors; */
 extern void *calloc(size_t nmemb, size_t size);
- 
+
 /*@ allocates \result;
   @ assigns __fc_heap_status \from size, __fc_heap_status;
   @ assigns \result \from indirect:size, indirect:__fc_heap_status;
@@ -562,6 +562,16 @@ extern char *__fc_env[ARG_MAX];
  */
 extern char *getenv(const char *name);
 
+// Non-POSIX, GNU extension
+/*@
+  requires valid_name: valid_read_string(name);
+  assigns \result \from __fc_env[0..], indirect:name,
+                        indirect:name[0 .. strlen(name)];
+  ensures null_or_valid_result:
+    \result == \null || (\valid(\result) && valid_read_string(\result));
+ */
+extern char *secure_getenv(const char *name);
+
 /*@
   requires valid_string: valid_read_string(string);
   assigns __fc_env[0..] \from __fc_env[0..], string;