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] several WP questions

At Mon, 16 Feb 2015 11:29:02 +0100,
Lo?c Correnson wrote:
> 
> Hi,
> Instead of an axiomatic definition of the permutation, you should introduce the inverse indices array as a ghost variable, say ?rev?, maintain this array during the loop with ghost code and prove that rev[ind[i]]==i in suitable ranges.
> We already used such a technique to prove a bubble-sort algorithm with permutation indices bookkeeping.
> This is much easier than converting C-arrays to abstract lists : I?m afraid you will need, at some point, some frame lemmas to compare `arrayToList{A}` and `arrayToList{B}` when you have memory updates between points `A` and `B`.
> L.

thanks for the recommendation. I pursued this a bit, but got stuck
again. The following PO is not discharged:

Goal Assigns (file partition-mine-momomorphic-ghost.c, line 17) in 'partition' (4/4):
Effect at line 21
partition-mine-momomorphic-ghost.c:21: warning from Typed Model:
 - Warning: Call assigns everything, looking for context inconsistency
   Reason: Cast with incompatible pointers types (source: sint8*) (target: sint32*)
Let x_0 = 4*(to_uint32 length_4).
Let a_0 = (shift arr_6 0).
Let a_1 = (shift ind_7 0).
Assume {
  (* Domain *)
  Type: (is_sint32 length_4).
  (* Heap *)
  Have: (linked Malloc_4).
  (* Pre-condition (file partition-mine-momomorphic-ghost.c, line 11) in 'partition' *)
  (* Pre-condition: *)
  Have: (0<=length_4) /\ (valid_rw Malloc_4 a_0 length_4)
        /\ (valid_rw Malloc_4 a_1 length_4).
  (* Pre-condition (file partition-mine-momomorphic-ghost.c, line 12) in 'partition' *)
  (* Pre-condition: *)
  Have: (separated a_0 length_4 a_1 length_4).
  (* Pre-condition (file partition-mine-momomorphic-ghost.c, line 13) in 'partition' *)
  (* Pre-condition: *)
  Have: (4*length_4)<=4294967295.
  (* Assertion 'rte,signed_overflow' (file partition-mine-momomorphic-ghost.c, line 20) *)
  (* partition-mine-momomorphic-ghost.c:20: Assertion 'rte,signed_overflow': *)
  Have: -2147483647<=length_4.
  (* Assertion 'rte,unsigned_overflow' (file partition-mine-momomorphic-ghost.c, line 21) *)
  (* partition-mine-momomorphic-ghost.c:21: Assertion 'rte,unsigned_overflow': *)
  Have: 0<=x_0.
  (* Assertion 'rte,unsigned_overflow' (file partition-mine-momomorphic-ghost.c, line 21) *)
  (* partition-mine-momomorphic-ghost.c:21: Assertion 'rte,unsigned_overflow': *)
  Have: x_0<=4294967295.
}
Prove: false.
Prover Alt-Ergo returns Unknown

I suspect it is related to the implicit use of __builtin_alloca, but
could not yet find or come up with a way to handle it.

Any hints, ideas?

Thanks in advance,

Marko

