From 8bec949fc84d8fe8dacbf38ff123b404f1eb4737 Mon Sep 17 00:00:00 2001
From: Timotej Kapus <timotej.kapus13@imperial.ac.uk>
Date: Wed, 13 Dec 2017 17:37:16 +0000
Subject: Add support for concretizing symbolic objects passed to external
functions
---
lib/Core/Memory.cpp | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
(limited to 'lib/Core/Memory.cpp')
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index cd13eada..5c855fb8 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -229,6 +229,22 @@ const UpdateList &ObjectState::getUpdates() const {
return updates;
}
+void ObjectState::flushToConcreteStore(TimingSolver *solver,
+ const ExecutionState &state) const {
+ for (unsigned i = 0; i < size; i++) {
+ if (isByteKnownSymbolic(i)) {
+ ref<ConstantExpr> ce;
+ bool success = solver->getValue(state, read8(i), ce);
+ if (!success)
+ klee_warning("Solver timed out when getting a value for external call, "
+ "byte %p+%u will have random value",
+ (void *)object->address, i);
+ else
+ ce->toMemory(concreteStore + i);
+ }
+ }
+}
+
void ObjectState::makeConcrete() {
delete concreteMask;
delete flushMask;
--
cgit 1.4.1