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

At Thu, 29 Jan 2015 19:47:52 +0100,
Claude Marche wrote:
> 
> 
> 
> On 01/29/2015 07:03 PM, Marko Sch?tz Schmuck wrote:
> > /*@ requires \valid(t)
> >      && \valid(t+i) && \valid(t+j);
> >    @*/
> 
> Why adding \valid(t) here ???

Thanks for your help.

That was one of the mutations I tried when getting all the POs of the
initial version discharged automatically. 

Even when I go back to that original version 

/*@ requires \valid_index(t,i) && \valid_index(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);
  @ assigns A[p..r];
  @*/
int partition (int A[], int p, int r)
{
  int x = A[r];
  int j, i = p-1;
  /*@ loop invariant p <= j <= r && p-1 <= i < j;
    @ loop variant (r-j);
    @*/
  for (j=p; j<r; j++)
    if (A[j] <= x) {
      swap(A,i,j);
      i++;
    }
  swap(A,i+1,r);
  return i+1;
}

the POs for the pre-condition of swap are not automatically discharged
and I'm left with e.g. 

Goal swap_pre_4: Pre-condition (file ../../frama-c/partition-10.3.c, line 1) in 'partition' at call 'swap' (file ../../frama-c/partition-10.3.c, line 20):
Let a_0 = (shift A_0 j_0).
Let x_1 = Mint_0[a_0].
Assume {
  (* Domain *)
  Type: (is_sint32 i_0) /\ (is_sint32 j_0) /\ (is_sint32 p_0)
        /\ (is_sint32 p_1) /\ (is_sint32 r_0) /\ (is_sint32 r_1)
        /\ (is_sint32 x_0) /\ (is_sint32 x_1).
  (* Heap *)
  Have: (linked Malloc_3).
  (* Pre-condition (file ../../frama-c/partition-10.3.c, line 8) in 'partition' *)
  (* Pre-condition: *)
  Have: (0<=p_1) /\ (p_1<=r_1)
        /\ (valid_rw Malloc_3 (shift A_3 p_1) (1+r_1-p_1)).
  (* Invariant (file ../../frama-c/partition-10.3.c, line 15) *)
  (* ../../frama-c/partition-10.3.c:18: Invariant: *)
  Have: (i_0<j_0) /\ (j_0<=r_0) /\ (p_0<=j_0) /\ (p_0<=(1+i_0)).
  (* ../../frama-c/partition-10.3.c:18: Then *)
  Have: j_0<r_0.
  (* ../../frama-c/partition-10.3.c:19: Then *)
  Have: x_1<=x_0.
}
Prove: (valid_rw Malloc_0 (shift A_0 i_0) 1) /\ (valid_rw Malloc_0 a_0 1).
Prover Alt-Ergo returns Unknown (Qed:1ms)

Is there some documentation about how to read this output?
Specifically, what do the _1, _3 etc mean? Do they stand for specific
program states? What does "linked" mean?

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/20150130/44610807/attachment.sig>