about summary refs log tree commit diff homepage
path: root/test/Feature
diff options
context:
space:
mode:
Diffstat (limited to 'test/Feature')
-rw-r--r--test/Feature/CallToUndefinedExternal.cpp5
-rw-r--r--test/Feature/DanglingConcreteReadExpr.c2
-rw-r--r--test/Feature/DoubleFree.c5
-rw-r--r--test/Feature/DumpStatesOnHalt.c5
-rw-r--r--test/Feature/ExprLogging.c8
-rw-r--r--test/Feature/InAndOutOfBounds.c14
-rw-r--r--test/Feature/IntrinsicTrap.ll8
-rw-r--r--test/Feature/KleeReportError.c9
-rw-r--r--test/Feature/LowerSwitch.c4
-rw-r--r--test/Feature/MakeConcreteSymbolic.c4
-rw-r--r--test/Feature/MultipleFreeResolution.c13
-rw-r--r--test/Feature/MultipleReallocResolution.c4
-rw-r--r--test/Feature/OneFreeError.c8
-rw-r--r--test/Feature/OneOutOfBounds.c10
-rw-r--r--test/Feature/OverlappedError.c4
-rw-r--r--test/Feature/PreferCex.c3
-rw-r--r--test/Feature/Realloc.c4
-rw-r--r--test/Feature/ReplayPath.c2
-rw-r--r--test/Feature/Vararg.c2
-rw-r--r--test/Feature/WriteCov.c4
20 files changed, 69 insertions, 49 deletions
diff --git a/test/Feature/CallToUndefinedExternal.cpp b/test/Feature/CallToUndefinedExternal.cpp
index 84b5a3b4..26e8fc55 100644
--- a/test/Feature/CallToUndefinedExternal.cpp
+++ b/test/Feature/CallToUndefinedExternal.cpp
@@ -1,10 +1,11 @@
 // RUN: %llvmgxx %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.external.err
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.external.err
 
 extern "C" void poof(void);
 
 int main() {
+  // CHECK: failed external call: poof
   poof();
 
   return 0;
diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c
index 1bf44c3f..204187a2 100644
--- a/test/Feature/DanglingConcreteReadExpr.c
+++ b/test/Feature/DanglingConcreteReadExpr.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc
-// RUN: grep "total queries = 2" klee-last/info
+// RUN: grep "total queries = 2" %T/klee-last/info
 
 #include <assert.h>
 
diff --git a/test/Feature/DoubleFree.c b/test/Feature/DoubleFree.c
index 3727ef2b..d97e0c08 100644
--- a/test/Feature/DoubleFree.c
+++ b/test/Feature/DoubleFree.c
@@ -1,10 +1,11 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 int main() {
   int *x = malloc(4);
   free(x);
+  // CHECK: memory error: invalid pointer: free
   free(x);
   return 0;
 }
diff --git a/test/Feature/DumpStatesOnHalt.c b/test/Feature/DumpStatesOnHalt.c
index d86b786b..c65d5568 100644
--- a/test/Feature/DumpStatesOnHalt.c
+++ b/test/Feature/DumpStatesOnHalt.c
@@ -1,8 +1,9 @@
 // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc
-// RUN: test -f klee-last/test000001.ktest
+// RUN: %klee --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ktest
 
 int main() {
   int x = 10;
   return x;
 }
+// CHECK: halting execution, dumping remaining states
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index 9e9df87a..abab8031 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -1,14 +1,14 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
 // 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 %T/klee-last/all-queries.pc > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
-// RUN: %kleaver -print-ast klee-last/solver-queries.pc > %t3.log
+// RUN: %kleaver -print-ast %T/klee-last/solver-queries.pc > %t3.log
 // 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 17
+// RUN: grep "^; Query" %T/klee-last/all-queries.smt2 | wc -l | grep -q 17
+// RUN: grep "^; Query" %T/klee-last/solver-queries.smt2 | wc -l | grep -q 17
 
 #include <assert.h>
 
diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c
index ba655b83..3a559075 100644
--- a/test/Feature/InAndOutOfBounds.c
+++ b/test/Feature/InAndOutOfBounds.c
@@ -1,8 +1,8 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err -o -f klee-last/test000002.ptr.err 
-// RUN: test ! -f klee-last/test000001.ptr.err -o ! -f klee-last/test000002.ptr.err 
-// RUN: test ! -f klee-last/test000003.ktest
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err -o -f %T/klee-last/test000002.ptr.err 
+// RUN: test ! -f %T/klee-last/test000001.ptr.err -o ! -f %T/klee-last/test000002.ptr.err 
+// RUN: test ! -f %T/klee-last/test000003.ktest
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
@@ -12,7 +12,9 @@ unsigned klee_urange(unsigned start, unsigned end) {
 }
 
 int main() {
-  int *x = malloc(4);
+  int *x = malloc(sizeof(int));
+  // FIXME: Use newer FileCheck syntax to support relative line numbers
+  // CHECK: InAndOutOfBounds.c:18: memory error: out of bound pointer
   x[klee_urange(0,2)] = 1;
   free(x);
   return 0;
diff --git a/test/Feature/IntrinsicTrap.ll b/test/Feature/IntrinsicTrap.ll
index 5af46225..13b93e4d 100644
--- a/test/Feature/IntrinsicTrap.ll
+++ b/test/Feature/IntrinsicTrap.ll
@@ -1,8 +1,6 @@
 ; 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
+; RUN: FileCheck %s --input-file=%T/klee-last/assembly.ll
 
 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"
@@ -15,6 +13,8 @@ entry:
   br i1 %c, label %btrue, label %bfalse
 
 btrue:
+  ; CHECK-NOT: call void @llvm.trap()
+  ; CHECK: call void @abort()
   call void @llvm.trap() noreturn nounwind
   unreachable
 
@@ -25,4 +25,6 @@ return:
   ret i32 0
 }
 
+; CHECK-NOT: call void @llvm.trap()
+; CHECK: declare void @abort()
 declare void @llvm.trap() noreturn nounwind
diff --git a/test/Feature/KleeReportError.c b/test/Feature/KleeReportError.c
index dda72fd0..37c07ed1 100644
--- a/test/Feature/KleeReportError.c
+++ b/test/Feature/KleeReportError.c
@@ -1,6 +1,6 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --emit-all-errors %t2.bc > %t3.log
-// RUN: ls klee-last/ | grep .my.err | wc -l | grep 2
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --emit-all-errors %t2.bc 2>&1 | FileCheck %s
+// RUN: ls %T/klee-last/ | grep .my.err | wc -l | grep 2
 #include <stdio.h>
 #include <assert.h>
 
@@ -16,6 +16,9 @@ int main(int argc, char** argv) {
 
   if (y) {
     fprintf(stderr, "My error\n");
+    // CHECK: KleeReportError.c:22: My error
+    // CHECK: KleeReportError.c:22: My error
+    // FIXME: Use FileCheck's relative line number syntax
     klee_report_error(__FILE__, __LINE__, "My error", "my.err");
   }
 
diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c
index 1b92e398..49cad076 100644
--- a/test/Feature/LowerSwitch.c
+++ b/test/Feature/LowerSwitch.c
@@ -1,8 +1,8 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc
 // RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc
-// RUN: not test -f klee-last/test000010.ktest
+// RUN: not test -f %T/klee-last/test000010.ktest
 // RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc
-// RUN: test -f klee-last/test000010.ktest
+// RUN: test -f %T/klee-last/test000010.ktest
 
 #include <stdio.h>
 
diff --git a/test/Feature/MakeConcreteSymbolic.c b/test/Feature/MakeConcreteSymbolic.c
index 29b43a04..bfbb807d 100644
--- a/test/Feature/MakeConcreteSymbolic.c
+++ b/test/Feature/MakeConcreteSymbolic.c
@@ -1,8 +1,8 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
 // RUN: %klee --exit-on-error %t1.bc
-// RUN: grep "done: total queries = 0" klee-last/info
+// RUN: grep "done: total queries = 0" %T/klee-last/info
 // RUN: %klee --make-concrete-symbolic=1 --exit-on-error %t1.bc
-// RUN: grep "done: total queries = 2" klee-last/info
+// RUN: grep "done: total queries = 2" %T/klee-last/info
 
 
 #include <assert.h>
diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c
index 8a36f459..cd8a383b 100644
--- a/test/Feature/MultipleFreeResolution.c
+++ b/test/Feature/MultipleFreeResolution.c
@@ -1,7 +1,7 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --emit-all-errors %t1.bc
-// RUN: ls klee-last/ | grep .ktest | wc -l | grep 4
-// RUN: ls klee-last/ | grep .err | wc -l | grep 3
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --emit-all-errors %t1.bc 2>&1 | FileCheck %s
+// RUN: ls %T/klee-last/ | grep .ktest | wc -l | grep 4
+// RUN: ls %T/klee-last/ | grep .err | wc -l | grep 3
 
 #include <stdlib.h>
 #include <stdio.h>
@@ -31,9 +31,14 @@ int main() {
 
   free(buf[s]);
 
+  // CHECK: MultipleFreeResolution.c:39: memory error: out of bound pointer
+  // CHECK: MultipleFreeResolution.c:39: memory error: out of bound pointer
+  // CHECK: MultipleFreeResolution.c:39: memory error: out of bound pointer
+  // FIXME: Use FileCheck's relative line numbers
   for (i=0; i<3; i++) {
     printf("*buf[%d] = %d\n", i, *buf[i]);
   }
 
   return 0;
 }
+// CHECK: KLEE: done: generated tests = 4
diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c
index b1a14ace..1f77485f 100644
--- a/test/Feature/MultipleReallocResolution.c
+++ b/test/Feature/MultipleReallocResolution.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc
-// RUN: ls klee-last/ | grep .err | wc -l | grep 2
-// RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2
+// RUN: ls %T/klee-last/ | grep .err | wc -l | grep 2
+// RUN: ls %T/klee-last/ | grep .ptr.err | wc -l | grep 2
 
 #include <assert.h>
 #include <stdlib.h>
diff --git a/test/Feature/OneFreeError.c b/test/Feature/OneFreeError.c
index 8eb13298..e83b535a 100644
--- a/test/Feature/OneFreeError.c
+++ b/test/Feature/OneFreeError.c
@@ -1,10 +1,12 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 int main() {
   int *x = malloc(4);
   free(x);
+  // CHECK: OneFreeError.c:10: memory error: out of bound pointer
+  // FIXME: Use FileCheck's relative line numbers
   x[0] = 1;
   return 0;
 }
diff --git a/test/Feature/OneOutOfBounds.c b/test/Feature/OneOutOfBounds.c
index 11a9eecb..72d36b70 100644
--- a/test/Feature/OneOutOfBounds.c
+++ b/test/Feature/OneOutOfBounds.c
@@ -1,9 +1,11 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 int main() {
-  int *x = malloc(4);
+  int *x = malloc(sizeof(int));
+  // CHECK: OneOutOfBounds.c:9: memory error: out of bound pointer
+  // FIXME: Use FileCheck's relative line numbers
   x[1] = 1;
   free(x);
   return 0;
diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c
index aa220ed9..886c7ec8 100644
--- a/test/Feature/OverlappedError.c
+++ b/test/Feature/OverlappedError.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc
-// RUN: ls klee-last/ | grep .ktest | wc -l | grep 4
-// RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2
+// RUN: ls %T/klee-last/ | grep .ktest | wc -l | grep 4
+// RUN: ls %T/klee-last/ | grep .ptr.err | wc -l | grep 2
 
 #include <stdlib.h>
 
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
index 97ce5101..6cdb8446 100644
--- a/test/Feature/PreferCex.c
+++ b/test/Feature/PreferCex.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee --exit-on-error %t1.bc
-// RUN: ktest-tool klee-last/test000001.ktest | grep -F 'Hi\x00\x00'
+// RUN: ktest-tool %T/klee-last/test000001.ktest | FileCheck %s
 
 #include <assert.h>
 #include <stdlib.h>
@@ -10,6 +10,7 @@ int main() {
   char buf[4];
 
   klee_make_symbolic(buf, sizeof buf);
+  // CHECK: Hi\x00\x00
   klee_prefer_cex(buf, buf[0]=='H');
   klee_prefer_cex(buf, buf[1]=='i');
   klee_prefer_cex(buf, buf[2]=='\0');
diff --git a/test/Feature/Realloc.c b/test/Feature/Realloc.c
index a47adad6..62aa170b 100644
--- a/test/Feature/Realloc.c
+++ b/test/Feature/Realloc.c
@@ -1,6 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --exit-on-error %t1.bc
-// RUN: grep "KLEE: WARNING ONCE: Large alloc" klee-last/warnings.txt
+// RUN: %klee --exit-on-error %t1.bc 2>&1 | FileCheck %s
 
 #include <assert.h>
 #include <stdlib.h>
@@ -11,6 +10,7 @@ int main() {
   assert(p);
   p[1] = 52;
 
+  // CHECK: KLEE: WARNING ONCE: Large alloc
   int *p2 = realloc(p, 1<<30);
   assert(p2[1] == 52);
 
diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c
index f88ad6dc..ccf59657 100644
--- a/test/Feature/ReplayPath.c
+++ b/test/Feature/ReplayPath.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -DCOND_EXIT -c -o %t1.bc
 // RUN: klee --write-paths %t1.bc > %t3.good
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --replay-path klee-last/test000001.path %t2.bc >%t3.log
+// RUN: %klee --replay-path %T/klee-last/test000001.path %t2.bc > %t3.log
 // RUN: diff %t3.log %t3.good
 
 #include <unistd.h>
diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c
index 9f6643bc..31eee235 100644
--- a/test/Feature/Vararg.c
+++ b/test/Feature/Vararg.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc > %t2.out
 // RUN: grep "types: (52, 37, 2.00, (9,12,15))" %t2.out
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 #include <stdarg.h>
 #include <assert.h>
diff --git a/test/Feature/WriteCov.c b/test/Feature/WriteCov.c
index bb2d64e8..45e7bc43 100644
--- a/test/Feature/WriteCov.c
+++ b/test/Feature/WriteCov.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t2.bc
 // RUN: %klee --exit-on-error --write-cov %t2.bc
-// RUN: grep -c WriteCov.c:15  klee-last/test000001.cov klee-last/test000002.cov  >%t3.txt
-// RUN: grep -c WriteCov.c:17  klee-last/test000001.cov klee-last/test000002.cov >>%t3.txt
+// RUN: grep -c WriteCov.c:15  %T/klee-last/test000001.cov %T/klee-last/test000002.cov  >%t3.txt
+// RUN: grep -c WriteCov.c:17  %T/klee-last/test000001.cov %T/klee-last/test000002.cov >>%t3.txt
 // RUN: grep klee-last/test000001.cov:0 %t3.txt
 // RUN: grep klee-last/test000001.cov:1 %t3.txt
 // RUN: grep klee-last/test000002.cov:0 %t3.txt
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-23 03:29:06 +0000