From 739d750c98e147a3282024497f4d4bd0a25fadbe Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 28 May 2020 22:01:48 +0200
Subject: [PATCH] [Libc] include error case for pthread_mutexattr_destroy

---
 share/libc/pthread.h                   | 5 +++--
 tests/libc/oracle/fc_libc.1.res.oracle | 8 ++++----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index 84131d8aab4..08c08ca6449 100644
--- a/share/libc/pthread.h
+++ b/share/libc/pthread.h
@@ -319,8 +319,9 @@ extern int pthread_mutex_unlock(pthread_mutex_t *mutex);
 
 /*@
   requires valid_attr: \valid(attr);
-  assigns \result, *attr \from \nothing;
-  ensures success: \result == 0;
+  assigns *attr \from *attr;
+  assigns \result \from indirect:*attr;
+  ensures success_or_error: \result == 0 || \result == EINVAL;
  */
 extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr);
 
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 29a563fb2eb..ce58bfc1d77 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -7789,10 +7789,10 @@ extern int pthread_mutex_lock(pthread_mutex_t *mutex);
 extern int pthread_mutex_unlock(pthread_mutex_t *mutex);
 
 /*@ requires valid_attr: \valid(attr);
-    ensures success: \result ≡ 0;
-    assigns \result, *attr;
-    assigns \result \from \nothing;
-    assigns *attr \from \nothing;
+    ensures success_or_error: \result ≡ 0 ∨ \result ≡ 22;
+    assigns *attr, \result;
+    assigns *attr \from *attr;
+    assigns \result \from (indirect: *attr);
  */
 extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr);
 
-- 
GitLab