better interpretation of ACSL annotations after commit 23496

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle

@@ -21,7 +21,7 @@ tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
 tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
 [value] using specification for function __initialized
 FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
-FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
+FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
@@ -31,7 +31,6 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
 [value] Values at end of function read_sensor_4:
   buf[0..11] ∈ {0} or UNINITIALIZED
 [value] Values at end of function main:
-  buf[0] ∈ {0}
-     [1..11] ∈ {0} or UNINITIALIZED
+  buf[0..11] ∈ {0}
   i ∈ {3}
   __retres ∈ {0}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle

@@ -21,7 +21,7 @@ tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
 tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
 [value] using specification for function __initialized
 FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
-FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
+FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
@@ -31,7 +31,6 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
 [value] Values at end of function read_sensor_4:
   buf[0..11] ∈ {0} or UNINITIALIZED
 [value] Values at end of function main:
-  buf[0] ∈ {0}
-     [1..11] ∈ {0} or UNINITIALIZED
+  buf[0..11] ∈ {0}
   i ∈ {3}
   __retres ∈ {0}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c

@@ -93,12 +93,13 @@ int main(void)
     read_sensor_4((unsigned int *)(buf) + i);
     i ++;
   }
-  /*@ assert \initialized((union msg *)buf); */
+  /*@ assert \initialized((union msg *)((unsigned char *)buf)); */
   {
     int __e_acsl_initialized;
     __e_acsl_initialized = __initialized((void *)(buf),sizeof(union msg));
     e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized((union msg *)buf)",25);
+                  (char *)"\\initialized((union msg *)((unsigned char *)buf))",
+                  25);
   }
   __retres = 0;
   __delete_block((void *)(buf));

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c

@@ -93,12 +93,13 @@ int main(void)
     read_sensor_4((unsigned int *)(buf) + i);
     i ++;
   }
-  /*@ assert \initialized((union msg *)buf); */
+  /*@ assert \initialized((union msg *)((unsigned char *)buf)); */
   {
     int __e_acsl_initialized;
     __e_acsl_initialized = __initialized((void *)(buf),sizeof(union msg));
     e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized((union msg *)buf)",25);
+                  (char *)"\\initialized((union msg *)((unsigned char *)buf))",
+                  25);
   }
   __retres = 0;
   __delete_block((void *)(buf));