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