From 4e2bbf47bf82370929a8dff75aec24a5ea9dabc1 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 24 Aug 2021 15:54:25 +0200
Subject: [PATCH] [libc] use indirect: labels for \from in pthread_setname_np
---
share/libc/pthread.h | 3 ++-
tests/libc/oracle/fc_libc.1.res.oracle | 4 +++-
2 files changed, 5 insertions(+), 2 deletions(-)
diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index a413079d88f..ad5dfb1baf7 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 bd1478e3864..293159f267a 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;
--
GitLab