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