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