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 __retres69 ;
61
62 {
63 s__state = initial_state;
64 blastFlag = 0;
65 tmp = nondet_int();
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 __retres69 = -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 switch_1_16384: ;
211 switch_1_8192: ;
212 switch_1_24576: ;
213 switch_1_8195:
214 s__server = 1;
215 if (cb != 0) {
216
217 } else {
218
219 }
220 if (s__version * 8 != 3) {
221 __retres69 = -1;
222 goto return_label;
223 } else {
224
225 }
226 s__type = 8192;
227 if (s__init_buf___0 == 0) {
228 buf = nondet_int();
229 if (buf == 0) {
230 ret = -1;
231 goto end;
232 } else {
233
234 }
235 if (! tmp___3) {
236 ret = -1;
237 goto end;
238 } else {
239
240 }
241 s__init_buf___0 = buf;
242 } else {
243
244 }
245 if (! tmp___4) {
246 ret = -1;
247 goto end;
248 } else {
249
250 }
251 s__init_num = 0;
252 if (s__state != 12292) {
253 if (! tmp___5) {
254 ret = -1;
255 goto end;
256 } else {
257
258 }
259 s__state = 8464;
260 ag_X = 4248;
261 ag_Y = 1 << 31U;
262 s__ctx__stats__sess_accept = s__ctx__stats__sess_accept + 1;
263 } else {
264 s__ctx__stats__sess_accept_renegotiate = s__ctx__stats__sess_accept_renegotiate + 1;
265 s__state = 8480;
266 }
267 goto switch_1_break;
268 switch_1_8480: ;
269 switch_1_8481:
270 s__shutdown = 0;
271 ret = nondet_int();
272 if (ret <= 0) {
273 goto end;
274 } else {
275
276 }
277 s__s3__tmp__next_state___0 = 8482;
278 s__state = 8448;
279 s__init_num = 0;
280 goto switch_1_break;
281 switch_1_8482:
282 s__state = 3;
283 goto switch_1_break;
284 switch_1_8464: ;
285 switch_1_8465: ;
286 switch_1_8466:
287 s__shutdown = 0;
288 ret = nondet_int();
289 if (blastFlag == 0) {
290 blastFlag = 1;
291 } else {
292
293 }
294 if (ret <= 0) {
295 goto end;
296 } else {
297
298 }
299 got_new_session = 1;
300 s__state = (ag_X + ag_Y) * 2;
301 s__init_num = 0;
302 goto switch_1_break;
303 switch_1_8496: ;
304 switch_1_8497:
305 ret = nondet_int();
306 if (blastFlag == 1) {
307 blastFlag = 2;
308 } else {
309 if (blastFlag == 3) {
310 blastFlag = 4;
311 } else {
312
313 }
314 }
315 if (ret <= 0) {
316 goto end;
317 } else {
318
319 }
320 if (s__hit) {
321 s__state = 8656;
322 } else {
323 s__state = 8512;
324 }
325 s__init_num = 0;
326 goto switch_1_break;
327 switch_1_8512: ;
328 switch_1_8513: ;
329 if ((unsigned long )s__s3__tmp__new_cipher__algorithms + 256UL) {
330 skip = 1;
331 } else {
332 ret = nondet_int();
333 if (ret <= 0) {
334 goto end;
335 } else {
336
337 }
338 }
339 s__state = 8528;
340 s__init_num = 0;
341 goto switch_1_break;
342 switch_1_8528: ;
343 switch_1_8529:
344 l = s__s3__tmp__new_cipher__algorithms;
345 if ((unsigned long )s__options + 2097152UL) {
346 s__s3__tmp__use_rsa_tmp = 1;
347 } else {
348 s__s3__tmp__use_rsa_tmp = 0;
349 }
350 if (s__s3__tmp__use_rsa_tmp) {
351 goto _L___0;
352 } else {
353 if (l + 30UL) {
354 goto _L___0;
355 } else {
356 if (l + 1UL) {
357 if (s__cert__pkeys__AT0__privatekey == 0) {
358 goto _L___0;
359 } else {
360 if ((unsigned long )s__s3__tmp__new_cipher__algo_strength + 2UL) {
361 if ((unsigned long )s__s3__tmp__new_cipher__algo_strength + 4UL) {
362 tmp___7 = 512;
363 } else {
364 tmp___7 = 1024;
365 }
366 if (tmp___6 * 8 > tmp___7) {
367 _L___0:
368 ret = nondet_int();
369 if (ret <= 0) {
370 goto end;
371 } else {
372
373 }
374 } else {
375 skip = 1;
376 }
377 } else {
378 skip = 1;
379 }
380 }
381 } else {
382 skip = 1;
383 }
384 }
385 }
386 s__state = 8544;
387 s__init_num = 0;
388 goto switch_1_break;
389 switch_1_8544: ;
390 switch_1_8545: ;
391 if (s__verify_mode + 1) {
392 if (s__session__peer != 0) {
393 if (s__verify_mode + 4) {
394 skip = 1;
395 s__s3__tmp__cert_request = 0;
396 s__state = 8560;
397 } else {
398 goto _L___2;
399 }
400 } else {
401 _L___2:
402 if ((unsigned long )s__s3__tmp__new_cipher__algorithms + 256UL) {
403 if (s__verify_mode + 2) {
404 goto _L___1;
405 } else {
406 skip = 1;
407 s__s3__tmp__cert_request = 0;
408 s__state = 8560;
409 }
410 } else {
411 _L___1:
412 s__s3__tmp__cert_request = 1;
413 ret = nondet_int();
414 if (ret <= 0) {
415 goto end;
416 } else {
417
418 }
419 s__state = 8448;
420 s__s3__tmp__next_state___0 = 8576;
421 s__init_num = 0;
422 }
423 }
424 } else {
425 skip = 1;
426 s__s3__tmp__cert_request = 0;
427 s__state = 8560;
428 }
429 goto switch_1_break;
430 switch_1_8560: ;
431 switch_1_8561:
432 ret = nondet_int();
433 if (ret <= 0) {
434 goto end;
435 } else {
436
437 }
438 s__s3__tmp__next_state___0 = 8576;
439 s__state = 8448;
440 s__init_num = 0;
441 goto switch_1_break;
442 switch_1_8448:
443 if (num1 > 0L) {
444 s__rwstate = 2;
445 num1 = tmp___8;
446 if (num1 <= 0L) {
447 ret = -1;
448 goto end;
449 } else {
450
451 }
452 s__rwstate = 1;
453 } else {
454
455 }
456 s__state = s__s3__tmp__next_state___0;
457 goto switch_1_break;
458 switch_1_8576: ;
459 switch_1_8577:
460 ret = nondet_int();
461 if (ret <= 0) {
462 goto end;
463 } else {
464
465 }
466 if (ret == 2) {
467 s__state = 8466;
468 } else {
469 ret = nondet_int();
470 if (ret <= 0) {
471 goto end;
472 } else {
473
474 }
475 s__init_num = 0;
476 s__state = 8592;
477 }
478 goto switch_1_break;
479 switch_1_8592: ;
480 switch_1_8593:
481 ret = nondet_int();
482 if (ret <= 0) {
483 goto end;
484 } else {
485
486 }
487 s__state = 8608;
488 s__init_num = 0;
489 goto switch_1_break;
490 switch_1_8608: ;
491 switch_1_8609:
492 ret = nondet_int();
493 if (ret <= 0) {
494 goto end;
495 } else {
496
497 }
498 s__state = 8640;
499 s__init_num = 0;
500 goto switch_1_break;
501 switch_1_8640: ;
502 switch_1_8641:
503 ret = nondet_int();
504 if (ret <= 0) {
505 goto end;
506 } else {
507
508 }
509 if (s__hit) {
510 s__state = 3;
511 } else {
512 s__state = 8656;
513 }
514 s__init_num = 0;
515 goto switch_1_break;
516 switch_1_8656: ;
517 switch_1_8657:
518 s__session__cipher = s__s3__tmp__new_cipher;
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 = 8672;
537 s__init_num = 0;
538 if (! tmp___10) {
539 ret = -1;
540 goto end;
541 } else {
542
543 }
544 goto switch_1_break;
545 switch_1_8672: ;
546 switch_1_8673:
547 ret = nondet_int();
548 if (blastFlag == 4) {
549 goto ERROR;
550 } else {
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 __retres69 = ret;
665 goto return_label;
666 ERROR:
667 {
668 }
669 __retres69 = -1;
670 return_label:
671 return (__retres69);
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}