diff options
Diffstat (limited to 'test/Feature')
66 files changed, 239 insertions, 146 deletions
diff --git a/test/Feature/Alias.c b/test/Feature/Alias.c index 9300e2c7..381bcc2a 100644 --- a/test/Feature/Alias.c +++ b/test/Feature/Alias.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc // Darwin does not have strong aliases. // XFAIL: darwin diff --git a/test/Feature/AliasFunction.c b/test/Feature/AliasFunction.c index 176b152e..019ebe67 100644 --- a/test/Feature/AliasFunction.c +++ b/test/Feature/AliasFunction.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc > %t1.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log // RUN: grep -c foo %t1.log | grep 5 // RUN: grep -c bar %t1.log | grep 4 diff --git a/test/Feature/AliasFunctionExit.c b/test/Feature/AliasFunctionExit.c index acfa4350..09ca8f46 100644 --- a/test/Feature/AliasFunctionExit.c +++ b/test/Feature/AliasFunctionExit.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc > %t1.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log // RUN: grep -c START %t1.log | grep 1 // RUN: grep -c END %t1.log | grep 2 diff --git a/test/Feature/AsmAddresses.c b/test/Feature/AsmAddresses.c index d0b89ef1..cfe566af 100644 --- a/test/Feature/AsmAddresses.c +++ b/test/Feature/AsmAddresses.c @@ -1,7 +1,10 @@ // RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s -// RUN: %klee --exit-on-error --use-asm-addresses %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --use-asm-addresses %t.bc + // RUN: %llvmgcc -emit-llvm -DOVERLAP -g -c -o %t.bc %s -// RUN: not %klee --exit-on-error --use-asm-addresses %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --use-asm-addresses %t.bc #include <assert.h> diff --git a/test/Feature/BitcastAlias.ll b/test/Feature/BitcastAlias.ll index 711ed7ad..e0e3653f 100644 --- a/test/Feature/BitcastAlias.ll +++ b/test/Feature/BitcastAlias.ll @@ -1,5 +1,6 @@ ; RUN: llvm-as %s -f -o %t1.bc -; RUN: %klee -disable-opt %t1.bc > %t2 +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 ; RUN: grep PASS %t2 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-n8:16:32:64" diff --git a/test/Feature/ByteSwap.c b/test/Feature/ByteSwap.c index f85ac3b1..b6500a13 100644 --- a/test/Feature/ByteSwap.c +++ b/test/Feature/ByteSwap.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --libc=klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=klee --exit-on-error %t1.bc #include <arpa/inet.h> #include <assert.h> diff --git a/test/Feature/CallToUndefinedExternal.cpp b/test/Feature/CallToUndefinedExternal.cpp index 26e8fc55..b300d4e4 100644 --- a/test/Feature/CallToUndefinedExternal.cpp +++ b/test/Feature/CallToUndefinedExternal.cpp @@ -1,6 +1,7 @@ // RUN: %llvmgxx %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee %t1.bc 2>&1 | FileCheck %s -// RUN: test -f %T/klee-last/test000001.external.err +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s +// RUN: test -f %t.klee-out/test000001.external.err extern "C" void poof(void); diff --git a/test/Feature/CheckForImpliedValue.c.failing b/test/Feature/CheckForImpliedValue.c.failing index 7a088354..bb643647 100644 --- a/test/Feature/CheckForImpliedValue.c.failing +++ b/test/Feature/CheckForImpliedValue.c.failing @@ -1,6 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -f %t1.log -// RUN: %klee --log-file %t1.log --debug-check-for-implied-values %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --log-file %t1.log --debug-check-for-implied-values %t1.bc // RUN: grep "= 0 (ok)" %t1.log // RUN: grep "= 2 (missed)" %t1.log diff --git a/test/Feature/CheckMemoryAccess.c b/test/Feature/CheckMemoryAccess.c index 30590f88..5347ac3d 100644 --- a/test/Feature/CheckMemoryAccess.c +++ b/test/Feature/CheckMemoryAccess.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc -// RUN: %klee %t.bc > %t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log // RUN: grep -q "good" %t.log // RUN: not grep -q "bad" %t.log diff --git a/test/Feature/ConstantStruct.ll b/test/Feature/ConstantStruct.ll index cfd7104e..4fe6b5d0 100644 --- a/test/Feature/ConstantStruct.ll +++ b/test/Feature/ConstantStruct.ll @@ -1,5 +1,6 @@ ; RUN: llvm-as %s -f -o %t1.bc -; RUN: %klee -disable-opt %t1.bc > %t2 +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 ; RUN: grep PASS %t2 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-n8:16:32:64" diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c index ce77c802..926e0a48 100644 --- a/test/Feature/CopyOnWrite.c +++ b/test/Feature/CopyOnWrite.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee --search=random-state --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=random-state --exit-on-error %t1.bc #include <assert.h> diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c index 204187a2..8e15b07d 100644 --- a/test/Feature/DanglingConcreteReadExpr.c +++ b/test/Feature/DanglingConcreteReadExpr.c @@ -1,6 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc -// RUN: grep "total queries = 2" %T/klee-last/info +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc +// RUN: grep "total queries = 2" %t.klee-out/info #include <assert.h> diff --git a/test/Feature/DefineFixedObject.c b/test/Feature/DefineFixedObject.c index 9f71f89b..2e601553 100644 --- a/test/Feature/DefineFixedObject.c +++ b/test/Feature/DefineFixedObject.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc -emit-llvm -c -o %t1.bc %s -// RUN: %klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc #include <stdio.h> diff --git a/test/Feature/DoubleFree.c b/test/Feature/DoubleFree.c index d97e0c08..b24de17d 100644 --- a/test/Feature/DoubleFree.c +++ b/test/Feature/DoubleFree.c @@ -1,6 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc 2>&1 | FileCheck %s -// RUN: test -f %T/klee-last/test000001.ptr.err +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s +// RUN: test -f %t.klee-out/test000001.ptr.err int main() { int *x = malloc(4); diff --git a/test/Feature/DumpStatesOnHalt.c b/test/Feature/DumpStatesOnHalt.c index 993fdb6a..bc302456 100644 --- a/test/Feature/DumpStatesOnHalt.c +++ b/test/Feature/DumpStatesOnHalt.c @@ -1,6 +1,7 @@ // 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 2>&1 | FileCheck %s -// RUN: test -f %T/klee-last/test000001.ktest +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck %s +// RUN: test -f %t.klee-out/test000001.ktest int main(int argc, char** argv) { int x = 1; diff --git a/test/Feature/Envp.c b/test/Feature/Envp.c index f1f62a72..ff4e2098 100644 --- a/test/Feature/Envp.c +++ b/test/Feature/Envp.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc #include <assert.h> diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index abab8031..bba0570e 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -1,14 +1,15 @@ // 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 %T/klee-last/all-queries.pc > %t3.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --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 %t.klee-out/all-queries.pc > %t3.log // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log -// RUN: %kleaver -print-ast %T/klee-last/solver-queries.pc > %t3.log +// RUN: %kleaver -print-ast %t.klee-out/solver-queries.pc > %t3.log // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log -// 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 +// RUN: grep "^; Query" %t.klee-out/all-queries.smt2 | wc -l | grep -q 17 +// RUN: grep "^; Query" %t.klee-out/solver-queries.smt2 | wc -l | grep -q 17 #include <assert.h> diff --git a/test/Feature/ExternalWeakLinkage.c b/test/Feature/ExternalWeakLinkage.c index c2008136..fd70884a 100644 --- a/test/Feature/ExternalWeakLinkage.c +++ b/test/Feature/ExternalWeakLinkage.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc #include <assert.h> diff --git a/test/Feature/Float.c b/test/Feature/Float.c index f7e4dde0..dce082c6 100644 --- a/test/Feature/Float.c +++ b/test/Feature/Float.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc -// RUN: %klee %t.bc > %t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log // RUN: grep "3.30* -1.10* 2.420*" %t.log #include <stdio.h> diff --git a/test/Feature/FloatingPt.c b/test/Feature/FloatingPt.c index bde9e19b..be087935 100644 --- a/test/Feature/FloatingPt.c +++ b/test/Feature/FloatingPt.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc #include <assert.h> diff --git a/test/Feature/FunctionPointer.c b/test/Feature/FunctionPointer.c index e1ae1e37..ac28ca00 100644 --- a/test/Feature/FunctionPointer.c +++ b/test/Feature/FunctionPointer.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee --no-output --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error %t1.bc #include <stdio.h> diff --git a/test/Feature/GetElementPtr.ll b/test/Feature/GetElementPtr.ll index 7f10c0a2..da94441c 100644 --- a/test/Feature/GetElementPtr.ll +++ b/test/Feature/GetElementPtr.ll @@ -1,5 +1,6 @@ ; RUN: llvm-as %s -f -o %t1.bc -; RUN: %klee -disable-opt %t1.bc > %t2 +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 ; RUN: grep PASS %t2 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-n8:16:32:64" diff --git a/test/Feature/GetValue.c b/test/Feature/GetValue.c index 5023c51c..828c8934 100644 --- a/test/Feature/GetValue.c +++ b/test/Feature/GetValue.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc -emit-llvm -c -o %t1.bc %s -// RUN: %klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc #include <stdio.h> #include <assert.h> diff --git a/test/Feature/ImpliedValue.c.failing b/test/Feature/ImpliedValue.c.failing index 2f169970..469c8f28 100644 --- a/test/Feature/ImpliedValue.c.failing +++ b/test/Feature/ImpliedValue.c.failing @@ -2,8 +2,9 @@ // RUN: %llvmgcc %s -emit-llvm -O2 -c -o %t1.bc // RUN: llvm-as -f ../_utils._ll -o %t2.bc // RUN: llvm-ld -disable-opt -link-as-library %t1.bc %t2.bc -o %t3.bc -// RUN: %klee --log-file %t4.log --debug-check-for-implied-values %t3.bc > %t4.out 2> %t4.err -// RUN: ls klee-last | not grep .err +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --log-file %t4.log --debug-check-for-implied-values %t3.bc > %t4.out 2> %t4.err +// RUN: ls %t.klee-out | not grep .err // RUN: not grep "(missed)" %t4.log #include <assert.h> diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c index 729d6b78..5a3dfa44 100644 --- a/test/Feature/InAndOutOfBounds.c +++ b/test/Feature/InAndOutOfBounds.c @@ -1,8 +1,9 @@ // 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: not test -f %T/klee-last/test000001.ptr.err -a -f %T/klee-last/test000002.ptr.err -// RUN: not test -f %T/klee-last/test000003.ktest +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s +// RUN: test -f %t.klee-out/test000001.ptr.err -o -f %t.klee-out/test000002.ptr.err +// RUN: not test -f %t.klee-out/test000001.ptr.err -a -f %t.klee-out/test000002.ptr.err +// RUN: not test -f %t.klee-out/test000003.ktest unsigned klee_urange(unsigned start, unsigned end) { unsigned x; @@ -14,7 +15,7 @@ unsigned klee_urange(unsigned start, unsigned end) { int main() { 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 + // CHECK: InAndOutOfBounds.c:19: memory error: out of bound pointer x[klee_urange(0,2)] = 1; free(x); return 0; diff --git a/test/Feature/IndirectCallToBuiltin.c b/test/Feature/IndirectCallToBuiltin.c index 591a5601..8c78dba5 100644 --- a/test/Feature/IndirectCallToBuiltin.c +++ b/test/Feature/IndirectCallToBuiltin.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc #include <stdlib.h> #include <stdio.h> diff --git a/test/Feature/IndirectCallToExternal.c b/test/Feature/IndirectCallToExternal.c index 4603213b..58eb2575 100644 --- a/test/Feature/IndirectCallToExternal.c +++ b/test/Feature/IndirectCallToExternal.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc #include <stdlib.h> #include <stdio.h> diff --git a/test/Feature/InsertExtractValue.ll b/test/Feature/InsertExtractValue.ll index fbce335b..83e8f851 100644 --- a/test/Feature/InsertExtractValue.ll +++ b/test/Feature/InsertExtractValue.ll @@ -1,5 +1,6 @@ ; RUN: llvm-as %s -f -o %t1.bc -; RUN: %klee -disable-opt %t1.bc > %t2 +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 ; RUN: grep PASS %t2 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-n8:16:32:64" diff --git a/test/Feature/IntrinsicTrap.ll b/test/Feature/IntrinsicTrap.ll index 13b93e4d..9caf4a62 100644 --- a/test/Feature/IntrinsicTrap.ll +++ b/test/Feature/IntrinsicTrap.ll @@ -1,6 +1,7 @@ ; RUN: llvm-as %s -f -o %t1.bc -; RUN: %klee -disable-opt %t1.bc -; RUN: FileCheck %s --input-file=%T/klee-last/assembly.ll +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc +; RUN: FileCheck %s --input-file=%t.klee-out/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" diff --git a/test/Feature/InvalidBitfieldAccess.c.failing b/test/Feature/InvalidBitfieldAccess.c.failing index ae8bfe5e..0e4ec594 100644 --- a/test/Feature/InvalidBitfieldAccess.c.failing +++ b/test/Feature/InvalidBitfieldAccess.c.failing @@ -1,5 +1,6 @@ // RUN: %llvmgcc -c -o %t1.bc %s -// RUN: %klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc // This is a bug in llvm-gcc4.0 but seems to be fixed in llvm-gcc4.2, // its included here mostly as a reminder. diff --git a/test/Feature/IsSymbolic.c b/test/Feature/IsSymbolic.c index 4a86368a..cd7f3dba 100644 --- a/test/Feature/IsSymbolic.c +++ b/test/Feature/IsSymbolic.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc #include <assert.h> diff --git a/test/Feature/KleeReportError.c b/test/Feature/KleeReportError.c index 37c07ed1..50aaf97d 100644 --- a/test/Feature/KleeReportError.c +++ b/test/Feature/KleeReportError.c @@ -1,6 +1,7 @@ // 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 +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s +// RUN: ls %t.klee-out/ | grep .my.err | wc -l | grep 2 #include <stdio.h> #include <assert.h> @@ -16,8 +17,8 @@ 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 + // CHECK: KleeReportError.c:23: My error + // CHECK: KleeReportError.c:23: My error // FIXME: Use FileCheck's relative line number syntax klee_report_error(__FILE__, __LINE__, "My error", "my.err"); } diff --git a/test/Feature/LargeReturnTypes.cpp b/test/Feature/LargeReturnTypes.cpp index 274da05e..937b0758 100644 --- a/test/Feature/LargeReturnTypes.cpp +++ b/test/Feature/LargeReturnTypes.cpp @@ -1,5 +1,6 @@ // RUN: %llvmgxx -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s -// RUN: %klee --libc=klee --no-output --exit-on-error %t.bc > %t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log /* Tests the ability to call external functions which return large values * (i.e. structs). In this test case, fstream::ftellg() returns a diff --git a/test/Feature/LongDouble.cpp b/test/Feature/LongDouble.cpp index 6e6baf6a..08924293 100644 --- a/test/Feature/LongDouble.cpp +++ b/test/Feature/LongDouble.cpp @@ -1,5 +1,6 @@ // RUN: %llvmgxx -I../../../include -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s -// RUN: %klee --libc=klee --no-output --exit-on-error %t.bc > %t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log // RUN: grep -q powl\(-11\\.0,0\)=1\\.0\\+ %t.log // RUN: grep -q powl\(-11\\.0,1\)=-11\\.0\\+ %t.log // RUN: grep -q powl\(-11\\.0,2\)=121\\.0\\+ %t.log diff --git a/test/Feature/LongDoubleSupport.c b/test/Feature/LongDoubleSupport.c index 185a5485..4ea9daee 100644 --- a/test/Feature/LongDoubleSupport.c +++ b/test/Feature/LongDoubleSupport.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --optimize=0 --exit-on-error %t1.bc > %t2.out +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --optimize=0 --exit-on-error %t1.bc > %t2.out #include <stdio.h> #include <float.h> diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c index 49cad076..1b280e72 100644 --- a/test/Feature/LowerSwitch.c +++ b/test/Feature/LowerSwitch.c @@ -1,8 +1,11 @@ // 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 %T/klee-last/test000010.ktest -// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc -// RUN: test -f %T/klee-last/test000010.ktest +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc +// RUN: not test -f %t.klee-out/test000010.ktest + +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc +// RUN: test -f %t.klee-out/test000010.ktest #include <stdio.h> diff --git a/test/Feature/MakeConcreteSymbolic.c b/test/Feature/MakeConcreteSymbolic.c index bfbb807d..dad618b3 100644 --- a/test/Feature/MakeConcreteSymbolic.c +++ b/test/Feature/MakeConcreteSymbolic.c @@ -1,8 +1,11 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc -// 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" %T/klee-last/info +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc +// RUN: grep "done: total queries = 0" %t.klee-out/info + +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --make-concrete-symbolic=1 --exit-on-error %t1.bc +// RUN: grep "done: total queries = 2" %t.klee-out/info #include <assert.h> diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c index a31b4a9b..fef731ab 100644 --- a/test/Feature/MakeSymbolicName.c +++ b/test/Feature/MakeSymbolicName.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc -// RUN: %klee --search=random-state --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=random-state --exit-on-error %t1.bc #include <assert.h> diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index a3c1250e..8837e2e5 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -1,7 +1,9 @@ // RUN: %llvmgcc -emit-llvm -DLITTLE_ALLOC -g -c %s -o %t.little.bc // RUN: %llvmgcc -emit-llvm -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: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --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 diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c index cd8a383b..3216de95 100644 --- a/test/Feature/MultipleFreeResolution.c +++ b/test/Feature/MultipleFreeResolution.c @@ -1,7 +1,8 @@ // 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 +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --emit-all-errors %t1.bc 2>&1 | FileCheck %s +// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 4 +// RUN: ls %t.klee-out/ | grep .err | wc -l | grep 3 #include <stdlib.h> #include <stdio.h> @@ -31,9 +32,9 @@ 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 + // CHECK: MultipleFreeResolution.c:40: memory error: out of bound pointer + // CHECK: MultipleFreeResolution.c:40: memory error: out of bound pointer + // CHECK: MultipleFreeResolution.c:40: 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]); diff --git a/test/Feature/MultipleReadResolution.c b/test/Feature/MultipleReadResolution.c index 9297cf8d..af42c012 100644 --- a/test/Feature/MultipleReadResolution.c +++ b/test/Feature/MultipleReadResolution.c @@ -3,7 +3,8 @@ // RUN: echo "x" >> %t1.res // RUN: echo "x" >> %t1.res // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc > %t1.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log // RUN: diff %t1.res %t1.log #include <stdio.h> diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c index 1f77485f..6530185d 100644 --- a/test/Feature/MultipleReallocResolution.c +++ b/test/Feature/MultipleReallocResolution.c @@ -1,7 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc -// RUN: ls %T/klee-last/ | grep .err | wc -l | grep 2 -// RUN: ls %T/klee-last/ | grep .ptr.err | wc -l | grep 2 +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc +// RUN: ls %t.klee-out/ | grep .err | wc -l | grep 2 +// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 2 #include <assert.h> #include <stdlib.h> diff --git a/test/Feature/MultipleWriteResolution.c b/test/Feature/MultipleWriteResolution.c index f07b9710..eb4b1694 100644 --- a/test/Feature/MultipleWriteResolution.c +++ b/test/Feature/MultipleWriteResolution.c @@ -3,7 +3,8 @@ // RUN: echo "x" >> %t1.res // RUN: echo "x" >> %t1.res // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc > %t1.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log // RUN: diff %t1.res %t1.log #include <stdio.h> diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c index 16da3117..6599d269 100644 --- a/test/Feature/NamedSeedMatching.c +++ b/test/Feature/NamedSeedMatching.c @@ -1,9 +1,11 @@ // RUN: %llvmgcc -emit-llvm -c -g %s -o %t.bc -// RUN: rm -rf %t.out -// RUN: %klee --output-dir=%t.out %t.bc "initial" -// RUN: test -f %t.out/test000001.ktest -// RUN: not test -f %t.out/test000002.ktest -// RUN: %klee --only-replay-seeds --named-seed-matching --seed-out %t.out/test000001.ktest %t.bc > %t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc "initial" +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: not test -f %t.klee-out/test000002.ktest + +// RUN: rm -rf %t.klee-out-2 +// RUN: %klee --output-dir=%t.klee-out-2 --only-replay-seeds --named-seed-matching --seed-out %t.klee-out/test000001.ktest %t.bc > %t.log // RUN: grep -q "a==3" %t.log // RUN: grep -q "b==4" %t.log // RUN: grep -q "c==5" %t.log diff --git a/test/Feature/OneFreeError.c b/test/Feature/OneFreeError.c index e83b535a..4f5a8c8c 100644 --- a/test/Feature/OneFreeError.c +++ b/test/Feature/OneFreeError.c @@ -1,11 +1,12 @@ // 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 +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s +// RUN: test -f %t.klee-out/test000001.ptr.err int main() { int *x = malloc(4); free(x); - // CHECK: OneFreeError.c:10: memory error: out of bound pointer + // CHECK: OneFreeError.c:11: 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 72d36b70..85fb2a79 100644 --- a/test/Feature/OneOutOfBounds.c +++ b/test/Feature/OneOutOfBounds.c @@ -1,10 +1,11 @@ // 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 +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s +// RUN: test -f %t.klee-out/test000001.ptr.err int main() { int *x = malloc(sizeof(int)); - // CHECK: OneOutOfBounds.c:9: memory error: out of bound pointer + // CHECK: OneOutOfBounds.c:10: memory error: out of bound pointer // FIXME: Use FileCheck's relative line numbers x[1] = 1; free(x); diff --git a/test/Feature/Optimize.c b/test/Feature/Optimize.c index 4789d089..9aa963ef 100644 --- a/test/Feature/Optimize.c +++ b/test/Feature/Optimize.c @@ -1,6 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc // RUN: rm -f %t2.log -// RUN: %klee --stop-after-n-instructions=100 --optimize %t2.bc > %t3.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --stop-after-n-instructions=100 --optimize %t2.bc > %t3.log // RUN: echo "good" > %t3.good // RUN: diff %t3.log %t3.good diff --git a/test/Feature/Overflow.ll b/test/Feature/Overflow.ll index 90ace60b..35dfbd10 100644 --- a/test/Feature/Overflow.ll +++ b/test/Feature/Overflow.ll @@ -1,5 +1,6 @@ ; RUN: llvm-as %s -f -o %t1.bc -; RUN: %klee -disable-opt %t1.bc > %t2 +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 ; RUN: grep PASS %t2 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-n8:16:32:64" diff --git a/test/Feature/OverflowMul.ll b/test/Feature/OverflowMul.ll index 7ab67502..7026aa74 100644 --- a/test/Feature/OverflowMul.ll +++ b/test/Feature/OverflowMul.ll @@ -1,5 +1,6 @@ ; RUN: llvm-as %s -f -o %t1.bc -; RUN: %klee -disable-opt %t1.bc > %t2 +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 ; RUN: grep PASS %t2 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-n8:16:32:64" diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c index 886c7ec8..a1b31f57 100644 --- a/test/Feature/OverlappedError.c +++ b/test/Feature/OverlappedError.c @@ -1,7 +1,8 @@ // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc -// RUN: ls %T/klee-last/ | grep .ktest | wc -l | grep 4 -// RUN: ls %T/klee-last/ | grep .ptr.err | wc -l | grep 2 +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc +// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 4 +// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 2 #include <stdlib.h> diff --git a/test/Feature/OvershiftCheck.c b/test/Feature/OvershiftCheck.c index bb967166..09cbf8ba 100644 --- a/test/Feature/OvershiftCheck.c +++ b/test/Feature/OvershiftCheck.c @@ -1,8 +1,9 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc -// RUN: %klee -check-overshift %t.bc 2> %t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -check-overshift %t.bc 2> %t.log // RUN: grep -c "overshift error" %t.log -// RUN: grep -c "OvershiftCheck.c:19: overshift error" %t.log -// RUN: grep -c "OvershiftCheck.c:23: overshift error" %t.log +// RUN: grep -c "OvershiftCheck.c:20: overshift error" %t.log +// RUN: grep -c "OvershiftCheck.c:24: overshift error" %t.log /* This test checks that two consecutive potential overshifts * are reported as errors. diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c index 6cdb8446..d562f968 100644 --- a/test/Feature/PreferCex.c +++ b/test/Feature/PreferCex.c @@ -1,6 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc -// RUN: ktest-tool %T/klee-last/test000001.ktest | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc +// RUN: ktest-tool %t.klee-out/test000001.ktest | FileCheck %s #include <assert.h> #include <stdlib.h> diff --git a/test/Feature/RaiseAsm.c b/test/Feature/RaiseAsm.c index 5b8acab4..6a4b7b3c 100644 --- a/test/Feature/RaiseAsm.c +++ b/test/Feature/RaiseAsm.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc #include <assert.h> diff --git a/test/Feature/Realloc.c b/test/Feature/Realloc.c index 62aa170b..76016fb7 100644 --- a/test/Feature/Realloc.c +++ b/test/Feature/Realloc.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --exit-on-error %t1.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc 2>&1 | FileCheck %s #include <assert.h> #include <stdlib.h> diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c index ccf59657..c367c3d9 100644 --- a/test/Feature/ReplayPath.c +++ b/test/Feature/ReplayPath.c @@ -1,7 +1,10 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -DCOND_EXIT -c -o %t1.bc -// RUN: klee --write-paths %t1.bc > %t3.good +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --write-paths %t1.bc > %t3.good + // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc -// RUN: %klee --replay-path %T/klee-last/test000001.path %t2.bc > %t3.log +// RUN: rm -rf %t.klee-out-2 +// RUN: %klee --output-dir=%t.klee-out-2 --replay-path %t.klee-out/test000001.path %t2.bc > %t3.log // RUN: diff %t3.log %t3.good #include <unistd.h> diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c index b120d354..284020eb 100644 --- a/test/Feature/Searchers.c +++ b/test/Feature/Searchers.c @@ -1,22 +1,40 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc -// RUN: %klee %t2.bc -// RUN: %klee --search=random-state %t2.bc -// RUN: %klee --search=nurs:depth %t2.bc -// RUN: %klee --search=nurs:qc %t2.bc -// RUN: %klee --use-batching-search %t2.bc -// RUN: %klee --use-batching-search --search=random-state %t2.bc -// RUN: %klee --use-batching-search --search=nurs:depth %t2.bc -// RUN: %klee --use-batching-search --search=nurs:qc %t2.bc -// RUN: %klee --search=random-path --search=nurs:qc %t2.bc -// RUN: %klee --use-merge --search=dfs --debug-log-merge --debug-log-state-merge %t2.bc -// RUN: %klee --use-merge --use-batching-search --search=dfs %t2.bc -// RUN: %klee --use-merge --use-batching-search --search=random-state %t2.bc -// RUN: %klee --use-merge --use-batching-search --search=nurs:depth %t2.bc -// RUN: %klee --use-merge --use-batching-search --search=nurs:qc %t2.bc -// RUN: %klee --use-iterative-deepening-time-search --use-batching-search %t2.bc -// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=random-state %t2.bc -// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=nurs:depth %t2.bc -// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=nurs:qc %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=random-state %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=nurs:depth %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=nurs:qc %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-batching-search %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-batching-search --search=random-state %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-batching-search --search=nurs:depth %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-batching-search --search=nurs:qc %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=random-path --search=nurs:qc %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-merge --search=dfs --debug-log-merge --debug-log-state-merge %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-merge --use-batching-search --search=dfs %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-merge --use-batching-search --search=random-state %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-merge --use-batching-search --search=nurs:depth %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-merge --use-batching-search --search=nurs:qc %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=random-state %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=nurs:depth %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=nurs:qc %t2.bc /* this test is basically just for coverage and doesn't really do any diff --git a/test/Feature/SetForking.c b/test/Feature/SetForking.c index cbae33c0..60799a0d 100644 --- a/test/Feature/SetForking.c +++ b/test/Feature/SetForking.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc -// RUN: %klee %t.bc > %t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log // RUN: sort %t.log | uniq -c > %t.uniq.log // RUN: grep "1 A" %t.uniq.log // RUN: grep "1 B" %t.uniq.log diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c index 34405c1f..2ef6d413 100644 --- a/test/Feature/SolverTimeout.c +++ b/test/Feature/SolverTimeout.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --max-solver-time=1 %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t1.bc #include <stdio.h> int main() { diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c index 31eee235..398ba6f8 100644 --- a/test/Feature/Vararg.c +++ b/test/Feature/Vararg.c @@ -1,7 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee %t1.bc > %t2.out +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t2.out // RUN: grep "types: (52, 37, 2.00, (9,12,15))" %t2.out -// RUN: test -f %T/klee-last/test000001.ptr.err +// RUN: test -f %t.klee-out/test000001.ptr.err #include <stdarg.h> #include <assert.h> diff --git a/test/Feature/WithLibc.c b/test/Feature/WithLibc.c index 5e84eb4a..cefef577 100644 --- a/test/Feature/WithLibc.c +++ b/test/Feature/WithLibc.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc -// RUN: %klee --libc=klee %t2.bc > %t3.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=klee %t2.bc > %t3.log // RUN: echo "good" > %t3.good // RUN: diff %t3.log %t3.good diff --git a/test/Feature/WriteCov.c b/test/Feature/WriteCov.c index 45e7bc43..3ecce3fc 100644 --- a/test/Feature/WriteCov.c +++ b/test/Feature/WriteCov.c @@ -1,20 +1,21 @@ // 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 %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 -// RUN: grep klee-last/test000002.cov:1 %t3.txt +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --write-cov %t2.bc +// RUN: grep -c WriteCov.c:16 %t.klee-out/test000001.cov %t.klee-out/test000002.cov >%t3.txt +// RUN: grep -c WriteCov.c:18 %t.klee-out/test000001.cov %t.klee-out/test000002.cov >>%t3.txt +// RUN: grep %t.klee-out/test000001.cov:0 %t3.txt +// RUN: grep %t.klee-out/test000001.cov:1 %t3.txt +// RUN: grep %t.klee-out/test000002.cov:0 %t3.txt +// RUN: grep %t.klee-out/test000002.cov:1 %t3.txt #include <assert.h> #include <stdio.h> int main() { if (klee_range(0,2, "range")) { - assert(__LINE__ == 15); printf("__LINE__ = %d\n", __LINE__); + assert(__LINE__ == 16); printf("__LINE__ = %d\n", __LINE__); } else { - assert(__LINE__ == 17); printf("__LINE__ = %d\n", __LINE__); + assert(__LINE__ == 18); printf("__LINE__ = %d\n", __LINE__); } return 0; } diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c index 81995b2b..a771bc75 100644 --- a/test/Feature/arithmetic-right-overshift-sym-conc.c +++ b/test/Feature/arithmetic-right-overshift-sym-conc.c @@ -1,7 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc -// RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc -// RUN: not grep "ASSERTION FAIL" %T/klee-last/messages.txt -// RUN: grep "KLEE: done: explored paths = 1" %T/klee-last/info +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc +// RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt +// RUN: grep "KLEE: done: explored paths = 1" %t.klee-out/info #include <stdio.h> #include <assert.h> diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c index c1185870..31124ea4 100644 --- a/test/Feature/consecutive_divide_by_zero.c +++ b/test/Feature/consecutive_divide_by_zero.c @@ -1,9 +1,10 @@ // RUN: %llvmgcc -emit-llvm -c -g -O0 %s -o %t.bc -// RUN: %klee -check-div-zero -emit-all-errors=0 %t.bc 2> %t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -check-div-zero -emit-all-errors=0 %t.bc 2> %t.log // RUN: grep "completed paths = 3" %t.log // RUN: grep "generated tests = 3" %t.log -// RUN: grep "consecutive_divide_by_zero.c:24: divide by zero" %t.log -// RUN: grep "consecutive_divide_by_zero.c:27: divide by zero" %t.log +// RUN: grep "consecutive_divide_by_zero.c:25: divide by zero" %t.log +// RUN: grep "consecutive_divide_by_zero.c:28: divide by zero" %t.log /* This test case captures a bug where two distinct division * by zero errors are treated as the same error and so diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c index 09ed07fd..ac43bdf7 100644 --- a/test/Feature/const_array_opt1.c +++ b/test/Feature/const_array_opt1.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc -// RUN: %klee --const-array-opt --max-time=10 --only-output-states-covering-new %t.bc >%t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --const-array-opt --max-time=10 --only-output-states-covering-new %t.bc >%t.log // grep -q "Finished successfully!\n" /* This is testing the const array optimization. On my 2.3GHz machine diff --git a/test/Feature/left-overshift-sym-conc.c b/test/Feature/left-overshift-sym-conc.c index e962fa28..8859c46c 100644 --- a/test/Feature/left-overshift-sym-conc.c +++ b/test/Feature/left-overshift-sym-conc.c @@ -1,7 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc -// RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc -// RUN: not grep "ASSERTION FAIL" %T/klee-last/messages.txt -// RUN: grep "KLEE: done: explored paths = 1" %T/klee-last/info +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc +// RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt +// RUN: grep "KLEE: done: explored paths = 1" %t.klee-out/info #include <stdio.h> #include <assert.h> diff --git a/test/Feature/logical-right-overshift-sym-conc.c b/test/Feature/logical-right-overshift-sym-conc.c index 00281ec4..950b5992 100644 --- a/test/Feature/logical-right-overshift-sym-conc.c +++ b/test/Feature/logical-right-overshift-sym-conc.c @@ -1,7 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc -// RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc -// RUN: not grep "ASSERTION FAIL" %T/klee-last/messages.txt -// RUN: grep "KLEE: done: explored paths = 1" %T/klee-last/info +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc +// RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt +// RUN: grep "KLEE: done: explored paths = 1" %t.klee-out/info #include <stdio.h> #include <assert.h> |