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