diff options
Diffstat (limited to 'test/regression')
-rw-r--r-- | test/regression/2016-11-24-bitcast-weak-alias.c | 1 | ||||
-rw-r--r-- | test/regression/2017-02-21-pathOS-id.c | 19 | ||||
-rw-r--r-- | test/regression/2017-03-23-early-exit-log-stats.c | 22 |
3 files changed, 42 insertions, 0 deletions
diff --git a/test/regression/2016-11-24-bitcast-weak-alias.c b/test/regression/2016-11-24-bitcast-weak-alias.c index f115731b..3e4ebe64 100644 --- a/test/regression/2016-11-24-bitcast-weak-alias.c +++ b/test/regression/2016-11-24-bitcast-weak-alias.c @@ -1,3 +1,4 @@ +// REQUIRES: not-darwin // RUN: %llvmgcc %s -Wall -emit-llvm -g -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: klee --output-dir=%t.klee-out -exit-on-error -search=nurs:covnew %t.bc DUMMY_ARG >%t1.log 2>&1 diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c new file mode 100644 index 00000000..d3bffbe0 --- /dev/null +++ b/test/regression/2017-02-21-pathOS-id.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -write-paths %t.bc 2> %t.log +// RUN: cat %t.klee-out/test000001.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1 +int main(){ + int a, b; + klee_make_symbolic (&a, sizeof(int), "a"); + klee_make_symbolic (&b, sizeof(int), "b"); + klee_assume(a<2); + klee_assume(a>=0); + malloc(a); + if(b){ + b++;//do something + } + return b; +} diff --git a/test/regression/2017-03-23-early-exit-log-stats.c b/test/regression/2017-03-23-early-exit-log-stats.c new file mode 100644 index 00000000..96d3c30f --- /dev/null +++ b/test/regression/2017-03-23-early-exit-log-stats.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// Delay writing instructions so that we ensure on exit that flush happens +// RUN: not %klee --output-dir=%t.klee-out -exit-on-error -stats-write-interval=0 -stats-write-after-instructions=999999 %t.bc 2> %t.log +// RUN: FileCheck -check-prefix=CHECK-KLEE -input-file=%t.log %s +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.klee-out/run.stats %s +#include "klee/klee.h" +#include <stdlib.h> +int main(){ + int a; + klee_make_symbolic (&a, sizeof(int), "a"); + if (a) { + // CHECK-KLEE: EXITING ON ERROR + // CHECK-KLEE-NEXT: Error: abort failure + abort(); + } + return 0; +} +// First check we find a line with the expected format +// CHECK-STATS:{{^\('Instructions'}} +// Now check that we eventually get a line where a non zero amount of instructions were executed +// CHECK-STATS:{{^\([ ]*([1-9]|([1-9]+)[0-9])}} |