1extern int nondet_int(void);
2
3
4
5int ssl3_accept(int initial_state )
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__hit ;
15 int s__rwstate ;
16 int s__init_buf___0 ;
17 int s__debug ;
18 int s__shutdown ;
19 int s__cert ;
20 int s__options ;
21 int s__verify_mode ;
22 int s__session__peer ;
23 int s__cert__pkeys__AT0__privatekey ;
24 int s__ctx__info_callback ;
25 int s__ctx__stats__sess_accept_renegotiate ;
26 int s__ctx__stats__sess_accept ;
27 int s__ctx__stats__sess_accept_good ;
28 int s__s3__tmp__cert_request ;
29 int s__s3__tmp__reuse_message ;
30 int s__s3__tmp__use_rsa_tmp ;
31 int s__s3__tmp__new_cipher ;
32 int s__s3__tmp__new_cipher__algorithms ;
33 int s__s3__tmp__next_state___0 ;
34 int s__s3__tmp__new_cipher__algo_strength ;
35 int s__session__cipher ;
36 int buf ;
37 unsigned long l ;
38 unsigned long Time ;
39 unsigned long tmp ;
40 int cb ;
41 long num1 ;
42 int ret ;
43 int new_state ;
44 int state ;
45 int skip ;
46 int got_new_session ;
47 int tmp___1 ;
48 int tmp___2 ;
49 int tmp___3 ;
50 int tmp___4 ;
51 int tmp___5 ;
52 int tmp___6 ;
53 int tmp___7 ;
54 long tmp___8 ;
55 int tmp___9 ;
56 int tmp___10 ;
57 int blastFlag ;
58 int __retres67 ;
59
60 {
61 s__state = initial_state;
62 blastFlag = 0;
63 Time = tmp;
64 cb = 0;
65 ret = -1;
66 skip = 0;
67 got_new_session = 0;
68 if (s__info_callback != 0) {
69 cb = s__info_callback;
70 } else {
71 if (s__ctx__info_callback != 0) {
72 cb = s__ctx__info_callback;
73 } else {
74
75 }
76 }
77 s__in_handshake = s__in_handshake + 1;
78 if (tmp___1 & 12288) {
79 if (tmp___2 & 16384) {
80
81 } else {
82
83 }
84 } else {
85
86 }
87 if (s__cert == 0) {
88 __retres67 = -1;
89 goto return_label;
90 } else {
91
92 }
93 {
94 while (1) {
95 while_0_continue: ;
96 state = s__state;
97 if (s__state == 12292) {
98 goto switch_1_12292;
99 } else {
100 if (s__state == 16384) {
101 goto switch_1_16384;
102 } else {
103 if (s__state == 8192) {
104 goto switch_1_8192;
105 } else {
106 if (s__state == 24576) {
107 goto switch_1_24576;
108 } else {
109 if (s__state == 8195) {
110 goto switch_1_8195;
111 } else {
112 if (s__state == 8480) {
113 goto switch_1_8480;
114 } else {
115 if (s__state == 8481) {
116 goto switch_1_8481;
117 } else {
118 if (s__state == 8482) {
119 goto switch_1_8482;
120 } else {
121 if (s__state == 8464) {
122 goto switch_1_8464;
123 } else {
124 if (s__state == 8465) {
125 goto switch_1_8465;
126 } else {
127 if (s__state == 8466) {
128 goto switch_1_8466;
129 } else {
130 if (s__state == 8496) {
131 goto switch_1_8496;
132 } else {
133 if (s__state == 8497) {
134 goto switch_1_8497;
135 } else {
136 if (s__state == 8512) {
137 goto switch_1_8512;
138 } else {
139 if (s__state == 8513) {
140 goto switch_1_8513;
141 } else {
142 if (s__state == 8528) {
143 goto switch_1_8528;
144 } else {
145 if (s__state == 8529) {
146 goto switch_1_8529;
147 } else {
148 if (s__state == 8544) {
149 goto switch_1_8544;
150 } else {
151 if (s__state == 8545) {
152 goto switch_1_8545;
153 } else {
154 if (s__state == 8560) {
155 goto switch_1_8560;
156 } else {
157 if (s__state == 8561) {
158 goto switch_1_8561;
159 } else {
160 if (s__state == 8448) {
161 goto switch_1_8448;
162 } else {
163 if (s__state == 8576) {
164 goto switch_1_8576;
165 } else {
166 if (s__state == 8577) {
167 goto switch_1_8577;
168 } else {
169 if (s__state == 8592) {
170 goto switch_1_8592;
171 } else {
172 if (s__state == 8593) {
173 goto switch_1_8593;
174 } else {
175 if (s__state == 8608) {
176 goto switch_1_8608;
177 } else {
178 if (s__state == 8609) {
179 goto switch_1_8609;
180 } else {
181 if (s__state == 8640) {
182 goto switch_1_8640;
183 } else {
184 if (s__state == 8641) {
185 goto switch_1_8641;
186 } else {
187 if (s__state == 8656) {
188 goto switch_1_8656;
189 } else {
190 if (s__state == 8657) {
191 goto switch_1_8657;
192 } else {
193 if (s__state == 8672) {
194 goto switch_1_8672;
195 } else {
196 if (s__state == 8673) {
197 goto switch_1_8673;
198 } else {
199 if (s__state == 3) {
200 goto switch_1_3;
201 } else {
202 {
203 goto switch_1_default;
204 if (0) {
205 switch_1_12292:
206 s__new_session = 1;
207 switch_1_16384: ;
208 switch_1_8192: ;
209 switch_1_24576: ;
210 switch_1_8195:
211 s__server = 1;
212 if (cb != 0) {
213
214 } else {
215
216 }
217 if (s__version >> 8 != 3) {
218 __retres67 = -1;
219 goto return_label;
220 } else {
221
222 }
223 s__type = 8192;
224 if (s__init_buf___0 == 0) {
225 tmp___3 = nondet_int();
226 if (! tmp___3) {
227 ret = -1;
228 goto end;
229 } else {
230
231 }
232 s__init_buf___0 = buf;
233 } else {
234
235 }
236 tmp___4 = nondet_int();
237 if (! tmp___4) {
238 ret = -1;
239 goto end;
240 } else {
241
242 }
243 s__init_num = 0;
244 if (s__state != 12292) {
245 tmp___5 = nondet_int();
246 if (! tmp___5) {
247 ret = -1;
248 goto end;
249 } else {
250
251 }
252 s__state = 8464;
253 s__ctx__stats__sess_accept = s__ctx__stats__sess_accept + 1;
254 } else {
255 s__ctx__stats__sess_accept_renegotiate = s__ctx__stats__sess_accept_renegotiate + 1;
256 s__state = 8480;
257 }
258 goto switch_1_break;
259 switch_1_8480: ;
260 switch_1_8481:
261 s__shutdown = 0;
262 ret = nondet_int();
263 if (ret <= 0) {
264 goto end;
265 } else {
266
267 }
268 s__s3__tmp__next_state___0 = 8482;
269 s__state = 8448;
270 s__init_num = 0;
271 goto switch_1_break;
272 switch_1_8482:
273 s__state = 3;
274 goto switch_1_break;
275 switch_1_8464: ;
276 switch_1_8465: ;
277 switch_1_8466:
278 s__shutdown = 0;
279 ret = nondet_int();
280 if (blastFlag == 0) {
281 blastFlag = 1;
282 } else {
283
284 }
285 if (ret <= 0) {
286 goto end;
287 } else {
288
289 }
290 got_new_session = 1;
291 s__state = 8496;
292 s__init_num = 0;
293 goto switch_1_break;
294 switch_1_8496: ;
295 switch_1_8497:
296 ret = nondet_int();
297 if (blastFlag == 1) {
298 blastFlag = 2;
299 } else {
300
301 }
302 if (ret <= 0) {
303 goto end;
304 } else {
305
306 }
307 if (s__hit) {
308 s__state = 8656;
309 } else {
310 s__state = 8512;
311 }
312 s__init_num = 0;
313 goto switch_1_break;
314 switch_1_8512: ;
315 switch_1_8513: ;
316 if ((unsigned long )s__s3__tmp__new_cipher__algorithms & 256UL) {
317 skip = 1;
318 } else {
319 ret = nondet_int();
320 if (ret <= 0) {
321 goto end;
322 } else {
323
324 }
325 }
326 s__state = 8528;
327 s__init_num = 0;
328 goto switch_1_break;
329 switch_1_8528: ;
330 switch_1_8529:
331 l = s__s3__tmp__new_cipher__algorithms;
332 if ((unsigned long )s__options & 2097152UL) {
333 s__s3__tmp__use_rsa_tmp = 1;
334 } else {
335 s__s3__tmp__use_rsa_tmp = 0;
336 }
337 if (s__s3__tmp__use_rsa_tmp) {
338 goto _L___0;
339 } else {
340 if (l & 30UL) {
341 goto _L___0;
342 } else {
343 if (l & 1UL) {
344 if (s__cert__pkeys__AT0__privatekey == 0) {
345 goto _L___0;
346 } else {
347 if ((unsigned long )s__s3__tmp__new_cipher__algo_strength & 2UL) {
348 tmp___6 = nondet_int();
349 if ((unsigned long )s__s3__tmp__new_cipher__algo_strength & 4UL) {
350 tmp___7 = 512;
351 } else {
352 tmp___7 = 1024;
353 }
354 if (tmp___6 * 8 > tmp___7) {
355 _L___0:
356 ret = nondet_int();
357 if (ret <= 0) {
358 goto end;
359 } else {
360
361 }
362 } else {
363 skip = 1;
364 }
365 } else {
366 skip = 1;
367 }
368 }
369 } else {
370 skip = 1;
371 }
372 }
373 }
374 s__state = 8544;
375 s__init_num = 0;
376 goto switch_1_break;
377 switch_1_8544: ;
378 switch_1_8545: ;
379 if (s__verify_mode & 1) {
380 if (s__session__peer != 0) {
381 if (s__verify_mode & 4) {
382 skip = 1;
383 s__s3__tmp__cert_request = 0;
384 s__state = 8560;
385 } else {
386 goto _L___2;
387 }
388 } else {
389 _L___2:
390 if ((unsigned long )s__s3__tmp__new_cipher__algorithms & 256UL) {
391 if (s__verify_mode & 2) {
392 goto _L___1;
393 } else {
394 skip = 1;
395 s__s3__tmp__cert_request = 0;
396 s__state = 8560;
397 }
398 } else {
399 _L___1:
400 s__s3__tmp__cert_request = 1;
401 ret = nondet_int();
402 if (ret <= 0) {
403 goto end;
404 } else {
405
406 }
407 s__state = 8448;
408 s__s3__tmp__next_state___0 = 8576;
409 s__init_num = 0;
410 }
411 }
412 } else {
413 skip = 1;
414 s__s3__tmp__cert_request = 0;
415 s__state = 8560;
416 }
417 goto switch_1_break;
418 switch_1_8560: ;
419 switch_1_8561:
420 ret = nondet_int();
421 if (ret <= 0) {
422 goto end;
423 } else {
424
425 }
426 s__s3__tmp__next_state___0 = 8576;
427 s__state = 8448;
428 s__init_num = 0;
429 goto switch_1_break;
430 switch_1_8448:
431 num1 = nondet_int();
432 if (num1 > 0L) {
433 s__rwstate = 2;
434 num1 = tmp___8;
435 if (num1 <= 0L) {
436 ret = -1;
437 goto end;
438 } else {
439
440 }
441 s__rwstate = 1;
442 } else {
443
444 }
445 s__state = s__s3__tmp__next_state___0;
446 goto switch_1_break;
447 switch_1_8576: ;
448 switch_1_8577:
449 ret = nondet_int();
450 if (ret <= 0) {
451 goto end;
452 } else {
453
454 }
455 if (ret == 2) {
456 s__state = 8466;
457 } else {
458 ret = nondet_int();
459 if (ret <= 0) {
460 goto end;
461 } else {
462
463 }
464 s__init_num = 0;
465 s__state = 8592;
466 }
467 goto switch_1_break;
468 switch_1_8592: ;
469 switch_1_8593:
470 ret = nondet_int();
471 if (ret <= 0) {
472 goto end;
473 } else {
474
475 }
476 s__state = 8608;
477 s__init_num = 0;
478 goto switch_1_break;
479 switch_1_8608: ;
480 switch_1_8609:
481 ret = nondet_int();
482 if (ret <= 0) {
483 goto end;
484 } else {
485
486 }
487 s__state = 8640;
488 s__init_num = 0;
489 goto switch_1_break;
490 switch_1_8640: ;
491 switch_1_8641:
492 ret = nondet_int();
493 if (blastFlag == 3) {
494 blastFlag = 4;
495 } else {
496
497 }
498 if (ret <= 0) {
499 goto end;
500 } else {
501
502 }
503 if (s__hit) {
504 s__state = 3;
505 } else {
506 s__state = 8656;
507 }
508 s__init_num = 0;
509 goto switch_1_break;
510 switch_1_8656: ;
511 switch_1_8657:
512 s__session__cipher = s__s3__tmp__new_cipher;
513 tmp___9 = nondet_int();
514 if (! tmp___9) {
515 ret = -1;
516 goto end;
517 } else {
518
519 }
520 ret = nondet_int();
521 if (blastFlag == 2) {
522 blastFlag = 3;
523 } else {
524
525 }
526 if (ret <= 0) {
527 goto end;
528 } else {
529
530 }
531 s__state = 8672;
532 s__init_num = 0;
533 tmp___10 = nondet_int();
534 if (! tmp___10) {
535 ret = -1;
536 goto end;
537 } else {
538
539 }
540 goto switch_1_break;
541 switch_1_8672: ;
542 switch_1_8673:
543 ret = nondet_int();
544 if (blastFlag == 4) {
545 goto ERROR;
546 } else {
547 if (blastFlag == 5) {
548 goto ERROR;
549 } else {
550
551 }
552 }
553 if (ret <= 0) {
554 goto end;
555 } else {
556
557 }
558 s__state = 8448;
559 if (s__hit) {
560 s__s3__tmp__next_state___0 = 8640;
561 } else {
562 s__s3__tmp__next_state___0 = 3;
563 }
564 s__init_num = 0;
565 goto switch_1_break;
566 switch_1_3:
567 s__init_buf___0 = 0;
568 s__init_num = 0;
569 if (got_new_session) {
570 s__new_session = 0;
571 s__ctx__stats__sess_accept_good = s__ctx__stats__sess_accept_good + 1;
572 if (cb != 0) {
573
574 } else {
575
576 }
577 } else {
578
579 }
580 ret = 1;
581 goto end;
582 switch_1_default:
583 ret = -1;
584 goto end;
585 } else {
586 switch_1_break: ;
587 }
588 }
589 }
590 }
591 }
592 }
593 }
594 }
595 }
596 }
597 }
598 }
599 }
600 }
601 }
602 }
603 }
604 }
605 }
606 }
607 }
608 }
609 }
610 }
611 }
612 }
613 }
614 }
615 }
616 }
617 }
618 }
619 }
620 }
621 }
622 }
623 }
624 if (! s__s3__tmp__reuse_message) {
625 if (! skip) {
626 if (s__debug) {
627 ret = nondet_int();
628 if (ret <= 0) {
629 goto end;
630 } else {
631
632 }
633 } else {
634
635 }
636 if (cb != 0) {
637 if (s__state != state) {
638 new_state = s__state;
639 s__state = state;
640 s__state = new_state;
641 } else {
642
643 }
644 } else {
645
646 }
647 } else {
648
649 }
650 } else {
651
652 }
653 skip = 0;
654 }
655 while_0_break: ;
656 }
657 end:
658 s__in_handshake = s__in_handshake - 1;
659 if (cb != 0) {
660
661 } else {
662
663 }
664 __retres67 = ret;
665 goto return_label;
666 ERROR:
667 {
668 }
669 __retres67 = -1;
670 return_label:
671 return (__retres67);
672}
673}
674int main(void)
675{ int s ;
676 int tmp ;
677
678 {
679 {
680 s = 8464;
681 tmp = ssl3_accept(s);
682 }
683 return (tmp);
684}
685}