1
2int main() {
3 int s__state ;
4 int s__hit ;
5 int s__verify_mode ;
6 int s__session__peer ;
7 unsigned long s__s3__tmp__new_cipher__algorithms ;
8 int buf ;
9 int cb ;
10 int blastFlag ;
11 int tmp___1;
12
13 s__state = 8466;
14 blastFlag = 0;
15
16 while (1) {
17 if (s__state <= 8512 && blastFlag > 2) { goto ERROR; }
18 {
19 {
20 {
21 {
22 {
23 if (s__state == 8466) {
24 goto switch_1_8466;
25 } else {
26 if (s__state == 8496) {
27 goto switch_1_8496;
28 } else {
29 {
30 if (s__state == 8512) {
31 goto switch_1_8512;
32 } else {
33 {
34 if (s__state == 8528) {
35 goto switch_1_8528;
36 } else {
37 {
38 if (s__state == 8544) {
39 goto switch_1_8544;
40 } else {
41 {
42 if (s__state == 8560) {
43 goto switch_1_8560;
44 } else {
45 {
46 if (s__state == 8576) {
47 goto switch_1_8576;
48 } else {
49 {
50 if (s__state == 8592) {
51 goto switch_1_8592;
52 } else {
53 {
54 if (s__state == 8608) {
55 goto switch_1_8608;
56 } else {
57 {
58 if (s__state == 8640) {
59 goto switch_1_8640;
60 } else {
61 {
62 if (s__state == 8656) {
63 goto switch_1_8656;
64 } else {
65 {
66 if (s__state == 8672) {
67 goto switch_1_8672;
68 } else {
69 goto end;
70
71 switch_1_8466:
72 if (blastFlag == 0) {
73 blastFlag = 1;
74 }
75 s__state = 8496;
76 goto switch_1_break;
77
78 switch_1_8496:
79 if (blastFlag == 1) {
80 blastFlag = 2;
81 }
82 if (s__hit) {
83 s__state = 8656;
84 } else {
85 s__state = 8512;
86 }
87 goto switch_1_break;
88
89 switch_1_8512:
90 s__state = 8528;
91 goto switch_1_break;
92
93 switch_1_8528:
94 s__state = 8544;
95 goto switch_1_break;
96
97 switch_1_8544:
98 if (s__verify_mode + 1) {
99 if (s__session__peer != 0) {
100 if (s__verify_mode + 4) {
101 s__state = 8560;
102 } else {
103 goto _L___2;
104 }
105 } else {
106 _L___2:
107 if (s__s3__tmp__new_cipher__algorithms + 256UL) {
108 if (s__verify_mode + 2) {
109 goto _L___1;
110 } else {
111 s__state = 8560;
112 }
113 } else {
114 _L___1:
115 s__state = 8576;
116 }
117 }
118 } else {
119 s__state = 8560;
120 }
121 goto switch_1_break;
122
123 switch_1_8560:
124 s__state = 8576;
125 goto switch_1_break;
126
127 switch_1_8576:
128 tmp___1 = __VERIFIER_nondet_int();
129 if (tmp___1 == 2) {
130 s__state = 8466;
131 } else {
132 s__state = 8592;
133 }
134 goto switch_1_break;
135
136 switch_1_8592:
137 s__state = 8608;
138 goto switch_1_break;
139
140 switch_1_8608:
141 s__state = 8640;
142 goto switch_1_break;
143
144 switch_1_8640:
145 if (blastFlag == 3) {
146 blastFlag = 4;
147 }
148 if (s__hit) {
149 goto end;
150 } else {
151 s__state = 8656;
152 }
153 goto switch_1_break;
154
155 switch_1_8656:
156 if (blastFlag == 2) {
157 blastFlag = 3;
158 }
159 s__state = 8672;
160 goto switch_1_break;
161
162 switch_1_8672:
163 if (blastFlag == 4) {
164 blastFlag = 5;
165 } else {
166 if (blastFlag == 5) {
167 goto ERROR;
168 }
169 }
170 if (s__hit) {
171 s__state = 8640;
172 } else {
173 goto end;
174 }
175 goto switch_1_break;
176
177 }
178 }
179 }
180 }
181 }
182 }
183 }
184 }
185 }
186 }
187 }
188 }
189 }
190 }
191 }
192 }
193 }
194 }
195 }
196 }
197 }
198 }
199 }
200 }
201 }
202 }
203 }
204 switch_1_break: ;
205 }
206
207 end:
208 return (-1);
209 ERROR:
210 return (-1);
211}