diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/Feature/IntrinsicTrap.ll | 28 | ||||
-rw-r--r-- | test/Runtime/POSIX/Futimesat.c | 43 | ||||
-rw-r--r-- | test/Runtime/POSIX/Openat.c | 18 |
3 files changed, 89 insertions, 0 deletions
diff --git a/test/Feature/IntrinsicTrap.ll b/test/Feature/IntrinsicTrap.ll new file mode 100644 index 00000000..5af46225 --- /dev/null +++ b/test/Feature/IntrinsicTrap.ll @@ -0,0 +1,28 @@ +; RUN: llvm-as %s -f -o %t1.bc +; RUN: %klee -disable-opt %t1.bc +; RUN: grep abort() klee-last/assembly.ll | wc -l | grep -q 2 +; RUN: echo "llvm.trap()" > %t2.ll +; RUN: grep llvm.trap() klee-last/assembly.ll %t2.ll | wc -l | grep -q 1 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-f128:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +define i32 @main() nounwind { +entry: + %a = add i32 1, 2 + %b = add i32 %a, 3 + %c = icmp ne i32 %b, 6 + br i1 %c, label %btrue, label %bfalse + +btrue: + call void @llvm.trap() noreturn nounwind + unreachable + +bfalse: + br label %return + +return: + ret i32 0 +} + +declare void @llvm.trap() noreturn nounwind 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; +} |