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