From 59f53ab1779a8a45599482e0b6942a8b09cad64a Mon Sep 17 00:00:00 2001
From: rlazarini <remi.lazarini@cea.fr>
Date: Fri, 1 Mar 2024 11:04:25 +0100
Subject: [PATCH] Added rmdir to libc

---
 share/libc/unistd.h                     | 8 ++++++++
 tests/libc/oracle/fc_libc.1.res.oracle  | 7 +++++++
 tests/libc/oracle/unistd_h.0.res.oracle | 8 ++++++++
 tests/libc/oracle/unistd_h.1.res.oracle | 8 ++++++++
 tests/libc/unistd_h.c                   | 3 +++
 tests/metrics/oracle/libc.json          | 1 +
 6 files changed, 35 insertions(+)

diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index a5ba5bf7da3..9be09d430cf 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -1226,6 +1226,14 @@ extern int optind, opterr, optopt;
  */
 extern int getopt(int argc, char * const argv[], const char *optstring);
 
+/*@
+  // missing: assigns 'filesystem' \from name[0..];
+  // missing: assigns errno one of 13 different possible values
+  requires valid_name: valid_read_string(name);
+  assigns \result \from indirect:name[0..strlen(name)];
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int rmdir(const char *name);
 
 __END_DECLS
 
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index bc1a0874a6a..06f9fb802ba 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8419,6 +8419,13 @@ extern int pipe(int pipefd[2]);
  */
 extern ssize_t read(int fd, void *buf, size_t count);
 
+/*@ requires valid_name: valid_read_string(name);
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: *(name + (0 .. strlen{Old}(name))));
+ */
+extern int rmdir(char const *name);
+
 /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns \result;
     assigns \result \from (indirect: gid);
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 24a810167ef..67d9d4401fe 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -12,6 +12,7 @@
   \return(lseek) == -1 (auto)
   \return(pipe) == 0 (auto)
   \return(read) == -1, 32 (auto)
+  \return(rmdir) == 0 (auto)
   \return(setegid) == 0 (auto)
   \return(seteuid) == 0 (auto)
   \return(setgid) == 0 (auto)
@@ -612,6 +613,13 @@
 [eva] computing for function read <- main.
   Called from unistd_h.c:118.
 [eva] Done for function read
+[eva] computing for function rmdir <- main.
+  Called from unistd_h.c:120.
+[eva] using specification for function rmdir
+[eva] unistd_h.c:120: 
+  function rmdir: precondition 'valid_name' got status valid.
+[eva] Done for function rmdir
+[eva] unistd_h.c:121: check 'ok' got status valid.
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 6700c7c0c09..03cb1465a19 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -12,6 +12,7 @@
   \return(lseek) == -1 (auto)
   \return(pipe) == 0 (auto)
   \return(read) == -1, 32 (auto)
+  \return(rmdir) == 0 (auto)
   \return(setegid) == 0 (auto)
   \return(seteuid) == 0 (auto)
   \return(setgid) == 0 (auto)
@@ -612,6 +613,13 @@
 [eva] computing for function read <- main.
   Called from unistd_h.c:118.
 [eva] Done for function read
+[eva] computing for function rmdir <- main.
+  Called from unistd_h.c:120.
+[eva] using specification for function rmdir
+[eva] unistd_h.c:120: 
+  function rmdir: precondition 'valid_name' got status valid.
+[eva] Done for function rmdir
+[eva] unistd_h.c:121: check 'ok' got status valid.
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index a8b8dbba169..89c9ac5baae 100644
--- a/tests/libc/unistd_h.c
+++ b/tests/libc/unistd_h.c
@@ -117,5 +117,8 @@ int main() {
   rread = read(fd, buf, SSIZE_MAX);
   rread = read(fd, buf, SIZE_MAX);
 
+  r = rmdir("/tmp/foo");
+  //@ check ok: r == 0 || r == -1;
+
   return 0;
 }
diff --git a/tests/metrics/oracle/libc.json b/tests/metrics/oracle/libc.json
index 7acca29f4fe..912a2a97651 100644
--- a/tests/metrics/oracle/libc.json
+++ b/tests/metrics/oracle/libc.json
@@ -104,6 +104,7 @@
     { "remove": { "calls": 0, "address_taken": false } },
     { "rename": { "calls": 0, "address_taken": false } },
     { "rewind": { "calls": 0, "address_taken": false } },
+    { "rmdir": { "calls": 0, "address_taken": false } },
     { "setbuf": { "calls": 0, "address_taken": false } },
     { "setegid": { "calls": 0, "address_taken": false } },
     { "seteuid": { "calls": 0, "address_taken": false } },
-- 
GitLab