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] New Specification Examples

  • Subject: [Frama-c-discuss] New Specification Examples
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Tue Oct 14 09:38:11 2008
Hello, besides the problems I described in my last Mail (dereferencing of \result and Labeling inside loops), I'd like to alter the ranging of my array into a c++ stl Style, meaning (int* first, int* last, ...). So far ok, but:

/*@
 requires last >= first;
 requires \valid_range(first, 0, last-first-1);
 behavior is_not_empty:  
  assumes last > first;
  ensures  \forall integer i; 0 <= i < last-first ==> first [i] == value;
 behavior is_empty:
  assumes last == first;
  ensures last == first; 
 
*/
void fill_int_array (int* first, int* last,  int value )
{
 //@ ghost int* a = first; 
 /*@
  loop invariant a <= first <= last;
  loop invariant \forall integer k; 0 <= k < first-a ==> a[k] == value;
    */
 while (first != last)  *first++ = value;
}

In this example the ensurance of the postcondition does not work due to the changing value of first.

Attempts to circumvent this with:

ensures \forall integer i; 0 <= i < last-first ==> *(\old(first)+i) == value;

have failed as well (to meet the postcondition in the Jessie-gui)



Is there a possibility to allocate the old first or is this error due to the limitations of jessie and pals.

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