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