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