klee_int: allow NULL as name

3 files changed, 14 insertions, 5 deletions

diff --git a/include/klee/klee.h b/include/klee/klee.h
index 8b9cd2e2..9dcc9f5f 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -31,16 +31,16 @@ extern "C" {
    * \arg addr - The start of the object.
    * \arg nbytes - The number of bytes to make symbolic; currently this *must*
    * be the entire contents of the object.
-   * \arg name - An optional name, used for identifying the object in messages,
-   * output files, etc.
+   * \arg name - A name used for identifying the object in messages, output
+   * files, etc. If NULL, object is called "unnamed".
    */
   void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
 
   /* klee_range - Construct a symbolic value in the signed interval
    * [begin,end).
    *
-   * \arg name - An optional name, used for identifying the object in messages,
-   * output files, etc.
+   * \arg name - A name used for identifying the object in messages, output
+   * files, etc. If NULL, object is called "unnamed".
    */
   int klee_range(int begin, int end, const char *name);
 
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index d85c5e93..11a73da3 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -762,7 +762,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
       klee_warning("klee_make_symbolic: deprecated number of arguments (2 instead of 3)");
       break;
     case 3:
-      name = readStringAtAddress(state, arguments[2]);
+      name = arguments[2]->isZero() ? "" : readStringAtAddress(state, arguments[2]);
       break;
     default:
       executor.terminateStateOnError(state, "illegal number of arguments to klee_make_symbolic(void*, size_t, char*)", Executor::User);
diff --git a/test/regression/2018-04-05-make-symbolic-null-name.c b/test/regression/2018-04-05-make-symbolic-null-name.c
new file mode 100644
index 00000000..f352ab21
--- /dev/null
+++ b/test/regression/2018-04-05-make-symbolic-null-name.c
@@ -0,0 +1,9 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t1.bc
+
+#include "klee/klee.h"
+
+int main(int argc, char * argv[]) {
+	int a = klee_int((void*)0);
+}