Syntax fixes 2

src/example-archive/c-testsuite/working/00021.working.c

@@ -4,8 +4,8 @@ foo(int a, int b)
 			let mid = (2i64 + (i64) a);
 			let res = mid - (i64) b;  
 			(i64) MINi32() <= mid; mid <= (i64) MAXi32(); 
-			(i64) MINi32() <= res; res <= (i64) MAXi32(); @*/
-/*@ ensures return == (2i32 + a) - b; @*/
+			(i64) MINi32() <= res; res <= (i64) MAXi32(); 
+    ensures return == (2i32 + a) - b; @*/
 {
 	return 2 + a - b;
 }

src/example-archive/c-testsuite/working/00023.working.c

@@ -2,8 +2,8 @@ int x;
 
 int
 main()
-/*@ accesses x; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    ensures return == 0i32; @*/
 {
 	x = 0;
 	return x;

src/example-archive/c-testsuite/working/00024.working.c

@@ -4,8 +4,8 @@ s v;
 
 int
 main()
-/*@ accesses v; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses v;
+    ensures return == 0i32; @*/
 {
 	v.x = 1;
 	v.y = 2;

src/example-archive/c-testsuite/working/00033.working.c

@@ -3,8 +3,8 @@ int g;
 int
 effect()
 /*@ requires 
-        take Pre = RW<int>(&g); @*/
-/*@ ensures 
+        take Pre = RW<int>(&g);
+    ensures 
         take Post = RW<int>(&g); 
         Post == 1i32;  
         return == 1i32; @*/
@@ -16,10 +16,10 @@ effect()
 int
 main()
 /*@ requires 
-        take Pre = RW<int>(&g); @*/
-/*@ ensures 
-        take Post = RW<int>(&g); @*/
-/*@ ensures return == 0i32; @*/
+        take Pre = RW<int>(&g);
+    ensures 
+        take Post = RW<int>(&g);
+        return == 0i32; @*/
 {
     int x;
 

src/example-archive/c-testsuite/working/00047.working.c

@@ -2,12 +2,12 @@ struct { int a; int b; int c; } s = {1, 2, 3};
 
 int
 main()
-/*@ accesses s; @*/
-/*@ requires 
+/*@ accesses s;
+    requires 
 			s.a == 1i32;
 			s.b == 2i32; 
-			s.c == 3i32; @*/
-/*@ ensures return == 0i32; @*/
+			s.c == 3i32;
+    ensures return == 0i32; @*/
 {
 	if (s.a != 1)
 		return 1;

src/example-archive/c-testsuite/working/00048.working.c

@@ -3,11 +3,11 @@ struct S s = { .b = 2, .a = 1};
 
 int
 main()
-/*@ accesses s; @*/
-/*@ requires 
+/*@ accesses s;
+    requires 
 			s.a == 1i32;
-			s.b == 2i32; @*/
-/*@ ensures return == 0i32; @*/
+			s.b == 2i32;
+    ensures return == 0i32; @*/
 {
 	if(s.a != 1)
 		return 1;

src/example-archive/c-testsuite/working/00062.working.c

@@ -16,9 +16,9 @@ int x = 0;
 
 int
 main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }

src/example-archive/c-testsuite/working/00067.working.c

@@ -13,9 +13,9 @@ int x = 1;
 #endif
 
 int main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }

src/example-archive/c-testsuite/working/00068.working.c

@@ -8,9 +8,9 @@ X
 
 int
 main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }

src/example-archive/c-testsuite/working/00069.working.c

@@ -8,9 +8,9 @@ int x = 0;
 
 int
 main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }

src/example-archive/c-testsuite/working/00070.working.c

@@ -10,9 +10,9 @@ X
 
 int
 main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }

src/example-archive/c-testsuite/working/00078.working.c

