From 87f317e9f9faf83475cc32e193c59d76a4e1ab88 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 6 Mar 2024 08:54:18 +0100
Subject: [PATCH] [libc] add assigns clauses for glob.h functions

---
 share/libc/glob.h | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/share/libc/glob.h b/share/libc/glob.h
index 8bd7b4828ab..01655d11eef 100644
--- a/share/libc/glob.h
+++ b/share/libc/glob.h
@@ -26,6 +26,7 @@
 __PUSH_FC_STDLIB
 
 #include "__fc_machdep.h"
+#include "__fc_string_axiomatic.h"
 
 #define	GLOB_ERR	(1 << 0)/* Return on read errors.  */
 #define	GLOB_MARK	(1 << 1)/* Append a slash to each name.  */
@@ -67,10 +68,17 @@ typedef struct __fc_glob_t {
 #endif
 } glob_t;
 
+/*@
+  assigns \result, *pglob \from indirect:pattern[0 .. strlen(pattern)],
+                                indirect:flags, indirect:errfunc;
+*/
 extern int glob(const char *pattern, int flags,
                 int (*errfunc) (const char *epath, int eerrno),
                 glob_t *pglob);
 
+/*@
+  assigns *pglob \from *pglob;
+ */
 extern void globfree(glob_t *pglob);
 
 __END_DECLS
-- 
GitLab