Added rmdir to libc

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
 

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);

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 ======

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 ======

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;
 }

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 } },