Print allocation info for adjacent objects in out-of-bounds message.

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

2 files changed, 15 insertions, 3 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 8338cb92..e17d8d93 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -506,7 +506,6 @@ void Executor::initializeGlobals(ExecutionState &state) {
 
       // XXX - DWD - hardcode some things until we decide how to fix.
 #ifndef WINDOWS
-      // TODO: is it 64-bit clean ?
       if (i->getName() == "_ZTVN10__cxxabiv117__class_type_infoE") {
         size = 0x2C;
       } else if (i->getName() == "_ZTVN10__cxxabiv120__si_class_type_infoE") {
@@ -2412,8 +2411,11 @@ std::string Executor::getAddressInfo(ExecutionState &state,
     info << "none\n";
   } else {
     const MemoryObject *mo = lower->first;
+    std::string alloc_info;
+    mo->getAllocInfo(alloc_info);
     info << "object at " << mo->address
-         << " of size " << mo->size << "\n";
+         << " of size " << mo->size << "\n"
+         << "\t\t" << alloc_info << "\n";
   }
   if (lower!=state.addressSpace.objects.begin()) {
     --lower;
@@ -2422,8 +2424,11 @@ std::string Executor::getAddressInfo(ExecutionState &state,
       info << "none\n";
     } else {
       const MemoryObject *mo = lower->first;
+      std::string alloc_info;
+      mo->getAllocInfo(alloc_info);
       info << "object at " << mo->address 
-           << " of size " << mo->size << "\n";
+           << " of size " << mo->size << "\n"
+           << "\t\t" << alloc_info << "\n";
     }
   }
 
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 281bdc59..c23d626c 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -319,6 +319,9 @@ void SpecialFunctionHandler::handleNew(ExecutionState &state,
 void SpecialFunctionHandler::handleDelete(ExecutionState &state,
                             KInstruction *target,
                             std::vector<ref<Expr> > &arguments) {
+  // FIXME: Should check proper pairing with allocation type (malloc/free,
+  // new/delete, new[]/delete[]).
+
   // XXX should type check args
   assert(arguments.size()==1 && "invalid number of arguments to delete");
   executor.executeFree(state, arguments[0]);
@@ -327,6 +330,8 @@ void SpecialFunctionHandler::handleDelete(ExecutionState &state,
 void SpecialFunctionHandler::handleNewArray(ExecutionState &state,
                               KInstruction *target,
                               std::vector<ref<Expr> > &arguments) {
+  // FIXME: This is broken, it doesn't allocate space for the count.
+
   // XXX should type check args
   assert(arguments.size()==1 && "invalid number of arguments to new[]");
   executor.executeAlloc(state, arguments[0], false, target);
@@ -335,6 +340,8 @@ void SpecialFunctionHandler::handleNewArray(ExecutionState &state,
 void SpecialFunctionHandler::handleDeleteArray(ExecutionState &state,
                                  KInstruction *target,
                                  std::vector<ref<Expr> > &arguments) {
+  // FIXME: This is broken, it doesn't allocate space for the count.
+
   // XXX should type check args
   assert(arguments.size()==1 && "invalid number of arguments to delete[]");
   executor.executeFree(state, arguments[0]);