KLEE64: Fix a type conversion problem with calls to klee_make_symbolic; there

are probably lots more of this -- we really need coercion and argument
validation to be checked outside of the individual intrinsic handlers.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77311 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 5 insertions, 2 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 9904f052..281bdc59 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -654,10 +654,13 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
       return;
     } 
 
+    // FIXME: Type coercion should be done consistently somewhere.
     bool res;
     bool success =
-      executor.solver->mustBeTrue(*s, EqExpr::create(arguments[1],
-                                                     mo->getSizeExpr()),
+      executor.solver->mustBeTrue(*s, 
+                                  EqExpr::create(ZExtExpr::create(arguments[1],
+                                                                  Context::get().getPointerWidth()),
+                                                 mo->getSizeExpr()),
                                   res);
     assert(success && "FIXME: Unhandled solver failure");