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