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_7.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 = 6;
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 == 6) {
486#line 364
487 blastFlag = 7;
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 == 8) {
558 goto ERROR;
559 }
560#line 418
561 if (ret <= 0) {
562 goto end;
563 }
564#line 423
565 s__state = 8448;
566#line 424
567 s__s3__tmp__next_state___0 = 8576;
568#line 425
569 s__init_num = 0;
570 }
571 }
572 }
573 } else {
574#line 429
575 skip = 1;
576#line 430
577 s__s3__tmp__cert_request = 0;
578#line 431
579 s__state = 8560;
580 }
581 goto switch_1_break;
582 switch_1_8560: ;
583 switch_1_8561:
584#line 436
585 ret = __VERIFIER_nondet_int();
586#line 437
587 if (ret <= 0) {
588 goto end;
589 }
590#line 442
591 s__s3__tmp__next_state___0 = 8576;
592#line 443
593 s__state = 8448;
594#line 444
595 s__init_num = 0;
596 goto switch_1_break;
597 switch_1_8448:
598#line 447
599 if (num1 > 0L) {
600#line 448
601 s__rwstate = 2;
602#line 449
603 num1 = tmp___8;
604#line 450
605 if (num1 <= 0L) {
606#line 451
607 ret = -1;
608 goto end;
609 }
610#line 456
611 s__rwstate = 1;
612 }
613#line 460
614 s__state = s__s3__tmp__next_state___0;
615 goto switch_1_break;
616 switch_1_8576: ;
617 switch_1_8577:
618#line 464
619 ret = __VERIFIER_nondet_int();
620#line 465
621 if (ret <= 0) {
622 goto end;
623 }
624#line 470
625 if (ret == 2) {
626#line 471
627 s__state = 8466;
628 } else {
629#line 473
630 ret = __VERIFIER_nondet_int();
631#line 474
632 if (ret <= 0) {
633 goto end;
634 }
635#line 479
636 s__init_num = 0;
637#line 480
638 s__state = 8592;
639 }
640 goto switch_1_break;
641 switch_1_8592: ;
642 switch_1_8593:
643#line 485
644 ret = __VERIFIER_nondet_int();
645#line 486
646 if (ret <= 0) {
647 goto end;
648 }
649#line 491
650 s__state = 8608;
651#line 492
652 s__init_num = 0;
653 goto switch_1_break;
654 switch_1_8608: ;
655 switch_1_8609:
656#line 496
657 ret = __VERIFIER_nondet_int();
658#line 497
659 if (ret <= 0) {
660 goto end;
661 }
662#line 502
663 s__state = 8640;
664#line 503
665 s__init_num = 0;
666 goto switch_1_break;
667 switch_1_8640: ;
668 switch_1_8641:
669#line 507
670 ret = __VERIFIER_nondet_int();
671#line 508
672 if (blastFlag == 5) {
673 goto ERROR;
674 }
675#line 513
676 if (ret <= 0) {
677 goto end;
678 }
679#line 518
680 if (s__hit) {
681#line 519
682 s__state = 3;
683 } else {
684#line 521
685 s__state = 8656;
686 }
687#line 523
688 s__init_num = 0;
689 goto switch_1_break;
690 switch_1_8656: ;
691 switch_1_8657:
692#line 527
693 s__session__cipher = s__s3__tmp__new_cipher;
694#line 528
695 if (! tmp___9) {
696#line 529
697 ret = -1;
698 goto end;
699 }
700#line 534
701 ret = __VERIFIER_nondet_int();
702#line 535
703 if (blastFlag == 2) {
704#line 536
705 blastFlag = 3;
706 } else {
707#line 538
708 if (blastFlag == 4) {
709#line 539
710 blastFlag = 5;
711 } else {
712#line 541
713 if (blastFlag == 7) {
714#line 542
715 blastFlag = 8;
716 }
717 }
718 }
719#line 548
720 if (ret <= 0) {
721 goto end;
722 }
723#line 553
724 s__state = 8672;
725#line 554
726 s__init_num = 0;
727#line 555
728 if (! tmp___10) {
729#line 556
730 ret = -1;
731 goto end;
732 }
733 goto switch_1_break;
734 switch_1_8672: ;
735 switch_1_8673:
736#line 564
737 ret = __VERIFIER_nondet_int();
738#line 565
739 if (blastFlag == 3) {
740#line 566
741 blastFlag = 4;
742 }
743#line 570
744 if (ret <= 0) {
745 goto end;
746 }
747#line 575
748 s__state = 8448;
749#line 576
750 if (s__hit) {
751#line 577
752 s__s3__tmp__next_state___0 = 8640;
753 } else {
754#line 579
755 s__s3__tmp__next_state___0 = 3;
756 }
757#line 581
758 s__init_num = 0;
759 goto switch_1_break;
760 switch_1_3:
761#line 584
762 s__init_buf___0 = 0;
763#line 585
764 s__init_num = 0;
765#line 586
766 if (got_new_session) {
767#line 587
768 s__new_session = 0;
769#line 588
770 s__ctx__stats__sess_accept_good ++;
771#line 589
772 if (cb != 0) {
773
774 }
775 }
776#line 597
777 ret = 1;
778 goto end;
779 switch_1_default:
780#line 600
781 ret = -1;
782 goto end;
783 } else {
784 switch_1_break: ;
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 }
815 }
816 }
817 }
818 }
819 }
820 }
821#line 641
822 if (! s__s3__tmp__reuse_message) {
823#line 642
824 if (! skip) {
825#line 643
826 if (s__debug) {
827#line 644
828 ret = __VERIFIER_nondet_int();
829#line 645
830 if (ret <= 0) {
831 goto end;
832 }
833 }
834#line 653
835 if (cb != 0) {
836#line 654
837 if (s__state != state) {
838#line 655
839 new_state = s__state;
840#line 656
841 s__state = state;
842#line 657
843 s__state = new_state;
844 }
845 }
846 }
847 }
848#line 670
849 skip = 0;
850 }
851 while_0_break: ;
852 }
853
854 end:
855#line 675
856 s__in_handshake --;
857#line 676
858 if (cb != 0) {
859
860 }
861#line 681
862 return (ret);
863 ERROR:
864#line 683
865 return (-1);
866}
867}
868#line 686 "s3_srvr_7.cil.c"
869int main(void)
870{ int s ;
871 int tmp ;
872
873 {
874 {
875#line 692
876 s = 8464;
877#line 693
878 tmp = ssl3_accept(s);
879 }
880#line 695
881 return (tmp);
882}
883}