#include <vcc.h>
#include <limits.h>

unsigned linsearch (int A[], unsigned len, int val)
  _(requires \thread_local_array(A,len))
  _(ensures (\result < UINT_MAX) ==> A[\result] == val)
  _(ensures (\result < UINT_MAX) ==> \forall unsigned k; (k < \result) ==> (A[k] != val))
  _(ensures (\result == UINT_MAX) ==> \forall unsigned k; (k < len) ==> (A[k] != val))
{
  unsigned i = 0;
  while (i < len)
    _(invariant (i <= len) && \forall unsigned k; (k < i) ==> (A[k] != val)) {
      if (A[i] == val)
	       return i;
      else
	       i++;
  }
  return UINT_MAX;
}