diff options
author | Daniel Dunbar <daniel@zuster.org> | 2014-09-12 17:03:35 -0700 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2014-09-12 17:39:18 -0700 |
commit | 9b715dfc40311247b08daf5fa8695a95fd66106f (patch) | |
tree | e45588fba94a530653d8b6bcddafc5cda3e2adef /test/Feature | |
parent | 9a3cf72b8979213bcc6d235856bb0ddba4ee37c8 (diff) | |
download | klee-9b715dfc40311247b08daf5fa8695a95fd66106f.tar.gz |
[tests] Set --output-dir on all test runs, in support of running tests in parallel.
- It would be nice if there was an easier way to do this that didn't involve editing all of the tests (like running each test in its own directory), but this approach fixes #146 and doesn't involve changing 'lit' or writing a wrapper harness. My assumption is a lot of tests start are derived from another one, so hopefully following this convention won't be burdensome, and I updated 'make check' so that it will produce an error if any test runs klee without --output-dir (by checking for the existing of klee-last files). - This also helps with #147 but I still can't fully run tests in parallel (I start hitting STP errors).
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> |