[wp] Format test files for chunk types

src/plugins/wp/tests/wp_acsl/chunk_typing.i

@@ -5,50 +5,50 @@
    OPT: -wp-rte -wp-prop="-NO_CHECK,-rte"
 */
 
-const char x[10] ;
+const char x[10];
 
 /*@
-	requires \valid(&i8[0..9])  && \valid(&u8[0..9])  && \valid(&i16[0..9]) && \valid(&u16[0..9])
-        && \valid(&i32[0..9]) && \valid(&u32[0..9]) && \valid(&i64[0..9]) && \valid(&u64[0..9]);
-	ensures \forall integer k ;
-	        0 <= k < 10 ==>
-					  x[k]+8   ==
-						i8[k]+7  == u8[k]+6 ==
-						i16[k]+5 ==	u16[k]+4 ==
-						i32[k]+3 ==	u32[k]+2 ==
-						i64[k]+1 ==	u64[k];
+  requires \valid(&i8[0..9])  && \valid(&u8[0..9])  && \valid(&i16[0..9])
+        && \valid(&u16[0..9]) && \valid(&i32[0..9]) && \valid(&u32[0..9])
+        && \valid(&i64[0..9]) && \valid(&u64[0..9]);
+  ensures
+    \forall integer k ; 0 <= k < 10 ==> x[k]+8
+                                     == i8[k]+7  == u8[k]+6
+                                     == i16[k]+5 == u16[k]+4
+                                     == i32[k]+3 == u32[k]+2
+                                     == i64[k]+1 == u64[k];
 */
 void function(signed char i8[10],
-							unsigned char u8[10],
-							signed short i16[10],
-							unsigned short u16[10],
-							signed int i32[10],
-							unsigned int u32[10],
-							signed long long int i64[10],
-							unsigned long long int u64[10])
+              unsigned char u8[10],
+              signed short i16[10],
+              unsigned short u16[10],
+              signed int i32[10],
+              unsigned int u32[10],
+              signed long long int i64[10],
+              unsigned long long int u64[10])
 {
-	/*@
-		loop invariant NO_CHECK: 0 <= i <= 10;
-		loop invariant \forall integer k ; 0 <= k < i ==> i8[k] == 1 ;
-		loop invariant \forall integer k ; 0 <= k < i ==> u8[k] == 2 ;
-		loop invariant \forall integer k ; 0 <= k < i ==> i16[k] == 3 ;
-		loop invariant \forall integer k ; 0 <= k < i ==> u16[k] == 4 ;
-		loop invariant \forall integer k ; 0 <= k < i ==> i32[k] == 5 ;
-		loop invariant \forall integer k ; 0 <= k < i ==> u32[k] == 6 ;
-		loop invariant \forall integer k ; 0 <= k < i ==> i64[k] == 7 ;
-		loop invariant \forall integer k ; 0 <= k < i ==> u64[k] == 8 ;
-		loop assigns NO_CHECK: i, i8[0..9], u8[0..9], i16[0..9], u16[0..9], i32[0..9], u32[0..9], i64[0..9], u64[0..9] ;
-		loop variant NO_CHECK: 10-i;
- 	*/
-	for(int i = 0; i < 10; ++i){
-		i8[i] = 1 ;
-		u8[i] = 2 ;
-		i16[i] = 3 ;
-		u16[i] = 4 ;
-		i32[i] = 5 ;
-		u32[i] = 6 ;
-		i64[i] = 7 ;
-		u64[i] = 8 ;
-	}
+  /*@
+    loop invariant NO_CHECK: 0 <= i <= 10;
+    loop invariant \forall integer k ; 0 <= k < i ==> i8[k] == 1 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> u8[k] == 2 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> i16[k] == 3 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> u16[k] == 4 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> i32[k] == 5 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> u32[k] == 6 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> i64[k] == 7 ;
+    loop invariant \forall integer k ; 0 <= k < i ==> u64[k] == 8 ;
+    loop assigns NO_CHECK: i, i8[0..9], u8[0..9], i16[0..9], u16[0..9],
+                           i32[0..9], u32[0..9], i64[0..9], u64[0..9] ;
+    loop variant NO_CHECK: 10-i;
+  */
+  for (int i = 0; i < 10; ++i) {
+    i8[i] = 1;
+    u8[i] = 2;
+    i16[i] = 3;
+    u16[i] = 4;
+    i32[i] = 5;
+    u32[i] = 6;
+    i64[i] = 7;
+    u64[i] = 8;
+  }
 }
-

src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i

@@ -39,8 +39,8 @@ void usable_axiom(int* a, unsigned b, unsigned e){
 */
 
 /*@
-	requires b < s <= e;
-	ensures \forall int v ; occ(v,a,b,e) == occ(v,a,b,s) + occ(v,a,s,e) ;
+  requires b < s <= e;
+  ensures \forall int v ; occ(v,a,b,e) == occ(v,a,b,s) + occ(v,a,s,e) ;
 */
 void usable_lemma(int* a, unsigned b, unsigned s, unsigned e){
 

src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle

@@ -7,7 +7,7 @@
   Function function
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_acsl/chunk_typing.i, line 13) in 'function':
+Goal Post-condition (file tests/wp_acsl/chunk_typing.i, line 15) in 'function':
 Let a = shift_sint8(i8_0, 0).
 Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, 10).
 Let a_2 = shift_uint8(u8_0, 0).