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