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