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 s__init_num = 0;
361 goto switch_1_break;
362 switch_1_4448: ;
363 switch_1_4449:
364 ret = nondet_int();
365 if (blastFlag == 4) {
366 blastFlag = 5;
367 } else {
368
369 }
370 if (ret <= 0) {
371 goto end;
372 } else {
373
374 }
375 if (s__s3__tmp__cert_req) {
376 s__state = ag_X * ag_Y + ag_Z;
377 } else {
378 s__state = 4480;
379 }
380 s__init_num = 0;
381 goto switch_1_break;
382 switch_1_4464: ;
383 switch_1_4465: ;
384 switch_1_4466: ;
385 switch_1_4467:
386 ret = nondet_int();
387 if (ret <= 0) {
388 goto end;
389 } else {
390
391 }
392 s__state = 4480;
393 s__init_num = 0;
394 goto switch_1_break;
395 switch_1_4480: ;
396 switch_1_4481:
397 ret = nondet_int();
398 if (ret <= 0) {
399 goto end;
400 } else {
401
402 }
403 l = s__s3__tmp__new_cipher__algorithms;
404 if (s__s3__tmp__cert_req == 1) {
405 s__state = 4496;
406 } else {
407 s__state = 4512;
408 s__s3__change_cipher_spec = 0;
409 }
410 s__init_num = 0;
411 goto switch_1_break;
412 switch_1_4496: ;
413 switch_1_4497:
414 ret = nondet_int();
415 if (ret <= 0) {
416 goto end;
417 } else {
418
419 }
420 s__state = 4512;
421 s__init_num = 0;
422 s__s3__change_cipher_spec = 0;
423 goto switch_1_break;
424 switch_1_4512: ;
425 switch_1_4513:
426 ret = nondet_int();
427 if (ret <= 0) {
428 goto end;
429 } else {
430
431 }
432 s__state = 4528;
433 s__init_num = 0;
434 s__session__cipher = s__s3__tmp__new_cipher;
435 if (s__s3__tmp__new_compression == 0) {
436 s__session__compress_meth = 0;
437 } else {
438 s__session__compress_meth = s__s3__tmp__new_compression__id;
439 }
440 if (! tmp___7) {
441 ret = -1;
442 goto end;
443 } else {
444
445 }
446 if (! tmp___8) {
447 ret = -1;
448 goto end;
449 } else {
450
451 }
452 goto switch_1_break;
453 switch_1_4528: ;
454 switch_1_4529:
455 ret = nondet_int();
456 if (ret <= 0) {
457 goto end;
458 } else {
459
460 }
461 s__state = 4352;
462 s__s3__flags = (long )s__s3__flags - -5L;
463 if (s__hit) {
464 s__s3__tmp__next_state___0 = 3;
465 if ((long )s__s3__flags - 2L) {
466 s__state = 3;
467 s__s3__flags = (long )s__s3__flags + 4L;
468 s__s3__delay_buf_pop_ret = 0;
469 } else {
470
471 }
472 } else {
473 s__s3__tmp__next_state___0 = 4560;
474 }
475 s__init_num = 0;
476 goto switch_1_break;
477 switch_1_4560: ;
478 switch_1_4561:
479 ret = nondet_int();
480 if (ret <= 0) {
481 goto end;
482 } else {
483
484 }
485 if (s__hit) {
486 s__state = 4512;
487 } else {
488 s__state = 3;
489 }
490 s__init_num = 0;
491 goto switch_1_break;
492 switch_1_4352:
493 if ((long )num1 > 0L) {
494 s__rwstate = 2;
495 num1 = tmp___9;
496 if ((long )num1 <= 0L) {
497 ret = -1;
498 goto end;
499 } else {
500
501 }
502 s__rwstate = 1;
503 } else {
504
505 }
506 s__state = s__s3__tmp__next_state___0;
507 goto switch_1_break;
508 switch_1_3:
509 if (s__init_buf___0 != 0) {
510 s__init_buf___0 = 0;
511 } else {
512
513 }
514 if (! ((long )s__s3__flags - 4L)) {
515
516 } else {
517
518 }
519 s__init_num = 0;
520 s__new_session = 0;
521 if (s__hit) {
522 s__ctx__stats__sess_hit = s__ctx__stats__sess_hit + 1;
523 } else {
524
525 }
526 ret = 1;
527 s__ctx__stats__sess_connect_good = s__ctx__stats__sess_connect_good + 1;
528 if (cb != 0) {
529
530 } else {
531
532 }
533 goto end;
534 switch_1_default:
535 ret = -1;
536 goto end;
537 } else {
538 switch_1_break: ;
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 }
564 }
565 }
566 }
567 }
568 }
569 }
570 }
571 }
572 }
573 }
574 if (! s__s3__tmp__reuse_message) {
575 if (! skip) {
576 if (s__debug) {
577 ret = nondet_int();
578 if (ret <= 0) {
579 goto end;
580 } else {
581
582 }
583 } else {
584
585 }
586 if (cb != 0) {
587 if (s__state != state) {
588 new_state = s__state;
589 s__state = state;
590 s__state = new_state;
591 } else {
592
593 }
594 } else {
595
596 }
597 } else {
598
599 }
600 } else {
601
602 }
603 skip = 0;
604 }
605 while_0_break: ;
606 }
607 end:
608 s__in_handshake = s__in_handshake - 1;
609 if (cb != 0) {
610
611 } else {
612
613 }
614 __retres62 = ret;
615 goto return_label;
616 ERROR:
617 {
618 }
619 __retres62 = -1;
620 return_label:
621 return (__retres62);
622}
623}
624int main(void)
625{ int __retres1 ;
626
627 {
628 {
629 ssl3_connect();
630 }
631 __retres1 = 0;
632 return (__retres1);
633}
634}