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