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