From 7fa96f70cf52b0f3112046962487e95eab0d88fe Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 5 Sep 2019 16:58:21 +0100 Subject: Mark all constant global memory objects as constant Fixes #264. We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory. After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic). --- test/regression/2019-09-06-make-const-symbolic.c | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test/regression/2019-09-06-make-const-symbolic.c (limited to 'test/regression') diff --git a/test/regression/2019-09-06-make-const-symbolic.c b/test/regression/2019-09-06-make-const-symbolic.c new file mode 100644 index 00000000..52d430a5 --- /dev/null +++ b/test/regression/2019-09-06-make-const-symbolic.c @@ -0,0 +1,15 @@ +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee -output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s +#include "klee/klee.h" + +const int c = 23; +int main(int argc, char **argv) { + klee_make_symbolic(&c, sizeof(c), "c"); + // CHECK: cannot make readonly object symbolic + + if (c > 20) + return 0; + else + return 1; +} \ No newline at end of file -- cgit 1.4.1