unsigned int pow(unsigned int n, unsigned int m) {
  unsigned int res = 1;
  unsigned int aux = n;
  while(m>1) {
    if (m%2 == 1) { res = res * aux; }
    m /= 2;
    aux = aux * aux;
  }
  if (m%2 == 1) { res *= aux; }
  return res;
}

unsigned int naive_pow(unsigned int n, unsigned int m) {
  unsigned int res = 1;
  while (m>0) { res*=n; m--; }
  return res;
}

volatile int entropy;

int interval(int a, int b) {
  int tmp = entropy;
  if (tmp <= a) { tmp = a; }
  if (tmp >= b) { tmp = b; }
  return tmp;
}

void main (void) {
  unsigned int m = interval(1,10);
  unsigned int n = interval(1,12);
  /*@ assert n == 1 || n == 2 || n == 3 || n == 4 || n == 5 || n == 6 || n == 7 || n == 8 || n == 9 || n == 10 || n == 11 || n == 12; */
  /*@ assert m == 1 || m == 2 || m == 3 || m == 4 || m == 5 || m == 6 || m == 7 || m == 8 || m == 9 || m == 10; */
  unsigned int res1 = pow(2,m);
  unsigned int res2 = naive_pow(n,m);
  Frama_C_show_each_res(m, res1);
  unsigned int ok = res1 == res2;
}