tests: use names in klee_make_symbolic

19 files changed, 30 insertions, 30 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) {