diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 16 | ||||
| -rw-r--r-- | test/regression/2019-09-06-make-const-symbolic.c | 15 |
2 files changed, 30 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index bc889f25..4ac848b0 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -788,6 +788,9 @@ void Executor::initializeGlobals(ExecutionState &state) { } // once all objects are allocated, do the actual initialization + // remember constant objects to initialise their counter part for external + // calls + std::vector<ObjectState *> constantObjects; for (Module::const_global_iterator i = m->global_begin(), e = m->global_end(); i != e; ++i) { @@ -799,9 +802,20 @@ void Executor::initializeGlobals(ExecutionState &state) { ObjectState *wos = state.addressSpace.getWriteable(mo, os); initializeGlobalObject(state, wos, i->getInitializer(), 0); - // if(i->isConstant()) os->setReadOnly(true); + if (i->isConstant()) + constantObjects.emplace_back(wos); } } + + // initialise constant memory that is potentially used with external calls + if (!constantObjects.empty()) { + // initialise the actual memory with constant values + state.addressSpace.copyOutConcretes(); + + // mark constant objects as read-only + for (auto obj : constantObjects) + obj->setReadOnly(true); + } } void Executor::branch(ExecutionState &state, 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 |