From 0343b44eced6d0da0bc4cb71c4d66df04d974989 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 18 Sep 2024 15:47:16 +0200
Subject: [PATCH] [libc] Add lchmod
---
share/libc/sys/stat.h | 15 +++++++++++++++
1 file changed, 15 insertions(+)
diff --git a/share/libc/sys/stat.h b/share/libc/sys/stat.h
index 94fdcb842d..98b7c5f85b 100644
--- a/share/libc/sys/stat.h
+++ b/share/libc/sys/stat.h
@@ -71,6 +71,21 @@ extern int fchmodat(int fd, const char *path, mode_t mode, int flag);
*/
extern int fchmod(int fildes, mode_t mode);
+// Non-POSIX; BSD
+/*@
+ // missing: assigns 'filesystem' \from path, path[0..], mode;
+ requires valid_path: valid_read_string(path);
+ assigns \result, __fc_errno
+ \from indirect:path, indirect:path[0 .. strlen(path)],
+ indirect:mode; //missing: \from 'filesystem'
+ ensures errno_set: __fc_errno == \old(__fc_errno) ||
+ __fc_errno \in {EACCES, EINTR, EINVAL, ELOOP,
+ ENAMETOOLONG, ENOENT, ENOTDIR, EPERM,
+ EROFS};
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int lchmod(const char *path, mode_t mode);
+
/*@
//TODO: define proper initialization postcondition; it involves only a few
// specific fields, and only a few bits within those fields.
--
GitLab