diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/Feature/CompressedExprLogging.c | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c new file mode 100644 index 00000000..a2a07d8b --- /dev/null +++ b/test/Feature/CompressedExprLogging.c @@ -0,0 +1,42 @@ +// 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: rm -rf %t.klee-out %t.klee-out2 +// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:pc %t1.bc +// RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:pc %t1.bc +// RUN: gunzip -d %t.klee-out2/all-queries.pc.gz +// RUN: diff %t.klee-out/all-queries.pc %t.klee-out/all-queries.pc + +#include <assert.h> + +int constantArr[16] = {1 << 0, 1 << 1, 1 << 2, 1 << 3, 1 << 4, 1 << 5, + 1 << 6, 1 << 7, 1 << 8, 1 << 9, 1 << 10, 1 << 11, + 1 << 12, 1 << 13, 1 << 14, 1 << 15}; + +int main() { + char buf[4]; + klee_make_symbolic(buf, sizeof buf); + + buf[1] = 'a'; + + constantArr[klee_range(0, 16, "idx.0")] = buf[0]; + + // Use this to trigger an interior update list usage. + int y = constantArr[klee_range(0, 16, "idx.1")]; + + constantArr[klee_range(0, 16, "idx.2")] = buf[3]; + + buf[klee_range(0, 4, "idx.3")] = 0; + klee_assume(buf[0] == 'h'); + + int x = *((int *)buf); + klee_assume(x > 2); + klee_assume(x == constantArr[12]); + + klee_assume(y != (1 << 5)); + + assert(0); + + return 0; +} |