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