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