Disable clang-format for quantifier regression tests

Several of them use implication (==>), which clang-format does not know how to
deal with as is isn't a native C/C++ operator. Line numbers in the test.desc
files are updated given the comment lines have been inserted.

Author: tautschnig

regression/cbmc/Quantifiers-assertion/main.c

@@ -7,6 +7,8 @@ int main()
   c[1][0]=1;
   c[1][1]=2;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assert(__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "Exists-Exists: successful");
 
   __CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-NotExists: successful");
@@ -18,6 +20,7 @@ int main()
   __CPROVER_assert(!__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotForall-Forall: successful");
 
   __CPROVER_assert(!__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotForall-NotForall: successful");
+  // clang-format on
 
   return 0;
 }

regression/cbmc/Quantifiers-assignment/main.c

@@ -4,10 +4,13 @@ int main()
   a[0]=1;
   a[1]=2;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   int x=__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 };
   int y=__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<2 };
   int z1=__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<1.5 };
   int z2=__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<2*10 };
+  // clang-format on
 
   assert(x);
   assert(y);

regression/cbmc/Quantifiers-copy/main.c

@@ -9,7 +9,10 @@ int main()
   a[3]=3;
   a[4]=4;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> b[i]==a[i]});
+  // clang-format on
 
   assert(b[0]==0);
   assert(b[1]==1);

regression/cbmc/Quantifiers-if/main.c

@@ -4,6 +4,8 @@ int main()
   a[0]=1;
   a[1]=2;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   if(__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
     __CPROVER_assert(0, "failure 1");
 
@@ -18,6 +20,7 @@ int main()
 
   if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 })
     __CPROVER_assert(0, "success 2");
+  // clang-format on
 
   return 0;
 }

regression/cbmc/Quantifiers-initialisation/main.c

@@ -2,7 +2,10 @@ int main()
 {
   int a[5];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> a[i]==i+1});
+  // clang-format on
 
   assert(a[0]==1);
   assert(a[1]==2);

regression/cbmc/Quantifiers-initialisation2/main.c

@@ -3,6 +3,8 @@ int main()
   int a[10];
   int c[10];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   // C# style
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<9+1) ==> a[i]>=1 && a[i]<=10 });
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<10) ==>  __CPROVER_forall{int j; (j>i && j<10) ==> a[j]>a[i]} });
@@ -14,5 +16,6 @@ int main()
   assert(a[2]>a[3]);
   __CPROVER_assert(__CPROVER_forall {unsigned i; (i>=1 && i<10) ==> c[i-1]<=c[i]}, "forall c[]");
   assert(c[3]>=c[1]);
+  // clang-format on
   return 0;
 }

regression/cbmc/Quantifiers-invalid-var-range/main.c

@@ -2,7 +2,10 @@ int main()
 {
 
   int a[3][3];
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==>  __CPROVER_exists{int j; (j>=i && j<3) ==> a[i][j]==10} });
+  // clang-format on
 
   assert(a[0][0]==10||a[0][1]==10||a[0][2]==10);
 

regression/cbmc/Quantifiers-not-exists/main.c

@@ -6,13 +6,16 @@ int main()
   int c[2][2];
   int d[2][2];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> a[i][j]<=10}) });
 
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> b[i][j]>=1 && b[i][j]<=10}) });
 
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });
 
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> d[i][j]>=1 && d[i][j]<=10}) });
+  // clang-format on
 
 
   assert(a[0][0]>10);

regression/cbmc/Quantifiers-not-exists/test.desc

@@ -2,12 +2,12 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 18 assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.2\] line 20 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.3\] line 21 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.4\] line 23 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.5\] line 25 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.6\] line 26 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.1\] line 21 assertion a\[.*\]\[.*\] > 10: SUCCESS$
+^\[main.assertion.2\] line 23 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.3\] line 24 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.4\] line 26 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.5\] line 28 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.6\] line 29 assertion tmp_if_expr\$\d+: SUCCESS$
 ^\*\* 0 of 6 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

regression/cbmc/Quantifiers-not/main.c

@@ -4,6 +4,8 @@ int main()
   a[0]=1;
   a[1]=2;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   if(!__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
     __CPROVER_assert(0, "success 1");
 
@@ -18,6 +20,7 @@ int main()
 
   if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 })
     __CPROVER_assert(0, "failure 2");
+  // clang-format on
 
   return 0;
 }

regression/cbmc/Quantifiers-two-dimension-array/main.c

@@ -3,8 +3,11 @@ int main()
   int a[2][2];
   int b[2][2];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> a[i][j]==i+j}) });
   __CPROVER_assume(__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> b[i][j]==i+j+1}) });
+  // clang-format on
 
   assert(a[0][0]==0);
   assert(a[0][1]==1);

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -2,11 +2,11 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 9 assertion a\[.*\]\[.*\] == 0: SUCCESS$
-^\[main.assertion.2\] line 10 assertion a\[.*\]\[.*\] == 1: SUCCESS$
-^\[main.assertion.3\] line 11 assertion a\[.*\]\[.*\] == 1: SUCCESS$
-^\[main.assertion.4\] line 12 assertion a\[.*\]\[.*\] == 2: SUCCESS$
-^\[main.assertion.5\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.1\] line 12 assertion a\[.*\]\[.*\] == 0: SUCCESS$
+^\[main.assertion.2\] line 13 assertion a\[.*\]\[.*\] == 1: SUCCESS$
+^\[main.assertion.3\] line 14 assertion a\[.*\]\[.*\] == 1: SUCCESS$
+^\[main.assertion.4\] line 15 assertion a\[.*\]\[.*\] == 2: SUCCESS$
+^\[main.assertion.5\] line 16 assertion tmp_if_expr\$\d+: SUCCESS$
 ^\*\* 0 of 5 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

regression/cbmc/Quantifiers-type/main.c

@@ -3,8 +3,11 @@ int main()
   int a[2];
   int b[2];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume( __CPROVER_forall { float i; (i>=0 && i<2) ==> a[i]>=10 && a[i]<=10 } );
   __CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
+  // clang-format on
 
   assert(a[0]==10 && a[1]==10);
   assert(b[0]==10 && b[1]==10);

regression/cbmc/Quantifiers-type/test.desc

@@ -2,8 +2,8 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 9 assertion tmp_if_expr(\$\d+)?: FAILURE$
-^\[main.assertion.2\] line 10 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.1\] line 12 assertion tmp_if_expr(\$\d+)?: FAILURE$
+^\[main.assertion.2\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
 ^\*\* 1 of 2 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/Quantifiers1/main.c

@@ -2,6 +2,8 @@ int zero_array[10];
 
 int main()
 {
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   // C# style
   assert(__CPROVER_forall { int i; (i>=0 && i<10) ==> zero_array[i]==0 });
 
@@ -20,4 +22,5 @@ int main()
 
   assert(__CPROVER_forall {unsigned i; i>9 || c[i]==i});
   return 0;
+  // clang-format on
 }