From b6939ec17b8341b3e0c9b56475e5986750380991 Mon Sep 17 00:00:00 2001
From: Paul Marinescu <paul.marinescu@imperial.ac.uk>
Date: Thu, 29 Aug 2013 15:59:16 +0100
Subject: Added some of the common *at functions to the model

---
 test/Runtime/POSIX/Futimesat.c | 43 ++++++++++++++++++++++++++++++++++++++++++
 test/Runtime/POSIX/Openat.c    | 18 ++++++++++++++++++
 2 files changed, 61 insertions(+)
 create mode 100644 test/Runtime/POSIX/Futimesat.c
 create mode 100644 test/Runtime/POSIX/Openat.c

(limited to 'test/Runtime/POSIX')

diff --git a/test/Runtime/POSIX/Futimesat.c b/test/Runtime/POSIX/Futimesat.c
new file mode 100644
index 00000000..fd9ea0de
--- /dev/null
+++ b/test/Runtime/POSIX/Futimesat.c
@@ -0,0 +1,43 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t2.bc
+// RUN: touch /tmp/futimesat-dummy
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: rm /tmp/futimesat-dummy
+
+#include <assert.h>
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <time.h>
+
+int main(int argc, char **argv) {
+  int r;
+  struct stat buf;
+  struct timeval times[2];
+
+  times[0].tv_sec = time(NULL)-3600;
+  times[0].tv_usec = 0;
+  times[1].tv_sec = time(NULL)-3600;
+  times[1].tv_usec = 0;
+
+  r = futimesat(AT_FDCWD, "A", times);
+  assert(r != -1);
+
+  r = fstatat(AT_FDCWD, "A", &buf, 0);
+  assert(r != -1);
+  assert(buf.st_atime == times[0].tv_sec &&
+         buf.st_mtime == times[1].tv_sec);
+
+  /* assumes /tmp exists and is writeable */
+  int fd = open("/tmp", O_RDONLY);
+  assert(fd > 0);
+  r = futimesat(fd, "futimesat-dummy", times);
+  assert(r != -1);
+
+  r = fstatat(fd, "futimesat-dummy", &buf, 0);
+  assert(r != -1);
+  assert(buf.st_atime == times[0].tv_sec &&
+         buf.st_mtime == times[1].tv_sec);
+
+  close(fd);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c
new file mode 100644
index 00000000..d417ee47
--- /dev/null
+++ b/test/Runtime/POSIX/Openat.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: test -f klee-last/test000001.ktest
+
+#include <assert.h>
+#include <fcntl.h>
+
+int main(int argc, char **argv) {
+  int fd = openat(AT_FDCWD, "A", O_RDWR|O_TRUNC);
+  if (fd != -1) {
+    char buf[10];
+    assert(read(fd, buf, 10) == 10);
+    assert(klee_is_symbolic(buf[0]));
+  } else {
+    klee_silent_exit(0);
+  }
+  return 0;
+}
-- 
cgit 1.4.1