@@ -1,8 +1,8 @@
 int
 f1(char *p)
 /*@ requires 
-			take PreP = RW<char>(p); @*/
-/*@ ensures 
+			take PreP = RW<char>(p);
+    ensures 
 			take PostP = RW<char>(p);
 			return == 1i32 + (i32) PreP; @*/
 {

src/example-archive/c-testsuite/working/00090.working.c

@@ -4,13 +4,13 @@ int a[3] = {0, 1, 2};
 
 int
 main()
-/*@ accesses a; @*/
-/*@ requires 
+/*@ accesses a;
+    requires 
 			a[0u64] == 0i32; 
 			a[1u64] == 1i32; 
 			a[2u64] == 2i32; 
-			@*/
-/*@ ensures return == 0i32; @*/
+
+    ensures return == 0i32; @*/
 {
 	/*@ focus RW<int>, 0u64; @*/
 	/*@ focus RW<int>, 1u64; @*/

src/example-archive/c-testsuite/working/00096.working.c

@@ -2,8 +2,8 @@ int x, x = 3, x;
 
 int
 main()
-/*@ accesses x; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    ensures return == 0i32; @*/
 {
 	if (x != 3)
 		return 0;

src/example-archive/c-testsuite/working/00107.working.c

@@ -3,9 +3,9 @@ myint x = (myint)1;
 
 int
 main(void)
-/*@ accesses x; @*/
-/*@ requires x == 1i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 1i32;
+    ensures return == 0i32; @*/
 {
 	return x-1;
 }

src/example-archive/c-testsuite/working/00146.working.c

@@ -3,11 +3,11 @@ struct S s = {1, 2};
 
 int
 main()
-/*@ accesses s; @*/
-/*@ requires 
+/*@ accesses s;
+    requires 
 			s.a == 1i32; 
-			s.b == 2i32; @*/
-/*@ ensures return == 0i32; @*/
+			s.b == 2i32;
+    ensures return == 0i32; @*/
 {
 	if(s.a != 1)
 		return 1;

src/example-archive/dafny-tutorial/working/abs_1.c

@@ -14,8 +14,8 @@ function (i32) abs_spec(i32 x)
 int abs(int x)
 /*@ requires 
       let MINi32 = (i64) -2147483647i64;
-      MINi32 < (i64) x; @*/
-/*@ ensures 
+      MINi32 < (i64) x;
+    ensures 
       0i32 <= return; 
       (x < 0i32 && return == (0i32 - x)) || (0i32 <= x && return == x); 
       0i32 <= return && (return == x || return == (0i32 - x));  // Same property

src/example-archive/dafny-tutorial/working/abs_2.c

@@ -6,8 +6,8 @@ int abs_2(int x)
       let MINi32 = (i64) -2147483647i64;
 
       MINi32 <= (i64) x; 
-      x < 0i32; @*/
-/*@ ensures 
+      x < 0i32;
+    ensures 
       0i32 <= return; 
       (return == x || return == (0i32 - x)); @*/
 {

src/example-archive/dafny-tutorial/working/abs_3.c

@@ -3,8 +3,8 @@
 
 int abs_3(int x)
 /*@ requires 
-      x == (0i32 - 1i32); @*/ // TODO: syntax is bad 
-/*@ ensures 
+      x == (0i32 - 1i32);  // TODO: syntax is bad 
+    ensures 
       0i32 <= return;
       (return == x || return == (0i32 - x)); 
       return == 1i32; @*/

src/example-archive/dafny-tutorial/working/binary_search.c

@@ -8,8 +8,8 @@ int binary_search(int *a, int length, int value)
       0i32 <= length; 
       (2i64 * (i64) length) <= MAXi32; 
       take IndexPre = each (i32 j; 0i32 <= j && j < length)
-                           {RW<int>(a + j)}; @*/
-/*@ ensures 
+                           {RW<int>(a + j)};
+    ensures 
       take IndexPost = each (i32 j; 0i32 <= j && j < length)
                             {RW<int>(a + j)}; 
       IndexPost == IndexPre; 

src/example-archive/dafny-tutorial/working/linear_search.c

@@ -4,8 +4,8 @@ int linear_search(int *a, int length, int key)
 /*@ requires 
       0i32 < length; 
       take IndexPre = each (i32 j; 0i32 <= j && j < length)
-                           {RW<int>(a + j)}; @*/
-/*@ ensures 
+                           {RW<int>(a + j)};
+    ensures 
       take IndexPost = each (i32 j; 0i32 <= j && j < length)
                             {RW<int>(a + j)};
       (return < 0i32) || (IndexPost[return] == key); 

src/example-archive/dafny-tutorial/working/max.c

@@ -14,8 +14,8 @@ function (i32) max_spec (i32 a, i32 b)
 
 int max(int a, int b)
 /*@ ensures 
-      (a >= b && return == a) || (a < b && return == b); @*/
-/*@ ensures 
+      (a >= b && return == a) || (a < b && return == b);
+
       return == max_spec(a,b); @*/
 {
   if (a > b)

src/example-archive/dafny-tutorial/working/multiple_returns.c

@@ -17,8 +17,8 @@ void multiple_returns(int x, int y, struct int_pair *ret)
       MINi32 <= (i64) x + (i64) y; 
       (i64) x + (i64) y <= MAXi32;
       MINi32 <= (i64) x - (i64) y; 
-      (i64) x - (i64) y <= MAXi32;  @*/
-/*@ ensures 
+      (i64) x - (i64) y <= MAXi32;
+    ensures 
       take PairPost = RW<struct int_pair>(ret);
       PairPost.fst == x + y;
       PairPost.snd == x - y; @*/

src/example-archive/should-fail/working/c_sequencing_race.c

@@ -2,9 +2,9 @@
 
 int
 f (int *x)
-/*@ requires take xv = RW(x); @*/
-/*@ requires 0i32 <= xv && xv < 500i32; @*/
-/*@ ensures take xv2 = RW(x); @*/
+/*@ requires take xv = RW(x);
+             0i32 <= xv && xv < 500i32;
+    ensures take xv2 = RW(x); @*/
 {
   return ((*x) + (*x));
 }

src/example-archive/simple-examples/working/add_1.c

@@ -3,8 +3,8 @@
 // non-faulting.
 
 signed int add_1(signed int x, signed int y)
-/*@ requires x == 0i32; y == 0i32; @*/
-/*@ ensures return == x + y; @*/
+/*@ requires x == 0i32; y == 0i32;
+    ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;

src/example-archive/simple-examples/working/add_2.c

@@ -2,8 +2,8 @@
 // requires-clause sets one integer to be zero 
 
 signed int add_2(signed int x, signed int y)
-/*@ requires x == 0i32; @*/
-/*@ ensures return == y; @*/
+/*@ requires x == 0i32;
+    ensures return == y; @*/
 {
   signed int i;
   i = x + y;

src/example-archive/simple-examples/working/add_3.c

@@ -6,8 +6,8 @@ signed int add_3(signed int x, signed int y)
       let MAXi32 = 2147483647i64; 
       let MINi32 = -2147483648i64;
       let sum = (i64) x + (i64) y;
-      MINi32 <= sum; sum <= MAXi32; @*/
-/*@ ensures return == x + y; @*/
+      MINi32 <= sum; sum <= MAXi32;
+    ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;

src/example-archive/simple-examples/working/add_4.c

@@ -3,8 +3,8 @@
 signed int inc_1(signed int i)
 /*@ requires 
       let MAXi32 = 2147483647i64; 
-      (i64) i + 1i64 <  MAXi32; @*/
-/*@ ensures return == i + 1i32; @*/
+      (i64) i + 1i64 <  MAXi32;
+    ensures return == i + 1i32; @*/
 {
   i = i + 1;
   return i;

src/example-archive/simple-examples/working/add_5.c

@@ -4,8 +4,8 @@
 signed int add_5(signed int x, signed int y)
 /*@ requires 
       let sum = (i64) x + (i64) y;
-      (i64) MINi32() <= sum; sum <= (i64) MAXi32(); @*/
-/*@ ensures return == x + y; @*/
+      (i64) MINi32() <= sum; sum <= (i64) MAXi32();
+    ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;

src/example-archive/simple-examples/working/add_uint_1.c

@@ -4,8 +4,8 @@
 unsigned int add_uint_1(unsigned int x, unsigned int y)
 /*@ requires 
       let MAXi32 = 2147483647i64;
-      (i64) x + (i64) y <= MAXi32; @*/
-/*@ ensures return == x + y; @*/
+      (i64) x + (i64) y <= MAXi32;
+    ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;

src/example-archive/simple-examples/working/array_1.c

@@ -4,8 +4,8 @@ void array_1(int *arr, int size, int off)
 /*@ requires 
       take arrayStart = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; 
       0i32 <= off; 
-      off < size; @*/
-/*@ ensures take arrayEnd = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; @*/
+      off < size;
+    ensures take arrayEnd = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; @*/
 {
   int i = off;
   /*@ focus RW<int>, i; @*/  // <-- required to read / write