--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on February 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] information for proof seems to get lost



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