tests: use names in klee_make_symbolic

30 files changed, 43 insertions, 43 deletions

diff --git a/test/Feature/ByteSwap.c b/test/Feature/ByteSwap.c
index b6500a13..a2228905 100644
--- a/test/Feature/ByteSwap.c
+++ b/test/Feature/ByteSwap.c
@@ -8,7 +8,7 @@
 int main() {
   
   uint32_t n = 0;
-  klee_make_symbolic(&n, sizeof(n));
+  klee_make_symbolic(&n, sizeof(n), "n");
   
   uint32_t h = ntohl(n);
   assert(htonl(h) == n);
diff --git a/test/Feature/CheckForImpliedValue.c.failing b/test/Feature/CheckForImpliedValue.c.failing
index bb643647..0aa50f0b 100644
--- a/test/Feature/CheckForImpliedValue.c.failing
+++ b/test/Feature/CheckForImpliedValue.c.failing
@@ -9,8 +9,8 @@
 int main() {
   unsigned x, y;
   
-  klee_make_symbolic(&x, sizeof x);
-  klee_make_symbolic(&y, sizeof y);
+  klee_make_symbolic(&x, sizeof x, "x");
+  klee_make_symbolic(&y, sizeof y, "y");
 
   if (!x) { // should give x = 0 hit by ivc
     printf("ok\n");
diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c
index 425c4551..ba20428d 100644
--- a/test/Feature/CompressedExprLogging.c
+++ b/test/Feature/CompressedExprLogging.c
@@ -16,7 +16,7 @@ int constantArr[16] = {1 << 0,  1 << 1,  1 << 2,  1 << 3, 1 << 4,  1 << 5,
 
 int main() {
   char buf[4];
-  klee_make_symbolic(buf, sizeof buf);
+  klee_make_symbolic(buf, sizeof buf, "buf");
 
   buf[1] = 'a';
 
diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c
index 926e0a48..2445d2b8 100644
--- a/test/Feature/CopyOnWrite.c
+++ b/test/Feature/CopyOnWrite.c
@@ -20,7 +20,7 @@ void explode(int *ap, int i, int *result) {
 int main() {
   int result = 0;
   int a[N];
-  klee_make_symbolic(a, sizeof a);
+  klee_make_symbolic(a, sizeof a, "a");
   explode(a,0,&result);
   assert(result==N);
   return 0;
diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c
index 9d2d5ecc..861f93eb 100644
--- a/test/Feature/DanglingConcreteReadExpr.c
+++ b/test/Feature/DanglingConcreteReadExpr.c
@@ -8,7 +8,7 @@
 int main() {
   unsigned char x, y;
 
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   
   y = x;
 
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index 4479e850..a85afc1b 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -23,7 +23,7 @@ int constantArr[16 ] = {
 
 int main() {
   char buf[4];
-  klee_make_symbolic(buf, sizeof buf);
+  klee_make_symbolic(buf, sizeof buf, "buf");
 
   buf[1] = 'a';
 
diff --git a/test/Feature/FunctionPointer.c b/test/Feature/FunctionPointer.c
index ac28ca00..cda35b11 100644
--- a/test/Feature/FunctionPointer.c
+++ b/test/Feature/FunctionPointer.c
@@ -26,7 +26,7 @@ int main(int argc, char **argv) {
   xx("called via xx");
 
 #if 0
-  klee_make_symbolic(&fp, sizeof fp);
+  klee_make_symbolic(&fp, sizeof fp, "fp");
   if(fp == baz) {
     printf("fp = %p, baz = %p\n", fp, baz);
     fp("calling via symbolic!");
diff --git a/test/Feature/ImpliedValue.c.failing b/test/Feature/ImpliedValue.c.failing
index 469c8f28..d3142456 100644
--- a/test/Feature/ImpliedValue.c.failing
+++ b/test/Feature/ImpliedValue.c.failing
@@ -15,15 +15,15 @@ int main() {
   unsigned char which;
   volatile unsigned char a,b,c,d,e,f,g,h;
 
-  klee_make_symbolic(&which, sizeof which);
-  klee_make_symbolic(&a, sizeof a);
-  klee_make_symbolic(&b, sizeof b);
-  klee_make_symbolic(&c, sizeof c);
-  klee_make_symbolic(&d, sizeof d);
-  klee_make_symbolic(&e, sizeof e);
-  klee_make_symbolic(&f, sizeof f);
-  klee_make_symbolic(&g, sizeof g);
-  klee_make_symbolic(&h, sizeof h);
+  klee_make_symbolic(&which, sizeof which, "which");
+  klee_make_symbolic(&a, sizeof a, "a");
+  klee_make_symbolic(&b, sizeof b, "b");
+  klee_make_symbolic(&c, sizeof c, "c");
+  klee_make_symbolic(&d, sizeof d, "d");
+  klee_make_symbolic(&e, sizeof e, "e");
+  klee_make_symbolic(&f, sizeof f, "f");
+  klee_make_symbolic(&g, sizeof g, "g");
+  klee_make_symbolic(&h, sizeof h, "h");
 
   switch (which) {
 // RUN: grep "simple read(2) = value case" %t4.out
diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c
index 5a3dfa44..6eb8784a 100644
--- a/test/Feature/InAndOutOfBounds.c
+++ b/test/Feature/InAndOutOfBounds.c
@@ -7,7 +7,7 @@
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   if (x-start>=end-start) klee_silent_exit(0);
   return x;
 }
diff --git a/test/Feature/IsSymbolic.c b/test/Feature/IsSymbolic.c
index cd7f3dba..02aa2332 100644
--- a/test/Feature/IsSymbolic.c
+++ b/test/Feature/IsSymbolic.c
@@ -6,8 +6,8 @@
 
 int main() {
   int x, y, z = 0;
-  klee_make_symbolic(&x, sizeof x);
-  klee_make_symbolic(&y, sizeof y);
+  klee_make_symbolic(&x, sizeof x, "x");
+  klee_make_symbolic(&y, sizeof y, "y");
   if (x) {
     assert(klee_is_symbolic(y));
   } else {
diff --git a/test/Feature/KleeReportError.c b/test/Feature/KleeReportError.c
index 50aaf97d..4e21df18 100644
--- a/test/Feature/KleeReportError.c
+++ b/test/Feature/KleeReportError.c
@@ -8,8 +8,8 @@
 int main(int argc, char** argv) {
   int x, y, *p = 0;
   
-  klee_make_symbolic(&x, sizeof x);
-  klee_make_symbolic(&y, sizeof y);
+  klee_make_symbolic(&x, sizeof x, "x");
+  klee_make_symbolic(&y, sizeof y, "y");
 
   if (x)
     fprintf(stderr, "x\n");
diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c
index 3216de95..704057f9 100644
--- a/test/Feature/MultipleFreeResolution.c
+++ b/test/Feature/MultipleFreeResolution.c
@@ -9,7 +9,7 @@
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   if (x-start>=end-start) klee_silent_exit(0);
   return x;
 }
diff --git a/test/Feature/MultipleReadResolution.c b/test/Feature/MultipleReadResolution.c
index af42c012..a586a3c8 100644
--- a/test/Feature/MultipleReadResolution.c
+++ b/test/Feature/MultipleReadResolution.c
@@ -11,7 +11,7 @@
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   if (x-start>=end-start) klee_silent_exit(0);
   return x;
 }
diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c
index 6530185d..a95d9d75 100644
--- a/test/Feature/MultipleReallocResolution.c
+++ b/test/Feature/MultipleReallocResolution.c
@@ -10,7 +10,7 @@
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   if (x-start>=end-start) klee_silent_exit(0);
   return x;
 }
diff --git a/test/Feature/MultipleWriteResolution.c b/test/Feature/MultipleWriteResolution.c
index eb4b1694..5f906836 100644
--- a/test/Feature/MultipleWriteResolution.c
+++ b/test/Feature/MultipleWriteResolution.c
@@ -11,7 +11,7 @@
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   if (x-start>=end-start) klee_silent_exit(0);
   return x;
 }
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
index 180e03cf..a765eea8 100644
--- a/test/Feature/PreferCex.c
+++ b/test/Feature/PreferCex.c
@@ -10,7 +10,7 @@
 int main() {
   char buf[4];
 
-  klee_make_symbolic(buf, sizeof buf);
+  klee_make_symbolic(buf, sizeof buf, "buf");
   // CHECK: Hi\x00\x00
   klee_prefer_cex(buf, buf[0]=='H');
   klee_prefer_cex(buf, buf[1]=='i');
diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c
index c367c3d9..4a973dfd 100644
--- a/test/Feature/ReplayPath.c
+++ b/test/Feature/ReplayPath.c
@@ -20,7 +20,7 @@ int main() {
   int res = 1;
   int x;
 
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
 
   if (x&1) res *= 2; else cond_exit();
   if (x&2) res *= 3; else cond_exit();
diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c
index 9e0bc722..a24cb7a3 100644
--- a/test/Feature/Searchers.c
+++ b/test/Feature/Searchers.c
@@ -54,7 +54,7 @@ int main(int argc, char **argv) {
   unsigned char *buf = malloc(N);
   int i;
   
-  klee_make_symbolic(buf, N);
+  klee_make_symbolic(buf, N, "buf");
   if (validate(buf, N))
     return buf[0];
   return 0;
diff --git a/test/Feature/WithLibc.c b/test/Feature/WithLibc.c
index cefef577..0eca8213 100644
--- a/test/Feature/WithLibc.c
+++ b/test/Feature/WithLibc.c
@@ -8,7 +8,7 @@ int main() {
   char buf[4];
   char *s = "foo";
 
-  klee_make_symbolic(buf, sizeof buf);
+  klee_make_symbolic(buf, sizeof buf, "buf");
   buf[3] = 0;
 
   if (strcmp(buf, s)==0) {
diff --git a/test/Programs/pcregrep.c b/test/Programs/pcregrep.c
index 5ed8f4fa..634e1cc6 100644
--- a/test/Programs/pcregrep.c
+++ b/test/Programs/pcregrep.c
@@ -486,8 +486,8 @@ llvm_cbe_cond_next69:
   ft_make_symbolic_array(ltmp_1_1, llvm_cbe_tmp22, "pattern");
   ft_make_symbolic_array(ltmp_3_1, llvm_cbe_tmp42, "source");
 #else
-  klee_make_symbolic(ltmp_1_1, llvm_cbe_tmp22);
-  klee_make_symbolic(ltmp_3_1, llvm_cbe_tmp42);
+  klee_make_symbolic(ltmp_1_1, llvm_cbe_tmp22, "ltmp_1_1");
+  klee_make_symbolic(ltmp_3_1, llvm_cbe_tmp42, "ltmp_3_1");
 #endif
   *(&ltmp_1_1[(llvm_cbe_tmp22 + ((unsigned int )-1))]) = ((unsigned char )0);
   *(&ltmp_3_1[(llvm_cbe_tmp42 + ((unsigned int )-1))]) = ((unsigned char )0);
diff --git a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c
index 611656bd..9b06a797 100644
--- a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c
+++ b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c
@@ -7,7 +7,7 @@
 int main(void) {
   char c[2];
 
-  klee_make_symbolic(&c, sizeof(c));
+  klee_make_symbolic(&c, sizeof(c), "c");
 
   if (c[0] > 10) {
     int x;
diff --git a/test/regression/2007-07-30-unflushed-byte.c b/test/regression/2007-07-30-unflushed-byte.c
index 20f60eef..b9f6b237 100644
--- a/test/regression/2007-07-30-unflushed-byte.c
+++ b/test/regression/2007-07-30-unflushed-byte.c
@@ -7,7 +7,7 @@
 int main() {
   char i, x[3];
 
-  klee_make_symbolic(&i, sizeof i);
+  klee_make_symbolic(&i, sizeof i, "i");
 
   x[0] = i;
 
diff --git a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c
index 0aa20896..47cd87d8 100644
--- a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c
+++ b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c
@@ -8,7 +8,7 @@
 int main() {  
   unsigned char x;
 
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   if (x >= 2) klee_silent_exit(0);
 
   char delete[2] = {0,1};
diff --git a/test/regression/2007-08-06-64bit-shift.c b/test/regression/2007-08-06-64bit-shift.c
index ac282dbd..c6c1f34d 100644
--- a/test/regression/2007-08-06-64bit-shift.c
+++ b/test/regression/2007-08-06-64bit-shift.c
@@ -7,7 +7,7 @@
 int main() {
   int d;
   
-  klee_make_symbolic( &d, sizeof(d) );
+  klee_make_symbolic(&d, sizeof(d), "d");
 
   int l = d - 1;
   unsigned long long m = ((unsigned long long) l << 32) / d;
diff --git a/test/regression/2007-08-06-access-after-free.c b/test/regression/2007-08-06-access-after-free.c
index ae80b8b8..783b3885 100644
--- a/test/regression/2007-08-06-access-after-free.c
+++ b/test/regression/2007-08-06-access-after-free.c
@@ -8,8 +8,8 @@ int main() {
   int a;
   unsigned char *p = malloc(4);
 
-  klee_make_symbolic(&a, sizeof a);
-  klee_make_symbolic(p, sizeof p);
+  klee_make_symbolic(&a, sizeof a, "a");
+  klee_make_symbolic(p, sizeof p, "p");
 
   p[0] |= 16;
 
diff --git a/test/regression/2007-08-16-invalid-constant-value.c b/test/regression/2007-08-16-invalid-constant-value.c
index e0b304f4..5b17e68b 100644
--- a/test/regression/2007-08-16-invalid-constant-value.c
+++ b/test/regression/2007-08-16-invalid-constant-value.c
@@ -12,7 +12,7 @@
 int main() {
   unsigned char a;
 
-  klee_make_symbolic(&a, sizeof a);
+  klee_make_symbolic(&a, sizeof a, "a");
 
   // demand was firing here because an invalid constant
   // value was being created when implied value did not
diff --git a/test/regression/2007-08-16-valid-write-to-freed-object.c b/test/regression/2007-08-16-valid-write-to-freed-object.c
index 1fca1cca..b3257100 100644
--- a/test/regression/2007-08-16-valid-write-to-freed-object.c
+++ b/test/regression/2007-08-16-valid-write-to-freed-object.c
@@ -4,7 +4,7 @@
 
 unsigned sym() {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   return x;
 }
 
diff --git a/test/regression/2007-10-11-illegal-access-after-free-and-branch.c b/test/regression/2007-10-11-illegal-access-after-free-and-branch.c
index c5cffa36..90490b56 100644
--- a/test/regression/2007-10-11-illegal-access-after-free-and-branch.c
+++ b/test/regression/2007-10-11-illegal-access-after-free-and-branch.c
@@ -9,7 +9,7 @@
 
 int main(int argc, char **argv) {
   unsigned char *buf = malloc(3);
-  klee_make_symbolic(buf, 3);
+  klee_make_symbolic(buf, 3, "buf");
   if (buf[0]>4) klee_silent_exit(0);
   unsigned char x = buf[1];
   free(buf);
diff --git a/test/regression/2015-08-30-empty-constraints.c b/test/regression/2015-08-30-empty-constraints.c
index 81439e21..b07beccd 100644
--- a/test/regression/2015-08-30-empty-constraints.c
+++ b/test/regression/2015-08-30-empty-constraints.c
@@ -13,7 +13,7 @@
 int main() {
   int d;
 
-  klee_make_symbolic( &d, sizeof(d) );
+  klee_make_symbolic(&d, sizeof(d), "d");
 
   // CHECK-NOT: unable to compute initial values (invalid constraints?)!
   if ((d & 2) / 4)
diff --git a/test/regression/2016-06-28-div-zero-bug.c b/test/regression/2016-06-28-div-zero-bug.c
index 11689aa0..76e70ad1 100644
--- a/test/regression/2016-06-28-div-zero-bug.c
+++ b/test/regression/2016-06-28-div-zero-bug.c
@@ -15,7 +15,7 @@ int safe_div(short p1, int p2) {
 }
 
 int main() {
-  klee_make_symbolic(&b, sizeof b);
+  klee_make_symbolic(&b, sizeof b, "b");
   if (safe_div(*c, 0))
     *f = (int)&b % *c;