valinit.c (4,351 bytes)
2011-04-14 16:27
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) { }