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