--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about partition.c



Dear All,

when analyzing the following C source
(from http://www3.di.uminho.pt/~jsp/RSD-book/Frama-c-safety.pdf) with
frama-c-Neon/WP in the typed model with split

/*@ requires \valid(t)
    && \valid(t+i) && \valid(t+j);
  @*/
void swap(int t[], int i, int j) {
  int tmp = t[i];
  t[i] = t[j];
  t[j] = tmp;
}
/*@ requires 0 <= p <= r && \valid_range(A,p,r);
  @*/
int partition (int A[], int p, int r)
{
  int x = A[r];
  int tmp, j, i = p-1;
  /*@ loop invariant p <= j <= r
                     && p-1 <= i < j
		     && \valid(A+j)
		     && \valid(A+i+1);
    @ loop variant (r-j);
    @*/
  for (j=p; j<r; j++)
    if (A[j] <= x) {
      i++;
      swap(A,i,j);
    }
  swap(A,i+1,r);
  return i+1;
}

there are 3 POs from the invariant that are not discharged. For
example:

Goal Preservation of Invariant (file ../../frama-c/partition-10.3.c, line 14) (5/12):
Tags: Then Then.
Let x_1 = 1+j_1.
Let x_2 = 1+i_1.
Let a_0 = (shift A_0 j_1).
Let x_3 = Mint_0[a_0].
Assume {
  (* Domain *)
  Type: (is_sint32 i_1) /\ (is_sint32 j_1) /\ (is_sint32 p_0)
        /\ (is_sint32 p_1) /\ (is_sint32 r_0) /\ (is_sint32 r_3)
        /\ (is_sint32 x_0) /\ (is_sint32 x_2) /\ (is_sint32 x_1)
        /\ (is_sint32 x_3).
  (* Heap *)
  Have: (linked Malloc_5).
  (* Pre-condition (file ../../frama-c/partition-10.3.c, line 8) in 'partition' *)
  (* Pre-condition: *)
  Have: (0<=p_1) /\ (p_1<=r_3)
        /\ (valid_rw Malloc_5 (shift A_3 p_1) (1+r_3-p_1)).
  (* Assertion 'rte,mem_access' (file ../../frama-c/partition-10.3.c, line 12) *)
  (* ../../frama-c/partition-10.3.c:12: Assertion 'rte,mem_access': *)
  Have: (valid_rd Malloc_5 (shift A_3 r_3) 1).
  (* Assertion 'rte,signed_overflow' (file ../../frama-c/partition-10.3.c, line 13) *)
  (* ../../frama-c/partition-10.3.c:13: Assertion 'rte,signed_overflow': *)
  Have: -2147483647<=p_1.
  (* Invariant (file ../../frama-c/partition-10.3.c, line 14) *)
  (* ../../frama-c/partition-10.3.c:17: Invariant: *)
  Have: (i_1<j_1) /\ (j_1<=r_0) /\ (p_0<=j_1) /\ (p_0<=x_2)
        /\ (valid_rw Malloc_1 a_0 1)
        /\ (valid_rw Malloc_1 (shift (shift A_0 i_1) 1) 1).
  (* ../../frama-c/partition-10.3.c:17: Then *)
  Have: j_1<r_0.
  (* Assertion 'rte,mem_access' (file ../../frama-c/partition-10.3.c, line 18) *)
  (* ../../frama-c/partition-10.3.c:18: Assertion 'rte,mem_access': *)
  Have: (valid_rd Malloc_1 a_0 1).
  (* ../../frama-c/partition-10.3.c:18: Then *)
  Have: x_3<=x_0.
  (* Assertion 'rte,signed_overflow' (file ../../frama-c/partition-10.3.c, line 19) *)
  (* ../../frama-c/partition-10.3.c:19: Assertion 'rte,signed_overflow': *)
  Have: i_1<=2147483646.
  (* ../../frama-c/partition-10.3.c:20: Call 'swap' *)
  Have: (valid_rw Malloc_1 A_0 1) /\ (valid_rw Malloc_1 (shift A_0 x_2) 1).
  (* Assertion 'rte,signed_overflow' (file ../../frama-c/partition-10.3.c, line 17) *)
  (* ../../frama-c/partition-10.3.c:17: Assertion 'rte,signed_overflow': *)
  Have: j_1<=2147483646.
}
Prove: (valid_rw Malloc_0 (shift A_0 x_1) 1).
Prover Alt-Ergo returns Unknown (Qed:3ms) (1s)

I fail to see why this PO is not automatically discharged. Also, how
are the _0, _1, etc suffixes supposed to be read?

Thanks in advance and best regards,

Marko
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP Digital Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150128/6cd07b8d/attachment.sig>