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_clnt_3_BUG.cil.c"
10int ssl3_connect(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__bbio = __VERIFIER_nondet_int() ;
20 int s__wbio = __VERIFIER_nondet_int() ;
21 int s__hit = __VERIFIER_nondet_int() ;
22 int s__rwstate ;
23 int s__init_buf___0 ;
24 int s__debug = __VERIFIER_nondet_int() ;
25 int s__shutdown ;
26 int s__ctx__info_callback = __VERIFIER_nondet_int() ;
27 int s__ctx__stats__sess_connect_renegotiate = __VERIFIER_nondet_int() ;
28 int s__ctx__stats__sess_connect = __VERIFIER_nondet_int() ;
29 int s__ctx__stats__sess_hit = __VERIFIER_nondet_int() ;
30 int s__ctx__stats__sess_connect_good = __VERIFIER_nondet_int() ;
31 int s__s3__change_cipher_spec ;
32 int s__s3__flags ;
33 int s__s3__delay_buf_pop_ret ;
34 int s__s3__tmp__cert_req = __VERIFIER_nondet_int() ;
35 int s__s3__tmp__new_compression = __VERIFIER_nondet_int() ;
36 int s__s3__tmp__reuse_message = __VERIFIER_nondet_int() ;
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_compression__id = __VERIFIER_nondet_int() ;
41 int s__session__cipher ;
42 int s__session__compress_meth ;
43 int buf ;
44 unsigned long tmp ;
45 unsigned long l ;
46 int num1 ;
47 int cb ;
48 int ret ;
49 int new_state ;
50 int state ;
51 int skip ;
52 int tmp___0 ;
53 int tmp___1 = __VERIFIER_nondet_int() ;
54 int tmp___2 = __VERIFIER_nondet_int() ;
55 int tmp___3 = __VERIFIER_nondet_int() ;
56 int tmp___4 = __VERIFIER_nondet_int() ;
57 int tmp___5 = __VERIFIER_nondet_int() ;
58 int tmp___6 = __VERIFIER_nondet_int() ;
59 int tmp___7 = __VERIFIER_nondet_int() ;
60 int tmp___8 = __VERIFIER_nondet_int() ;
61 int tmp___9 = __VERIFIER_nondet_int() ;
62 int blastFlag ;
63 int __cil_tmp55 ;
64 void *__cil_tmp56 ;
65 unsigned long __cil_tmp57 ;
66 unsigned long __cil_tmp58 ;
67 void *__cil_tmp59 ;
68 unsigned long __cil_tmp60 ;
69 unsigned long __cil_tmp61 ;
70 unsigned long __cil_tmp62 ;
71 unsigned long __cil_tmp63 ;
72 unsigned long __cil_tmp64 ;
73 long __cil_tmp65 ;
74 long __cil_tmp66 ;
75 long __cil_tmp67 ;
76 long __cil_tmp68 ;
77 long __cil_tmp69 ;
78 long __cil_tmp70 ;
79 long __cil_tmp71 ;
80 long __cil_tmp72 ;
81 long __cil_tmp73 ;
82 long __cil_tmp74 ;
83
84 {
85#line 60
86;
87 s__state = initial_state;
88#line 61
89 blastFlag = 0;
90#line 62
91 tmp = __VERIFIER_nondet_int();
92#line 63
93 cb = 0;
94#line 64
95 ret = -1;
96#line 65
97 skip = 0;
98#line 66
99 tmp___0 = 0;
100#line 67
101 if (s__info_callback != 0) {
102#line 68
103 cb = s__info_callback;
104 } else {
105#line 70
106 if (s__ctx__info_callback != 0) {
107#line 71
108 cb = s__ctx__info_callback;
109 }
110 }
111#line 76
112 s__in_handshake ++;
113#line 77
114 if (tmp___1 + 12288) {
115#line 78
116 if (tmp___2 + 16384) {
117
118 }
119 }
120 {
121#line 87
122 while (1) {
123 while_0_continue: ;
124#line 89
125 state = s__state;
126#line 90
127 if (s__state == 12292) {
128 goto switch_1_12292;
129 } else {
130#line 93
131 if (s__state == 16384) {
132 goto switch_1_16384;
133 } else {
134#line 96
135 if (s__state == 4096) {
136 goto switch_1_4096;
137 } else {
138#line 99
139 if (s__state == 20480) {
140 goto switch_1_20480;
141 } else {
142#line 102
143 if (s__state == 4099) {
144 goto switch_1_4099;
145 } else {
146#line 105
147 if (s__state == 4368) {
148 goto switch_1_4368;
149 } else {
150#line 108
151 if (s__state == 4369) {
152 goto switch_1_4369;
153 } else {
154#line 111
155 if (s__state == 4384) {
156 goto switch_1_4384;
157 } else {
158#line 114
159 if (s__state == 4385) {
160 goto switch_1_4385;
161 } else {
162#line 117
163 if (s__state == 4400) {
164 goto switch_1_4400;
165 } else {
166#line 120
167 if (s__state == 4401) {
168 goto switch_1_4401;
169 } else {
170#line 123
171 if (s__state == 4416) {
172 goto switch_1_4416;
173 } else {
174#line 126
175 if (s__state == 4417) {
176 goto switch_1_4417;
177 } else {
178#line 129
179 if (s__state == 4432) {
180 goto switch_1_4432;
181 } else {
182#line 132
183 if (s__state == 4433) {
184 goto switch_1_4433;
185 } else {
186#line 135
187 if (s__state == 4448) {
188 goto switch_1_4448;
189 } else {
190#line 138
191 if (s__state == 4449) {
192 goto switch_1_4449;
193 } else {
194#line 141
195 if (s__state == 4464) {
196 goto switch_1_4464;
197 } else {
198#line 144
199 if (s__state == 4465) {
200 goto switch_1_4465;
201 } else {
202#line 147
203 if (s__state == 4466) {
204 goto switch_1_4466;
205 } else {
206#line 150
207 if (s__state == 4467) {
208 goto switch_1_4467;
209 } else {
210#line 153
211 if (s__state == 4480) {
212 goto switch_1_4480;
213 } else {
214#line 156
215 if (s__state == 4481) {
216 goto switch_1_4481;
217 } else {
218#line 159
219 if (s__state == 4496) {
220 goto switch_1_4496;
221 } else {
222#line 162
223 if (s__state == 4497) {
224 goto switch_1_4497;
225 } else {
226#line 165
227 if (s__state == 4512) {
228 goto switch_1_4512;
229 } else {
230#line 168
231 if (s__state == 4513) {
232 goto switch_1_4513;
233 } else {
234#line 171
235 if (s__state == 4528) {
236 goto switch_1_4528;
237 } else {
238#line 174
239 if (s__state == 4529) {
240 goto switch_1_4529;
241 } else {
242#line 177
243 if (s__state == 4560) {
244 goto switch_1_4560;
245 } else {
246#line 180
247 if (s__state == 4561) {
248 goto switch_1_4561;
249 } else {
250#line 183
251 if (s__state == 4352) {
252 goto switch_1_4352;
253 } else {
254#line 186
255 if (s__state == 3) {
256 goto switch_1_3;
257 } else {
258 goto switch_1_default;
259#line 191
260 if (0) {
261 switch_1_12292:
262#line 193
263 s__new_session = 1;
264#line 194
265 s__state = 4096;
266#line 195
267 s__ctx__stats__sess_connect_renegotiate ++;
268 switch_1_16384: ;
269 switch_1_4096: ;
270 switch_1_20480: ;
271 switch_1_4099:
272#line 200
273 s__server = 0;
274#line 201
275 if (cb != 0) {
276
277 }
278 {
279#line 206
280 __cil_tmp55 = s__version + 65280;
281#line 206
282 if (__cil_tmp55 != 768) {
283#line 207
284 ret = -1;
285 goto end;
286 }
287 }
288#line 212
289 s__type = 4096;
290 {
291#line 213
292 __cil_tmp56 = (void *)0;
293#line 213
294 __cil_tmp57 = (unsigned long )__cil_tmp56;
295#line 213
296 __cil_tmp58 = (unsigned long )s__init_buf___0;
297#line 213
298 if (__cil_tmp58 == __cil_tmp57) {
299#line 214
300 buf = __VERIFIER_nondet_int();
301 {
302#line 215
303 __cil_tmp59 = (void *)0;
304#line 215
305 __cil_tmp60 = (unsigned long )__cil_tmp59;
306#line 215
307 __cil_tmp61 = (unsigned long )buf;
308#line 215
309 if (__cil_tmp61 == __cil_tmp60) {
310#line 216
311 ret = -1;
312 goto end;
313 }
314 }
315#line 221
316 if (! tmp___3) {
317#line 222
318 ret = -1;
319 goto end;
320 }
321#line 227
322 s__init_buf___0 = buf;
323 }
324 }
325#line 231
326 if (! tmp___4) {
327#line 232
328 ret = -1;
329 goto end;
330 }
331#line 237
332 if (! tmp___5) {
333#line 238
334 ret = -1;
335 goto end;
336 }
337#line 243
338 s__state = 4368;
339#line 244
340 s__ctx__stats__sess_connect ++;
341#line 245
342 s__init_num = 0;
343 goto switch_1_break;
344 switch_1_4368: ;
345 switch_1_4369:
346#line 249
347 s__shutdown = 0;
348#line 250
349 ret = __VERIFIER_nondet_int();
350#line 251
351 if (blastFlag == 0) {
352#line 252
353 blastFlag = 1;
354 }
355#line 256
356 if (ret <= 0) {
357 goto end;
358 }
359#line 261
360 s__state = 4384;
361#line 262
362 s__init_num = 0;
363 {
364#line 263
365 __cil_tmp62 = (unsigned long )s__wbio;
366#line 263
367 __cil_tmp63 = (unsigned long )s__bbio;
368#line 263
369 if (__cil_tmp63 != __cil_tmp62) {
370
371 }
372 }
373 goto switch_1_break;
374 switch_1_4384: ;
375 switch_1_4385:
376#line 271
377 ret = __VERIFIER_nondet_int();
378#line 272
379 if (blastFlag == 1) {
380#line 273
381 blastFlag = 2;
382 } else {
383#line 275
384 if (blastFlag == 4) {
385#line 276
386 blastFlag = 5;
387 }
388 }
389#line 281
390 if (ret <= 0) {
391 goto end;
392 }
393#line 286
394 if (s__hit) {
395#line 287
396 s__state = 4560;
397 } else {
398#line 289
399 s__state = 4400;
400 }
401#line 291
402 s__init_num = 0;
403 goto switch_1_break;
404 switch_1_4400: ;
405 switch_1_4401: ;
406 {
407#line 295
408 __cil_tmp64 = (unsigned long )s__s3__tmp__new_cipher__algorithms;
409#line 295
410 if (__cil_tmp64 + 256UL) {
411#line 296
412 skip = 1;
413 } else {
414#line 298
415 ret = __VERIFIER_nondet_int();
416#line 299
417 if (blastFlag == 2) {
418#line 300
419 blastFlag = 3;
420 }
421#line 304
422 if (ret <= 0) {
423 goto end;
424 }
425 }
426 }
427#line 310
428 s__state = 4416;
429#line 311
430 s__init_num = 0;
431 goto switch_1_break;
432 switch_1_4416: ;
433 switch_1_4417:
434#line 315
435 ret = __VERIFIER_nondet_int();
436#line 316
437 if (blastFlag == 3) {
438#line 317
439 blastFlag = 4;
440 }
441#line 321
442 if (ret <= 0) {
443 goto end;
444 }
445#line 326
446 s__state = 4432;
447#line 327
448 s__init_num = 0;
449#line 328
450 if (! tmp___6) {
451#line 329
452 ret = -1;
453 goto end;
454 }
455 goto switch_1_break;
456 switch_1_4432: ;
457 switch_1_4433:
458#line 337
459 ret = __VERIFIER_nondet_int();
460#line 338
461 if (blastFlag == 4) {
462 goto ERROR;
463 }
464#line 343
465 if (ret <= 0) {
466 goto end;
467 }
468#line 348
469 s__state = 4448;
470#line 349
471 s__init_num = 0;
472 goto switch_1_break;
473 switch_1_4448: ;
474 switch_1_4449:
475#line 353
476 ret = __VERIFIER_nondet_int();
477#line 354
478 if (ret <= 0) {
479 goto end;
480 }
481#line 359
482 if (s__s3__tmp__cert_req) {
483#line 360
484 s__state = 4464;
485 } else {
486#line 362
487 s__state = 4480;
488 }
489#line 364
490 s__init_num = 0;
491 goto switch_1_break;
492 switch_1_4464: ;
493 switch_1_4465: ;
494 switch_1_4466: ;
495 switch_1_4467:
496#line 370
497 ret = __VERIFIER_nondet_int();
498#line 371
499 if (ret <= 0) {
500 goto end;
501 }
502#line 376
503 s__state = 4480;
504#line 377
505 s__init_num = 0;
506 goto switch_1_break;
507 switch_1_4480: ;
508 switch_1_4481:
509#line 381
510 ret = __VERIFIER_nondet_int();
511#line 382
512 if (ret <= 0) {
513 goto end;
514 }
515#line 387
516 l = (unsigned long )s__s3__tmp__new_cipher__algorithms;
517#line 388
518 if (s__s3__tmp__cert_req == 1) {
519#line 389
520 s__state = 4496;
521 } else {
522#line 391
523 s__state = 4512;
524#line 392
525 s__s3__change_cipher_spec = 0;
526 }
527#line 394
528 s__init_num = 0;
529 goto switch_1_break;
530 switch_1_4496: ;
531 switch_1_4497:
532#line 398
533 ret = __VERIFIER_nondet_int();
534#line 399
535 if (ret <= 0) {
536 goto end;
537 }
538#line 404
539 s__state = 4512;
540#line 405
541 s__init_num = 0;
542#line 406
543 s__s3__change_cipher_spec = 0;
544 goto switch_1_break;
545 switch_1_4512: ;
546 switch_1_4513:
547#line 410
548 ret = __VERIFIER_nondet_int();
549#line 411
550 if (ret <= 0) {
551 goto end;
552 }
553#line 416
554 s__state = 4528;
555#line 417
556 s__init_num = 0;
557#line 418
558 s__session__cipher = s__s3__tmp__new_cipher;
559#line 419
560 if (s__s3__tmp__new_compression == 0) {
561#line 420
562 s__session__compress_meth = 0;
563 } else {
564#line 422
565 s__session__compress_meth = s__s3__tmp__new_compression__id;
566 }
567#line 424
568 if (! tmp___7) {
569#line 425
570 ret = -1;
571 goto end;
572 }
573#line 430
574 if (! tmp___8) {
575#line 431
576 ret = -1;
577 goto end;
578 }
579 goto switch_1_break;
580 switch_1_4528: ;
581 switch_1_4529:
582#line 439
583 ret = __VERIFIER_nondet_int();
584#line 440
585 if (ret <= 0) {
586 goto end;
587 }
588#line 445
589 s__state = 4352;
590#line 446
591 __cil_tmp65 = (long )s__s3__flags;
592#line 446
593 __cil_tmp66 = __cil_tmp65 - 5;
594#line 446
595 s__s3__flags = (int )__cil_tmp66;
596#line 447
597 if (s__hit) {
598#line 448
599 s__s3__tmp__next_state___0 = 3;
600 {
601#line 449
602 __cil_tmp67 = (long )s__s3__flags;
603#line 449
604 if (__cil_tmp67 + 2L) {
605#line 450
606 s__state = 3;
607#line 451
608 __cil_tmp68 = (long )s__s3__flags;
609#line 451
610 __cil_tmp69 = __cil_tmp68 * 4L;
611#line 451
612 s__s3__flags = (int )__cil_tmp69;
613#line 452
614 s__s3__delay_buf_pop_ret = 0;
615 }
616 }
617 } else {
618#line 457
619 s__s3__tmp__next_state___0 = 4560;
620 }
621#line 459
622 s__init_num = 0;
623 goto switch_1_break;
624 switch_1_4560: ;
625 switch_1_4561:
626#line 463
627 ret = __VERIFIER_nondet_int();
628#line 464
629 if (ret <= 0) {
630 goto end;
631 }
632#line 469
633 if (s__hit) {
634#line 470
635 s__state = 4512;
636 } else {
637#line 472
638 s__state = 3;
639 }
640#line 474
641 s__init_num = 0;
642 goto switch_1_break;
643 switch_1_4352:
644 {
645#line 477
646 __cil_tmp70 = (long )num1;
647#line 477
648 if (__cil_tmp70 > 0L) {
649#line 478
650 s__rwstate = 2;
651#line 479
652 __cil_tmp71 = (long )tmp___9;
653#line 479
654 num1 = (int )__cil_tmp71;
655 {
656#line 480
657 __cil_tmp72 = (long )num1;
658#line 480
659 if (__cil_tmp72 <= 0L) {
660#line 481
661 ret = -1;
662 goto end;
663 }
664 }
665#line 486
666 s__rwstate = 1;
667 }
668 }
669#line 490
670 s__state = s__s3__tmp__next_state___0;
671 goto switch_1_break;
672 switch_1_3:
673#line 493
674 if (s__init_buf___0 != 0) {
675#line 494
676 s__init_buf___0 = 0;
677 }
678 {
679#line 498
680 __cil_tmp73 = (long )s__s3__flags;
681#line 498
682 __cil_tmp74 = __cil_tmp73 + 4L;
683#line 498
684 if (! __cil_tmp74) {
685
686 }
687 }
688#line 503
689 s__init_num = 0;
690#line 504
691 s__new_session = 0;
692#line 505
693 if (s__hit) {
694#line 506
695 s__ctx__stats__sess_hit ++;
696 }
697#line 510
698 ret = 1;
699#line 511
700 s__ctx__stats__sess_connect_good ++;
701#line 512
702 if (cb != 0) {
703
704 }
705 goto end;
706 switch_1_default:
707#line 519
708 ret = -1;
709 goto end;
710 } else {
711 switch_1_break: ;
712 }
713 }
714 }
715 }
716 }
717 }
718 }
719 }
720 }
721 }
722 }
723 }
724 }
725 }
726 }
727 }
728 }
729 }
730 }
731 }
732 }
733 }
734 }
735 }
736 }
737 }
738 }
739 }
740 }
741 }
742 }
743 }
744 }
745 }
746#line 558
747 if (! s__s3__tmp__reuse_message) {
748#line 559
749 if (! skip) {
750#line 560
751 if (s__debug) {
752#line 561
753 ret = __VERIFIER_nondet_int();
754#line 562
755 if (ret <= 0) {
756 goto end;
757 }
758 }
759#line 570
760 if (cb != 0) {
761#line 571
762 if (s__state != state) {
763#line 572
764 new_state = s__state;
765#line 573
766 s__state = state;
767#line 574
768 s__state = new_state;
769 }
770 }
771 }
772 }
773#line 587
774 skip = 0;
775 }
776 while_0_break: ;
777 }
778
779 end:
780#line 592
781 s__in_handshake --;
782#line 593
783 if (cb != 0) {
784
785 }
786#line 598
787 return (ret);
788 ERROR:
789#line 600
790 return (-1);
791}
792}
793#line 603 "s3_clnt_3_BUG.cil.c"
794int main(void)
795{ int s ;
796
797 {
798 {
799#line 608
800 s = 12292;
801#line 609
802 ssl3_connect(s);
803 }
804#line 611
805 return (0);
806}
807}