clang-format recently moved tests

Author: tautschnig

regression/cbmc/Array_UF1/main.c

@@ -1,13 +1,14 @@
 int main()
 {
   int a[10], b[10];
-  int x,y,z;
-  __CPROVER_assume(2<=y && y<=4);
-  __CPROVER_assume(6<=z && z<=8);
+  int x, y, z;
+  __CPROVER_assume(2 <= y && y <= 4);
+  __CPROVER_assume(6 <= z && z <= 8);
   b[y] = x;
   b[z] = x;
-  for(unsigned i = 0;i<10;i++) {
+  for(unsigned i = 0; i < 10; i++)
+  {
     a[i] = b[i];
   }
-  __CPROVER_assert(a[y]==a[z], "a[y]==a[z]");
+  __CPROVER_assert(a[y] == a[z], "a[y]==a[z]");
 }

regression/cbmc/Array_UF10/main.c

@@ -1,21 +1,26 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error() __attribute__((__noreturn__));
 
 int __VERIFIER_nondet_int();
 
-  char x[100], y[100];
-  int i,j,k;
+char x[100], y[100];
+int i, j, k;
 
-void main() {
+void main()
+{
   k = __VERIFIER_nondet_int();
 
   i = 0;
-  while(x[i] != 0){
+  while(x[i] != 0)
+  {
     y[i] = x[i];
     i++;
   }
   y[i] = 0;
 
   if(k >= 0 && k < i)
     if(y[k] == 0)
-      {ERROR: __VERIFIER_error();}
+    {
+    ERROR:
+      __VERIFIER_error();
+    }
 }

regression/cbmc/Array_UF11/main.c

@@ -1,32 +1,33 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
-
-void __VERIFIER_assert(int cond) {
-  if (!(cond)) {
-    ERROR: __VERIFIER_error();
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+
+void __VERIFIER_assert(int cond)
+{
+  if(!(cond))
+  {
+  ERROR:
+    __VERIFIER_error();
   }
   return;
 }
 
 _Bool __VERIFIER_nondet_bool();
 
-int main(){
-   int a[5];
-   int len=0;
-   _Bool c=__VERIFIER_nondet_bool();
-   int i;
-
-
-   while(c){
+int main()
+{
+  int a[5];
+  int len = 0;
+  _Bool c = __VERIFIER_nondet_bool();
+  int i;
 
-      if (len==4)
-         len =0;
-
-      a[len]=0;
-
-      len++;
-   }
-   __VERIFIER_assert(len==5);
-   return 1;
+  while(c)
+  {
+    if(len == 4)
+      len = 0;
 
+    a[len] = 0;
 
+    len++;
+  }
+  __VERIFIER_assert(len == 5);
+  return 1;
 }

regression/cbmc/Array_UF12/main.c

@@ -1,40 +1,47 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error() __attribute__((__noreturn__));
 
-void __VERIFIER_assert(int cond) {
-  if (!(cond)) {
-    ERROR: __VERIFIER_error();
+void __VERIFIER_assert(int cond)
+{
+  if(!(cond))
+  {
+  ERROR:
+    __VERIFIER_error();
   }
   return;
 }
 int b;
 _Bool __VERIFIER_nondet_bool();
-int main(){
-   _Bool k=__VERIFIER_nondet_bool();
-   int i,n,j;
-   int a[1025];
+int main()
+{
+  _Bool k = __VERIFIER_nondet_bool();
+  int i, n, j;
+  int a[1025];
 
-   if (k){
-      n=0;
-   } else {
-      n=1023;
-   }
-
-   i=0;
+  if(k)
+  {
+    n = 0;
+  }
+  else
+  {
+    n = 1023;
+  }
 
-   while ( i <= n){
-      i++;
-      j= j +2;
-   }
+  i = 0;
 
-   a[i]=0;
-   a[j]=0;
-   __VERIFIER_assert(j<1025);
-   a[b]=0;
-   if (b >= 0 && b < 1023)
-      a[b]=1;
-   else
-      a[b%1023] =1;
+  while(i <= n)
+  {
+    i++;
+    j = j + 2;
+  }
 
-   return 1;
+  a[i] = 0;
+  a[j] = 0;
+  __VERIFIER_assert(j < 1025);
+  a[b] = 0;
+  if(b >= 0 && b < 1023)
+    a[b] = 1;
+  else
+    a[b % 1023] = 1;
 
+  return 1;
 }

regression/cbmc/Array_UF13/main.c

@@ -1,27 +1,34 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error() __attribute__((__noreturn__));
 
-void __VERIFIER_assert(int cond) {
-  if (!(cond)) {
-    ERROR: __VERIFIER_error();
+void __VERIFIER_assert(int cond)
+{
+  if(!(cond))
+  {
+  ERROR:
+    __VERIFIER_error();
   }
   return;
 }
 int __VERIFIER_nondet_int();
 
-  char x[100], y[100];
-  int i,j,k;
+char x[100], y[100];
+int i, j, k;
 
-void main() {
+void main()
+{
   k = __VERIFIER_nondet_int();
 
   i = 0;
-  while(x[i] != 0){
+  while(x[i] != 0)
+  {
     y[i] = x[i];
     i++;
   }
   y[i] = 0;
 
   if(k >= 0 && k < i)
     if(y[k] != 0)
-      {__VERIFIER_assert(0);}
+    {
+      __VERIFIER_assert(0);
+    }
 }

regression/cbmc/Array_UF14/main.c

@@ -1,59 +1,57 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error() __attribute__((__noreturn__));
 
 extern void __VERIFIER_assume(int);
-void __VERIFIER_assert(int cond) {
-  if (!(cond)) {
-    ERROR: __VERIFIER_error();
+void __VERIFIER_assert(int cond)
+{
+  if(!(cond))
+  {
+  ERROR:
+    __VERIFIER_error();
   }
   return;
 }
 
-
-
 extern char __VERIFIER_nondet_char();
 
 main()
 {
   char string_A[5], string_B[5];
-  int i, j, nc_A, nc_B, found=0;
+  int i, j, nc_A, nc_B, found = 0;
 
+  for(i = 0; i < 5; i++)
+    string_A[i] = __VERIFIER_nondet_char();
+  __VERIFIER_assume(string_A[5 - 1] == '\0');
 
-  for(i=0; i<5; i++)
-    string_A[i]=__VERIFIER_nondet_char();
-  __VERIFIER_assume(string_A[5 -1]=='\0');
-
-  for(i=0; i<5; i++)
-    string_B[i]=__VERIFIER_nondet_char();
-  __VERIFIER_assume(string_B[5 -1]=='\0');
+  for(i = 0; i < 5; i++)
+    string_B[i] = __VERIFIER_nondet_char();
+  __VERIFIER_assume(string_B[5 - 1] == '\0');
 
   nc_A = 0;
-  while(string_A[nc_A]!='\0')
+  while(string_A[nc_A] != '\0')
     nc_A++;
 
   nc_B = 0;
-  while(string_B[nc_B]!='\0')
+  while(string_B[nc_B] != '\0')
     nc_B++;
 
   __VERIFIER_assume(nc_B >= nc_A);
 
-
-  i=j=0;
-  while((i<nc_A) && (j<nc_B))
+  i = j = 0;
+  while((i < nc_A) && (j < nc_B))
   {
     if(string_A[i] == string_B[j])
     {
-       i++;
-       j++;
+      i++;
+      j++;
     }
     else
     {
-       i = i-j+1;
-       j = 0;
+      i = i - j + 1;
+      j = 0;
     }
   }
 
-  found = (j>nc_B-1)<<i;
+  found = (j > nc_B - 1) << i;
 
   __VERIFIER_assert(found == 0 || found == 1);
-
 }

regression/cbmc/Array_UF15/main.c

@@ -1,56 +1,57 @@
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error() __attribute__((__noreturn__));
 
 extern void __VERIFIER_assume(int);
-void __VERIFIER_assert(int cond) {
-  if (!(cond)) {
-    ERROR: __VERIFIER_error();
+void __VERIFIER_assert(int cond)
+{
+  if(!(cond))
+  {
+  ERROR:
+    __VERIFIER_error();
   }
   return;
 }
 
-
 extern char __VERIFIER_nondet_char();
 
 main()
 {
   char string_A[5], string_B[5];
-  int i, j, nc_A, nc_B, found=0;
+  int i, j, nc_A, nc_B, found = 0;
 
-  for(i=0; i<5; i++)
-    string_A[i]=__VERIFIER_nondet_char();
-  __VERIFIER_assume(string_A[5 -1]=='\0');
+  for(i = 0; i < 5; i++)
+    string_A[i] = __VERIFIER_nondet_char();
+  __VERIFIER_assume(string_A[5 - 1] == '\0');
 
-  for(i=0; i<5; i++)
-    string_B[i]=__VERIFIER_nondet_char();
-  __VERIFIER_assume(string_B[5 -1]=='\0');
+  for(i = 0; i < 5; i++)
+    string_B[i] = __VERIFIER_nondet_char();
+  __VERIFIER_assume(string_B[5 - 1] == '\0');
 
   nc_A = 0;
-  while(string_A[nc_A]!='\0')
+  while(string_A[nc_A] != '\0')
     nc_A++;
 
   nc_B = 0;
-  while(string_B[nc_B]!='\0')
+  while(string_B[nc_B] != '\0')
     nc_B++;
 
   __VERIFIER_assume(nc_B >= nc_A);
 
-
-  i=j=0;
-  while((i<nc_A) && (j<nc_B))
+  i = j = 0;
+  while((i < nc_A) && (j < nc_B))
   {
     if(string_A[i] == string_B[j])
     {
-       i++;
-       j++;
+      i++;
+      j++;
     }
     else
     {
-       i = i-j+1;
-       j = 0;
+      i = i - j + 1;
+      j = 0;
     }
   }
 
-  found = (j>nc_B-1);
+  found = (j > nc_B - 1);
 
   __VERIFIER_assert(found == 0 || found == 1);
 }