gen_bts1398.c

/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
  int __retres;
  int x;
  int t[2];
  int i;
  x = 0;
  i = 1;
  t[0] = 1;
  t[1] = 2;
  printf("X=%d, t[0]=%d, t[1]=%d\n",x,t[0],t[i]);
  __retres = 0;
  return __retres;
}