typedef struct {
  int i;
  short s;
  short pad;
  int* p;} T_STR1;

#define CTE1 3

#define CTE2 4

typedef struct {
  int i;
  short s;
  short pad;
  T_STR1 ts[CTE2];
} T_STR2;

T_STR2 tab[CTE1];

/*@
  @ requires 0<=index1<CTE1; 
  @ requires 0<=index2<CTE2; 
  @*/
int f1(int index1, int index2, short ref)
{
  short local;
  if (ref == tab[index1].ts[index2].s)
    {
      local =  tab[index1].ts[index2].s;
      return 0;
    }

  return -1;
}