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