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