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