1
2
3
4#line 4 "s3_srvr_8.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 s__s3__tmp__reuse_message = 0;
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#line 318
400 __cil_tmp56 = (unsigned long )s__s3__tmp__new_cipher__algorithms;
401#line 318
402 if (__cil_tmp56 + 256UL) {
403#line 319
404 skip = 1;
405 } else {
406#line 321
407 ret = __VERIFIER_nondet_int();
408#line 322
409 if (ret <= 0) {
410 goto end;
411 }
412 }
413 }
414#line 328
415 s__state = 8528;
416#line 329
417 s__init_num = 0;
418 goto switch_1_break;
419 switch_1_8528: ;
420 switch_1_8529:
421#line 333
422 l = (unsigned long )s__s3__tmp__new_cipher__algorithms;
423 {
424#line 334
425 __cil_tmp57 = (unsigned long )s__options;
426#line 334
427 if (__cil_tmp57 + 2097152UL) {
428#line 335
429 s__s3__tmp__use_rsa_tmp = 1;
430 } else {
431#line 337
432 s__s3__tmp__use_rsa_tmp = 0;
433 }
434 }
435#line 339
436 if (s__s3__tmp__use_rsa_tmp) {
437 goto _L___0;
438 } else {
439#line 342
440 if (l + 30UL) {
441 goto _L___0;
442 } else {
443#line 345
444 if (l + 1UL) {
445#line 346
446 if (s__cert__pkeys__AT0__privatekey == 0) {
447 goto _L___0;
448 } else {
449 {
450#line 349
451 __cil_tmp58 = (unsigned long )s__s3__tmp__new_cipher__algo_strength;
452#line 349
453 if (__cil_tmp58 + 2UL) {
454 {
455#line 350
456 __cil_tmp59 = (unsigned long )s__s3__tmp__new_cipher__algo_strength;
457#line 350
458 if (__cil_tmp59 + 4UL) {
459#line 351
460 tmp___7 = 512;
461 } else {
462#line 353
463 tmp___7 = 1024;
464 }
465 }
466 {
467#line 355
468 __cil_tmp60 = tmp___6 * 8;
469#line 355
470 if (__cil_tmp60 > tmp___7) {
471 _L___0:
472#line 357
473 ret = __VERIFIER_nondet_int();
474#line 358
475 if (ret <= 0) {
476 goto end;
477 }
478 } else {
479#line 364
480 skip = 1;
481 }
482 }
483 } else {
484#line 367
485 skip = 1;
486 }
487 }
488 }
489 } else {
490#line 371
491 skip = 1;
492 }
493 }
494 }
495#line 375
496 s__state = 8544;
497#line 376
498 s__init_num = 0;
499 goto switch_1_break;
500 switch_1_8544: ;
501 switch_1_8545: ;
502#line 380
503 if (s__verify_mode + 1) {
504#line 381
505 if (s__session__peer != 0) {
506#line 382
507 if (s__verify_mode + 4) {
508#line 383
509 skip = 1;
510#line 384
511 s__s3__tmp__cert_request = 0;
512#line 385
513 s__state = 8560;
514 } else {
515 goto _L___2;
516 }
517 } else {
518 _L___2:
519 {
520#line 391
521 __cil_tmp61 = (unsigned long )s__s3__tmp__new_cipher__algorithms;
522#line 391
523 if (__cil_tmp61 + 256UL) {
524#line 392
525 if (s__verify_mode + 2) {
526 goto _L___1;
527 } else {
528#line 395
529 skip = 1;
530#line 396
531 s__s3__tmp__cert_request = 0;
532#line 397
533 s__state = 8560;
534 }
535 } else {
536 _L___1:
537#line 401
538 s__s3__tmp__cert_request = 1;
539#line 402
540 ret = __VERIFIER_nondet_int();
541#line 403
542 if (ret <= 0) {
543 goto end;
544 }
545#line 408
546 s__state = 8448;
547#line 409
548 s__s3__tmp__next_state___0 = 8576;
549#line 410
550 s__init_num = 0;
551 }
552 }
553 }
554 } else {
555#line 414
556 skip = 1;
557#line 415
558 s__s3__tmp__cert_request = 0;
559#line 416
560 s__state = 8560;
561 }
562 goto switch_1_break;
563 switch_1_8560: ;
564 switch_1_8561:
565#line 421
566 ret = __VERIFIER_nondet_int();
567#line 422
568 if (ret <= 0) {
569 goto end;
570 }
571#line 427
572 s__s3__tmp__next_state___0 = 8576;
573#line 428
574 s__state = 8448;
575#line 429
576 s__init_num = 0;
577 goto switch_1_break;
578 switch_1_8448:
579#line 432
580 if (num1 > 0L) {
581#line 433
582 s__rwstate = 2;
583#line 434
584 num1 = tmp___8;
585#line 435
586 if (num1 <= 0L) {
587#line 436
588 ret = -1;
589 goto end;
590 }
591#line 441
592 s__rwstate = 1;
593 }
594#line 445
595 s__state = s__s3__tmp__next_state___0;
596 goto switch_1_break;
597 switch_1_8576: ;
598 switch_1_8577:
599#line 449
600 ret = __VERIFIER_nondet_int();
601#line 450
602 if (ret <= 0) {
603 goto end;
604 }
605#line 455
606 if (ret == 2) {
607#line 456
608 s__state = 8466;
609 } else {
610#line 458
611 ret = __VERIFIER_nondet_int();
612#line 459
613 if (ret <= 0) {
614 goto end;
615 }
616#line 464
617 s__init_num = 0;
618#line 465
619 s__state = 8592;
620 }
621 goto switch_1_break;
622 switch_1_8592: ;
623 switch_1_8593:
624#line 470
625 ret = __VERIFIER_nondet_int();
626#line 471
627 if (ret <= 0) {
628 goto end;
629 }
630#line 476
631 s__state = 8608;
632#line 477
633 s__init_num = 0;
634 goto switch_1_break;
635 switch_1_8608: ;
636 switch_1_8609:
637#line 481
638 ret = __VERIFIER_nondet_int();
639#line 482
640 if (ret <= 0) {
641 goto end;
642 }
643#line 487
644 s__state = 8640;
645#line 488
646 s__init_num = 0;
647 goto switch_1_break;
648 switch_1_8640: ;
649 switch_1_8641:
650#line 492
651 ret = __VERIFIER_nondet_int();
652#line 493
653 if (blastFlag == 4) {
654#line 494
655 blastFlag = 5;
656 } else {
657#line 496
658 if (blastFlag == 7) {
659#line 497
660 blastFlag = 8;
661 } else {
662#line 499
663 if (blastFlag == 10) {
664 goto ERROR;
665 }
666 }
667 }
668#line 506
669 if (ret <= 0) {
670 goto end;
671 }
672#line 511
673 if (s__hit) {
674#line 512
675 s__state = 3;
676 } else {
677#line 514
678 s__state = 8656;
679 }
680#line 516
681 s__init_num = 0;
682 goto switch_1_break;
683 switch_1_8656: ;
684 switch_1_8657:
685#line 520
686 s__session__cipher = s__s3__tmp__new_cipher;
687#line 521
688 if (! tmp___9) {
689#line 522
690 ret = -1;
691 goto end;
692 }
693#line 527
694 ret = __VERIFIER_nondet_int();
695#line 528
696 if (blastFlag == 2) {
697#line 529
698 blastFlag = 3;
699 } else {
700#line 531
701 if (blastFlag == 5) {
702#line 532
703 blastFlag = 6;
704 } else {
705#line 534
706 if (blastFlag == 8) {
707#line 535
708 blastFlag = 9;
709 }
710 }
711 }
712#line 541
713 if (ret <= 0) {
714 goto end;
715 }
716#line 546
717 s__state = 8672;
718#line 547
719 s__init_num = 0;
720#line 548
721 if (! tmp___10) {
722#line 549
723 ret = -1;
724 goto end;
725 }
726 goto switch_1_break;
727 switch_1_8672: ;
728 switch_1_8673:
729#line 557
730 ret = __VERIFIER_nondet_int();
731#line 558
732 if (blastFlag == 3) {
733#line 559
734 blastFlag = 4;
735 } else {
736#line 561
737 if (blastFlag == 6) {
738#line 562
739 blastFlag = 7;
740 } else {
741#line 564
742 if (blastFlag == 9) {
743#line 565
744 blastFlag = 10;
745 }
746 }
747 }
748#line 571
749 if (ret <= 0) {
750 goto end;
751 }
752#line 576
753 s__state = 8448;
754#line 577
755 if (s__hit) {
756#line 578
757 s__s3__tmp__next_state___0 = 8640;
758 } else {
759#line 580
760 s__s3__tmp__next_state___0 = 3;
761 }
762#line 582
763 s__init_num = 0;
764 goto switch_1_break;
765 switch_1_3:
766#line 585
767 s__init_buf___0 = 0;
768#line 586
769 s__init_num = 0;
770#line 587
771 if (got_new_session) {
772#line 588
773 s__new_session = 0;
774#line 589
775 s__ctx__stats__sess_accept_good ++;
776#line 590
777 if (cb != 0) {
778
779 }
780 }
781#line 598
782 ret = 1;
783 goto end;
784 switch_1_default:
785#line 601
786 ret = -1;
787 goto end;
788 } else {
789 switch_1_break: ;
790 }
791 }
792 }
793 }
794 }
795 }
796 }
797 }
798 }
799 }
800 }
801 }
802 }
803 }
804 }
805 }
806 }
807 }
808 }
809 }
810 }
811 }
812 }
813 }
814 }
815 }
816 }
817 }
818 }
819 }
820 }
821 }
822 }
823 }
824 }
825 }
826#line 642
827 if (! s__s3__tmp__reuse_message) {
828#line 643
829 if (! skip) {
830 if(tmp___1 != -12288){
831 if(s__state != 8656){
832 if(tmp___2 != -16384){
833 if(state == 8496){
834 goto ERROR;
835 }
836 }
837 }
838 }
839
840 if (s__debug) {
841#line 645
842 ret = __VERIFIER_nondet_int();
843#line 646
844 if (ret <= 0) {
845 goto end;
846 }
847 }
848#line 654
849 if (cb != 0) {
850#line 655
851 if (s__state != state) {
852#line 656
853 new_state = s__state;
854#line 657
855 s__state = state;
856#line 658
857 s__state = new_state;
858 }
859 }
860 }
861 }
862#line 671
863 skip = 0;
864 }
865 while_0_break: ;
866 }
867
868 end:
869#line 676
870 s__in_handshake --;
871#line 677
872 if (cb != 0) {
873
874 }
875#line 682
876 return (ret);
877 ERROR:
878#line 684
879 return (-1);
880}
881}
882#line 687 "s3_srvr_8.cil.c"
883int main(void)
884{ int s ;
885 int tmp ;
886
887 {
888 {
889#line 693
890 s = 8464;
891#line 694
892 tmp = ssl3_accept(s);
893 }
894#line 696
895 return (tmp);
896}
897}