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