Merge branch 'fixes/patrick/acsl-cast-from-ptr-to-array' into 'master'

[ACSL] replace (T[size])(ptr) by *((T(*)[size])(ptr))

Closes #780

See merge request frama-c/frama-c!2510

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

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);

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;
 }

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];

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)) {