about summary refs log tree commit diff homepage
path: root/test/Feature
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2014-01-12 21:34:59 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2014-01-20 14:45:07 +0000
commit38a084fb50cfb38570d0194bb076805e4f752c99 (patch)
tree598b00ceae9e12773e61b6e6657d654afc00360e /test/Feature
parent313390c68fc808d5fe7cf746a7a65b1e018362dc (diff)
downloadklee-38a084fb50cfb38570d0194bb076805e4f752c99.tar.gz
Fixed many tests that make use of the file tool to check
a file created by KLEE exists. A big difference between
DejaGNU and llvm-lit is that in DejaGNU the working directory
is the test output directory (e.g. test/Feature/Output) but
in llvm-lit the working directory is the test directory
(e.g. test/Feature )

To fix this I have used the %T substitution variable for llvm-lit.

I have also improved some tests by using LLVM's FileCheck tool
and removing of hard coded constants for data type size in
some places.

This commit inevitably breaks running the tests under DejaGNU.
Although it is possible to hack by introducing the %T substitution
variable some tests would still be broken because the use of shell
pipes in DejaGNU doesn't seem to work properly. I could work around
this but it's really not worth the effort.
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