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_Y = 1 << 31U;
261 s__ctx__stats__sess_accept = s__ctx__stats__sess_accept + 1;
262 } else {
263 s__ctx__stats__sess_accept_renegotiate = s__ctx__stats__sess_accept_renegotiate + 1;
264 s__state = 8480;
265 }
266 goto switch_1_break;
267 switch_1_8480: ;
268 switch_1_8481:
269 s__shutdown = 0;
270 ret = nondet_int();
271 if (ret <= 0) {
272 goto end;
273 } else {
274
275 }
276 s__s3__tmp__next_state___0 = 8482;
277 s__state = 8448;
278 s__init_num = 0;
279 goto switch_1_break;
280 switch_1_8482:
281 s__state = 3;
282 goto switch_1_break;
283 switch_1_8464: ;
284 switch_1_8465: ;
285 switch_1_8466:
286 s__shutdown = 0;
287 ret = nondet_int();
288 if (blastFlag == 0) {
289 blastFlag = 1;
290 } else {
291
292 }
293 if (ret <= 0) {
294 goto end;
295 } else {
296
297 }
298 got_new_session = 1;
299 s__state = (ag_X + ag_Y) * 2;
300 s__init_num = 0;
301 goto switch_1_break;
302 switch_1_8496: ;
303 switch_1_8497:
304 ret = nondet_int();
305 if (blastFlag == 1) {
306 blastFlag = 2;
307 } else {
308 if (blastFlag == 3) {
309 blastFlag = 4;
310 } else {
311
312 }
313 }
314 if (ret <= 0) {
315 goto end;
316 } else {
317
318 }
319 if (s__hit) {
320 s__state = 8656;
321 } else {
322 s__state = 8512;
323 }
324 s__init_num = 0;
325 goto switch_1_break;
326 switch_1_8512: ;
327 switch_1_8513: ;
328 if ((unsigned long )s__s3__tmp__new_cipher__algorithms + 256UL) {
329 skip = 1;
330 } else {
331 ret = nondet_int();
332 if (ret <= 0) {
333 goto end;
334 } else {
335
336 }
337 }
338 s__state = 8528;
339 s__init_num = 0;
340 goto switch_1_break;
341 switch_1_8528: ;
342 switch_1_8529:
343 l = s__s3__tmp__new_cipher__algorithms;
344 if ((unsigned long )s__options + 2097152UL) {
345 s__s3__tmp__use_rsa_tmp = 1;
346 } else {
347 s__s3__tmp__use_rsa_tmp = 0;
348 }
349 if (s__s3__tmp__use_rsa_tmp) {
350 goto _L___0;
351 } else {
352 if (l + 30UL) {
353 goto _L___0;
354 } else {
355 if (l + 1UL) {
356 if (s__cert__pkeys__AT0__privatekey == 0) {
357 goto _L___0;
358 } else {
359 if ((unsigned long )s__s3__tmp__new_cipher__algo_strength + 2UL) {
360 if ((unsigned long )s__s3__tmp__new_cipher__algo_strength + 4UL) {
361 tmp___7 = 512;
362 } else {
363 tmp___7 = 1024;
364 }
365 if (tmp___6 * 8 > tmp___7) {
366 _L___0:
367 ret = nondet_int();
368 if (ret <= 0) {
369 goto end;
370 } else {
371
372 }
373 } else {
374 skip = 1;
375 }
376 } else {
377 skip = 1;
378 }
379 }
380 } else {
381 skip = 1;
382 }
383 }
384 }
385 s__state = 8544;
386 s__init_num = 0;
387 goto switch_1_break;
388 switch_1_8544: ;
389 switch_1_8545: ;
390 if (s__verify_mode + 1) {
391 if (s__session__peer != 0) {
392 if (s__verify_mode + 4) {
393 skip = 1;
394 s__s3__tmp__cert_request = 0;
395 s__state = 8560;
396 } else {
397 goto _L___2;
398 }
399 } else {
400 _L___2:
401 if ((unsigned long )s__s3__tmp__new_cipher__algorithms + 256UL) {
402 if (s__verify_mode + 2) {
403 goto _L___1;
404 } else {
405 skip = 1;
406 s__s3__tmp__cert_request = 0;
407 s__state = 8560;
408 }
409 } else {
410 _L___1:
411 s__s3__tmp__cert_request = 1;
412 ret = nondet_int();
413 if (ret <= 0) {
414 goto end;
415 } else {
416
417 }
418 s__state = 8448;
419 s__s3__tmp__next_state___0 = 8576;
420 s__init_num = 0;
421 }
422 }
423 } else {
424 skip = 1;
425 s__s3__tmp__cert_request = 0;
426 s__state = 8560;
427 }
428 goto switch_1_break;
429 switch_1_8560: ;
430 switch_1_8561:
431 ret = nondet_int();
432 if (ret <= 0) {
433 goto end;
434 } else {
435
436 }
437 s__s3__tmp__next_state___0 = 8576;
438 s__state = 8448;
439 s__init_num = 0;
440 goto switch_1_break;
441 switch_1_8448:
442 if (num1 > 0L) {
443 s__rwstate = 2;
444 num1 = tmp___8;
445 if (num1 <= 0L) {
446 ret = -1;
447 goto end;
448 } else {
449
450 }
451 s__rwstate = 1;
452 } else {
453
454 }
455 s__state = s__s3__tmp__next_state___0;
456 goto switch_1_break;
457 switch_1_8576: ;
458 switch_1_8577:
459 ret = nondet_int();
460 if (ret <= 0) {
461 goto end;
462 } else {
463
464 }
465 if (ret == 2) {
466 s__state = 8466;
467 } else {
468 ret = nondet_int();
469 if (ret <= 0) {
470 goto end;
471 } else {
472
473 }
474 s__init_num = 0;
475 s__state = 8592;
476 }
477 goto switch_1_break;
478 switch_1_8592: ;
479 switch_1_8593:
480 ret = nondet_int();
481 if (ret <= 0) {
482 goto end;
483 } else {
484
485 }
486 s__state = 8608;
487 s__init_num = 0;
488 goto switch_1_break;
489 switch_1_8608: ;
490 switch_1_8609:
491 ret = nondet_int();
492 if (ret <= 0) {
493 goto end;
494 } else {
495
496 }
497 s__state = 8640;
498 s__init_num = 0;
499 goto switch_1_break;
500 switch_1_8640: ;
501 switch_1_8641:
502 ret = nondet_int();
503 if (ret <= 0) {
504 goto end;
505 } else {
506
507 }
508 if (s__hit) {
509 s__state = 3;
510 } else {
511 s__state = 8656;
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 if (! tmp___9) {
519 ret = -1;
520 goto end;
521 } else {
522
523 }
524 ret = nondet_int();
525 if (blastFlag == 2) {
526 blastFlag = 3;
527 } else {
528
529 }
530 if (ret <= 0) {
531 goto end;
532 } else {
533
534 }
535 s__state = 8672;
536 s__init_num = 0;
537 if (! tmp___10) {
538 ret = -1;
539 goto end;
540 } else {
541
542 }
543 goto switch_1_break;
544 switch_1_8672: ;
545 switch_1_8673:
546 ret = nondet_int();
547 if (blastFlag == 4) {
548 goto ERROR;
549 } else {
550
551 }
552 if (ret <= 0) {
553 goto end;
554 } else {
555
556 }
557 s__state = 8448;
558 if (s__hit) {
559 s__s3__tmp__next_state___0 = 8640;
560 } else {
561 s__s3__tmp__next_state___0 = 3;
562 }
563 s__init_num = 0;
564 goto switch_1_break;
565 switch_1_3:
566 s__init_buf___0 = 0;
567 s__init_num = 0;
568 if (got_new_session) {
569 s__new_session = 0;
570 s__ctx__stats__sess_accept_good = s__ctx__stats__sess_accept_good + 1;
571 if (cb != 0) {
572
573 } else {
574
575 }
576 } else {
577
578 }
579 ret = 1;
580 goto end;
581 switch_1_default:
582 ret = -1;
583 goto end;
584 } else {
585 switch_1_break: ;
586 }
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 if (! s__s3__tmp__reuse_message) {
624 if (! skip) {
625 if (s__debug) {
626 ret = nondet_int();
627 if (ret <= 0) {
628 goto end;
629 } else {
630
631 }
632 } else {
633
634 }
635 if (cb != 0) {
636 if (s__state != state) {
637 new_state = s__state;
638 s__state = state;
639 s__state = new_state;
640 } else {
641
642 }
643 } else {
644
645 }
646 } else {
647
648 }
649 } else {
650
651 }
652 skip = 0;
653 }
654 while_0_break: ;
655 }
656 end:
657 s__in_handshake = s__in_handshake - 1;
658 if (cb != 0) {
659
660 } else {
661
662 }
663 __retres69 = ret;
664 goto return_label;
665 ERROR:
666 {
667 }
668 __retres69 = -1;
669 return_label:
670 return (__retres69);
671}
672}
673int main(void)
674{ int s ;
675 int tmp ;
676
677 {
678 {
679 s = 8464;
680 tmp = ssl3_accept(s);
681 }
682 return (tmp);
683}
684}