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

// To illustrate \thread_local, \mutable, \writes

int main()
{
  int x;
  int* q;
  
  foo(q);
  return 0;
}

void foo(int* p)
_(requires \thread_local(p))
{
  int x = *p;
}