> > Le 12 f?vr. 2015 ? 18:48, Marko Sch?tz Schmuck <MarkoSchuetz at web.de> a ?crit :
> > 
> > Dear All,
> > 
> > verifying an implementation of partition I have something like
> > 
> > /*@ axiomatic List {
> >  @ type listInt;
> >  @ logic listInt nil;
> >  @ logic listInt cons(integer x, listInt xs);
> >  @ logic listInt append(listInt xs, listInt ys);
> >  @ logic listInt arrayToList{L}(int *arr, integer length);
> >  @ logic boolean member(integer elem, listInt xs);
> >  @ axiom appendNil:
> >  @   \forall listInt ys; append(nil, ys) == ys;
> >  @ axiom appendCons:
> >  @   \forall listInt xs, ys; \forall integer x; append(cons(x, xs), ys) == cons(x, append(xs, ys));
> >  @ axiom arrayToListNull{L}:
> >  @   \forall int *arr; \forall integer i; i == 0 ==> arrayToList{L}(arr, i) == nil;
> >  @ axiom arrayToListN{L}:
> >  @   \forall int *arr; \forall integer length, newLength; length > 0 && newLength == length-1
> >  @   ==> arrayToList{L}(arr, length) == cons(\at(arr[0], L), arrayToList{L}(arr+1, newLength));
> >  @ axiom memberNil:
> >  @   \forall integer elem; !member(elem, nil);
> >  @ axiom memberConsHead:
> >  @   \forall integer elem; \forall listInt xs; member(elem, cons(elem, xs));
> >  @ axiom memberConsTail:
> >  @   \forall integer elem, x; \forall listInt xs; member(elem, xs) ==> member(elem, cons(x, xs));
> >  @ predicate permutationLists(listInt a, listInt b);
> >  @ axiom permutationListsNil:
> >  @   permutationLists(nil, nil);
> >  @ axiom permutationListsCons:
> >  @   \forall listInt a1, a2, a3, ta, b1, b2, b3, tb; ta == append(a1, append(a2, a3))
> >  @   && tb == append(b1, append(b2, b3)) && a2 != nil && a2 == b2
> >  @   && permutationLists(append(a1, a3), append(b1, b3))
> >  @   ==> permutationLists(ta, b1);
> >  @}
> >  @*/
> > 
> > /*@
> >  @predicate permutation{L1, L2}(int *a, int *b, integer count) =
> >  @  permutationLists(arrayToList{L1}(a, count), arrayToList{L2}(b, count));
> >  @
> >  @predicate property(integer x);
> >  @*/
> > 
> > /*@ assigns \nothing;
> >  @ ensures \result == \true <==> property(x);
> >  @*/
> > int property(int x);
> > 
> > /*@ requires length >= 0 && \valid(arr+(0..length-1)) && \valid(ind+(0..length-1));
> >  @ ensures 0 <= \result < length;
> >  @ ensures \forall int i; 0 <= i <= \result ==> property(arr[ind[i]]);
> >  @ ensures \forall int i; \result + 1 <= i < length ==> !property(arr[ind[i]]);
> >  @ assigns ind[0..length-1];
> >  @*/
> > int partition(int *arr, int *ind, int length) {
> >  int gr = 0, j = length-1;
> >  /*@ loop invariant 0 <= gr <= j+1 <= length ;
> >    @ loop invariant \forall integer i; 0 <= i < gr ==> property(arr[ind[i]]);
> >    @ loop invariant \forall integer i; j+1 <= i < length ==> !property(arr[ind[i]]);
> >    @ loop invariant permutationLists(append(arrayToList{Here}(ind, gr), arrayToList{Here}(ind+j+1, length-j)), arrayToList{Here}(arr, gr + length - j));
> >    @ loop variant j - gr;
> >    @*/
> >  while (gr <= j) {
> >    if (property(arr[gr + length - 1 - j])) {
> >      ind[gr] = gr + length - 1 - j;
> >      //@ assert ind[gr] == gr + length - 1 - j && property(arr[gr + length - 1 - j]) && property(arr[ind[gr]]);
> >      gr++;
> >    } else {
> >      ind[j] = gr + length - 1 - j;
> >      j--;
> >    }
> >  }
> >  return gr-1;
> > }
> > 
> > Frama-C Neon/WP failed to discharge the second part of the invariant,
> > so I started experimenting with some assertions. When I write the
> > assertion as above the PO is not discharged. When I turn on 'split'
> > the first of the three generated POs is discharged. When I write the
> > three assertions as separate assertions:
> > 
> >      //@ assert ind[gr] == gr + length - 1 - j;
> >      //@ assert property(arr[gr + length - 1 - j]);
> >      //@ assert property(arr[ind[gr]]);
> > 
> > then the first and the last are discharged.
> > 
> > Any hints on how I should deal with this and how I could get the
> > invariant proved?
> > 
> > Thanks and best regards,
> > 
> > Marko_______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
-------------- next part --------------
A non-text attachment was scrubbed...
Name: partition-mine-momomorphic-ghost.c
Type: application/octet-stream
Size: 1712 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150225/614030ea/attachment.obj>
-------------- 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/20150225/614030ea/attachment.sig>