From 6f290d8f9e9d7faac295cb51fc96884a18f4ded4 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 21 May 2009 04:36:41 +0000 Subject: Initial KLEE checkin. - Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8 --- test/Feature/ReplayPath.c | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 test/Feature/ReplayPath.c (limited to 'test/Feature/ReplayPath.c') diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c new file mode 100644 index 00000000..3f01fa80 --- /dev/null +++ b/test/Feature/ReplayPath.c @@ -0,0 +1,27 @@ +// RUN: echo "1" > %t1.path +// RUN: echo "0" >> %t1.path +// RUN: echo "1" >> %t1.path +// RUN: echo "0" >> %t1.path +// RUN: echo "1" >> %t1.path +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc +// RUN: %klee --replay-path %t1.path %t2.bc > %t3.log +// RUN: echo "res: 110" > %t3.good +// RUN: diff %t3.log %t3.good + +int main() { + int res = 1; + int x; + + klee_make_symbolic(&x, sizeof x); + + if (x&1) res *= 2; + if (x&2) res *= 3; + if (x&4) res *= 5; + + // get forced branch coverage + if (x&2) res *= 7; + if (!(x&2)) res *= 11; + printf("res: %d\n", res); + + return 0; +} -- cgit 1.4.1