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

int x;
int y;

void main()
  _(writes &x,&y)
{
  x = 10;
  y = 20;
  copy();
  _(assert y == 20)
}

void copy()
  _(requires \thread_local(&y))
  _(writes &x)
// _(ensures x == y)
{
  int *p = &x;
  int *q = &y;
  *p = *q;
}

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

void arrayint(int *A, int len)
_(requires len >= 0)
_(writes \array_range(A, (unsigned) len))
_(ensures \forall int k; (0 <= k && k < len) ==> A[k] == 0) 
{
	int i = 0;
	while (i < len)
	_(invariant i <= len && \forall int k; (0 <= k && k < i) ==> A[k] == 0)
	{
		A[i] = 0;
		i++;
	}
}