diff options
31 files changed, 123 insertions, 89 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 diff --git a/test/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c index b42e03bf..624329fc 100644 --- a/test/Runtime/POSIX/FD_Fail2.c +++ b/test/Runtime/POSIX/FD_Fail2.c @@ -1,12 +1,12 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: %klee --libc=uclibc --posix-runtime --search=dfs %t1.bc --sym-files 1 10 --max-fail 1 -// RUN: test -f klee-last/test000001.ktest -// RUN: test -f klee-last/test000002.ktest -// RUN: test -f klee-last/test000003.ktest -// RUN: test -f klee-last/test000004.ktest -// RUN: test -f klee-last/test000005.ktest -// RUN: test -f klee-last/test000006.ktest -// RUN: test -f klee-last/test000007.ktest +// RUN: test -f %T/klee-last/test000001.ktest +// RUN: test -f %T/klee-last/test000002.ktest +// RUN: test -f %T/klee-last/test000003.ktest +// RUN: test -f %T/klee-last/test000004.ktest +// RUN: test -f %T/klee-last/test000005.ktest +// RUN: test -f %T/klee-last/test000006.ktest +// RUN: test -f %T/klee-last/test000007.ktest #include <stdio.h> #include <assert.h> diff --git a/test/Runtime/POSIX/FilePerm.c b/test/Runtime/POSIX/FilePerm.c index d387c2a9..1346c09a 100644 --- a/test/Runtime/POSIX/FilePerm.c +++ b/test/Runtime/POSIX/FilePerm.c @@ -1,8 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: %klee --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log -// RUN: test -f klee-last/test000001.ktest -// RUN: test -f klee-last/test000002.ktest -// RUN: test -f klee-last/test000003.ktest +// RUN: test -f %T/klee-last/test000001.ktest +// RUN: test -f %T/klee-last/test000002.ktest +// RUN: test -f %T/klee-last/test000003.ktest #include <stdio.h> #include <sys/types.h> diff --git a/test/Runtime/POSIX/FreeArgv.c b/test/Runtime/POSIX/FreeArgv.c index ceec4de2..4d2e5b75 100644 --- a/test/Runtime/POSIX/FreeArgv.c +++ b/test/Runtime/POSIX/FreeArgv.c @@ -1,18 +1,22 @@ -// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc -// RUN: %klee --posix-runtime %t.bc --sym-args 1 1 1 -// RUN: test -f klee-last/test000001.free.err -// RUN: test -f klee-last/test000002.free.err -// RUN: test -f klee-last/test000003.free.err +// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t.bc +// RUN: %klee --posix-runtime %t.bc --sym-args 1 1 1 2>&1 | FileCheck %s +// RUN: test -f %T/klee-last/test000001.free.err +// RUN: test -f %T/klee-last/test000002.free.err +// RUN: test -f %T/klee-last/test000003.free.err int main(int argc, char **argv) { + // FIXME: Use FileCheck's CHECK-DAG to check source locations switch(klee_range(0, 3, "range")) { case 0: + // CHECK: free of global free(argv); break; case 1: + // CHECK: free of global free(argv[0]); break; case 2: + // CHECK: free of global free(argv[1]); break; } diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c index 293ee653..bd514d48 100644 --- a/test/Runtime/POSIX/Isatty.c +++ b/test/Runtime/POSIX/Isatty.c @@ -1,9 +1,9 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: %klee --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout 2>%t.log -// RUN: test -f klee-last/test000001.ktest -// RUN: test -f klee-last/test000002.ktest -// RUN: test -f klee-last/test000003.ktest -// RUN: test -f klee-last/test000004.ktest +// RUN: test -f %T/klee-last/test000001.ktest +// RUN: test -f %T/klee-last/test000002.ktest +// RUN: test -f %T/klee-last/test000003.ktest +// RUN: test -f %T/klee-last/test000004.ktest // RUN: grep -q "stdin is a tty" %t.log // RUN: grep -q "stdin is NOT a tty" %t.log // RUN: grep -q "stdout is a tty" %t.log @@ -15,16 +15,21 @@ #include <stdio.h> #include <assert.h> +// FIXME: Use new FileCheck to check klee's output int main(int argc, char** argv) { int fd0 = 0; // stdin int fd1 = 1; // stdout int r = isatty(fd0); + // CHECK-DAG: stdin is a tty + // CHECK-DAG: stdin is NOT a tty if (r) fprintf(stderr, "stdin is a tty\n"); else fprintf(stderr, "stdin is NOT a tty\n"); r = isatty(fd1); + // CHECK-DAG: stdout is a tty + // CHECK-DAG: stdout is NOT a tty if (r) fprintf(stderr, "stdout is a tty\n"); else fprintf(stderr, "stdout is NOT a tty\n"); diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c index d417ee47..3c17f976 100644 --- a/test/Runtime/POSIX/Openat.c +++ b/test/Runtime/POSIX/Openat.c @@ -1,6 +1,6 @@ // 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 +// RUN: test -f %T/klee-last/test000001.ktest #include <assert.h> #include <fcntl.h> diff --git a/test/Runtime/POSIX/PrgName.c b/test/Runtime/POSIX/PrgName.c index dc6a4b8c..6bc682ca 100644 --- a/test/Runtime/POSIX/PrgName.c +++ b/test/Runtime/POSIX/PrgName.c @@ -1,7 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc // RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-arg 10 >%t.log -// RUN: test -f klee-last/test000001.ktest -// RUN: test -f klee-last/test000002.ktest +// RUN: test -f %T/klee-last/test000001.ktest +// RUN: test -f %T/klee-last/test000002.ktest // RUN: grep -q "No" %t.log // RUN: grep -qv "Yes" %t.log diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c index 740db664..d9bd7f8d 100644 --- a/test/Runtime/POSIX/SeedAndFail.c +++ b/test/Runtime/POSIX/SeedAndFail.c @@ -1,8 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc -// RUN: rm -rf tmp-123 -// 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 +// RUN: rm -rf %T/tmp-123 +// RUN: %klee --libc=uclibc --output-dir=%T/tmp-123 --posix-runtime %t.bc --sym-files 1 10 2>%t.log +// RUN: %klee --seed-out-dir=%T/tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1 +// RUN: ls %T/klee-last | grep -c assert | grep 4 #include <string.h> #include <assert.h> diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.pc index 53ff3a51..e0921393 100644 --- a/test/Solver/LargeIntegers.pc +++ b/test/Solver/LargeIntegers.pc @@ -2,16 +2,16 @@ array a[64] : w32 -> w8 = symbolic -# RUN: grep -A 1 \"Query 0\" %t > %t2 -# RUN: grep \"Expr 0:\t18446744073709551618\" %t2 +# RUN: grep -A 1 "Query 0" %t > %t2 +# RUN: grep "Expr 0: 18446744073709551618" %t2 (query [] false [(Concat w128 (w64 1) (w64 2))]) -# RUN: grep -A 1 \"Query 1\" %t > %t2 -# RUN: grep \"Expr 0:\t16\" %t2 +# RUN: grep -A 1 "Query 1" %t > %t2 +# RUN: grep "Expr 0: 16" %t2 (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\" %t2 +# RUN: grep -A 1 "Query 2" %t > %t2 +# RUN: grep "Array 0: a.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]) diff --git a/test/regression/2007-10-11-free-of-alloca.c b/test/regression/2007-10-11-free-of-alloca.c index 71a16f6b..44a9ed4e 100644 --- a/test/regression/2007-10-11-free-of-alloca.c +++ b/test/regression/2007-10-11-free-of-alloca.c @@ -1,9 +1,10 @@ -// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc -// RUN: test -f klee-last/test000001.free.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.free.err int main() { int buf[4]; + // CHECK: 2007-10-11-free-of-alloca.c:8: free of alloca free(buf); // this should give runtime error, not crash return 0; } diff --git a/test/regression/2007-10-11-illegal-access-after-free-and-branch.c b/test/regression/2007-10-11-illegal-access-after-free-and-branch.c index fbbb99c3..73b3ed3f 100644 --- a/test/regression/2007-10-11-illegal-access-after-free-and-branch.c +++ b/test/regression/2007-10-11-illegal-access-after-free-and-branch.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee --optimize %t1.bc -// RUN: test -f klee-last/test000001.ptr.err +// RUN: %klee --optimize %t1.bc 2>&1 | FileCheck %s +// RUN: test -f %T/klee-last/test000001.ptr.err #include <stdlib.h> #include <stdio.h> @@ -13,7 +13,10 @@ int main(int argc, char **argv) { unsigned char x = buf[1]; free(buf); if (x) + { + // CHECK: 2007-10-11-illegal-access-after-free-and-branch.c:18: memory error: out of bound pointer return buf[2]; + } klee_silent_exit(0); return 0; } diff --git a/test/regression/2008-03-04-free-of-global.c b/test/regression/2008-03-04-free-of-global.c index 7821398d..5351128d 100644 --- a/test/regression/2008-03-04-free-of-global.c +++ b/test/regression/2008-03-04-free-of-global.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.free.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.free.err int buf[4]; int main() { + // CHECK: 2008-03-04-free-of-global.c:9: free of global free(buf); // this should give runtime error, not crash return 0; } |