diff options
| -rw-r--r-- | test/regression/2015-08-05-invalid-fork.c | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regression/2015-08-05-invalid-fork.c b/test/regression/2015-08-05-invalid-fork.c new file mode 100644 index 00000000..7c35872c --- /dev/null +++ b/test/regression/2015-08-05-invalid-fork.c @@ -0,0 +1,24 @@ +/* Reported by @kren1 in #262 + The test makes sure that the string "Should be printed once" + is printed a single time. +*/ + +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc | FileCheck %s + +static int g_10 = 0x923607A9L; + +int main(int argc, char* argv[]) { + klee_make_symbolic(&g_10,sizeof(g_10), "g_10"); + if (g_10 < (int)0x923607A9L) klee_silent_exit(0); + if (g_10 > (int)0x923607A9L) klee_silent_exit(0); + + int b = 2; + int i = g_10 % (1 % g_10); + i || b; + printf("Should be printed once\n"); + // CHECK: Should be printed once + // CHECK-NOT: Should be printed once + return 0; +} |