Commit 13bb0479 authored by Patrick Baudin's avatar Patrick Baudin Committed by Virgile Prevosto
Browse files

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

parent 787a94b0
......@@ -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
......
......@@ -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);
......
......@@ -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;
}
......
......@@ -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];
......
......@@ -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)) {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment