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