int x = 3 ;
int t1[1] = {3} ;
int t2[2] = {3,4} ;
int t3[3] = {3,4} ;
int t15[15] = {3} ;
int t20[20] = {3} ;
int t40[40] = {0,1,2,3,4,5,6,7,8,9,
	      10,11,12,13,14,15,16,17,18,19,
	      20,22,22,33,34,35,36,37,38,39,
	      30,33,33,33,34,35,36,37,38,39} ;
int t50[50] = {0,1,2,3,4,5,6,7,8,9,
	      10,11,12,13,14,15,16,17,18,19,
	      20,22,22,33,34,35,36,37,38,39,
	      30,33,33,33,34,35,36,37,38,39,
	      40,44,42,43,44,45,46,47,48,49} ;
int t60[60] = {0,1,2,3,4,5,6,7,8,9,
	      10,11,12,13,14,15,16,17,18,19,
	      20,22,22,33,34,35,36,37,38,39,
	      30,33,33,33,34,35,36,37,38,39,
	      40,44,42,43,44,45,46,47,48,49,
	      50,55,52,53,55,55,56,57,58,59} ;

enum nb { ONE = 1, ZERO = 0 } ;
enum nb one = ONE ;
unsigned char uca = 'a' ;
int *px = &x, **ppx = &px, *pt4 = &t40[4] ;
char * str = "str" ;

struct st { int b ; int a ; } ;
struct st vs = { 2, 1 };
struct st vs_bis = { 2, 1 };
struct st  *pvs = &vs ;
struct st ts[56] = {
  4, 1, 6, 1, 7, 1, 1, 2, 1, 1, 8, 1, 2, 2, 12, 2, 10, 1, 6, 2, 
  9, 1, 3, 2, 4, 2, 5, 2, 6, 2, 7, 2, 9, 2, 10, 1, 2, 1, 10, 2, 
  11, 1, 12, 1, 12, 2, 16, 2, 18, 2, 19, 2, 30, 2, 31, 1, 12, 1, 9, 2, 
  11, 1, 20, 1, 12, 2, 11, 1, 21, 2, 5, 1, 16, 1, 8, 1, 9, 1, 22, 1, 
  22, 1, 22, 2, 22, 2, 22, 2, 22, 1, 22, 1, 22, 1, 22, 2, 22, 2, 22, 1, 
  22, 1, 22, 2, 22, 1, 22, 2, 22, 2, 22, 2
};

/*@ ensures       ok: x==3;
  @ ensures       ok: one==ONE;
  @ ensures       ok: uca=='a';
  @ ensures       ok: px==&x;
  @ ensures       ok: *px==3;
  @ ensures       ok: ppx==&px;
  @ ensures       ok: *ppx==&x;
  @ ensures       ok: pt4==&t40[4];
  @ ensures       ok: *pt4==4;
  @ ensures p0: bts794: str[0]=='s' && str[1]=='t' && str[2]=='r' && str[3]=='\0';
  @ ensures       ok: t1[0]==3;
  @ ensures       ok: t15[2]==0;
  @ ensures p1: bts788: t20[2]==0;
  @ ensures       ok: \forall integer i ; 0<i<40 ==> t40[i]>0;
  @ ensures       ok: \forall integer i ; 0<i<50 ==> t50[i]>0;
  @ ensures p2: todo: \forall integer i ; 0<i<60 ==> t60[i]>0;
  @ ensures p3: todo: \forall integer i ; 0<i<60 ==> t60[i]>0;
  @ ensures       ok: vs.a == 1 && vs.b == 2;
  @ ensures p5:     vs == vs_bis;
  @ ensures p5_bis: *pvs == vs_bis;
  @ ensures p4: bts793: 
              ts[0].b==4 && ts[0].a==1 && ts[1].b==6 && ts[1].a==1 && 
              ts[2].b==7 && ts[2].a==1 && ts[3].b==1 && ts[3].a==2 && 
              ts[4].b==1 && ts[4].a==1 && ts[5].b==8 && ts[5].a==1 && 
              ts[6].b==2 && ts[6].a==2 && ts[7].b==12 && ts[7].a==2 && 
              ts[8].b==10 && ts[8].a==1 && ts[9].b==6 && ts[9].a==2 && 
              ts[10].b==9 && ts[10].a==1 && ts[11].b==3 && ts[11].a==2 && 
              ts[12].b==4 && ts[12].a==2 && ts[13].b==5 && ts[13].a==2 && 
              ts[14].b==6 && ts[14].a==2 && ts[15].b==7 && ts[15].a==2 && 
              ts[16].b==9 && ts[16].a==2 && ts[17].b==10 && ts[17].a==1 && 
              ts[18].b==2 && ts[18].a==1 && ts[19].b==10 && ts[19].a==2 && 
              ts[20].b==11 && ts[20].a==1 && ts[21].b==12 && ts[21].a==1 && 
              ts[22].b==12 && ts[22].a==2 && ts[23].b==16 && ts[23].a==2 && 
              ts[24].b==18 && ts[24].a==2 && ts[25].b==19 && ts[25].a==2 && 
              ts[26].b==30 && ts[26].a==2 && ts[27].b==31 && ts[27].a==1 && 
              ts[28].b==12 && ts[28].a==1 && ts[29].b==9 && ts[29].a==2 && 
              ts[30].b==11 && ts[30].a==1 && ts[31].b==20 && ts[31].a==1 && 
              ts[32].b==12 && ts[32].a==2 && ts[33].b==11 && ts[33].a==1 && 
              ts[34].b==21 && ts[34].a==2 && ts[35].b==5 && ts[35].a==1 && 
              ts[36].b==16 && ts[36].a==1 && ts[37].b==8 && ts[37].a==1 && 
              ts[38].b==9 && ts[38].a==1 && ts[39].b==22 && ts[39].a==1 && 
              ts[40].b==22 && ts[40].a==1 && ts[41].b==22 && ts[41].a==2 && 
              ts[42].b==22 && ts[42].a==2 && ts[43].b==22 && ts[43].a==2 && 
              ts[44].b==22 && ts[44].a==1 && ts[45].b==22 && ts[45].a==1 && 
              ts[46].b==22 && ts[46].a==1 && ts[47].b==22 && ts[47].a==2 && 
              ts[48].b==22 && ts[48].a==2 && ts[49].b==22 && ts[49].a==1 && 
              ts[50].b==22 && ts[50].a==1 && ts[51].b==22 && ts[51].a==2 && 
              ts[52].b==22 && ts[52].a==1 && ts[53].b==22 && ts[53].a==2 && 
              ts[54].b==22 && ts[54].a==2 && ts[55].b==22 && ts[55].a==2 ;



*/
void main (void) { }