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