From 427ca8a02671b3576f6f5157f358c15fa888a3cf Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 18 Sep 2024 15:48:47 +0200
Subject: [PATCH] [libc] Add mkostemp and mkostemps

---
 share/libc/stdlib.h | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 2171e8c3c2..1c516ccb5a 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -823,6 +823,19 @@ extern int posix_memalign(void **memptr, size_t alignment, size_t size);
  */
 extern int mkstemp(char *templat);
 
+/*@
+  // missing: requires 'last 6 characters of template must be XXXXXX'
+  // missing: assigns \result, templat[0..] \from 'filesystem', 'RNG';
+  // missing: flags == O_APPEND || O_CLOEXEC || O_SYNC
+  requires valid_template: valid_string(templat);
+  requires template_len: strlen(templat) >= 6;
+  assigns templat[0..] \from \nothing;
+  assigns \result \from \nothing;
+  ensures result_error_or_valid_fd: \result == -1 ||
+                                    0 <= \result < __FC_FOPEN_MAX;
+ */
+extern int mkostemp(char *templat, int flags);
+
 /*@
   // missing: requires 'last (6+suffixlen) characters of template must be X's'
   // missing: assigns \result, templat[0..] \from 'filesystem', 'RNG';
@@ -836,6 +849,20 @@ extern int mkstemp(char *templat);
  */
 extern int mkstemps(char *templat, int suffixlen);
 
+/*@
+  // missing: requires 'last (6+suffixlen) characters of template must be X's'
+  // missing: assigns \result, templat[0..] \from 'filesystem', 'RNG';
+  // missing: flags == O_APPEND || O_CLOEXEC || O_SYNC
+  requires valid_template: valid_string(templat);
+  requires template_len: strlen(templat) >= 6 + suffixlen;
+  requires non_negative_suffixlen: suffixlen >= 0;
+  assigns templat[0..] \from \nothing;
+  assigns \result \from \nothing;
+  ensures result_error_or_valid_fd: \result == -1 ||
+                                    0 <= \result < __FC_FOPEN_MAX;
+ */
+extern int mkostemps(char *templat, int suffixlen, int flags);
+
 // 'realpath' may allocate memory for the result, which is not supported by
 // some plugins such as Eva. In such cases, it is preferable to use the stub
 // provided in stdlib.c.
-- 
GitLab