1extern int nondet_int(void);
2
3
4
5int ssl3_connect(void)
6{ int s__info_callback ;
7 int s__in_handshake ;
8 int s__state ;
9 int s__new_session ;
10 int s__server ;
11 int s__version ;
12 int s__type ;
13 int s__init_num ;
14 int s__bbio ;
15 int s__wbio ;
16 int s__hit ;
17 int s__rwstate ;
18 int s__init_buf___0 ;
19 int s__debug ;
20 int s__shutdown ;
21 int s__ctx__info_callback ;
22 int s__ctx__stats__sess_connect_renegotiate ;
23 int s__ctx__stats__sess_connect ;
24 int s__ctx__stats__sess_hit ;
25 int s__ctx__stats__sess_connect_good ;
26 int s__s3__change_cipher_spec ;
27 int s__s3__flags ;
28 int s__s3__delay_buf_pop_ret ;
29 int s__s3__tmp__cert_req ;
30 int s__s3__tmp__new_compression ;
31 int s__s3__tmp__reuse_message ;
32 int s__s3__tmp__new_cipher ;
33 int s__s3__tmp__new_cipher__algorithms ;
34 int s__s3__tmp__next_state___0 ;
35 int s__s3__tmp__new_compression__id ;
36 int s__session__cipher ;
37 int s__session__compress_meth ;
38 int buf ;
39 unsigned long tmp ;
40 unsigned long l ;
41 int num1 ;
42 int cb ;
43 int ret ;
44 int new_state ;
45 int state ;
46 int skip ;
47 int tmp___0 ;
48 int tmp___1 ;
49 int tmp___2 ;
50 int tmp___3 ;
51 int tmp___4 ;
52 int tmp___5 ;
53 int tmp___6 ;
54 int tmp___7 ;
55 int tmp___8 ;
56 int tmp___9 ;
57 int blastFlag ;
58 int ag_X ;
59 int ag_Y ;
60 int __retres59 ;
61
62 {
63 s__state = 12292;
64 blastFlag = 0;
65 tmp = nondet_int();
66 cb = 0;
67 ret = -1;
68 skip = 0;
69 tmp___0 = 0;
70 if (s__info_callback != 0) {
71 cb = s__info_callback;
72 } else {
73 if (s__ctx__info_callback != 0) {
74 cb = s__ctx__info_callback;
75 } else {
76
77 }
78 }
79 s__in_handshake = s__in_handshake + 1;
80 if (tmp___1 - 12288) {
81 if (tmp___2 - 16384) {
82
83 } else {
84
85 }
86 } else {
87
88 }
89 {
90 while (1) {
91 while_0_continue: ;
92 state = s__state;
93 if (s__state == 12292) {
94 goto switch_1_12292;
95 } else {
96 if (s__state == 16384) {
97 goto switch_1_16384;
98 } else {
99 if (s__state == 4096) {
100 goto switch_1_4096;
101 } else {
102 if (s__state == 20480) {
103 goto switch_1_20480;
104 } else {
105 if (s__state == 4099) {
106 goto switch_1_4099;
107 } else {
108 if (s__state == 4368) {
109 goto switch_1_4368;
110 } else {
111 if (s__state == 4369) {
112 goto switch_1_4369;
113 } else {
114 if (s__state == 4384) {
115 goto switch_1_4384;
116 } else {
117 if (s__state == 4385) {
118 goto switch_1_4385;
119 } else {
120 if (s__state == 4400) {
121 goto switch_1_4400;
122 } else {
123 if (s__state == 4401) {
124 goto switch_1_4401;
125 } else {
126 if (s__state == 4416) {
127 goto switch_1_4416;
128 } else {
129 if (s__state == 4417) {
130 goto switch_1_4417;
131 } else {
132 if (s__state == 4432) {
133 goto switch_1_4432;
134 } else {
135 if (s__state == 4433) {
136 goto switch_1_4433;
137 } else {
138 if (s__state == 4448) {
139 goto switch_1_4448;
140 } else {
141 if (s__state == 4449) {
142 goto switch_1_4449;
143 } else {
144 if (s__state == 4464) {
145 goto switch_1_4464;
146 } else {
147 if (s__state == 4465) {
148 goto switch_1_4465;
149 } else {
150 if (s__state == 4466) {
151 goto switch_1_4466;
152 } else {
153 if (s__state == 4467) {
154 goto switch_1_4467;
155 } else {
156 if (s__state == 4480) {
157 goto switch_1_4480;
158 } else {
159 if (s__state == 4481) {
160 goto switch_1_4481;
161 } else {
162 if (s__state == 4496) {
163 goto switch_1_4496;
164 } else {
165 if (s__state == 4497) {
166 goto switch_1_4497;
167 } else {
168 if (s__state == 4512) {
169 goto switch_1_4512;
170 } else {
171 if (s__state == 4513) {
172 goto switch_1_4513;
173 } else {
174 if (s__state == 4528) {
175 goto switch_1_4528;
176 } else {
177 if (s__state == 4529) {
178 goto switch_1_4529;
179 } else {
180 if (s__state == 4560) {
181 goto switch_1_4560;
182 } else {
183 if (s__state == 4561) {
184 goto switch_1_4561;
185 } else {
186 if (s__state == 4352) {
187 goto switch_1_4352;
188 } else {
189 if (s__state == 3) {
190 goto switch_1_3;
191 } else {
192 {
193 goto switch_1_default;
194 if (0) {
195 switch_1_12292:
196 s__new_session = 1;
197 s__state = 4096;
198 s__ctx__stats__sess_connect_renegotiate = s__ctx__stats__sess_connect_renegotiate + 1;
199 switch_1_16384: ;
200 switch_1_4096: ;
201 switch_1_20480: ;
202 switch_1_4099:
203 s__server = 0;
204 if (cb != 0) {
205
206 } else {
207
208 }
209 if (s__version - 65280 != 768) {
210 ret = -1;
211 goto end;
212 } else {
213
214 }
215 s__type = 4096;
216 if (s__init_buf___0 == 0) {
217 buf = nondet_int();
218 if (buf == 0) {
219 ret = -1;
220 goto end;
221 } else {
222
223 }
224 if (! tmp___3) {
225 ret = -1;
226 goto end;
227 } else {
228
229 }
230 s__init_buf___0 = buf;
231 } else {
232
233 }
234 if (! tmp___4) {
235 ret = -1;
236 goto end;
237 } else {
238
239 }
240 if (! tmp___5) {
241 ret = -1;
242 goto end;
243 } else {
244
245 }
246 s__state = 4368;
247 s__ctx__stats__sess_connect = s__ctx__stats__sess_connect + 1;
248 s__init_num = 0;
249 goto switch_1_break;
250 switch_1_4368: ;
251 switch_1_4369:
252 s__shutdown = 0;
253 ret = nondet_int();
254 if (blastFlag == 0) {
255 blastFlag = 1;
256 } else {
257 if (blastFlag == 4) {
258 blastFlag = 5;
259 } else {
260
261 }
262 }
263 if (ret <= 0) {
264 goto end;
265 } else {
266
267 }
268 s__state = 4384;
269 s__init_num = 0;
270 if (s__bbio != s__wbio) {
271
272 } else {
273
274 }
275 goto switch_1_break;
276 switch_1_4384: ;
277 switch_1_4385:
278 ret = nondet_int();
279 if (blastFlag == 1) {
280 blastFlag = 2;
281 } else {
282
283 }
284 if (ret <= 0) {
285 goto end;
286 } else {
287
288 }
289 if (s__hit) {
290 s__state = 4560;
291 } else {
292 s__state = 4400;
293 }
294 s__init_num = 0;
295 goto switch_1_break;
296 switch_1_4400: ;
297 switch_1_4401: ;
298 if ((unsigned long )s__s3__tmp__new_cipher__algorithms - 256UL) {
299 skip = 1;
300 } else {
301 ret = nondet_int();
302 if (blastFlag == 2) {
303 blastFlag = 3;
304 } else {
305
306 }
307 if (ret <= 0) {
308 goto end;
309 } else {
310
311 }
312 }
313 ag_Y = 61087;
314 s__state = 4416;
315 s__init_num = 0;
316 goto switch_1_break;
317 switch_1_4416: ;
318 switch_1_4417:
319 ret = nondet_int();
320 if (blastFlag == 3) {
321 blastFlag = 4;
322 } else {
323
324 }
325 if (ret <= 0) {
326 goto end;
327 } else {
328
329 }
330 s__state = 4432;
331 ag_X = (unsigned short)65535;
332 s__init_num = 0;
333 if (! tmp___6) {
334 ret = -1;
335 goto end;
336 } else {
337
338 }
339 goto switch_1_break;
340 switch_1_4432: ;
341 switch_1_4433:
342 ret = nondet_int();
343 if (blastFlag == 5) {
344 goto ERROR;
345 } else {
346
347 }
348 if (ret <= 0) {
349 goto end;
350 } else {
351
352 }
353 s__state = ag_X ^ ag_Y;
354 s__init_num = 0;
355 goto switch_1_break;
356 switch_1_4448: ;
357 switch_1_4449:
358 ret = nondet_int();
359 if (ret <= 0) {
360 goto end;
361 } else {
362
363 }
364 if (s__s3__tmp__cert_req) {
365 s__state = 4464;
366 } else {
367 s__state = 4480;
368 }
369 s__init_num = 0;
370 goto switch_1_break;
371 switch_1_4464: ;
372 switch_1_4465: ;
373 switch_1_4466: ;
374 switch_1_4467:
375 ret = nondet_int();
376 if (ret <= 0) {
377 goto end;
378 } else {
379
380 }
381 s__state = 4480;
382 s__init_num = 0;
383 goto switch_1_break;
384 switch_1_4480: ;
385 switch_1_4481:
386 ret = nondet_int();
387 if (ret <= 0) {
388 goto end;
389 } else {
390
391 }
392 l = s__s3__tmp__new_cipher__algorithms;
393 if (s__s3__tmp__cert_req == 1) {
394 s__state = 4496;
395 } else {
396 s__state = 4512;
397 s__s3__change_cipher_spec = 0;
398 }
399 s__init_num = 0;
400 goto switch_1_break;
401 switch_1_4496: ;
402 switch_1_4497:
403 ret = nondet_int();
404 if (ret <= 0) {
405 goto end;
406 } else {
407
408 }
409 s__state = 4512;
410 s__init_num = 0;
411 s__s3__change_cipher_spec = 0;
412 goto switch_1_break;
413 switch_1_4512: ;
414 switch_1_4513:
415 ret = nondet_int();
416 if (ret <= 0) {
417 goto end;
418 } else {
419
420 }
421 s__state = 4528;
422 s__init_num = 0;
423 s__session__cipher = s__s3__tmp__new_cipher;
424 if (s__s3__tmp__new_compression == 0) {
425 s__session__compress_meth = 0;
426 } else {
427 s__session__compress_meth = s__s3__tmp__new_compression__id;
428 }
429 if (! tmp___7) {
430 ret = -1;
431 goto end;
432 } else {
433
434 }
435 if (! tmp___8) {
436 ret = -1;
437 goto end;
438 } else {
439
440 }
441 goto switch_1_break;
442 switch_1_4528: ;
443 switch_1_4529:
444 ret = nondet_int();
445 if (ret <= 0) {
446 goto end;
447 } else {
448
449 }
450 s__state = 4352;
451 s__s3__flags = (long )s__s3__flags - -5L;
452 if (s__hit) {
453 s__s3__tmp__next_state___0 = 3;
454 if ((long )s__s3__flags - 2L) {
455 s__state = 3;
456 s__s3__flags = (long )s__s3__flags + 4L;
457 s__s3__delay_buf_pop_ret = 0;
458 } else {
459
460 }
461 } else {
462 s__s3__tmp__next_state___0 = 4560;
463 }
464 s__init_num = 0;
465 goto switch_1_break;
466 switch_1_4560: ;
467 switch_1_4561:
468 ret = nondet_int();
469 if (ret <= 0) {
470 goto end;
471 } else {
472
473 }
474 if (s__hit) {
475 s__state = 4512;
476 } else {
477 s__state = 3;
478 }
479 s__init_num = 0;
480 goto switch_1_break;
481 switch_1_4352:
482 if ((long )num1 > 0L) {
483 s__rwstate = 2;
484 num1 = tmp___9;
485 if ((long )num1 <= 0L) {
486 ret = -1;
487 goto end;
488 } else {
489
490 }
491 s__rwstate = 1;
492 } else {
493
494 }
495 s__state = s__s3__tmp__next_state___0;
496 goto switch_1_break;
497 switch_1_3:
498 if (s__init_buf___0 != 0) {
499 s__init_buf___0 = 0;
500 } else {
501
502 }
503 if (! ((long )s__s3__flags - 4L)) {
504
505 } else {
506
507 }
508 s__init_num = 0;
509 s__new_session = 0;
510 if (s__hit) {
511 s__ctx__stats__sess_hit = s__ctx__stats__sess_hit + 1;
512 } else {
513
514 }
515 ret = 1;
516 s__ctx__stats__sess_connect_good = s__ctx__stats__sess_connect_good + 1;
517 if (cb != 0) {
518
519 } else {
520
521 }
522 goto end;
523 switch_1_default:
524 ret = -1;
525 goto end;
526 } else {
527 switch_1_break: ;
528 }
529 }
530 }
531 }
532 }
533 }
534 }
535 }
536 }
537 }
538 }
539 }
540 }
541 }
542 }
543 }
544 }
545 }
546 }
547 }
548 }
549 }
550 }
551 }
552 }
553 }
554 }
555 }
556 }
557 }
558 }
559 }
560 }
561 }
562 }
563 if (! s__s3__tmp__reuse_message) {
564 if (! skip) {
565 if (s__debug) {
566 ret = nondet_int();
567 if (ret <= 0) {
568 goto end;
569 } else {
570
571 }
572 } else {
573
574 }
575 if (cb != 0) {
576 if (s__state != state) {
577 new_state = s__state;
578 s__state = state;
579 s__state = new_state;
580 } else {
581
582 }
583 } else {
584
585 }
586 } else {
587
588 }
589 } else {
590
591 }
592 skip = 0;
593 }
594 while_0_break: ;
595 }
596 end:
597 s__in_handshake = s__in_handshake - 1;
598 if (cb != 0) {
599
600 } else {
601
602 }
603 __retres59 = ret;
604 goto return_label;
605 ERROR:
606 {
607 }
608 __retres59 = -1;
609 return_label:
610 return (__retres59);
611}
612}
613int main(void)
614{ int __retres1 ;
615
616 {
617 {
618 ssl3_connect();
619 }
620 __retres1 = 0;
621 return (__retres1);
622}
623}