From 26d0fcbccd09143307c1e0f0a95cacbee7d3a940 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 25 Jul 2017 13:54:16 +0100 Subject: Added regression test for bug reported by @kren1 in #262 --- test/regression/2015-08-05-invalid-fork.c | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test/regression/2015-08-05-invalid-fork.c 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; +} -- cgit 1.4.1