From 13bb04796abe461e65f48c3d5bf00e87c68b738e Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 4 Mar 2020 16:26:13 +0100
Subject: [PATCH] [ACSL] replace (T[size])(ptr) by *((T(*)[size])(ptr))

---
 src/kernel_services/ast_queries/logic_typing.ml | 6 +++++-
 tests/spec/oracle/bsearch.res.oracle            | 2 +-
 tests/spec/oracle/bts0698.res.oracle            | 4 ++--
 tests/spec/oracle/logic_type.res.oracle         | 2 +-
 tests/spec/oracle/max.res.oracle                | 4 ++--
 5 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 3b44f67953d..6b9c41fd271 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1098,7 +1098,11 @@ struct
         (* we have converted from array to ptr, but the pointed type might
            differ. Just do another round of conversion. *)
         c_mk_cast e oldt newt
-      end else begin
+      end else if isPointerType oldt && isArrayType newt then
+        (* transforms '(T[size])ptr' into an equivalent '*(T( * )[size])ptr'
+           to get an explicit access to the memory *)
+        mk_mem (c_mk_cast ~force e oldt (TPtr(newt,[]))) TNoOffset
+      else begin
         match Cil.unrollType newt, e.term_node with
         | TEnum (ei,[]), TConst (LEnum { eihost = ei'})
           when ei.ename = ei'.ename && not force -> e
diff --git a/tests/spec/oracle/bsearch.res.oracle b/tests/spec/oracle/bsearch.res.oracle
index a98b495d6d0..eda650f839b 100644
--- a/tests/spec/oracle/bsearch.res.oracle
+++ b/tests/spec/oracle/bsearch.res.oracle
@@ -9,7 +9,7 @@ predicate sorted{L}(int t[], ℤ n) =
   ∀ ℤ i, ℤ j; 0 ≤ i ≤ j ≤ n ⇒ t[i] ≤ t[j];
  */
 /*@ requires
-      n ≥ 0 ∧ \valid(t + (0 .. n - 1)) ∧ sorted((int [])t, n - 1);
+      n ≥ 0 ∧ \valid(t + (0 .. n - 1)) ∧ sorted(*((int (*)[])t), n - 1);
     
     behavior search_success:
       ensures \result ≥ 0 ⇒ *(\old(t) + \result) ≡ \old(v);
diff --git a/tests/spec/oracle/bts0698.res.oracle b/tests/spec/oracle/bts0698.res.oracle
index ba90e50ce66..5de673e30c6 100644
--- a/tests/spec/oracle/bts0698.res.oracle
+++ b/tests/spec/oracle/bts0698.res.oracle
@@ -6,7 +6,7 @@
  */
 /*@ predicate Q{L}(int *x) = *(x + 0) < *(x + 1);
  */
-/*@ predicate Correct{L}(int *x) = P((int [2])x);
+/*@ predicate Correct{L}(int *x) = P(*((int (*)[2])x));
  */
 int t[2];
 int *a;
@@ -24,7 +24,7 @@ void g(void)
 {
   *(a + 0) = 10;
   *(a + 1) = 20;
-  /*@ assert P((int [2])a); */ ;
+  /*@ assert P(*((int (*)[2])a)); */ ;
   /*@ assert Q(a); */ ;
   return;
 }
diff --git a/tests/spec/oracle/logic_type.res.oracle b/tests/spec/oracle/logic_type.res.oracle
index c7f4d27c228..1343fa5755c 100644
--- a/tests/spec/oracle/logic_type.res.oracle
+++ b/tests/spec/oracle/logic_type.res.oracle
@@ -39,7 +39,7 @@ axiomatic A {
   }
  */
 /*@ ensures Q(\old(q));
-    ensures P((Point [3])\old(q)); */
+    ensures P(*((Point (*)[3])\old(q))); */
 void f(Point *q);
 
 Point tab[3];
diff --git a/tests/spec/oracle/max.res.oracle b/tests/spec/oracle/max.res.oracle
index cc622e41cea..e0dd4a2052e 100644
--- a/tests/spec/oracle/max.res.oracle
+++ b/tests/spec/oracle/max.res.oracle
@@ -26,7 +26,7 @@ axiomatic IsMax {
         0 ≤ \result < \old(n) ∧
         (∀ int i;
            0 ≤ i < \old(n) ⇒ *(\old(t) + \result) ≥ *(\old(t) + i)) ∧
-        is_max(*(\old(t) + \result), (int [])\old(t), \old(n));
+        is_max(*(\old(t) + \result), *((int (*)[])\old(t)), \old(n));
     
     behavior empty:
       assumes n ≤ 0;
@@ -46,7 +46,7 @@ int max(int *t, int n)
   i = 1;
   /*@ loop invariant
         (∀ int j; 0 ≤ j < i ⇒ *(t + imax) ≥ *(t + j)) ∧
-        is_max(max_0, (int [])t, i - 1);
+        is_max(max_0, *((int (*)[])t), i - 1);
   */
   while (i < n) {
     if (*(t + i) > *(t + imax)) {
-- 
GitLab