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