tests: use names in klee_make_symbolic

10 files changed, 11 insertions, 11 deletions

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;