framac.ast

/* Generated by Frama-C */
#include "stdlib.h"
int N;
int *t;
int chk(int x, int y)
{
  int i;
  int r;
  i = 0;
  r = i;
  while (i < 8) {
    r += *(t + (x + 8 * i));
    r += *(t + (i + 8 * y));
    if (x + i < 8) 
      if (y + i < 8) r += *(t + ((x + i) + 8 * (y + i)));
    if (x + i < 8) 
      if (y - i >= 0) r += *(t + ((x + i) + 8 * (y - i)));
    if (x - i >= 0) 
      if (y + i < 8) r += *(t + ((x - i) + 8 * (y + i)));
    if (x - i >= 0) 
      if (y - i >= 0) r += *(t + ((x - i) + 8 * (y - i)));
    i ++;
  }
  return r;
}

/*@ assigns *(t + (0 .. 63));
    assigns *(t + (0 .. 63))
      \from *(t + (0 .. 63)), (indirect: n), (indirect: x), (indirect: y);
 */
int go(int n, int x, int y)
{
  int __retres;
  if (n == 8) {
    N ++;
    __retres = 0;
    goto return_label;
  }
  /*@ slevel 0; */
  /*@ loop unroll 0; */
  while (y < 8) {
    /*@ loop unroll 0; */
    while (x < 8) {
      int tmp;
      tmp = chk(x,y);
      if (tmp == 0) {
        (*(t + (x + 8 * y))) ++;
        go(n + 1,x,y);
        (*(t + (x + 8 * y))) --;
      }
      x ++;
    }
    x = 0;
    y ++;
  }
  __retres = 0;
  return_label: return __retres;
}

int main(void)
{
  int __retres;
  t = (int *)calloc((size_t)64,sizeof(int));
  go(0,0,0);
  if (N != 92) {
    __retres = 1;
    goto return_label;
  }
  __retres = 0;
  return_label: return __retres;
}