diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index a413079d88f4697f0ed90c7c6b40cd52e65fde2b..ad5dfb1baf746906e9b062a4e9c14d0ba474a08d 100644
--- a/share/libc/pthread.h
+++ b/share/libc/pthread.h
@@ -388,8 +388,9 @@ extern int pthread_spin_unlock(pthread_spinlock_t *);
 extern void pthread_testcancel(void);
 
 // GNU extensions
+
 /*@ requires valid_name: valid_read_string(name);
-    assigns \result \from thread, name[..];
+    assigns \result \from indirect:thread, indirect:name[0 .. strlen(name)];
     //FIXME: it should assign thread, but our current
     // definition of the type does not allow this.
     behavior ko:
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index bd1478e3864f776394508e8a757d96cbb927273f..293159f267aae40a3d53a36ea3f8c59794ca35d3 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8621,7 +8621,9 @@ extern int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type);
 
 /*@ requires valid_name: valid_read_string(name);
     assigns \result;
-    assigns \result \from thread, *(name + (..));
+    assigns \result
+      \from (indirect: thread),
+            (indirect: *(name + (0 .. strlen{Old}(name))));
     
     behavior ko:
       assumes name_too_long: strlen(name) > 15;