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