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

8 files changed, 19 insertions, 36 deletions

diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c
index 88ec5026..56f0f9dc 100644
--- a/runtime/Intrinsic/klee_int.c
+++ b/runtime/Intrinsic/klee_int.c
@@ -12,6 +12,6 @@
 
 int klee_int(const char *name) {
   int x;
-  klee_make_symbolic_name(&x, sizeof x, name);
+  klee_make_symbolic(&x, sizeof x, name);
   return x;
 }
diff --git a/runtime/Intrinsic/klee_make_symbolic.c b/runtime/Intrinsic/klee_make_symbolic.c
deleted file mode 100644
index b9dec2a7..00000000
--- a/runtime/Intrinsic/klee_make_symbolic.c
+++ /dev/null
@@ -1,14 +0,0 @@
-//===-- klee_make_symbolic.c ----------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include <klee/klee.h>
-
-void klee_make_symbolic(void *addr, unsigned nbytes) {
-  klee_make_symbolic_name(addr, nbytes, "unnamed");
-}
diff --git a/runtime/Intrinsic/klee_range.c b/runtime/Intrinsic/klee_range.c
index 59d1a05e..5da6a7a5 100644
--- a/runtime/Intrinsic/klee_range.c
+++ b/runtime/Intrinsic/klee_range.c
@@ -13,12 +13,13 @@
 int klee_range(int start, int end, const char* name) {
   int x;
 
-  assert(start < end);
+  if (start >= end)
+    klee_report_error(__FILE__, __LINE__, "invalid range", "user");
 
   if (start+1==end) {
     return start;
   } else {
-    klee_make_symbolic_name(&x, sizeof x, name); 
+    klee_make_symbolic(&x, sizeof x, name); 
 
     /* Make nicer constraint when simple... */
     if (start==0) {
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c
index 61e49893..d976b0b4 100644
--- a/runtime/POSIX/fd_init.c
+++ b/runtime/POSIX/fd_init.c
@@ -56,9 +56,9 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
 
   dfile->size = size;
   dfile->contents = malloc(dfile->size);
-  klee_make_symbolic_name(dfile->contents, dfile->size, name);
+  klee_make_symbolic(dfile->contents, dfile->size, name);
   
-  klee_make_symbolic_name(s, sizeof(*s), sname);
+  klee_make_symbolic(s, sizeof(*s), sname);
 
   /* For broken tests */
   if (!klee_is_symbolic(s->st_ino) && 
@@ -96,7 +96,7 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
 
 static unsigned __sym_uint32(const char *name) {
   unsigned x;
-  klee_make_symbolic_name(&x, sizeof x, name);
+  klee_make_symbolic(&x, sizeof x, name);
   return x;
 }
 
@@ -139,11 +139,11 @@ void klee_init_fds(unsigned n_files, unsigned file_length,
     __exe_fs.ftruncate_fail = malloc(sizeof(*__exe_fs.ftruncate_fail));
     __exe_fs.getcwd_fail = malloc(sizeof(*__exe_fs.getcwd_fail));
 
-    klee_make_symbolic_name(__exe_fs.read_fail, sizeof(*__exe_fs.read_fail), "read_fail");
-    klee_make_symbolic_name(__exe_fs.write_fail, sizeof(*__exe_fs.write_fail), "write_fail");
-    klee_make_symbolic_name(__exe_fs.close_fail, sizeof(*__exe_fs.close_fail), "close_fail");
-    klee_make_symbolic_name(__exe_fs.ftruncate_fail, sizeof(*__exe_fs.ftruncate_fail), "ftruncate_fail");
-    klee_make_symbolic_name(__exe_fs.getcwd_fail, sizeof(*__exe_fs.getcwd_fail), "getcwd_fail");
+    klee_make_symbolic(__exe_fs.read_fail, sizeof(*__exe_fs.read_fail), "read_fail");
+    klee_make_symbolic(__exe_fs.write_fail, sizeof(*__exe_fs.write_fail), "write_fail");
+    klee_make_symbolic(__exe_fs.close_fail, sizeof(*__exe_fs.close_fail), "close_fail");
+    klee_make_symbolic(__exe_fs.ftruncate_fail, sizeof(*__exe_fs.ftruncate_fail), "ftruncate_fail");
+    klee_make_symbolic(__exe_fs.getcwd_fail, sizeof(*__exe_fs.getcwd_fail), "getcwd_fail");
   }
 
   /* setting symbolic stdout */
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index 83e9fde6..f5609973 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -62,7 +62,7 @@ static char *__get_sym_str(int numChars, char *name) {
   int i;
   char *s = malloc(numChars+1);
   klee_mark_global(s);
-  klee_make_symbolic_name(s, numChars+1, name);
+  klee_make_symbolic(s, numChars+1, name);
 
   for (i=0; i<numChars; i++)
     klee_prefer_cex(s, __isprint(s[i]));
diff --git a/runtime/POSIX/misc.c b/runtime/POSIX/misc.c
index 12ff2f58..d0e88290 100644
--- a/runtime/POSIX/misc.c
+++ b/runtime/POSIX/misc.c
@@ -69,7 +69,7 @@ char *getenv(const char *name) {
       if (__klee_sym_env_count < __klee_sym_env_nvars) {
         if (klee_range(0, 2, name)) {
           char *s = malloc(__klee_sym_env_var_size+1);
-          klee_make_symbolic(s, __klee_sym_env_var_size+1);
+          klee_make_symbolic(s, __klee_sym_env_var_size+1. "env");
           s[__klee_sym_env_var_size] = '\0';
           
           memcpy(__klee_sym_env[__klee_sym_env_count].name, name, len+1);
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 1a2fd030..36efb5c2 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -31,7 +31,7 @@ static unsigned char rand_byte(void) {
   return x & 0xFF;
 }
 
-void klee_make_symbolic_name(void *array, unsigned nbytes, const char *name) {
+void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
   static int rand_init = -1;
 
   if (rand_init == -1) {
@@ -94,10 +94,6 @@ void klee_make_symbolic_name(void *array, unsigned nbytes, const char *name) {
   }
 }
 
-void klee_make_symbolic(void *array, unsigned nbytes) {
-  klee_make_symbolic_name(array, nbytes, "unnamed");
-}
-
 void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment) {
 #if 1
   return mmap((void*) 0x90000000, nelems*size, PROT_READ|PROT_WRITE, 
@@ -119,7 +115,7 @@ void klee_silent_exit(int x) {
 
 unsigned klee_choose(unsigned n) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "klee_choose");
   if(x >= n)
     fprintf(stderr, "ERROR: max = %d, got = %d\n", n, x);
   assert(x < n);
@@ -136,9 +132,9 @@ unsigned klee_get_value(unsigned x) {
   return x;
 }
 
-int klee_range_name(int begin, int end, const char* name) {
+int klee_range(int begin, int end, const char* name) {
   int x;
-  klee_make_symbolic_name(&x, sizeof x, name);
+  klee_make_symbolic(&x, sizeof x, name);
   if (x<begin || x>=end) {
     fprintf(stderr, 
             "KLEE: ERROR: invalid klee_range(%u,%u,%s) value, got: %u\n", 
diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c
index 106b4f89..347933df 100644
--- a/runtime/klee-libc/klee-choose.c
+++ b/runtime/klee-libc/klee-choose.c
@@ -11,7 +11,7 @@
 
 unsigned klee_choose(unsigned n) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "klee_choose");
 
   // NB: this will *not* work if they don't compare to n values.
   if(x >= n)