--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on February 2009 ---
Hello again. I have added an algorithm with its auxiliary function. The algorithm shifts the elements from a[middle..length-1] to b[0.. length-middle-1] and appends the elements a[0..middle] at th elements allready copied. My problem is that the informantion of the assert clause seems to get lost. To be more precise: copy_array (a + middle, length-middle, b); //@ assert \forall integer i; 0 <= i < length-middle ==> a[i+middle] == b[i] ; copy_array (a, middle, b + length-middle); //@ assert \forall integer i; 0 <= i < middle ==> a[i] == b[i+length-middle] ; //these lines get proven //regardless the first assertion, if it is placed again, after function call, the prover fails: //@ assert \forall integer i; 0 <= i < length-middle ==> a[i+middle] == b[i] ; I would appreciate any help Cheers Chrisotoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090216/04c733d1/attachment.htm -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: rotate_copy.c Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090216/04c733d1/attachment.txt