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] information for proof seems to get lost

  • Subject: [Frama-c-discuss] information for proof seems to get lost
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Mon, 16 Feb 2009 14:19:12 +0100
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