Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] question about partition.c
  • From: MarkoSchuetz at web.de (Marko Schütz Schmuck)
  • Date: Wed, 28 Jan 2015 10:25:41 -0400
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>