#include "__fc_builtin.h"

int u[100] = { 1, 1 };

int fibo(int n) {
  int m = n;
  while (u[m]==0) { Frama_C_show_each_last_comp(m); m--; }
  if (n == m) return u[m];
  while(m<n) {
    Frama_C_show_each_fib(m,u[m]);
    u[m+1] = u[m] + u[m-1];
    m++;
  }
  return u[m];
}

int main1 () {
  return fibo(4);
}