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