Fixed formatting issues

Author: SaswatPadhi

regression/contracts/invar_check_break_fail/main.c

@@ -7,17 +7,17 @@ int main()
 
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
-  { 
-    --r;
-    if (r <= 1)
-    {
-      break;
-    }
-    else
     {
       --r;
+      if(r <= 1)
+      {
+        break;
+      }
+      else
+      {
+        --r;
+      }
     }
-  }
 
   assert(r == 0);
 

regression/contracts/invar_check_break_pass/main.c

@@ -7,17 +7,17 @@ int main()
 
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
-  { 
-    --r;
-    if (r <= 1)
-    {
-      break;
-    }
-    else
     {
       --r;
+      if(r <= 1)
+      {
+        break;
+      }
+      else
+      {
+        --r;
+      }
     }
-  }
 
   assert(r == 0 || r == 1);
 

regression/contracts/invar_check_continue/main.c

@@ -7,17 +7,17 @@ int main()
 
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
-  { 
-    --r;
-    if (r < 5)
-    {
-      continue;
-    }
-    else
     {
       --r;
+      if(r < 5)
+      {
+        continue;
+      }
+      else
+      {
+        --r;
+      }
     }
-  }
 
   assert(r == 0);
 

regression/contracts/invar_check_large/main.c

@@ -8,13 +8,13 @@ void swap(int *a, int *b)
 }
 
 int main()
-{ 
+{
   int arr0, arr1, arr2, arr3, arr4;
   arr0 = 1;
   arr1 = 2;
   arr2 = 0;
   arr3 = 4;
-  arr4 = 3; 
+  arr4 = 3;
   int *arr[5] = {&arr0, &arr1, &arr2, &arr3, &arr4};
   int pivot = 2;
 
@@ -23,6 +23,8 @@ int main()
   int r = 1;
   while(h > l)
     __CPROVER_loop_invariant(
+      // Turn off `clang-format` because it breaks the `==>` operator.
+      /* clang-format off */
       h >= l &&
       0 <= l && l < 5 &&
       0 <= h && h < 5 &&
@@ -42,27 +44,35 @@ int main()
       (2 > h ==> arr2 >= pivot) &&
       (3 > h ==> arr3 >= pivot) &&
       (4 > h ==> arr4 >= pivot)
+      /* clang-format on */
     )
-  {
-    if(*(arr[h]) <= pivot && *(arr[l]) >= pivot) {
-      swap(arr[h], arr[l]);
-      if (r == h) {
-        r = l;
-        h--;
+    {
+      if(*(arr[h]) <= pivot && *(arr[l]) >= pivot)
+      {
+        swap(arr[h], arr[l]);
+        if(r == h)
+        {
+          r = l;
+          h--;
+        }
+        else if(r == l)
+        {
+          r = h;
+          l++;
+        }
       }
-      else if(r == l) {
-        r = h;
+      else if(*(arr[h]) <= pivot)
+      {
         l++;
       }
+      else
+      {
+        h--;
+      }
     }
-    else if(*(arr[h]) <= pivot) {
-      l++;
-    }
-    else {
-      h--;
-    }
-  }
 
+  // Turn off `clang-format` because it breaks the `==>` operator.
+  /* clang-format off */
   assert(0 <= r && r < 5);
   assert(*(arr[r]) == pivot);
   assert(0 < r ==> arr0 <= pivot);
@@ -75,6 +85,7 @@ int main()
   assert(2 > r ==> arr2 >= pivot);
   assert(3 > r ==> arr3 >= pivot);
   assert(4 > r ==> arr4 >= pivot);
+  /* clang-format on */
 
   return r;
 }

regression/contracts/invar_check_multiple_loops/main.c

@@ -6,22 +6,16 @@ int main()
   __CPROVER_assume(n > 0 && x == y);
 
   for(r = 0; r < n; ++r)
-    __CPROVER_loop_invariant(
-      0 <= r && r <= n &&
-      x == y + r
-    )
-  {
-    x++;
-  }
+    __CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)
+    {
+      x++;
+    }
   while(r > 0)
-    __CPROVER_loop_invariant(
-      r >= 0 &&
-      x == y + n + (n - r)
-    )
-  {
-    y--;
-    r--;
-  }
+    __CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))
+    {
+      y--;
+      r--;
+    }
 
   assert(x == y + 2 * n);
 

regression/contracts/invar_check_nested_loops/main.c

@@ -6,26 +6,20 @@ int main()
   __CPROVER_assume(n >= 0);
 
   for(int i = 0; i < n; ++i)
-    __CPROVER_loop_invariant(
-      i <= n &&
-      s == i
-    )
-  {
-    int a, b;
-    __CPROVER_assume(b >= 0 && a == b);
-
-    while(a > 0)
-      __CPROVER_loop_invariant(
-        a >= 0 &&
-        s == i + (b - a)
-      )
+    __CPROVER_loop_invariant(i <= n && s == i)
     {
-      s++;
-      a--;
-    }
+      int a, b;
+      __CPROVER_assume(b >= 0 && a == b);
 
-    s -= (b - 1);
-  }
+      while(a > 0)
+        __CPROVER_loop_invariant(a >= 0 && s == i + (b - a))
+        {
+          s++;
+          a--;
+        }
+
+      s -= (b - 1);
+    }
 
   assert(s == n);
 

regression/contracts/invar_check_sufficiency/main.c

@@ -7,9 +7,9 @@ int main()
 
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
-  {
-    --r;
-  }
+    {
+      --r;
+    }
 
   assert(r == 0);
 

regression/contracts/invar_loop_constant_fail/main.c

@@ -7,10 +7,10 @@ int main()
   __CPROVER_assume(r >= 0);
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
-  {
-    s = 1;
-    r--;
-  }
+    {
+      s = 1;
+      r--;
+    }
   assert(r == 0);
   assert(s == 1);
 

regression/contracts/invar_loop_constant_no_modify/main.c

@@ -7,9 +7,9 @@ int main()
   __CPROVER_assume(r >= 0);
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
-  {
-    r--;
-  }
+    {
+      r--;
+    }
   assert(r == 0);
   assert(s == 1);
 

regression/contracts/invar_loop_constant_pass/main.c

@@ -6,10 +6,10 @@ int main()
   __CPROVER_assume(r >= 0);
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0 && s == 1)
-  {
-    s = 1;
-    r--;
-  }
+    {
+      s = 1;
+      r--;
+    }
   assert(r == 0);
   assert(s == 1);