diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index a5ba5bf7da343d2590a12be9a56d68c547ecd89e..9be09d430cf2857e1dbc173429c9282abef1bb46 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 bc1a0874a6a93bd9e5e05847cfa88d8d8b87858c..06f9fb802baed599d110bb2ce231aa39b7d831f2 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 24a810167ef1b8fa7ffc5041926c514863c09381..67d9d4401fef5a0c8a18b573223b6dc28430953b 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 6700c7c0c09d7703e48a21bede0c3d93060c8d80..03cb1465a1931d15e35283c9f6b6dbee89388c8f 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 a8b8dbba169df6fe6632a2f50137619af62162b1..89c9ac5baae555a1d8d91918abca6148f7b2420a 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 7acca29f4fea0e177826075be8ee65194383e8da..912a2a97651516f781c7c5ec2cd1328614c060f7 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 } },