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] YASE yet another specification example :)

  • Subject: [Frama-c-discuss] YASE yet another specification example :)
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Fri Oct 17 08:54:05 2008
Hello again,

I'm trying to explore a new example combining array_cpy(int* a, int n, int* b); and fill_int_array(int* first, int* last, int value).

This one is called copy_int_array (int* first, int* last, int* result).

 DESCRIPTION:
  Copies the elements in the range [first,last) into a range beginning at result.
  Returns an iterator to the last element in the destination range.
  
 Parameters:  
  first, last:
   Pointers to the initial and final positions of the searched sequence. The range 
   used is [first,last), which contains all the elements between first and last,
   including the element pointed by first but not the element pointed by last.
  result
   Pointer to the initial position in the destination sequence. This shall 
   not point to any element in the range [first,last).
  Return value:
   A pointer to the last element of the destination sequence where elements 
   have been copied.

   CODE:

/*@ predicate disjoint_arrays(int* a, int* b, integer i) =
     \forall integer k1, k2; 
        0 <= k1 < i && 0 <= k2 < i ==> a + k1 != b + k2;
*/
/*@
 requires last > first;
 requires disjoint_arrays(first, result, last-first); 
 
 requires \valid_range  (first, 0, last-first-1);
 requires \valid_range  (result, 0, last-first-1);
 ensures  \forall integer i; 0 <= i < last-first ==> result[i] == first[i];  
*/

int* copy_int_array (int* first, int* last, int* result)
{
 //@ ghost int* a = first;
 //@ ghost int* b = result;
 //@ ghost int length = last-first;

    /*@
     loop invariant a <= first <= last;
     loop invariant b <= result <= b+length;     
     loop invariant \forall integer k; 0 <= k < first-a ==> result[k] == first[k];
    */
  while (first!=last) *result++ = *first++;
  return result;
}

Up to this moment Jessie is unable to solve it entirely.

Am I missing something or is it due to my Hydrogen version.

Greets

Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081017/10c0cc6c/attachment.html