1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
typedef short Guard;

/* In order to be able to inspect the result... */
int res;
int T_res;

void search(const int *tab, int length, int x)
{
{
/*TP*/ const int *T_tab = tab;
/*TP*/ int T_length = length;
/*TP*/ int T_x = x;
/*TP*/ Guard Ret = 0;
/*TP*/ Guard T_Ret = 0;
{
{
int tmp;
int T_tmp;
/* {char *CP0;} */
int stop;
int T_stop;
/* {char *CP1;} */
int start;
int T_start;
/* {char *CP2;} */
int result;
int T_result;
/* {char *CP3;} */
int i;
int T_i;
/* {char *CP4;} */
if (!Ret) start = 0;
if (!T_Ret) T_start = 0;
/* {char *CP5;} */
if (!Ret) stop = length;
if (!T_Ret) T_stop = T_length;
/* {char *CP6;} */
L1:;
T_L1:;
{
{
Guard G0 = 1;
Guard T_G0 = 1;
if (!Ret) G0 = (start != stop);
if (!T_Ret) T_G0 = (T_start != T_stop);
/* {char *CP7;} */
{
{
if (!Ret) if (G0) i = ((start + stop) / 2);
if (!T_Ret) if (T_G0) T_i = ((T_start + T_stop) / 2);
/* {char *CP8;} */
if (!Ret) if (G0) tmp = tab[i];
if (!T_Ret) if (T_G0) T_tmp = T_tab[T_i];
/* {char *CP9;} */
{
{
Guard G1 = 1;
Guard T_G1 = 1;
if (!Ret) if (G0) G1 = (x == tmp);
if (!T_Ret) if (T_G0) T_G1 = (T_x == T_tmp);
/* {char *CP10;} */
{
{
if (!Ret) if (G0) if (G1) start = i;
if (!T_Ret) if (T_G0) if (T_G1) T_start = T_i;
/* {char *CP11;} */
if (!T_Ret) if (T_G0) if (T_G1) goto T_L3;
if (!Ret) if (G0) if (G1) stop = i;
/* {char *CP12;} */
}
}
{
{
}
}
{
{
Guard G2 = 1;
Guard T_G2 = 1;
if (!T_Ret) if (T_G0) T_G2 = (T_x > T_tmp);
if (!Ret) if (G0) if (!G1) G2 = (x < tmp);
/* {char *CP13;} */
{
{
if (!T_Ret) if (T_G0) if (T_G2) T_start = (T_i + 1);
if (!T_Ret) if (T_G0) if (T_G2) goto T_L2;
if (!Ret) if (G0) if (!G1) if (G2) stop = i;
/* {char *CP14;} */
}
}
{
{
}
}
{
{
Guard G3 = 1;
Guard T_G3 = 1;
if (!T_Ret) if (T_G0) T_G3 = (T_x < T_tmp);
if (!Ret) if (G0) if (!G1) if (!G2) G3 = (x > tmp);
/* {char *CP15;} */
{
{
if (!T_Ret) if (T_G0) if (T_G3) T_stop = T_i;
if (!Ret) if (G0) if (!G1) if (!G2) if (G3) start = (i + 1);
/* {char *CP16;} */
}
}
{
{
}
}
}
}
}
}
}
}
}
}
L2:;
T_L2:;
if (!Ret) if (G0) goto L1;
if (!T_Ret) if (T_G0) goto T_L1;
/* {char *CP17;} */
L3:;
T_L3:;
}
}
if (!Ret) tmp = tab[start];
if (!T_Ret) T_tmp = T_tab[T_start];
/* {char *CP18;} */
{
{
Guard G4 = 1;
Guard T_G4 = 1;
if (!Ret) G4 = (tmp == x);
if (!T_Ret) T_G4 = (T_tmp == T_x);
/* {char *CP19;} */
{
{
if (!Ret) if (G4) result = start;
if (!T_Ret) if (T_G4) T_result = T_start;
/* {char *CP20;} */
}
}
{
{
if (!Ret) if (!G4) result = (0 - 1);
if (!T_Ret) if (!T_G4) T_result = (0 - 1);
/* {char *CP21;} */
}
}
}
}
if (!Ret) res = result;
if (!T_Ret) T_res = T_result;
{char *CP22;}
}
}
}
}