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