about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/Feature/ExprLogging.c5
-rw-r--r--test/Feature/IntrinsicTrap.ll28
-rw-r--r--test/Feature/MemoryLimit.c24
-rw-r--r--test/Runtime/POSIX/Futimesat.c43
-rw-r--r--test/Runtime/POSIX/Openat.c18
-rw-r--r--test/Runtime/POSIX/SeedAndFail.c6
-rw-r--r--test/Runtime/POSIX/Stdin.c2
-rw-r--r--test/Solver/LargeIntegers.pc2
8 files changed, 112 insertions, 16 deletions
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index ad671a5e..9e9df87a 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -1,5 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
-// RUN: %klee --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log
+// We disable the cex-cache to eliminate nondeterminism across different solvers, in particular when counting the number of queries in the last two commands
+// RUN: %klee --use-cex-cache=false --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log
 // RUN: %kleaver -print-ast klee-last/all-queries.pc > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
@@ -7,7 +8,7 @@
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
 // RUN: grep "^; Query" klee-last/all-queries.smt2 | wc -l | grep -q 17
-// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 10
+// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 17
 
 #include <assert.h>
 
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/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c
index 3b1bacaf..d959c3de 100644
--- a/test/Feature/MemoryLimit.c
+++ b/test/Feature/MemoryLimit.c
@@ -2,35 +2,43 @@
 // RUN: %llvmgcc -g -c %s -o %t.big.bc
 // RUN: %klee --max-memory=20 %t.little.bc > %t.little.log
 // RUN: %klee --max-memory=20 %t.big.bc > %t.big.log
+// RUN: not grep -q "MALLOC FAILED" %t.little.log
+// RUN: not grep -q "MALLOC FAILED" %t.big.log
 // RUN: not grep -q "DONE" %t.little.log
 // RUN: not grep -q "DONE" %t.big.log
 
 #include <stdlib.h>
+#include <stdio.h>
 
 int main() {
-  int i, j, x=0;
+  int i, j, x=0, malloc_failed = 0;
   
 #ifdef LITTLE_ALLOC
   printf("IN LITTLE ALLOC\n");
     
   // 200 MBs total (in 32 byte chunks)
-  for (i=0; i<100; i++) {
-    for (j=0; j<(1<<16); j++)
-      malloc(1<<5);
+  for (i=0; i<100 && !malloc_failed; i++) {
+    for (j=0; j<(1<<16); j++){
+      void * p = malloc(1<<5);
+      malloc_failed |= (p == 0);
+    }
   }
 #else
   printf("IN BIG ALLOC\n");
   
   // 200 MBs total
-  for (i=0; i<100; i++) {
-    malloc(1<<21);
-    
+  for (i=0; i<100 && !malloc_failed; i++) {
+    void *p = malloc(1<<21);
+    malloc_failed |= (p == 0);
     // Ensure we hit the periodic check
+    // Use the pointer to be not optimized out by the compiler
     for (j=0; j<10000; j++)
-      x++;
+      x+=(unsigned)p;
   }
 #endif
 
+  if (malloc_failed)
+    printf("MALLOC FAILED\n");
   printf("DONE!\n");
 
   return x;
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;
+}
diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c
index db02217a..740db664 100644
--- a/test/Runtime/POSIX/SeedAndFail.c
+++ b/test/Runtime/POSIX/SeedAndFail.c
@@ -1,12 +1,10 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf tmp-123
-// RUN: %klee --libc=klee --output-dir=tmp-123 --posix-runtime %t.bc --sym-files 1 10  2>%t.log
+// RUN: %klee --libc=uclibc --output-dir=tmp-123 --posix-runtime %t.bc --sym-files 1 10  2>%t.log
 // RUN: %klee --seed-out-dir=tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1
 // RUN: ls klee-last | grep -c assert | grep 4
 
-
-
-#include <stdio.h>
+#include <string.h>
 #include <assert.h>
 #include <unistd.h>
 #include <sys/types.h>
diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c
index e7e3f2ff..b5402cf1 100644
--- a/test/Runtime/POSIX/Stdin.c
+++ b/test/Runtime/POSIX/Stdin.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --libc=klee --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log
+// RUN: %klee --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log
 // RUN: grep "mode:file" %t.log
 // RUN: grep "mode:dir" %t.log
 // RUN: grep "mode:chr" %t.log
diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.pc
index 99d1a61b..53ff3a51 100644
--- a/test/Solver/LargeIntegers.pc
+++ b/test/Solver/LargeIntegers.pc
@@ -11,7 +11,7 @@ array a[64] : w32 -> w8 = symbolic
 (query [] false [(Extract w5 60 (Concat w128 (w64 1) (w64 2)))])
 
 # RUN: grep -A 1 \"Query 2\" %t > %t2
-# RUN: grep \"Array 0:\ta.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0\" %t2
+# RUN: grep \"Array 0:\ta.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1\" %t2
 (query [(Eq 0x0102030405060708090A0B0C0D0E0F10 (ReadLSB w128 0 a))] 
        false 
        [] [a])
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-10-05 15:51:25 +0000