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