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