#include "__fc_builtin.h"

int fact() {
  int x = Frama_C_interval(0,10);
  int y = 1;
  while(x>0) {
    y = y * x;
    x = x - 1;
  }
  return y;
}