From cdbacc6c0967499ff308e3bf191491317a6ff87d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Virgile=20Pr=C3=A9vosto?= <virgile.prevosto@cea.fr>
Date: Mon, 2 Sep 2013 13:59:12 +0000
Subject: [PATCH] better interpretation of ACSL annotations after commit 23496

---
 .../e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle  | 5 ++---
 .../e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle    | 5 ++---
 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c | 5 +++--
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c        | 5 +++--
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
index 7b027042371..15d013870c8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/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}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
index 7b027042371..15d013870c8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
+++ b/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}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
index 0b2f40b6bce..43635a8d405 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
+++ b/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));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
index 0b2f40b6bce..43635a8d405 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
+++ b/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));
-- 
GitLab