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

1 files changed, 7 insertions, 0 deletions

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]);