next to frama-c!1574: annotation changed in test files (preserving the semantics)

src/plugins/e-acsl/tests/runtime/base_addr.c

@@ -10,10 +10,10 @@ int *PA;
 int main(void) {
   /* Global memory */
   PA = (int*)&A;
-  /*@ assert \base_addr(A) == \base_addr(PA); */
+  /*@ assert \base_addr(&A[0]) == \base_addr(PA); */
   /*@ assert \base_addr(A+3) == \base_addr(PA); */
   PA++;
-  /*@ assert \base_addr(PA) == \base_addr(A); */
+  /*@ assert \base_addr(PA) == \base_addr(&A[0]); */
   /*@ assert \base_addr(PA+2) == \base_addr(A+3); */
 
   /* Stack memory [long blocks] */
@@ -21,11 +21,11 @@ int main(void) {
   int *pa;
   pa = (int*)&a;
 
-  /*@ assert \base_addr(a) == \base_addr(pa); */
+  /*@ assert \base_addr(&a[0]) == \base_addr(pa); */
   /*@ assert \base_addr(a+3) == \base_addr(pa); */
   pa++;
-  /*@ assert \base_addr(pa) == \base_addr(a); */
-  /*@ assert \base_addr(pa+2) == \base_addr(a); */
+  /*@ assert \base_addr(pa) == \base_addr(&a[0]); */
+  /*@ assert \base_addr(pa+2) == \base_addr(&a[0]); */
 
   /* Stack memory [Short blocks] */
   long l = 4;

src/plugins/e-acsl/tests/runtime/block_length.c

@@ -17,7 +17,7 @@ int main(void) {
 
   /* Global memory */
   PA = (int*)&A;
-  /*@ assert \block_length(A) == sizeof(A); */
+  /*@ assert \block_length(&A[0]) == sizeof(A); */
   /*@ assert \block_length(A+3) == sizeof(A); */
   /*@ assert \block_length(PA) == sizeof(A); */
   PA++;
@@ -26,7 +26,7 @@ int main(void) {
   /* Stack memory [long blocks] */
   int a[] = { 1, 2, 3, 4};
   int *pa = (int*)&a;
-  /*@ assert \block_length(a) == sizeof(a); */
+  /*@ assert \block_length(&a[0]) == sizeof(a); */
   /*@ assert \block_length(a+3) == sizeof(a); */
   /*@ assert \block_length(pa) == sizeof(a); */
   pa++;

src/plugins/e-acsl/tests/runtime/compound_initializers.c

@@ -30,12 +30,12 @@ struct ST _G[] = {
 };
 
 int main(int argc, char **argv) {
-    /*@ assert \valid(_A); */
+    /*@ assert \valid(&_A[0]); */
     /*@ assert \valid_read(_A[0]); */
     /*@ assert \valid_read(_A[1]); */
     /*@ assert \valid_read(_B); */
     /*@ assert \valid(&_C); */
-    /*@ assert \valid(_D); */
+    /*@ assert \valid(&_D[0]); */
     /*@ assert \valid(&_E); */
     /*@ assert \valid(&_F); */
     /*@ assert _E == 44; */

src/plugins/e-acsl/tests/runtime/freeable.c

@@ -21,6 +21,6 @@ int main(void) {
   /*@ assert ! \freeable(p); */
 
   // test cases for BTS #1830
-  /*@ assert ! \freeable(array); */
+  /*@ assert ! \freeable(&(array[0])); */
   /*@ assert ! \freeable(&(array[5])); */
 }

src/plugins/e-acsl/tests/runtime/initialized.c

@@ -41,21 +41,21 @@ int main(void) {
   /*@assert \initialized(&b); */
 
   r = d;
-  /*@assert ! \initialized(d); */
+  /*@assert ! \initialized(&d[0]); */
   /*@assert ! \initialized(d+1); */
   /*@assert ! \initialized(&d); */
   /*@assert ! \initialized(r); */
   /*@assert ! \initialized(r+1); */
 
   d[0] = 1;
-  /*@assert \initialized(d); */
+  /*@assert \initialized(&d[0]); */
   /*@assert ! \initialized(d+1); */
   /*@assert ! \initialized(&d); */
   /*@assert \initialized(r); */
   /*@assert ! \initialized(r+1); */
 
   d[1] = 1;
-  /*@assert \initialized(d); */
+  /*@assert \initialized(&d[0]); */
   /*@assert \initialized(d+1); */
   /*@assert \initialized(&d); */
   /*@assert \initialized(r); */

src/plugins/e-acsl/tests/runtime/offset.c

@@ -10,7 +10,7 @@ int *PA;
 int main(void) {
   /* Global memory */
   PA = (int*)&A;
-  /*@ assert \offset(A) == 0; */
+  /*@ assert \offset(&A[0]) == 0; */
   /*@ assert \offset(A+3) == 12; */
   /*@ assert \offset(PA) == 0; */
   PA++;
@@ -18,7 +18,7 @@ int main(void) {
 
   /* Stack memory [long blocks] */
   int a[] = { 1, 2, 3, 4};
-  /*@ assert \offset(a)   == 0; */
+  /*@ assert \offset(&a[0])   == 0; */
   /*@ assert \offset(a+1) == 4; */
   /*@ assert \offset(a+3) == 12; */