--- layout: fc_discuss_archives title: Message 30 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



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>