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] adjacent_find problem

  • Subject: [Frama-c-discuss] adjacent_find problem
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Sat, 16 Jan 2010 11:59:43 +0100
Hi,

here is a specification and implementation of the function adjacent_find
that returns the smallest index i of of an array a where a[i] == a[i+1] holds.
If no such index exists it returns the length of the array.
(It's a simplified version of the C++ standard algorithms http://www.sgi.com/tech/stl/adjacent_find.html)


/*@
  predicate
    have_equal_neighbours{Label}(int* a, int n) =
      \exists int i; 0 <= i < n-1 && a[i] == a[i+1];
*/

/*@
  requires 0 <= n;
  requires \valid_range(a, 0, n);

  assigns \nothing;

  behavior some:
    assumes  have_equal_neighbours(a, n);
    ensures  0 <= \result < n-1;
    ensures  a[\result] == a[\result+1];
    ensures  !have_equal_neighbours(a, \result);

  behavior none:
    assumes  !have_equal_neighbours(a, n);
    ensures  \result == n;

  complete behaviors some, none;
  disjoint behaviors some, none;
*/
int adjacent_find(int* a, int n)
{
  if (0 == n) return n;

  /*@
    loop invariant 0 <= i < n;
    loop   variant n-i;
    loop invariant !have_equal_neighbours(a, i+1);
    //loop invariant !have_equal_neighbours(a, i);
    //loop invariant 0 < i ==> a[i-1] != a[i];
  */
  for (int i = 0; i < n-1; i++)
    if (a[i] == a[i+1])
      return i;

  return n;
}

When I compile it with 

	frama-c -jessie  -jessie-no-regions -jessie-why-opt="-exp goal" adjacent_find.c 

then I obtain the error message 

	adjacent_find.c:34:[kernel] user error: Error during annotations analysis: invalid implicit conversion from integer to int 

which refers to the third loop invariant.
I am not sure whether it's a bug or a feature, but when I replace this loop invariant by the 
following (in my opinion equivalent) loop invariants then most atp can proof all verification conditions.

    loop invariant !have_equal_neighbours(a, i);
    loop invariant 0 < i ==> a[i-1] != a[i];
Regards Jens

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100116/476d3b2a/attachment.htm