Merge pull request #317 from johnfxgalea/symex_va_arg

Support for va_args in path-symex

Author: Daniel Kroening

regression/symex/va_args_1/main.c

@@ -0,0 +1,37 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+
+  int y = 7;
+  int u = 2;
+  m = max(3, y, u, 9);
+
+  assert(m == 9);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+  return largest;
+}

regression/symex/va_args_1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex/va_args_10/main.c

@@ -0,0 +1,41 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  int m2;
+  int m3;
+
+  m = max(3, 2, 6, 9);
+  
+  m2 = max(3, 4, 11, 1);
+
+  m3 = max(2, m, m2);
+
+  assert(m3 == 6);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+  return largest;
+}

regression/symex/va_args_10/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/symex/va_args_2/main.c

@@ -0,0 +1,35 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  int y;
+  m = max(2, y, 8);
+
+  assert(m == 8);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+  return largest;
+}

regression/symex/va_args_2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/symex/va_args_3/main.c

@@ -0,0 +1,34 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  m = max(2, 1, 8);
+
+  assert(m == 1);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+ 	va_end(vl);
+  return largest;
+}

regression/symex/va_args_3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/symex/va_args_4/main.c

@@ -0,0 +1,38 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main()
+{
+  int m;
+  m = max(2, 2, 8, 10);
+
+  assert(m == 10);
+
+  return 0;
+}
+
+int max(int repeat,int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+ 
+  for (i = 0; i < repeat; i++){
+	  printf("%d. Result is: %d", i, largest);	
+  }
+
+ 	va_end(vl);
+  return largest;
+}

regression/symex/va_args_4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex/va_args_5/main.c

@@ -0,0 +1,35 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int n;
+  int m;
+  m = max(7, 7, 8);
+
+  assert(m == 8);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+
+ 	va_end(vl);
+  return largest;
+}

regression/symex/va_args_5/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/symex/va_args_6/main.c

@@ -0,0 +1,34 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+  m = max(8, 2, 7, 8);
+
+	assert(m == 2);
+
+	return 0;
+}
+
+int max (int j, int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int);
+
+	for (i=1;i<j;i++)
+  {
+    val=va_arg(vl,int);
+    largest=(largest>val)?largest:val;
+  }
+
+  va_end(vl);
+  return largest;
+}

regression/symex/va_args_6/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--unwind 8
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/symex/va_args_7/main.c

@@ -0,0 +1,23 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int main ()
+{
+    
+  int eva_arguments;
+  int n;
+
+  int init_eva = eva_arguments;
+
+  for (unsigned int i = 0; i < n; i++){
+  
+    eva_arguments++;  
+  }
+
+  if (init_eva == 0){
+    assert(eva_arguments == n);  
+  }
+
+  return 0;
+}

regression/symex/va_args_7/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--unwind 8
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

regression/symex/va_args_8/main.c

@@ -0,0 +1,37 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+int max(int n, ...);
+
+int main ()
+{
+  int m;
+
+  int y = 7;
+  int u = 2;
+  m = max(3, y, u, 9);
+
+  assert(m == 10);
+
+  return 0;
+}
+
+int max(int n, ...)
+{
+  int i,val,largest;
+
+  va_list vl;
+
+  va_start(vl,n);
+  largest=va_arg(vl,int) + 1;
+
+  for (i=1;i<n;i++)
+  {
+    val=va_arg(vl,int) + 1;
+    largest=(largest>val)?largest:val;
+  }
+ 
+  va_end(vl);
+  return largest;
+}

regression/symex/va_args_8/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring