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