1
2
3
4int __VERIFIER_nondet_int() { int x; return x; }
5
6typedef unsigned int size_t;
7typedef long __time_t;
8struct buf_mem_st {
9 int length ;
10 char *data ;
11 int max ;
12};
13typedef struct buf_mem_st BUF_MEM;
14typedef __time_t time_t;
15struct stack_st {
16 int num ;
17 char **data ;
18 int sorted ;
19 int num_alloc ;
20 int (*comp)(char const * const * , char const * const * ) ;
21};
22typedef struct stack_st STACK;
23struct bio_st;
24struct bio_st;
25struct crypto_ex_data_st {
26 STACK *sk ;
27 int dummy ;
28};
29typedef struct crypto_ex_data_st CRYPTO_EX_DATA;
30typedef struct bio_st BIO;
31typedef void bio_info_cb(struct bio_st * , int , char const * , int , long ,
32 long );
33struct bio_method_st {
34 int type ;
35 char const *name ;
36 int (*bwrite)(BIO * , char const * , int ) ;
37 int (*bread)(BIO * , char * , int ) ;
38 int (*bputs)(BIO * , char const * ) ;
39 int (*bgets)(BIO * , char * , int ) ;
40 long (*ctrl)(BIO * , int , long , void * ) ;
41 int (*create)(BIO * ) ;
42 int (*destroy)(BIO * ) ;
43 long (*callback_ctrl)(BIO * , int , bio_info_cb * ) ;
44};
45typedef struct bio_method_st BIO_METHOD;
46struct bio_st {
47 BIO_METHOD *method ;
48 long (*callback)(struct bio_st * , int , char const * , int , long , long ) ;
49 char *cb_arg ;
50 int init ;
51 int shutdown ;
52 int flags ;
53 int retry_reason ;
54 int num ;
55 void *ptr ;
56 struct bio_st *next_bio ;
57 struct bio_st *prev_bio ;
58 int references ;
59 unsigned long num_read ;
60 unsigned long num_write ;
61 CRYPTO_EX_DATA ex_data ;
62};
63struct bignum_st {
64 unsigned long *d ;
65 int top ;
66 int dmax ;
67 int neg ;
68 int flags ;
69};
70typedef struct bignum_st BIGNUM;
71struct bignum_ctx {
72 int tos ;
73 BIGNUM bn[16] ;
74 int flags ;
75 int depth ;
76 int pos[12] ;
77 int too_many ;
78};
79typedef struct bignum_ctx BN_CTX;
80struct bn_blinding_st {
81 int init ;
82 BIGNUM *A ;
83 BIGNUM *Ai ;
84 BIGNUM *mod ;
85};
86typedef struct bn_blinding_st BN_BLINDING;
87struct bn_mont_ctx_st {
88 int ri ;
89 BIGNUM RR ;
90 BIGNUM N ;
91 BIGNUM Ni ;
92 unsigned long n0 ;
93 int flags ;
94};
95typedef struct bn_mont_ctx_st BN_MONT_CTX;
96struct X509_algor_st;
97struct X509_algor_st;
98struct X509_algor_st;
99struct asn1_object_st {
100 char const *sn ;
101 char const *ln ;
102 int nid ;
103 int length ;
104 unsigned char *data ;
105 int flags ;
106};
107typedef struct asn1_object_st ASN1_OBJECT;
108struct asn1_string_st {
109 int length ;
110 int type ;
111 unsigned char *data ;
112 long flags ;
113};
114typedef struct asn1_string_st ASN1_STRING;
115typedef struct asn1_string_st ASN1_INTEGER;
116typedef struct asn1_string_st ASN1_ENUMERATED;
117typedef struct asn1_string_st ASN1_BIT_STRING;
118typedef struct asn1_string_st ASN1_OCTET_STRING;
119typedef struct asn1_string_st ASN1_PRINTABLESTRING;
120typedef struct asn1_string_st ASN1_T61STRING;
121typedef struct asn1_string_st ASN1_IA5STRING;
122typedef struct asn1_string_st ASN1_GENERALSTRING;
123typedef struct asn1_string_st ASN1_UNIVERSALSTRING;
124typedef struct asn1_string_st ASN1_BMPSTRING;
125typedef struct asn1_string_st ASN1_UTCTIME;
126typedef struct asn1_string_st ASN1_TIME;
127typedef struct asn1_string_st ASN1_GENERALIZEDTIME;
128typedef struct asn1_string_st ASN1_VISIBLESTRING;
129typedef struct asn1_string_st ASN1_UTF8STRING;
130typedef int ASN1_BOOLEAN;
131union __anonunion_value_19 {
132 char *ptr ;
133 ASN1_BOOLEAN boolean ;
134 ASN1_STRING *asn1_string ;
135 ASN1_OBJECT *object ;
136 ASN1_INTEGER *integer ;
137 ASN1_ENUMERATED *enumerated ;
138 ASN1_BIT_STRING *bit_string ;
139 ASN1_OCTET_STRING *octet_string ;
140 ASN1_PRINTABLESTRING *printablestring ;
141 ASN1_T61STRING *t61string ;
142 ASN1_IA5STRING *ia5string ;
143 ASN1_GENERALSTRING *generalstring ;
144 ASN1_BMPSTRING *bmpstring ;
145 ASN1_UNIVERSALSTRING *universalstring ;
146 ASN1_UTCTIME *utctime ;
147 ASN1_GENERALIZEDTIME *generalizedtime ;
148 ASN1_VISIBLESTRING *visiblestring ;
149 ASN1_UTF8STRING *utf8string ;
150 ASN1_STRING *set ;
151 ASN1_STRING *sequence ;
152};
153struct asn1_type_st {
154 int type ;
155 union __anonunion_value_19 value ;
156};
157typedef struct asn1_type_st ASN1_TYPE;
158struct MD5state_st {
159 unsigned int A ;
160 unsigned int B ;
161 unsigned int C ;
162 unsigned int D ;
163 unsigned int Nl ;
164 unsigned int Nh ;
165 unsigned int data[16] ;
166 int num ;
167};
168typedef struct MD5state_st MD5_CTX;
169struct SHAstate_st {
170 unsigned int h0 ;
171 unsigned int h1 ;
172 unsigned int h2 ;
173 unsigned int h3 ;
174 unsigned int h4 ;
175 unsigned int Nl ;
176 unsigned int Nh ;
177 unsigned int data[16] ;
178 int num ;
179};
180typedef struct SHAstate_st SHA_CTX;
181struct MD2state_st {
182 int num ;
183 unsigned char data[16] ;
184 unsigned int cksm[16] ;
185 unsigned int state[16] ;
186};
187typedef struct MD2state_st MD2_CTX;
188struct MD4state_st {
189 unsigned int A ;
190 unsigned int B ;
191 unsigned int C ;
192 unsigned int D ;
193 unsigned int Nl ;
194 unsigned int Nh ;
195 unsigned int data[16] ;
196 int num ;
197};
198typedef struct MD4state_st MD4_CTX;
199struct RIPEMD160state_st {
200 unsigned int A ;
201 unsigned int B ;
202 unsigned int C ;
203 unsigned int D ;
204 unsigned int E ;
205 unsigned int Nl ;
206 unsigned int Nh ;
207 unsigned int data[16] ;
208 int num ;
209};
210typedef struct RIPEMD160state_st RIPEMD160_CTX;
211typedef unsigned char des_cblock[8];
212union __anonunion_ks_20 {
213 des_cblock cblock ;
214 unsigned long deslong[2] ;
215};
216struct des_ks_struct {
217 union __anonunion_ks_20 ks ;
218 int weak_key ;
219};
220typedef struct des_ks_struct des_key_schedule[16];
221struct rc4_key_st {
222 unsigned int x ;
223 unsigned int y ;
224 unsigned int data[256] ;
225};
226typedef struct rc4_key_st RC4_KEY;
227struct rc2_key_st {
228 unsigned int data[64] ;
229};
230typedef struct rc2_key_st RC2_KEY;
231struct rc5_key_st {
232 int rounds ;
233 unsigned long data[34] ;
234};
235typedef struct rc5_key_st RC5_32_KEY;
236struct bf_key_st {
237 unsigned int P[18] ;
238 unsigned int S[1024] ;
239};
240typedef struct bf_key_st BF_KEY;
241struct cast_key_st {
242 unsigned long data[32] ;
243 int short_key ;
244};
245typedef struct cast_key_st CAST_KEY;
246struct idea_key_st {
247 unsigned int data[9][6] ;
248};
249typedef struct idea_key_st IDEA_KEY_SCHEDULE;
250struct mdc2_ctx_st {
251 int num ;
252 unsigned char data[8] ;
253 des_cblock h ;
254 des_cblock hh ;
255 int pad_type ;
256};
257typedef struct mdc2_ctx_st MDC2_CTX;
258struct rsa_st;
259struct rsa_st;
260typedef struct rsa_st RSA;
261struct rsa_meth_st {
262 char const *name ;
263 int (*rsa_pub_enc)(int flen , unsigned char *from , unsigned char *to , RSA *rsa ,
264 int padding ) ;
265 int (*rsa_pub_dec)(int flen , unsigned char *from , unsigned char *to , RSA *rsa ,
266 int padding ) ;
267 int (*rsa_priv_enc)(int flen , unsigned char *from , unsigned char *to , RSA *rsa ,
268 int padding ) ;
269 int (*rsa_priv_dec)(int flen , unsigned char *from , unsigned char *to , RSA *rsa ,
270 int padding ) ;
271 int (*rsa_mod_exp)(BIGNUM *r0 , BIGNUM *I , RSA *rsa ) ;
272 int (*bn_mod_exp)(BIGNUM *r , BIGNUM *a , BIGNUM const *p , BIGNUM const *m ,
273 BN_CTX *ctx , BN_MONT_CTX *m_ctx ) ;
274 int (*init)(RSA *rsa ) ;
275 int (*finish)(RSA *rsa ) ;
276 int flags ;
277 char *app_data ;
278 int (*rsa_sign)(int type , unsigned char *m , unsigned int m_len , unsigned char *sigret ,
279 unsigned int *siglen , RSA *rsa ) ;
280 int (*rsa_verify)(int dtype , unsigned char *m , unsigned int m_len , unsigned char *sigbuf ,
281 unsigned int siglen , RSA *rsa ) ;
282};
283typedef struct rsa_meth_st RSA_METHOD;
284struct rsa_st {
285 int pad ;
286 int version ;
287 RSA_METHOD *meth ;
288 BIGNUM *n ;
289 BIGNUM *e ;
290 BIGNUM *d ;
291 BIGNUM *p ;
292 BIGNUM *q ;
293 BIGNUM *dmp1 ;
294 BIGNUM *dmq1 ;
295 BIGNUM *iqmp ;
296 CRYPTO_EX_DATA ex_data ;
297 int references ;
298 int flags ;
299 BN_MONT_CTX *_method_mod_n ;
300 BN_MONT_CTX *_method_mod_p ;
301 BN_MONT_CTX *_method_mod_q ;
302 char *bignum_data ;
303 BN_BLINDING *blinding ;
304};
305struct dh_st;
306struct dh_st;
307typedef struct dh_st DH;
308struct dh_method {
309 char const *name ;
310 int (*generate_key)(DH *dh ) ;
311 int (*compute_key)(unsigned char *key , BIGNUM *pub_key , DH *dh ) ;
312 int (*bn_mod_exp)(DH *dh , BIGNUM *r , BIGNUM *a , BIGNUM const *p , BIGNUM const *m ,
313 BN_CTX *ctx , BN_MONT_CTX *m_ctx ) ;
314 int (*init)(DH *dh ) ;
315 int (*finish)(DH *dh ) ;
316 int flags ;
317 char *app_data ;
318};
319typedef struct dh_method DH_METHOD;
320struct dh_st {
321 int pad ;
322 int version ;
323 BIGNUM *p ;
324 BIGNUM *g ;
325 int length ;
326 BIGNUM *pub_key ;
327 BIGNUM *priv_key ;
328 int flags ;
329 char *method_mont_p ;
330 BIGNUM *q ;
331 BIGNUM *j ;
332 unsigned char *seed ;
333 int seedlen ;
334 BIGNUM *counter ;
335 int references ;
336 CRYPTO_EX_DATA ex_data ;
337 DH_METHOD *meth ;
338};
339struct dsa_st;
340struct dsa_st;
341typedef struct dsa_st DSA;
342struct DSA_SIG_st {
343 BIGNUM *r ;
344 BIGNUM *s ;
345};
346typedef struct DSA_SIG_st DSA_SIG;
347struct dsa_method {
348 char const *name ;
349 DSA_SIG *(*dsa_do_sign)(unsigned char const *dgst , int dlen , DSA *dsa ) ;
350 int (*dsa_sign_setup)(DSA *dsa , BN_CTX *ctx_in , BIGNUM **kinvp , BIGNUM **rp ) ;
351 int (*dsa_do_verify)(unsigned char const *dgst , int dgst_len , DSA_SIG *sig ,
352 DSA *dsa ) ;
353 int (*dsa_mod_exp)(DSA *dsa , BIGNUM *rr , BIGNUM *a1 , BIGNUM *p1 , BIGNUM *a2 ,
354 BIGNUM *p2 , BIGNUM *m , BN_CTX *ctx , BN_MONT_CTX *in_mont ) ;
355 int (*bn_mod_exp)(DSA *dsa , BIGNUM *r , BIGNUM *a , BIGNUM const *p , BIGNUM const *m ,
356 BN_CTX *ctx , BN_MONT_CTX *m_ctx ) ;
357 int (*init)(DSA *dsa ) ;
358 int (*finish)(DSA *dsa ) ;
359 int flags ;
360 char *app_data ;
361};
362typedef struct dsa_method DSA_METHOD;
363struct dsa_st {
364 int pad ;
365 int version ;
366 int write_params ;
367 BIGNUM *p ;
368 BIGNUM *q ;
369 BIGNUM *g ;
370 BIGNUM *pub_key ;
371 BIGNUM *priv_key ;
372 BIGNUM *kinv ;
373 BIGNUM *r ;
374 int flags ;
375 char *method_mont_p ;
376 int references ;
377 CRYPTO_EX_DATA ex_data ;
378 DSA_METHOD *meth ;
379};
380union __anonunion_pkey_21 {
381 char *ptr ;
382 struct rsa_st *rsa ;
383 struct dsa_st *dsa ;
384 struct dh_st *dh ;
385};
386struct evp_pkey_st {
387 int type ;
388 int save_type ;
389 int references ;
390 union __anonunion_pkey_21 pkey ;
391 int save_parameters ;
392 STACK *attributes ;
393};
394typedef struct evp_pkey_st EVP_PKEY;
395struct env_md_st {
396 int type ;
397 int pkey_type ;
398 int md_size ;
399 void (*init)() ;
400 void (*update)() ;
401 void (*final)() ;
402 int (*sign)() ;
403 int (*verify)() ;
404 int required_pkey_type[5] ;
405 int block_size ;
406 int ctx_size ;
407};
408typedef struct env_md_st EVP_MD;
409union __anonunion_md_22 {
410 unsigned char base[4] ;
411 MD2_CTX md2 ;
412 MD5_CTX md5 ;
413 MD4_CTX md4 ;
414 RIPEMD160_CTX ripemd160 ;
415 SHA_CTX sha ;
416 MDC2_CTX mdc2 ;
417};
418struct env_md_ctx_st {
419 EVP_MD const *digest ;
420 union __anonunion_md_22 md ;
421};
422typedef struct env_md_ctx_st EVP_MD_CTX;
423struct evp_cipher_st;
424struct evp_cipher_st;
425typedef struct evp_cipher_st EVP_CIPHER;
426struct evp_cipher_ctx_st;
427struct evp_cipher_ctx_st;
428typedef struct evp_cipher_ctx_st EVP_CIPHER_CTX;
429struct evp_cipher_st {
430 int nid ;
431 int block_size ;
432 int key_len ;
433 int iv_len ;
434 unsigned long flags ;
435 int (*init)(EVP_CIPHER_CTX *ctx , unsigned char const *key , unsigned char const *iv ,
436 int enc ) ;
437 int (*do_cipher)(EVP_CIPHER_CTX *ctx , unsigned char *out , unsigned char const *in ,
438 unsigned int inl ) ;
439 int (*cleanup)(EVP_CIPHER_CTX * ) ;
440 int ctx_size ;
441 int (*set_asn1_parameters)(EVP_CIPHER_CTX * , ASN1_TYPE * ) ;
442 int (*get_asn1_parameters)(EVP_CIPHER_CTX * , ASN1_TYPE * ) ;
443 int (*ctrl)(EVP_CIPHER_CTX * , int type , int arg , void *ptr ) ;
444 void *app_data ;
445};
446struct __anonstruct_rc4_24 {
447 unsigned char key[16] ;
448 RC4_KEY ks ;
449};
450struct __anonstruct_desx_cbc_25 {
451 des_key_schedule ks ;
452 des_cblock inw ;
453 des_cblock outw ;
454};
455struct __anonstruct_des_ede_26 {
456 des_key_schedule ks1 ;
457 des_key_schedule ks2 ;
458 des_key_schedule ks3 ;
459};
460struct __anonstruct_rc2_27 {
461 int key_bits ;
462 RC2_KEY ks ;
463};
464struct __anonstruct_rc5_28 {
465 int rounds ;
466 RC5_32_KEY ks ;
467};
468union __anonunion_c_23 {
469 struct __anonstruct_rc4_24 rc4 ;
470 des_key_schedule des_ks ;
471 struct __anonstruct_desx_cbc_25 desx_cbc ;
472 struct __anonstruct_des_ede_26 des_ede ;
473 IDEA_KEY_SCHEDULE idea_ks ;
474 struct __anonstruct_rc2_27 rc2 ;
475 struct __anonstruct_rc5_28 rc5 ;
476 BF_KEY bf_ks ;
477 CAST_KEY cast_ks ;
478};
479struct evp_cipher_ctx_st {
480 EVP_CIPHER const *cipher ;
481 int encrypt ;
482 int buf_len ;
483 unsigned char oiv[8] ;
484 unsigned char iv[8] ;
485 unsigned char buf[8] ;
486 int num ;
487 void *app_data ;
488 int key_len ;
489 union __anonunion_c_23 c ;
490};
491struct comp_method_st {
492 int type ;
493 char const *name ;
494 int (*init)() ;
495 void (*finish)() ;
496 int (*compress)() ;
497 int (*expand)() ;
498 long (*ctrl)() ;
499 long (*callback_ctrl)() ;
500};
501typedef struct comp_method_st COMP_METHOD;
502struct comp_ctx_st {
503 COMP_METHOD *meth ;
504 unsigned long compress_in ;
505 unsigned long compress_out ;
506 unsigned long expand_in ;
507 unsigned long expand_out ;
508 CRYPTO_EX_DATA ex_data ;
509};
510typedef struct comp_ctx_st COMP_CTX;
511struct X509_algor_st {
512 ASN1_OBJECT *algorithm ;
513 ASN1_TYPE *parameter ;
514};
515typedef struct X509_algor_st X509_ALGOR;
516struct X509_val_st {
517 ASN1_TIME *notBefore ;
518 ASN1_TIME *notAfter ;
519};
520typedef struct X509_val_st X509_VAL;
521struct X509_pubkey_st {
522 X509_ALGOR *algor ;
523 ASN1_BIT_STRING *public_key ;
524 EVP_PKEY *pkey ;
525};
526typedef struct X509_pubkey_st X509_PUBKEY;
527struct X509_name_st {
528 STACK *entries ;
529 int modified ;
530 BUF_MEM *bytes ;
531 unsigned long hash ;
532};
533typedef struct X509_name_st X509_NAME;
534struct x509_cinf_st {
535 ASN1_INTEGER *version ;
536 ASN1_INTEGER *serialNumber ;
537 X509_ALGOR *signature ;
538 X509_NAME *issuer ;
539 X509_VAL *validity ;
540 X509_NAME *subject ;
541 X509_PUBKEY *key ;
542 ASN1_BIT_STRING *issuerUID ;
543 ASN1_BIT_STRING *subjectUID ;
544 STACK *extensions ;
545};
546typedef struct x509_cinf_st X509_CINF;
547struct x509_cert_aux_st {
548 STACK *trust ;
549 STACK *reject ;
550 ASN1_UTF8STRING *alias ;
551 ASN1_OCTET_STRING *keyid ;
552 STACK *other ;
553};
554typedef struct x509_cert_aux_st X509_CERT_AUX;
555struct AUTHORITY_KEYID_st;
556struct AUTHORITY_KEYID_st;
557struct x509_st {
558 X509_CINF *cert_info ;
559 X509_ALGOR *sig_alg ;
560 ASN1_BIT_STRING *signature ;
561 int valid ;
562 int references ;
563 char *name ;
564 CRYPTO_EX_DATA ex_data ;
565 long ex_pathlen ;
566 unsigned long ex_flags ;
567 unsigned long ex_kusage ;
568 unsigned long ex_xkusage ;
569 unsigned long ex_nscert ;
570 ASN1_OCTET_STRING *skid ;
571 struct AUTHORITY_KEYID_st *akid ;
572 unsigned char sha1_hash[20] ;
573 X509_CERT_AUX *aux ;
574};
575typedef struct x509_st X509;
576struct lhash_node_st {
577 void *data ;
578 struct lhash_node_st *next ;
579 unsigned long hash ;
580};
581typedef struct lhash_node_st LHASH_NODE;
582struct lhash_st {
583 LHASH_NODE **b ;
584 int (*comp)() ;
585 unsigned long (*hash)() ;
586 unsigned int num_nodes ;
587 unsigned int num_alloc_nodes ;
588 unsigned int p ;
589 unsigned int pmax ;
590 unsigned long up_load ;
591 unsigned long down_load ;
592 unsigned long num_items ;
593 unsigned long num_expands ;
594 unsigned long num_expand_reallocs ;
595 unsigned long num_contracts ;
596 unsigned long num_contract_reallocs ;
597 unsigned long num_hash_calls ;
598 unsigned long num_comp_calls ;
599 unsigned long num_insert ;
600 unsigned long num_replace ;
601 unsigned long num_delete ;
602 unsigned long num_no_delete ;
603 unsigned long num_retrieve ;
604 unsigned long num_retrieve_miss ;
605 unsigned long num_hash_comps ;
606 int error ;
607};
608struct x509_store_ctx_st;
609struct x509_store_ctx_st;
610typedef struct x509_store_ctx_st X509_STORE_CTX;
611struct x509_store_st {
612 int cache ;
613 STACK *objs ;
614 STACK *get_cert_methods ;
615 int (*verify)(X509_STORE_CTX *ctx ) ;
616 int (*verify_cb)(int ok , X509_STORE_CTX *ctx ) ;
617 CRYPTO_EX_DATA ex_data ;
618 int references ;
619 int depth ;
620};
621typedef struct x509_store_st X509_STORE;
622struct x509_store_ctx_st {
623 X509_STORE *ctx ;
624 int current_method ;
625 X509 *cert ;
626 STACK *untrusted ;
627 int purpose ;
628 int trust ;
629 time_t check_time ;
630 unsigned long flags ;
631 void *other_ctx ;
632 int (*verify)(X509_STORE_CTX *ctx ) ;
633 int (*verify_cb)(int ok , X509_STORE_CTX *ctx ) ;
634 int (*get_issuer)(X509 **issuer , X509_STORE_CTX *ctx , X509 *x ) ;
635 int (*check_issued)(X509_STORE_CTX *ctx , X509 *x , X509 *issuer ) ;
636 int (*cleanup)(X509_STORE_CTX *ctx ) ;
637 int depth ;
638 int valid ;
639 int last_untrusted ;
640 STACK *chain ;
641 int error_depth ;
642 int error ;
643 X509 *current_cert ;
644 X509 *current_issuer ;
645 CRYPTO_EX_DATA ex_data ;
646};
647typedef int pem_password_cb(char *buf , int size , int rwflag , void *userdata );
648struct ssl_st;
649struct ssl_st;
650struct ssl_cipher_st {
651 int valid ;
652 char const *name ;
653 unsigned long id ;
654 unsigned long algorithms ;
655 unsigned long algo_strength ;
656 unsigned long algorithm2 ;
657 int strength_bits ;
658 int alg_bits ;
659 unsigned long mask ;
660 unsigned long mask_strength ;
661};
662typedef struct ssl_cipher_st SSL_CIPHER;
663typedef struct ssl_st SSL;
664struct ssl_ctx_st;
665struct ssl_ctx_st;
666typedef struct ssl_ctx_st SSL_CTX;
667struct ssl3_enc_method;
668struct ssl3_enc_method;
669struct ssl_method_st {
670 int version ;
671 int (*ssl_new)(SSL *s ) ;
672 void (*ssl_clear)(SSL *s ) ;
673 void (*ssl_free)(SSL *s ) ;
674 int (*ssl_accept)(SSL *s ) ;
675 int (*ssl_connect)(SSL *s ) ;
676 int (*ssl_read)(SSL *s , void *buf , int len ) ;
677 int (*ssl_peek)(SSL *s , void *buf , int len ) ;
678 int (*ssl_write)(SSL *s , void const *buf , int len ) ;
679 int (*ssl_shutdown)(SSL *s ) ;
680 int (*ssl_renegotiate)(SSL *s ) ;
681 int (*ssl_renegotiate_check)(SSL *s ) ;
682 long (*ssl_ctrl)(SSL *s , int cmd , long larg , char *parg ) ;
683 long (*ssl_ctx_ctrl)(SSL_CTX *ctx , int cmd , long larg , char *parg ) ;
684 SSL_CIPHER *(*get_cipher_by_char)(unsigned char const *ptr ) ;
685 int (*put_cipher_by_char)(SSL_CIPHER const *cipher , unsigned char *ptr ) ;
686 int (*ssl_pending)(SSL *s ) ;
687 int (*num_ciphers)(void) ;
688 SSL_CIPHER *(*get_cipher)(unsigned int ncipher ) ;
689 struct ssl_method_st *(*get_ssl_method)(int version ) ;
690 long (*get_timeout)(void) ;
691 struct ssl3_enc_method *ssl3_enc ;
692 int (*ssl_version)() ;
693 long (*ssl_callback_ctrl)(SSL *s , int cb_id , void (*fp)() ) ;
694 long (*ssl_ctx_callback_ctrl)(SSL_CTX *s , int cb_id , void (*fp)() ) ;
695};
696typedef struct ssl_method_st SSL_METHOD;
697struct sess_cert_st;
698struct sess_cert_st;
699struct ssl_session_st {
700 int ssl_version ;
701 unsigned int key_arg_length ;
702 unsigned char key_arg[8] ;
703 int master_key_length ;
704 unsigned char master_key[48] ;
705 unsigned int session_id_length ;
706 unsigned char session_id[32] ;
707 unsigned int sid_ctx_length ;
708 unsigned char sid_ctx[32] ;
709 int not_resumable ;
710 struct sess_cert_st *sess_cert ;
711 X509 *peer ;
712 long verify_result ;
713 int references ;
714 long timeout ;
715 long time ;
716 int compress_meth ;
717 SSL_CIPHER *cipher ;
718 unsigned long cipher_id ;
719 STACK *ciphers ;
720 CRYPTO_EX_DATA ex_data ;
721 struct ssl_session_st *prev ;
722 struct ssl_session_st *next ;
723};
724typedef struct ssl_session_st SSL_SESSION;
725struct ssl_comp_st {
726 int id ;
727 char *name ;
728 COMP_METHOD *method ;
729};
730typedef struct ssl_comp_st SSL_COMP;
731struct __anonstruct_stats_37 {
732 int sess_connect ;
733 int sess_connect_renegotiate ;
734 int sess_connect_good ;
735 int sess_accept ;
736 int sess_accept_renegotiate ;
737 int sess_accept_good ;
738 int sess_miss ;
739 int sess_timeout ;
740 int sess_cache_full ;
741 int sess_hit ;
742 int sess_cb_hit ;
743};
744struct cert_st;
745struct cert_st;
746struct ssl_ctx_st {
747 SSL_METHOD *method ;
748 unsigned long options ;
749 unsigned long mode ;
750 STACK *cipher_list ;
751 STACK *cipher_list_by_id ;
752 struct x509_store_st *cert_store ;
753 struct lhash_st *sessions ;
754 unsigned long session_cache_size ;
755 struct ssl_session_st *session_cache_head ;
756 struct ssl_session_st *session_cache_tail ;
757 int session_cache_mode ;
758 long session_timeout ;
759 int (*new_session_cb)(struct ssl_st *ssl , SSL_SESSION *sess ) ;
760 void (*remove_session_cb)(struct ssl_ctx_st *ctx , SSL_SESSION *sess ) ;
761 SSL_SESSION *(*get_session_cb)(struct ssl_st *ssl , unsigned char *data , int len ,
762 int *copy ) ;
763 struct __anonstruct_stats_37 stats ;
764 int references ;
765 void (*info_callback)() ;
766 int (*app_verify_callback)() ;
767 char *app_verify_arg ;
768 struct cert_st *cert ;
769 int read_ahead ;
770 int verify_mode ;
771 int verify_depth ;
772 unsigned int sid_ctx_length ;
773 unsigned char sid_ctx[32] ;
774 int (*default_verify_callback)(int ok , X509_STORE_CTX *ctx ) ;
775 int purpose ;
776 int trust ;
777 pem_password_cb *default_passwd_callback ;
778 void *default_passwd_callback_userdata ;
779 int (*client_cert_cb)() ;
780 STACK *client_CA ;
781 int quiet_shutdown ;
782 CRYPTO_EX_DATA ex_data ;
783 EVP_MD const *rsa_md5 ;
784 EVP_MD const *md5 ;
785 EVP_MD const *sha1 ;
786 STACK *extra_certs ;
787 STACK *comp_methods ;
788};
789struct ssl2_state_st;
790struct ssl2_state_st;
791struct ssl3_state_st;
792struct ssl3_state_st;
793struct ssl_st {
794 int version ;
795 int type ;
796 SSL_METHOD *method ;
797 BIO *rbio ;
798 BIO *wbio ;
799 BIO *bbio ;
800 int rwstate ;
801 int in_handshake ;
802 int (*handshake_func)() ;
803 int server ;
804 int new_session ;
805 int quiet_shutdown ;
806 int shutdown ;
807 int state ;
808 int rstate ;
809 BUF_MEM *init_buf ;
810 int init_num ;
811 int init_off ;
812 unsigned char *packet ;
813 unsigned int packet_length ;
814 struct ssl2_state_st *s2 ;
815 struct ssl3_state_st *s3 ;
816 int read_ahead ;
817 int hit ;
818 int purpose ;
819 int trust ;
820 STACK *cipher_list ;
821 STACK *cipher_list_by_id ;
822 EVP_CIPHER_CTX *enc_read_ctx ;
823 EVP_MD const *read_hash ;
824 COMP_CTX *expand ;
825 EVP_CIPHER_CTX *enc_write_ctx ;
826 EVP_MD const *write_hash ;
827 COMP_CTX *compress ;
828 struct cert_st *cert ;
829 unsigned int sid_ctx_length ;
830 unsigned char sid_ctx[32] ;
831 SSL_SESSION *session ;
832 int verify_mode ;
833 int verify_depth ;
834 int (*verify_callback)(int ok , X509_STORE_CTX *ctx ) ;
835 void (*info_callback)() ;
836 int error ;
837 int error_code ;
838 SSL_CTX *ctx ;
839 int debug ;
840 long verify_result ;
841 CRYPTO_EX_DATA ex_data ;
842 STACK *client_CA ;
843 int references ;
844 unsigned long options ;
845 unsigned long mode ;
846 int first_packet ;
847 int client_version ;
848};
849struct __anonstruct_tmp_38 {
850 unsigned int conn_id_length ;
851 unsigned int cert_type ;
852 unsigned int cert_length ;
853 unsigned int csl ;
854 unsigned int clear ;
855 unsigned int enc ;
856 unsigned char ccl[32] ;
857 unsigned int cipher_spec_length ;
858 unsigned int session_id_length ;
859 unsigned int clen ;
860 unsigned int rlen ;
861};
862struct ssl2_state_st {
863 int three_byte_header ;
864 int clear_text ;
865 int escape ;
866 int ssl2_rollback ;
867 unsigned int wnum ;
868 int wpend_tot ;
869 unsigned char const *wpend_buf ;
870 int wpend_off ;
871 int wpend_len ;
872 int wpend_ret ;
873 int rbuf_left ;
874 int rbuf_offs ;
875 unsigned char *rbuf ;
876 unsigned char *wbuf ;
877 unsigned char *write_ptr ;
878 unsigned int padding ;
879 unsigned int rlength ;
880 int ract_data_length ;
881 unsigned int wlength ;
882 int wact_data_length ;
883 unsigned char *ract_data ;
884 unsigned char *wact_data ;
885 unsigned char *mac_data ;
886 unsigned char *pad_data_UNUSED ;
887 unsigned char *read_key ;
888 unsigned char *write_key ;
889 unsigned int challenge_length ;
890 unsigned char challenge[32] ;
891 unsigned int conn_id_length ;
892 unsigned char conn_id[16] ;
893 unsigned int key_material_length ;
894 unsigned char key_material[48] ;
895 unsigned long read_sequence ;
896 unsigned long write_sequence ;
897 struct __anonstruct_tmp_38 tmp ;
898};
899struct ssl3_record_st {
900 int type ;
901 unsigned int length ;
902 unsigned int off ;
903 unsigned char *data ;
904 unsigned char *input ;
905 unsigned char *comp ;
906};
907typedef struct ssl3_record_st SSL3_RECORD;
908struct ssl3_buffer_st {
909 unsigned char *buf ;
910 int offset ;
911 int left ;
912};
913typedef struct ssl3_buffer_st SSL3_BUFFER;
914struct __anonstruct_tmp_39 {
915 unsigned char cert_verify_md[72] ;
916 unsigned char finish_md[72] ;
917 int finish_md_len ;
918 unsigned char peer_finish_md[72] ;
919 int peer_finish_md_len ;
920 unsigned long message_size ;
921 int message_type ;
922 SSL_CIPHER *new_cipher ;
923 DH *dh ;
924 int next_state ;
925 int reuse_message ;
926 int cert_req ;
927 int ctype_num ;
928 char ctype[7] ;
929 STACK *ca_names ;
930 int use_rsa_tmp ;
931 int key_block_length ;
932 unsigned char *key_block ;
933 EVP_CIPHER const *new_sym_enc ;
934 EVP_MD const *new_hash ;
935 SSL_COMP const *new_compression ;
936 int cert_request ;
937};
938struct ssl3_state_st {
939 long flags ;
940 int delay_buf_pop_ret ;
941 unsigned char read_sequence[8] ;
942 unsigned char read_mac_secret[36] ;
943 unsigned char write_sequence[8] ;
944 unsigned char write_mac_secret[36] ;
945 unsigned char server_random[32] ;
946 unsigned char client_random[32] ;
947 SSL3_BUFFER rbuf ;
948 SSL3_BUFFER wbuf ;
949 SSL3_RECORD rrec ;
950 SSL3_RECORD wrec ;
951 unsigned char alert_fragment[2] ;
952 unsigned int alert_fragment_len ;
953 unsigned char handshake_fragment[4] ;
954 unsigned int handshake_fragment_len ;
955 unsigned int wnum ;
956 int wpend_tot ;
957 int wpend_type ;
958 int wpend_ret ;
959 unsigned char const *wpend_buf ;
960 EVP_MD_CTX finish_dgst1 ;
961 EVP_MD_CTX finish_dgst2 ;
962 int change_cipher_spec ;
963 int warn_alert ;
964 int fatal_alert ;
965 int alert_dispatch ;
966 unsigned char send_alert[2] ;
967 int renegotiate ;
968 int total_renegotiations ;
969 int num_renegotiations ;
970 int in_read_app_data ;
971 struct __anonstruct_tmp_39 tmp ;
972};
973struct cert_pkey_st {
974 X509 *x509 ;
975 EVP_PKEY *privatekey ;
976};
977typedef struct cert_pkey_st CERT_PKEY;
978struct cert_st {
979 CERT_PKEY *key ;
980 int valid ;
981 unsigned long mask ;
982 unsigned long export_mask ;
983 RSA *rsa_tmp ;
984 RSA *(*rsa_tmp_cb)(SSL *ssl , int is_export , int keysize ) ;
985 DH *dh_tmp ;
986 DH *(*dh_tmp_cb)(SSL *ssl , int is_export , int keysize ) ;
987 CERT_PKEY pkeys[5] ;
988 int references ;
989};
990struct sess_cert_st {
991 STACK *cert_chain ;
992 int peer_cert_type ;
993 CERT_PKEY *peer_key ;
994 CERT_PKEY peer_pkeys[5] ;
995 RSA *peer_rsa_tmp ;
996 DH *peer_dh_tmp ;
997 int references ;
998};
999struct ssl3_enc_method {
1000 int (*enc)(SSL * , int ) ;
1001 int (*mac)(SSL * , unsigned char * , int ) ;
1002 int (*setup_key_block)(SSL * ) ;
1003 int (*generate_master_secret)(SSL * , unsigned char * , unsigned char * , int ) ;
1004 int (*change_cipher_state)(SSL * , int ) ;
1005 int (*final_finish_mac)(SSL * , EVP_MD_CTX * , EVP_MD_CTX * , char const * ,
1006 int , unsigned char * ) ;
1007 int finish_mac_length ;
1008 int (*cert_verify_mac)(SSL * , EVP_MD_CTX * , unsigned char * ) ;
1009 char const *client_finished_label ;
1010 int client_finished_label_len ;
1011 char const *server_finished_label ;
1012 int server_finished_label_len ;
1013 int (*alert_value)(int ) ;
1014};
1015extern void *memcpy(void * __restrict __dest , void const * __restrict __src ,
1016 size_t __n ) ;
1017SSL_METHOD *SSLv3_client_method(void) ;
1018extern SSL_METHOD *sslv3_base_method(void) ;
1019int ssl3_connect(SSL *s ) ;
1020static SSL_METHOD *ssl3_get_client_method(int ver ) ;
1021static SSL_METHOD *ssl3_get_client_method(int ver )
1022{ SSL_METHOD *tmp ;
1023
1024 {
1025 if (ver == 768) {
1026 {
1027 tmp = SSLv3_client_method();
1028 }
1029 return (tmp);
1030 } else {
1031 return ((SSL_METHOD *)((void *)0));
1032 }
1033}
1034}
1035static int init = 1;
1036static SSL_METHOD SSLv3_client_data ;
1037SSL_METHOD *SSLv3_client_method(void)
1038{ char *tmp ;
1039 SSL_METHOD *tmp___0 ;
1040
1041 {
1042 if (init) {
1043 {
1044 init = 0;
1045 tmp___0 = sslv3_base_method();
1046 tmp = (char *)tmp___0;
1047 memcpy((void *)((char *)(& SSLv3_client_data)), (void const *)tmp, sizeof(SSL_METHOD ));
1048 SSLv3_client_data.ssl_connect = & ssl3_connect;
1049 SSLv3_client_data.get_ssl_method = & ssl3_get_client_method;
1050 }
1051 } else {
1052
1053 }
1054 return (& SSLv3_client_data);
1055}
1056}
1057int main(void)
1058{ SSL *s ;
1059
1060 {
1061 {
1062 s->s3 = malloc(sizeof(struct ssl3_state_st));
1063 s->state = 12292;
1064 ssl3_connect(s);
1065 }
1066 return (0);
1067}
1068}
1069int ssl3_connect(SSL *s )
1070{ BUF_MEM *buf ;
1071 unsigned long tmp ;
1072 unsigned long l ;
1073 long num1 ;
1074 void (*cb)() ;
1075 int ret ;
1076 int new_state ;
1077 int state ;
1078 int skip ;
1079 int *tmp___0 ;
1080 int tmp___1 ;
1081 int tmp___2 ;
1082 int tmp___3 ;
1083 int tmp___4 ;
1084 int tmp___5 ;
1085 int tmp___6 ;
1086 int tmp___7 ;
1087 int tmp___8 ;
1088 long tmp___9 ;
1089
1090 int blastFlag ;
1091
1092 {
1093 blastFlag = 0;
1094 s->state = 12292;
1095 tmp = __VERIFIER_nondet_int();
1096 cb = (void (*)())((void *)0);
1097 ret = -1;
1098 skip = 0;
1099 *tmp___0 = 0;
1100 if ((unsigned long )s->info_callback != (unsigned long )((void *)0)) {
1101 cb = s->info_callback;
1102 } else {
1103 if ((unsigned long )(s->ctx)->info_callback != (unsigned long )((void *)0)) {
1104 cb = (s->ctx)->info_callback;
1105 } else {
1106
1107 }
1108 }
1109 s->in_handshake += 1;
1110 if (tmp___1 & 12288) {
1111 if (tmp___2 & 16384) {
1112
1113 } else {
1114
1115 }
1116 } else {
1117
1118 }
1119 {
1120 while (1) {
1121 while_0_continue: ;
1122 state = s->state;
1123 if (s->state == 12292) {
1124 goto switch_1_12292;
1125 } else {
1126 if (s->state == 16384) {
1127 goto switch_1_16384;
1128 } else {
1129 if (s->state == 4096) {
1130 goto switch_1_4096;
1131 } else {
1132 if (s->state == 20480) {
1133 goto switch_1_20480;
1134 } else {
1135 if (s->state == 4099) {
1136 goto switch_1_4099;
1137 } else {
1138 if (s->state == 4368) {
1139 goto switch_1_4368;
1140 } else {
1141 if (s->state == 4369) {
1142 goto switch_1_4369;
1143 } else {
1144 if (s->state == 4384) {
1145 goto switch_1_4384;
1146 } else {
1147 if (s->state == 4385) {
1148 goto switch_1_4385;
1149 } else {
1150 if (s->state == 4400) {
1151 goto switch_1_4400;
1152 } else {
1153 if (s->state == 4401) {
1154 goto switch_1_4401;
1155 } else {
1156 if (s->state == 4416) {
1157 goto switch_1_4416;
1158 } else {
1159 if (s->state == 4417) {
1160 goto switch_1_4417;
1161 } else {
1162 if (s->state == 4432) {
1163 goto switch_1_4432;
1164 } else {
1165 if (s->state == 4433) {
1166 goto switch_1_4433;
1167 } else {
1168 if (s->state == 4448) {
1169 goto switch_1_4448;
1170 } else {
1171 if (s->state == 4449) {
1172 goto switch_1_4449;
1173 } else {
1174 if (s->state == 4464) {
1175 goto switch_1_4464;
1176 } else {
1177 if (s->state == 4465) {
1178 goto switch_1_4465;
1179 } else {
1180 if (s->state == 4466) {
1181 goto switch_1_4466;
1182 } else {
1183 if (s->state == 4467) {
1184 goto switch_1_4467;
1185 } else {
1186 if (s->state == 4480) {
1187 goto switch_1_4480;
1188 } else {
1189 if (s->state == 4481) {
1190 goto switch_1_4481;
1191 } else {
1192 if (s->state == 4496) {
1193 goto switch_1_4496;
1194 } else {
1195 if (s->state == 4497) {
1196 goto switch_1_4497;
1197 } else {
1198 if (s->state == 4512) {
1199 goto switch_1_4512;
1200 } else {
1201 if (s->state == 4513) {
1202 goto switch_1_4513;
1203 } else {
1204 if (s->state == 4528) {
1205 goto switch_1_4528;
1206 } else {
1207 if (s->state == 4529) {
1208 goto switch_1_4529;
1209 } else {
1210 if (s->state == 4560) {
1211 goto switch_1_4560;
1212 } else {
1213 if (s->state == 4561) {
1214 goto switch_1_4561;
1215 } else {
1216 if (s->state == 4352) {
1217 goto switch_1_4352;
1218 } else {
1219 if (s->state == 3) {
1220 goto switch_1_3;
1221 } else {
1222 {
1223 goto switch_1_default;
1224 if (0) {
1225 switch_1_12292:
1226 s->new_session = 1;
1227 s->state = 4096;
1228 (s->ctx)->stats.sess_connect_renegotiate += 1;
1229 switch_1_16384: ;
1230 switch_1_4096: ;
1231 switch_1_20480: ;
1232 switch_1_4099:
1233 s->server = 0;
1234 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1235
1236 } else {
1237
1238 }
1239 if ((s->version & 65280) != 768) {
1240 ret = -1;
1241 goto end;
1242 } else {
1243
1244 }
1245 s->type = 4096;
1246 if ((unsigned long )s->init_buf == (unsigned long )((void *)0)) {
1247 tmp___3 = __VERIFIER_nondet_int();
1248 if (! tmp___3) {
1249 ret = -1;
1250 goto end;
1251 } else {
1252
1253 }
1254 s->init_buf = buf;
1255 } else {
1256
1257 }
1258 tmp___4 = __VERIFIER_nondet_int();
1259 if (! tmp___4) {
1260 ret = -1;
1261 goto end;
1262 } else {
1263
1264 }
1265 tmp___5 = __VERIFIER_nondet_int();
1266 if (! tmp___5) {
1267 ret = -1;
1268 goto end;
1269 } else {
1270
1271 }
1272 s->state = 4368;
1273 (s->ctx)->stats.sess_connect += 1;
1274 s->init_num = 0;
1275 goto switch_1_break;
1276 switch_1_4368: ;
1277 switch_1_4369:
1278 s->shutdown = 0;
1279 ret = __VERIFIER_nondet_int();
1280 if (blastFlag == 0) {
1281 blastFlag = 1;
1282 } else {
1283
1284 }
1285 if (ret <= 0) {
1286 goto end;
1287 } else {
1288
1289 }
1290 s->state = 4384;
1291 s->init_num = 0;
1292 if ((unsigned long )s->bbio != (unsigned long )s->wbio) {
1293
1294 } else {
1295
1296 }
1297 goto switch_1_break;
1298 switch_1_4384: ;
1299 switch_1_4385:
1300 ret = __VERIFIER_nondet_int();
1301 if (blastFlag == 1) {
1302 blastFlag = 2;
1303 } else {
1304
1305 }
1306 if (ret <= 0) {
1307 goto end;
1308 } else {
1309
1310 }
1311 if (s->hit) {
1312 s->state = 4560;
1313 } else {
1314 s->state = 4400;
1315 }
1316 s->init_num = 0;
1317 goto switch_1_break;
1318 switch_1_4400: ;
1319 switch_1_4401: ;
1320 if (((s->s3)->tmp.new_cipher)->algorithms & 256UL) {
1321 skip = 1;
1322 } else {
1323 ret = __VERIFIER_nondet_int();
1324 if (blastFlag == 2) {
1325 blastFlag = 3;
1326 } else {
1327
1328 }
1329 if (ret <= 0) {
1330 goto end;
1331 } else {
1332
1333 }
1334 }
1335 s->state = 4416;
1336 s->init_num = 0;
1337 goto switch_1_break;
1338 switch_1_4416: ;
1339 switch_1_4417:
1340 ret = __VERIFIER_nondet_int();
1341 if (blastFlag == 3) {
1342 blastFlag = 4;
1343 } else {
1344
1345 }
1346 if (ret <= 0) {
1347 goto end;
1348 } else {
1349
1350 }
1351 s->state = 4432;
1352 s->init_num = 0;
1353 tmp___6 = __VERIFIER_nondet_int();
1354 if (! tmp___6) {
1355 ret = -1;
1356 goto end;
1357 } else {
1358
1359 }
1360 goto switch_1_break;
1361 switch_1_4432: ;
1362 switch_1_4433:
1363 ret = __VERIFIER_nondet_int();
1364 if (blastFlag == 5) {
1365 goto ERROR;
1366 } else {
1367
1368 }
1369 if (ret <= 0) {
1370 goto end;
1371 } else {
1372
1373 }
1374 s->state = 4448;
1375 s->init_num = 0;
1376 goto switch_1_break;
1377 switch_1_4448: ;
1378 switch_1_4449:
1379 ret = __VERIFIER_nondet_int();
1380 if (blastFlag == 4) {
1381 goto ERROR;
1382 } else {
1383
1384 }
1385 if (ret <= 0) {
1386 goto end;
1387 } else {
1388
1389 }
1390 if ((s->s3)->tmp.cert_req) {
1391 s->state = 4464;
1392 } else {
1393 s->state = 4480;
1394 }
1395 s->init_num = 0;
1396 goto switch_1_break;
1397 switch_1_4464: ;
1398 switch_1_4465: ;
1399 switch_1_4466: ;
1400 switch_1_4467:
1401 ret = __VERIFIER_nondet_int();
1402 if (ret <= 0) {
1403 goto end;
1404 } else {
1405
1406 }
1407 s->state = 4480;
1408 s->init_num = 0;
1409 goto switch_1_break;
1410 switch_1_4480: ;
1411 switch_1_4481:
1412 ret = __VERIFIER_nondet_int();
1413 if (ret <= 0) {
1414 goto end;
1415 } else {
1416
1417 }
1418 l = ((s->s3)->tmp.new_cipher)->algorithms;
1419 if ((s->s3)->tmp.cert_req == 1) {
1420 s->state = 4496;
1421 } else {
1422 s->state = 4512;
1423 (s->s3)->change_cipher_spec = 0;
1424 }
1425 s->init_num = 0;
1426 goto switch_1_break;
1427 switch_1_4496: ;
1428 switch_1_4497:
1429 ret = __VERIFIER_nondet_int();
1430 if (ret <= 0) {
1431 goto end;
1432 } else {
1433
1434 }
1435 s->state = 4512;
1436 s->init_num = 0;
1437 (s->s3)->change_cipher_spec = 0;
1438 goto switch_1_break;
1439 switch_1_4512: ;
1440 switch_1_4513:
1441 ret = __VERIFIER_nondet_int();
1442 if (ret <= 0) {
1443 goto end;
1444 } else {
1445
1446 }
1447 s->state = 4528;
1448 s->init_num = 0;
1449 (s->session)->cipher = (s->s3)->tmp.new_cipher;
1450 if ((unsigned long )(s->s3)->tmp.new_compression == (unsigned long )((void *)0)) {
1451 (s->session)->compress_meth = 0;
1452 } else {
1453 (s->session)->compress_meth = ((s->s3)->tmp.new_compression)->id;
1454 }
1455 tmp___7 = __VERIFIER_nondet_int();
1456 if (! tmp___7) {
1457 ret = -1;
1458 goto end;
1459 } else {
1460
1461 }
1462 tmp___8 = __VERIFIER_nondet_int();
1463 if (! tmp___8) {
1464 ret = -1;
1465 goto end;
1466 } else {
1467
1468 }
1469 goto switch_1_break;
1470 switch_1_4528: ;
1471 switch_1_4529:
1472 ret = __VERIFIER_nondet_int();
1473 if (ret <= 0) {
1474 goto end;
1475 } else {
1476
1477 }
1478 s->state = 4352;
1479 (s->s3)->flags &= -5L;
1480 if (s->hit) {
1481 (s->s3)->tmp.next_state = 3;
1482 if ((s->s3)->flags & 2L) {
1483 s->state = 3;
1484 (s->s3)->flags |= 4L;
1485 (s->s3)->delay_buf_pop_ret = 0;
1486 } else {
1487
1488 }
1489 } else {
1490 (s->s3)->tmp.next_state = 4560;
1491 }
1492 s->init_num = 0;
1493 goto switch_1_break;
1494 switch_1_4560: ;
1495 switch_1_4561:
1496 ret = __VERIFIER_nondet_int();
1497 if (ret <= 0) {
1498 goto end;
1499 } else {
1500
1501 }
1502 if (s->hit) {
1503 s->state = 4512;
1504 } else {
1505 s->state = 3;
1506 }
1507 s->init_num = 0;
1508 goto switch_1_break;
1509 switch_1_4352:
1510 num1 = __VERIFIER_nondet_int();
1511 if (num1 > 0L) {
1512 s->rwstate = 2;
1513 tmp___9 = __VERIFIER_nondet_int();
1514 num1 = (long )((int )tmp___9);
1515 if (num1 <= 0L) {
1516 ret = -1;
1517 goto end;
1518 } else {
1519
1520 }
1521 s->rwstate = 1;
1522 } else {
1523
1524 }
1525 s->state = (s->s3)->tmp.next_state;
1526 goto switch_1_break;
1527 switch_1_3:
1528 if ((unsigned long )s->init_buf != (unsigned long )((void *)0)) {
1529 s->init_buf = (BUF_MEM *)((void *)0);
1530 } else {
1531
1532 }
1533 if (! ((s->s3)->flags & 4L)) {
1534
1535 } else {
1536
1537 }
1538 s->init_num = 0;
1539 s->new_session = 0;
1540 if (s->hit) {
1541 (s->ctx)->stats.sess_hit += 1;
1542 } else {
1543
1544 }
1545 ret = 1;
1546 s->handshake_func = (int (*)())(& ssl3_connect);
1547 (s->ctx)->stats.sess_connect_good += 1;
1548 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1549
1550 } else {
1551
1552 }
1553 goto end;
1554 switch_1_default:
1555 ret = -1;
1556 goto end;
1557 } else {
1558 switch_1_break: ;
1559 }
1560 }
1561 }
1562 }
1563 }
1564 }
1565 }
1566 }
1567 }
1568 }
1569 }
1570 }
1571 }
1572 }
1573 }
1574 }
1575 }
1576 }
1577 }
1578 }
1579 }
1580 }
1581 }
1582 }
1583 }
1584 }
1585 }
1586 }
1587 }
1588 }
1589 }
1590 }
1591 }
1592 }
1593 }
1594 if (! (s->s3)->tmp.reuse_message) {
1595 if (! skip) {
1596 if (s->debug) {
1597 ret = __VERIFIER_nondet_int();
1598 if (ret <= 0) {
1599 goto end;
1600 } else {
1601
1602 }
1603 } else {
1604
1605 }
1606 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1607 if (s->state != state) {
1608 new_state = s->state;
1609 s->state = state;
1610 s->state = new_state;
1611 } else {
1612
1613 }
1614 } else {
1615
1616 }
1617 } else {
1618
1619 }
1620 } else {
1621
1622 }
1623 skip = 0;
1624 }
1625 while_0_break: ;
1626 }
1627 end:
1628 s->in_handshake -= 1;
1629 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1630
1631 } else {
1632
1633 }
1634 return (ret);
1635 ERROR:
1636 goto ERROR;
1637}
1638}