# 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.

# [Frama-c-discuss] several WP questions

```Several mistakes in your code:
- loop assigns are incomplete : missing `rev`. Indeed, assigns must be completely proved _before_ any attempt to prove another property (otherwise, proof-obligations are inconsistent) ;
- you need to specify that, during the loop, indices are monotonic. With proper renaming of variables, during loop:
* P elements have been found with the desired property, and Q without.
* 0 <= P && 0 <= Q && P+Q <= length
* first indices ind[0..P-1] are all in range (0..P+Q-1)
* last indices ind[length-Q..length-1] are all in range (0..P+Q-1)
* ind[rev[k]] == k for all k in (0..P+Q-1)

The monotonicity of indices is necessary to apply the induction hypothesis ind[ref[k]]==k for small enough k?s.

L.

> Le 25 f?vr. 2015 ? 13:49, Marko Sch?tz Schmuck <MarkoSchuetz at web.de> a ?crit :
>
> 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 <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>
> <partition-mine-momomorphic-ghost.c>_______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150225/6907f0a7/attachment-0001.html>

```