1
2
3
4#line 4 "s3_srvr_1.cil.c"
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 __cil_tmp55 ;
59 unsigned long __cil_tmp56 ;
60 unsigned long __cil_tmp57 ;
61 unsigned long __cil_tmp58 ;
62 unsigned long __cil_tmp59 ;
63 int __cil_tmp60 ;
64 unsigned long __cil_tmp61 ;
65
66 {
67 s__s3__tmp__new_cipher__algorithms = 0;
68 __cil_tmp56 = 0;
69 __cil_tmp57 = 0;
70 __cil_tmp58 = 0;
71 __cil_tmp59 = 0;
72 __cil_tmp60 = 0;
73 __cil_tmp61 = 0;
74 s__s3__tmp__reuse_message = 0;
75 s__state = initial_state;
76#line 61
77 blastFlag = 0;
78#line 62
79 Time = tmp;
80#line 63
81 cb = 0;
82#line 64
83 ret = -1;
84#line 65
85 skip = 0;
86#line 66
87 got_new_session = 0;
88#line 67
89 if (s__info_callback != 0) {
90#line 68
91 cb = s__info_callback;
92 } else {
93#line 70
94 if (s__ctx__info_callback != 0) {
95#line 71
96 cb = s__ctx__info_callback;
97 }
98 }
99#line 76
100 s__in_handshake ++;
101#line 77
102 if (tmp___1 + 12288) {
103#line 78
104 if (tmp___2 + 16384) {
105
106 }
107 }
108#line 86
109 if (s__cert == 0) {
110#line 87
111 return (-1);
112 }
113 {
114#line 92
115 while (1) {
116 while_0_continue: ;
117#line 94
118 state = s__state;
119#line 95
120 if (s__state == 12292) {
121 goto switch_1_12292;
122 } else {
123#line 98
124 if (s__state == 16384) {
125 goto switch_1_16384;
126 } else {
127#line 101
128 if (s__state == 8192) {
129 goto switch_1_8192;
130 } else {
131#line 104
132 if (s__state == 24576) {
133 goto switch_1_24576;
134 } else {
135#line 107
136 if (s__state == 8195) {
137 goto switch_1_8195;
138 } else {
139#line 110
140 if (s__state == 8480) {
141 goto switch_1_8480;
142 } else {
143#line 113
144 if (s__state == 8481) {
145 goto switch_1_8481;
146 } else {
147#line 116
148 if (s__state == 8482) {
149 goto switch_1_8482;
150 } else {
151#line 119
152 if (s__state == 8464) {
153 goto switch_1_8464;
154 } else {
155#line 122
156 if (s__state == 8465) {
157 goto switch_1_8465;
158 } else {
159#line 125
160 if (s__state == 8466) {
161 goto switch_1_8466;
162 } else {
163#line 128
164 if (s__state == 8496) {
165 goto switch_1_8496;
166 } else {
167#line 131
168 if (s__state == 8497) {
169 goto switch_1_8497;
170 } else {
171#line 134
172 if (s__state == 8512) {
173 goto switch_1_8512;
174 } else {
175#line 137
176 if (s__state == 8513) {
177 goto switch_1_8513;
178 } else {
179#line 140
180 if (s__state == 8528) {
181 goto switch_1_8528;
182 } else {
183#line 143
184 if (s__state == 8529) {
185 goto switch_1_8529;
186 } else {
187#line 146
188 if (s__state == 8544) {
189 goto switch_1_8544;
190 } else {
191#line 149
192 if (s__state == 8545) {
193 goto switch_1_8545;
194 } else {
195#line 152
196 if (s__state == 8560) {
197 goto switch_1_8560;
198 } else {
199#line 155
200 if (s__state == 8561) {
201 goto switch_1_8561;
202 } else {
203#line 158
204 if (s__state == 8448) {
205 goto switch_1_8448;
206 } else {
207#line 161
208 if (s__state == 8576) {
209 goto switch_1_8576;
210 } else {
211#line 164
212 if (s__state == 8577) {
213 goto switch_1_8577;
214 } else {
215#line 167
216 if (s__state == 8592) {
217 goto switch_1_8592;
218 } else {
219#line 170
220 if (s__state == 8593) {
221 goto switch_1_8593;
222 } else {
223#line 173
224 if (s__state == 8608) {
225 goto switch_1_8608;
226 } else {
227#line 176
228 if (s__state == 8609) {
229 goto switch_1_8609;
230 } else {
231#line 179
232 if (s__state == 8640) {
233 goto switch_1_8640;
234 } else {
235#line 182
236 if (s__state == 8641) {
237 goto switch_1_8641;
238 } else {
239#line 185
240 if (s__state == 8656) {
241 goto switch_1_8656;
242 } else {
243#line 188
244 if (s__state == 8657) {
245 goto switch_1_8657;
246 } else {
247#line 191
248 if (s__state == 8672) {
249 goto switch_1_8672;
250 } else {
251#line 194
252 if (s__state == 8673) {
253 goto switch_1_8673;
254 } else {
255#line 197
256 if (s__state == 3) {
257 goto switch_1_3;
258 } else {
259 goto switch_1_default;
260#line 202
261 if (0) {
262 switch_1_12292:
263#line 204
264 s__new_session = 1;
265 switch_1_16384: ;
266 switch_1_8192: ;
267 switch_1_24576: ;
268 switch_1_8195:
269#line 209
270 s__server = 1;
271#line 210
272 if (cb != 0) {
273
274 }
275 {
276#line 215
277 __cil_tmp55 = s__version * 8;
278#line 215
279 if (__cil_tmp55 != 3) {
280#line 216
281 return (-1);
282 }
283 }
284#line 220
285 s__type = 8192;
286#line 221
287 if (s__init_buf___0 == 0) {
288#line 222
289 tmp___3 = __VERIFIER_nondet_int();
290#line 223
291 if (! tmp___3) {
292#line 224
293 ret = -1;
294 goto end;
295 }
296#line 229
297 s__init_buf___0 = buf;
298 }
299#line 233
300 tmp___4 = __VERIFIER_nondet_int();
301#line 234
302 if (! tmp___4) {
303#line 235
304 ret = -1;
305 goto end;
306 }
307#line 240
308 s__init_num = 0;
309#line 241
310 if (s__state != 12292) {
311#line 242
312 tmp___5 = __VERIFIER_nondet_int();
313#line 243
314 if (! tmp___5) {
315#line 244
316 ret = -1;
317 goto end;
318 }
319#line 249
320 s__state = 8464;
321#line 250
322 s__ctx__stats__sess_accept ++;
323 } else {
324#line 252
325 s__ctx__stats__sess_accept_renegotiate ++;
326#line 253
327 s__state = 8480;
328 }
329 goto switch_1_break;
330 switch_1_8480: ;
331 switch_1_8481:
332#line 258
333 s__shutdown = 0;
334#line 259
335 ret = __VERIFIER_nondet_int();
336#line 260
337 if (ret <= 0) {
338 goto end;
339 }
340#line 265
341 s__s3__tmp__next_state___0 = 8482;
342#line 266
343 s__state = 8448;
344#line 267
345 s__init_num = 0;
346 goto switch_1_break;
347 switch_1_8482:
348#line 270
349 s__state = 3;
350 goto switch_1_break;
351 switch_1_8464: ;
352 switch_1_8465: ;
353 switch_1_8466:
354#line 275
355 s__shutdown = 0;
356#line 276
357 ret = __VERIFIER_nondet_int();
358#line 277
359 if (blastFlag == 0) {
360#line 278
361 blastFlag = 1;
362 }
363#line 282
364 if (ret <= 0) {
365 goto end;
366 }
367#line 287
368 got_new_session = 1;
369#line 288
370 s__state = 8496;
371#line 289
372 s__init_num = 0;
373 goto switch_1_break;
374 switch_1_8496: ;
375 switch_1_8497:
376#line 293
377 ret = __VERIFIER_nondet_int();
378#line 294
379 if (blastFlag == 1) {
380#line 295
381 blastFlag = 2;
382 }
383#line 299
384 if (ret <= 0) {
385 goto end;
386 }
387#line 304
388 if (s__hit) {
389#line 305
390 s__state = 8656;
391 } else {
392#line 307
393 s__state = 8512;
394 }
395#line 309
396 s__init_num = 0;
397 goto switch_1_break;
398 switch_1_8512: ;
399 switch_1_8513: ;
400 {
401#line 313
402 __cil_tmp56 = (unsigned long )s__s3__tmp__new_cipher__algorithms;
403#line 313
404 if (__cil_tmp56 + 256UL) {
405#line 314
406 skip = 1;
407 } else {
408#line 316
409 ret = __VERIFIER_nondet_int();
410#line 317
411 if (ret <= 0) {
412 goto end;
413 }
414 }
415 }
416#line 323
417 s__state = 8528;
418#line 324
419 s__init_num = 0;
420 goto switch_1_break;
421 switch_1_8528: ;
422 switch_1_8529:
423#line 328
424 l = (unsigned long )s__s3__tmp__new_cipher__algorithms;
425 {
426#line 329
427 __cil_tmp57 = (unsigned long )s__options;
428#line 329
429 if (__cil_tmp57 + 2097152UL) {
430#line 330
431 s__s3__tmp__use_rsa_tmp = 1;
432 } else {
433#line 332
434 s__s3__tmp__use_rsa_tmp = 0;
435 }
436 }
437#line 334
438 if (s__s3__tmp__use_rsa_tmp) {
439 goto _L___0;
440 } else {
441#line 337
442 if (l + 30UL) {
443 goto _L___0;
444 } else {
445#line 340
446 if (l + 1UL) {
447#line 341
448 if (s__cert__pkeys__AT0__privatekey == 0) {
449 goto _L___0;
450 } else {
451 {
452#line 344
453 __cil_tmp58 = (unsigned long )s__s3__tmp__new_cipher__algo_strength;
454#line 344
455 if (__cil_tmp58 + 2UL) {
456#line 345
457 tmp___6 = __VERIFIER_nondet_int();
458 {
459#line 346
460 __cil_tmp59 = (unsigned long )s__s3__tmp__new_cipher__algo_strength;
461#line 346
462 if (__cil_tmp59 + 4UL) {
463#line 347
464 tmp___7 = 512;
465 } else {
466#line 349
467 tmp___7 = 1024;
468 }
469 }
470 {
471#line 351
472 __cil_tmp60 = tmp___6 * 8;
473#line 351
474 if (__cil_tmp60 > tmp___7) {
475 _L___0:
476#line 353
477 ret = __VERIFIER_nondet_int();
478#line 354
479 if (ret <= 0) {
480 goto end;
481 }
482 } else {
483#line 360
484 skip = 1;
485 }
486 }
487 } else {
488#line 363
489 skip = 1;
490 }
491 }
492 }
493 } else {
494#line 367
495 skip = 1;
496 }
497 }
498 }
499#line 371
500 s__state = 8544;
501#line 372
502 s__init_num = 0;
503 goto switch_1_break;
504 switch_1_8544: ;
505 switch_1_8545: ;
506#line 376
507 if (s__verify_mode + 1) {
508#line 377
509 if (s__session__peer != 0) {
510#line 378
511 if (s__verify_mode + 4) {
512#line 379
513 skip = 1;
514#line 380
515 s__s3__tmp__cert_request = 0;
516#line 381
517 s__state = 8560;
518 } else {
519 goto _L___2;
520 }
521 } else {
522 _L___2:
523 {
524#line 387
525 __cil_tmp61 = (unsigned long )s__s3__tmp__new_cipher__algorithms;
526#line 387
527 if (__cil_tmp61 + 256UL) {
528#line 388
529 if (s__verify_mode + 2) {
530 goto _L___1;
531 } else {
532#line 391
533 skip = 1;
534#line 392
535 s__s3__tmp__cert_request = 0;
536#line 393
537 s__state = 8560;
538 }
539 } else {
540 _L___1:
541#line 397
542 s__s3__tmp__cert_request = 1;
543#line 398
544 ret = __VERIFIER_nondet_int();
545#line 399
546 if (ret <= 0) {
547 goto end;
548 }
549#line 404
550 s__state = 8448;
551#line 405
552 s__s3__tmp__next_state___0 = 8576;
553#line 406
554 s__init_num = 0;
555 }
556 }
557 }
558 } else {
559#line 410
560 skip = 1;
561#line 411
562 s__s3__tmp__cert_request = 0;
563#line 412
564 s__state = 8560;
565 }
566 goto switch_1_break;
567 switch_1_8560: ;
568 switch_1_8561:
569#line 417
570 ret = __VERIFIER_nondet_int();
571#line 418
572 if (ret <= 0) {
573 goto end;
574 }
575#line 423
576 s__s3__tmp__next_state___0 = 8576;
577#line 424
578 s__state = 8448;
579#line 425
580 s__init_num = 0;
581 goto switch_1_break;
582 switch_1_8448:
583#line 428
584
585 num1 = __VERIFIER_nondet_int();
586#line 429
587 if (num1 > 0L) {
588#line 430
589 s__rwstate = 2;
590#line 431
591 num1 = tmp___8;
592#line 432
593 if (num1 <= 0L) {
594#line 433
595 ret = -1;
596 goto end;
597 }
598#line 438
599 s__rwstate = 1;
600 }
601#line 442
602 s__state = s__s3__tmp__next_state___0;
603 goto switch_1_break;
604 switch_1_8576: ;
605 switch_1_8577:
606#line 446
607 ret = __VERIFIER_nondet_int();
608#line 447
609 if (ret <= 0) {
610 goto end;
611 }
612#line 452
613 if (ret == 2) {
614#line 453
615 s__state = 8466;
616 } else {
617#line 455
618 ret = __VERIFIER_nondet_int();
619#line 456
620 if (ret <= 0) {
621 goto end;
622 }
623#line 461
624 s__init_num = 0;
625#line 462
626 s__state = 8592;
627 }
628 goto switch_1_break;
629 switch_1_8592: ;
630 switch_1_8593:
631#line 467
632 ret = __VERIFIER_nondet_int();
633#line 468
634 if (ret <= 0) {
635 goto end;
636 }
637#line 473
638 s__state = 8608;
639#line 474
640 s__init_num = 0;
641 goto switch_1_break;
642 switch_1_8608: ;
643 switch_1_8609:
644#line 478
645 ret = __VERIFIER_nondet_int();
646#line 479
647 if (ret <= 0) {
648 goto end;
649 }
650#line 484
651 s__state = 8640;
652#line 485
653 s__init_num = 0;
654 goto switch_1_break;
655 switch_1_8640: ;
656 switch_1_8641:
657#line 489
658 ret = __VERIFIER_nondet_int();
659#line 490
660 if (blastFlag == 3) {
661#line 491
662 blastFlag = 4;
663 }
664#line 495
665 if (ret <= 0) {
666 goto end;
667 }
668#line 500
669 if (s__hit) {
670#line 501
671 s__state = 3;
672 } else {
673#line 503
674 s__state = 8656;
675 }
676#line 505
677 s__init_num = 0;
678 goto switch_1_break;
679 switch_1_8656: ;
680 switch_1_8657:
681#line 509
682 s__session__cipher = s__s3__tmp__new_cipher;
683#line 510
684 tmp___9 = __VERIFIER_nondet_int();
685#line 511
686 if (! tmp___9) {
687#line 512
688 ret = -1;
689 goto end;
690 }
691#line 517
692 ret = __VERIFIER_nondet_int();
693#line 518
694 if (blastFlag == 2) {
695#line 519
696 blastFlag = 3;
697 }
698#line 523
699 if (ret <= 0) {
700 goto end;
701 }
702#line 528
703 s__state = 8672;
704#line 529
705 s__init_num = 0;
706#line 530
707 tmp___10 = __VERIFIER_nondet_int();
708#line 531
709 if (! tmp___10) {
710#line 532
711 ret = -1;
712 goto end;
713 }
714 goto switch_1_break;
715 switch_1_8672: ;
716 switch_1_8673:
717#line 540
718 ret = __VERIFIER_nondet_int();
719#line 541
720 if (blastFlag == 4) {
721#line 542
722 blastFlag = 5;
723 } else {
724#line 544
725 if (blastFlag == 5) {
726 goto ERROR;
727 }
728 }
729#line 550
730 if (ret <= 0) {
731 goto end;
732 }
733#line 555
734 s__state = 8448;
735#line 556
736 if (s__hit) {
737#line 557
738 s__s3__tmp__next_state___0 = 8640;
739 } else {
740#line 559
741 s__s3__tmp__next_state___0 = 3;
742 }
743#line 561
744 s__init_num = 0;
745 goto switch_1_break;
746 switch_1_3:
747#line 564
748 s__init_buf___0 = 0;
749#line 565
750 s__init_num = 0;
751#line 566
752 if (got_new_session) {
753#line 567
754 s__new_session = 0;
755#line 568
756 s__ctx__stats__sess_accept_good ++;
757#line 569
758 if (cb != 0) {
759
760 }
761 }
762#line 577
763 ret = 1;
764 goto end;
765 switch_1_default:
766#line 580
767 ret = -1;
768 goto end;
769 } else {
770 switch_1_break: ;
771 }
772 }
773 }
774 }
775 }
776 }
777 }
778 }
779 }
780 }
781 }
782 }
783 }
784 }
785 }
786 }
787 }
788 }
789 }
790 }
791 }
792 }
793 }
794 }
795 }
796 }
797 }
798 }
799 }
800 }
801 }
802 }
803 }
804 }
805 }
806 }
807#line 621
808 if (! s__s3__tmp__reuse_message) {
809#line 622
810 if (! skip) {
811 if(state == 8464){
812 if(s__state == 8496){
813 if(cb != 0){
814 if(s__info_callback != 0){
815 goto ERROR;
816 }
817 }
818 }
819 }
820 if (s__debug) {
821#line 624
822 ret = __VERIFIER_nondet_int();
823#line 625
824 if (ret <= 0) {
825 goto end;
826 }
827 }
828#line 633
829 if (cb != 0) {
830#line 634
831 if (s__state != state) {
832#line 635
833 new_state = s__state;
834#line 636
835 s__state = state;
836#line 637
837 s__state = new_state;
838 }
839 }
840 }
841 }
842#line 650
843 skip = 0;
844 }
845 while_0_break: ;
846 }
847
848 end:
849#line 655
850 s__in_handshake --;
851#line 656
852 if (cb != 0) {
853
854 }
855#line 661
856 return (ret);
857 ERROR:
858#line 663
859 return (-1);
860}
861}
862
863#line 666 "s3_srvr_1.cil.c"
864int main(void)
865{ int s ;
866 int tmp ;
867
868 {
869 {
870#line 672
871 s = 8464;
872#line 673
873 tmp = ssl3_accept(s);
874 }
875#line 675
876 return (tmp);
877}
878}