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 ;
27 int s__session__peer = __VERIFIER_nondet_int() ;
28 int s__cert__pkeys__AT0__privatekey ;
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 ;
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 ;
38 int s__s3__tmp__next_state___0 ;
39 int s__s3__tmp__new_cipher__algo_strength ;
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 s__s3__tmp__new_cipher__algorithms = __VERIFIER_nondet_int();
405 __cil_tmp56 = (unsigned long )s__s3__tmp__new_cipher__algorithms;
406#line 318
407 if (__cil_tmp56 + 256UL) {
408 __cil_tmp56 = 256345;
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 s__s3__tmp__new_cipher__algorithms = __VERIFIER_nondet_int();
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 s__cert__pkeys__AT0__privatekey = 100;
461 s__s3__tmp__new_cipher__algo_strength = __VERIFIER_nondet_int();
462 __cil_tmp58 = (unsigned long )s__s3__tmp__new_cipher__algo_strength;
463#line 354
464 if (__cil_tmp58 + 2UL) {
465 {
466 s__s3__tmp__new_cipher__algo_strength = __VERIFIER_nondet_int();
467 __cil_tmp59 = (unsigned long )s__s3__tmp__new_cipher__algo_strength;
468#line 355
469 if (__cil_tmp59 + 4UL) {
470#line 356
471 tmp___7 = 512;
472 } else {
473#line 358
474 tmp___7 = 1024;
475 }
476 }
477 {
478#line 360
479 __cil_tmp60 = tmp___6 * 8;
480#line 360
481 if (__cil_tmp60 > tmp___7) {
482 _L___0:
483#line 362
484 ret = __VERIFIER_nondet_int();
485#line 363
486 if (blastFlag == 3) {
487#line 364
488 blastFlag = 4;
489 }
490#line 368
491 if (ret <= 0) {
492 goto end;
493 }
494 } else {
495#line 374
496 skip = 1;
497 }
498 }
499 } else {
500#line 377
501 skip = 1;
502 }
503 }
504 }
505 } else {
506#line 381
507 skip = 1;
508 }
509 }
510 }
511#line 385
512 s__state = 8544;
513#line 386
514 s__init_num = 0;
515 goto switch_1_break;
516 switch_1_8544: ;
517 switch_1_8545: ;
518#line 390
519 if (s__verify_mode + 1) {
520#line 391
521 if (s__session__peer != 0) {
522#line 392
523 if (s__verify_mode + 4) {
524 s__verify_mode = 123;
525 skip = 1;
526#line 394
527 s__s3__tmp__cert_request = 0;
528#line 395
529 s__state = 8560;
530 } else {
531 goto _L___2;
532 }
533 } else {
534 _L___2:
535 {
536#line 401
537
538#line 401
539 if (__cil_tmp61 + 256UL) {
540 __cil_tmp61 = 9021;
541 if (s__verify_mode + 2) {
542 s__verify_mode = 124;
543 goto _L___1;
544 } else {
545#line 405
546 skip = 1;
547#line 406
548 s__s3__tmp__cert_request = 0;
549#line 407
550 s__state = 8560;
551 }
552 } else {
553 _L___1:
554#line 411
555 s__s3__tmp__cert_request = 1;
556#line 412
557 ret = __VERIFIER_nondet_int();
558#line 413
559 if (blastFlag == 4) {
560#line 414
561 blastFlag = 5;
562 }
563#line 418
564 if (ret <= 0) {
565 goto end;
566 }
567#line 423
568 s__state = 8448;
569#line 424
570 s__s3__tmp__next_state___0 = 8576;
571#line 425
572 s__init_num = 0;
573 }
574 }
575 }
576 } else {
577#line 429
578 skip = 1;
579#line 430
580 s__s3__tmp__cert_request = 0;
581#line 431
582 s__state = 8560;
583 }
584 goto switch_1_break;
585 switch_1_8560: ;
586 switch_1_8561:
587#line 436
588 ret = __VERIFIER_nondet_int();
589#line 437
590 if (ret <= 0) {
591 goto end;
592 }
593#line 442
594 s__s3__tmp__next_state___0 = 8576;
595#line 443
596 s__state = 8448;
597#line 444
598 s__init_num = 0;
599 goto switch_1_break;
600 switch_1_8448:
601#line 447
602 if (num1 > 0L) {
603#line 448
604 s__rwstate = 2;
605#line 449
606 num1 = tmp___8;
607#line 450
608 if (num1 <= 0L) {
609#line 451
610 ret = -1;
611 goto end;
612 }
613#line 456
614 s__rwstate = 1;
615 }
616#line 460
617 s__state = s__s3__tmp__next_state___0;
618 goto switch_1_break;
619 switch_1_8576: ;
620 switch_1_8577:
621#line 464
622 ret = __VERIFIER_nondet_int();
623#line 465
624 if (blastFlag == 5) {
625#line 466
626 blastFlag = 6;
627 }
628#line 470
629 if (ret <= 0) {
630 goto end;
631 }
632#line 475
633 if (ret == 2) {
634#line 476
635 s__state = 8466;
636 } else {
637#line 478
638 ret = __VERIFIER_nondet_int();
639#line 479
640 if (blastFlag == 6) {
641#line 480
642 blastFlag = 7;
643 }
644#line 484
645 if (ret <= 0) {
646 goto end;
647 }
648#line 489
649 s__init_num = 0;
650#line 490
651 s__state = 8592;
652 }
653 goto switch_1_break;
654 switch_1_8592: ;
655 switch_1_8593:
656#line 495
657 ret = __VERIFIER_nondet_int();
658#line 496
659 if (blastFlag == 7) {
660#line 497
661 blastFlag = 8;
662 }
663#line 501
664 if (ret <= 0) {
665 goto end;
666 }
667#line 506
668 s__state = 8608;
669#line 507
670 s__init_num = 0;
671 goto switch_1_break;
672 switch_1_8608: ;
673 switch_1_8609:
674#line 511
675 ret = __VERIFIER_nondet_int();
676#line 512
677 if (blastFlag == 8) {
678#line 513
679 blastFlag = 9;
680 }
681#line 517
682 if (ret <= 0) {
683 goto end;
684 }
685#line 522
686 s__state = 8640;
687#line 523
688 s__init_num = 0;
689 goto switch_1_break;
690 switch_1_8640: ;
691 switch_1_8641:
692#line 527
693 ret = __VERIFIER_nondet_int();
694#line 528
695 if (blastFlag == 9) {
696#line 529
697 blastFlag = 10;
698 } else {
699#line 531
700 if (blastFlag == 12) {
701#line 532
702 blastFlag = 13;
703 } else {
704#line 534
705 if (blastFlag == 15) {
706#line 535
707 blastFlag = 16;
708 } else {
709#line 537
710 if (blastFlag == 18) {
711#line 538
712 blastFlag = 19;
713 } else {
714#line 540
715 if (blastFlag == 21) {
716 goto ERROR;
717 }
718 }
719 }
720 }
721 }
722#line 549
723 if (ret <= 0) {
724 goto end;
725 }
726#line 554
727 if (s__hit) {
728#line 555
729 s__state = 3;
730 } else {
731#line 557
732 s__state = 8656;
733 }
734#line 559
735 s__init_num = 0;
736 goto switch_1_break;
737 switch_1_8656: ;
738 switch_1_8657:
739#line 563
740 s__session__cipher = s__s3__tmp__new_cipher;
741#line 564
742 if (! tmp___9) {
743#line 565
744 ret = -1;
745 goto end;
746 }
747#line 570
748 ret = __VERIFIER_nondet_int();
749#line 571
750 if (blastFlag == 10) {
751#line 572
752 blastFlag = 11;
753 } else {
754#line 574
755 if (blastFlag == 13) {
756#line 575
757 blastFlag = 14;
758 } else {
759#line 577
760 if (blastFlag == 16) {
761#line 578
762 blastFlag = 17;
763 } else {
764#line 580
765 if (blastFlag == 19) {
766#line 581
767 blastFlag = 20;
768 }
769 }
770 }
771 }
772#line 588
773 if (ret <= 0) {
774 goto end;
775 }
776#line 593
777 s__state = 8672;
778#line 594
779 s__init_num = 0;
780#line 595
781 if (! tmp___10) {
782#line 596
783 ret = -1;
784 goto end;
785 }
786 goto switch_1_break;
787 switch_1_8672: ;
788 switch_1_8673:
789#line 604
790 ret = __VERIFIER_nondet_int();
791#line 605
792 if (blastFlag == 11) {
793#line 606
794 blastFlag = 12;
795 } else {
796#line 608
797 if (blastFlag == 14) {
798#line 609
799 blastFlag = 15;
800 } else {
801#line 611
802 if (blastFlag == 17) {
803#line 612
804 blastFlag = 18;
805 } else {
806#line 614
807 if (blastFlag == 20) {
808#line 615
809 blastFlag = 21;
810 }
811 }
812 }
813 }
814#line 622
815 if (ret <= 0) {
816 goto end;
817 }
818#line 627
819 s__state = 8448;
820#line 628
821 if (s__hit) {
822#line 629
823 s__s3__tmp__next_state___0 = 8640;
824 } else {
825#line 631
826 s__s3__tmp__next_state___0 = 3;
827 }
828#line 633
829 s__init_num = 0;
830 goto switch_1_break;
831 switch_1_3:
832#line 636
833 s__init_buf___0 = 0;
834#line 637
835 s__init_num = 0;
836#line 638
837 if (got_new_session) {
838#line 639
839 s__new_session = 0;
840#line 640
841 s__ctx__stats__sess_accept_good ++;
842#line 641
843 if (cb != 0) {
844
845 }
846 }
847#line 649
848 ret = 1;
849 goto end;
850 switch_1_default:
851#line 652
852 ret = -1;
853 goto end;
854 } else {
855 switch_1_break: ;
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 }
891 }
892#line 693
893 s__s3__tmp__reuse_message = __VERIFIER_nondet_int();
894 if (! s__s3__tmp__reuse_message) {
895#line 694
896 if (! skip) {
897 if(state == 8560){
898 if(s__state == 8448){
899 if(s__verify_mode != -1){
900 if(s__verify_mode != -2){
901 if(__cil_tmp61 != 9021){
902 if(__cil_tmp58 != 4294967294){
903 if(blastFlag != 4){
904 if(tmp___7 != 1024){
905 goto ERROR;
906 }
907 }
908 }
909 }
910 }
911 }
912 }
913 }
914 if (s__debug) {
915#line 696
916 ret = __VERIFIER_nondet_int();
917#line 697
918 if (ret <= 0) {
919 goto end;
920 }
921 }
922#line 705
923 if (cb != 0) {
924#line 706
925 if (s__state != state) {
926#line 707
927 new_state = s__state;
928#line 708
929 s__state = state;
930#line 709
931 s__state = new_state;
932 }
933 }
934 }
935 }
936#line 722
937 skip = 0;
938 }
939 while_0_break: ;
940 }
941
942 end:
943#line 727
944 s__in_handshake --;
945#line 728
946 if (cb != 0) {
947
948 }
949#line 733
950 return (ret);
951 ERROR:
952#line 735
953 return (-1);
954}
955}
956#line 738 "s3_srvr_6.cil.c"
957int main(void)
958{ int s ;
959 int tmp ;
960
961 {
962 {
963#line 744
964 s = 8464;
965#line 745
966 tmp = ssl3_accept(s);
967 }
968#line 747
969 return (tmp);
970}
971}