diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-09-05 16:58:21 +0100 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-11-05 14:51:18 +0000 |
| commit | 7fa96f70cf52b0f3112046962487e95eab0d88fe (patch) | |
| tree | bb594fdff186f558f01bda4f91cb7af085fb37a9 /test/regression | |
| parent | 2429db65ea2a005c76d8c4613e833d8f79cb4db1 (diff) | |
| download | klee-7fa96f70cf52b0f3112046962487e95eab0d88fe.tar.gz | |
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).
Diffstat (limited to 'test/regression')
| -rw-r--r-- | test/regression/2019-09-06-make-const-symbolic.c | 15 |
1 files changed, 15 insertions, 0 deletions
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 |