Add "name" argument to klee_make_symbolic, and kill off klee_make_symbolic_name.

 - For compatibility we still accept 2 argument form of klee_make_symbolic, but
   this will go away eventually.


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

1 files changed, 13 insertions, 4 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index da2a4a49..2e423785 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -72,7 +72,7 @@ HandlerInfo handlerInfo[] = {
   add("klee_get_obj_size", handleGetObjSize, true),
   add("klee_get_errno", handleGetErrno, true),
   add("klee_is_symbolic", handleIsSymbolic, true),
-  add("klee_make_symbolic_name", handleMakeSymbolic, false),
+  add("klee_make_symbolic", handleMakeSymbolic, false),
   add("klee_mark_global", handleMarkGlobal, false),
   add("klee_malloc_n", handleMallocN, true),
   add("klee_merge", handleMerge, false),
@@ -670,8 +670,18 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
 void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
                                                 KInstruction *target,
                                                 std::vector<ref<Expr> > &arguments) {
-  assert(arguments.size()==3 &&
-         "invalid number of arguments to klee_make_symbolic[_name]");  
+  std::string name;
+
+  // FIXME: For backwards compatibility, we should eventually enforce the
+  // correct arguments.
+  if (arguments.size() == 2) {
+    name = "unnamed";
+  } else {
+    // FIXME: Should be a user.err, not an assert.
+    assert(arguments.size()==3 &&
+           "invalid number of arguments to klee_make_symbolic");  
+    name = readStringAtAddress(state, arguments[2]);
+  }
 
   Executor::ExactResolutionList rl;
   executor.resolveExact(state, arguments[0], rl, "make_symbolic");
@@ -679,7 +689,6 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
   for (Executor::ExactResolutionList::iterator it = rl.begin(), 
          ie = rl.end(); it != ie; ++it) {
     MemoryObject *mo = (MemoryObject*) it->first.first;
-    std::string name = readStringAtAddress(state, arguments[2]);
     mo->setName(name);
     
     const ObjectState *old = it->first.second;