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 int blastFlag ;
1090
1091 {
1092 blastFlag = 0;
1093 s->state = 12292;
1094 tmp = __VERIFIER_nondet_int();
1095 cb = (void (*)())((void *)0);
1096 ret = -1;
1097 skip = 0;
1098 *tmp___0 = 0;
1099 if ((unsigned long )s->info_callback != (unsigned long )((void *)0)) {
1100 cb = s->info_callback;
1101 } else {
1102 if ((unsigned long )(s->ctx)->info_callback != (unsigned long )((void *)0)) {
1103 cb = (s->ctx)->info_callback;
1104 } else {
1105
1106 }
1107 }
1108 s->in_handshake += 1;
1109 if (tmp___1 & 12288) {
1110 if (tmp___2 & 16384) {
1111
1112 } else {
1113
1114 }
1115 } else {
1116
1117 }
1118 {
1119 while (1) {
1120 while_0_continue: ;
1121 state = s->state;
1122 if (s->state == 12292) {
1123 goto switch_1_12292;
1124 } else {
1125 if (s->state == 16384) {
1126 goto switch_1_16384;
1127 } else {
1128 if (s->state == 4096) {
1129 goto switch_1_4096;
1130 } else {
1131 if (s->state == 20480) {
1132 goto switch_1_20480;
1133 } else {
1134 if (s->state == 4099) {
1135 goto switch_1_4099;
1136 } else {
1137 if (s->state == 4368) {
1138 goto switch_1_4368;
1139 } else {
1140 if (s->state == 4369) {
1141 goto switch_1_4369;
1142 } else {
1143 if (s->state == 4384) {
1144 goto switch_1_4384;
1145 } else {
1146 if (s->state == 4385) {
1147 goto switch_1_4385;
1148 } else {
1149 if (s->state == 4400) {
1150 goto switch_1_4400;
1151 } else {
1152 if (s->state == 4401) {
1153 goto switch_1_4401;
1154 } else {
1155 if (s->state == 4416) {
1156 goto switch_1_4416;
1157 } else {
1158 if (s->state == 4417) {
1159 goto switch_1_4417;
1160 } else {
1161 if (s->state == 4432) {
1162 goto switch_1_4432;
1163 } else {
1164 if (s->state == 4433) {
1165 goto switch_1_4433;
1166 } else {
1167 if (s->state == 4448) {
1168 goto switch_1_4448;
1169 } else {
1170 if (s->state == 4449) {
1171 goto switch_1_4449;
1172 } else {
1173 if (s->state == 4464) {
1174 goto switch_1_4464;
1175 } else {
1176 if (s->state == 4465) {
1177 goto switch_1_4465;
1178 } else {
1179 if (s->state == 4466) {
1180 goto switch_1_4466;
1181 } else {
1182 if (s->state == 4467) {
1183 goto switch_1_4467;
1184 } else {
1185 if (s->state == 4480) {
1186 goto switch_1_4480;
1187 } else {
1188 if (s->state == 4481) {
1189 goto switch_1_4481;
1190 } else {
1191 if (s->state == 4496) {
1192 goto switch_1_4496;
1193 } else {
1194 if (s->state == 4497) {
1195 goto switch_1_4497;
1196 } else {
1197 if (s->state == 4512) {
1198 goto switch_1_4512;
1199 } else {
1200 if (s->state == 4513) {
1201 goto switch_1_4513;
1202 } else {
1203 if (s->state == 4528) {
1204 goto switch_1_4528;
1205 } else {
1206 if (s->state == 4529) {
1207 goto switch_1_4529;
1208 } else {
1209 if (s->state == 4560) {
1210 goto switch_1_4560;
1211 } else {
1212 if (s->state == 4561) {
1213 goto switch_1_4561;
1214 } else {
1215 if (s->state == 4352) {
1216 goto switch_1_4352;
1217 } else {
1218 if (s->state == 3) {
1219 goto switch_1_3;
1220 } else {
1221 {
1222 goto switch_1_default;
1223 if (0) {
1224 switch_1_12292:
1225 s->new_session = 1;
1226 s->state = 4096;
1227 (s->ctx)->stats.sess_connect_renegotiate += 1;
1228 switch_1_16384: ;
1229 switch_1_4096: ;
1230 switch_1_20480: ;
1231 switch_1_4099:
1232 s->server = 0;
1233 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1234
1235 } else {
1236
1237 }
1238 if ((s->version & 65280) != 768) {
1239 ret = -1;
1240 goto end;
1241 } else {
1242
1243 }
1244 s->type = 4096;
1245 if ((unsigned long )s->init_buf == (unsigned long )((void *)0)) {
1246 buf = __VERIFIER_nondet_int();
1247 if ((unsigned long )buf == (unsigned long )((void *)0)) {
1248 ret = -1;
1249 goto end;
1250 } else {
1251
1252 }
1253 if (! tmp___3) {
1254 ret = -1;
1255 goto end;
1256 } else {
1257
1258 }
1259 s->init_buf = buf;
1260 } else {
1261
1262 }
1263 if (! tmp___4) {
1264 ret = -1;
1265 goto end;
1266 } else {
1267
1268 }
1269 if (! tmp___5) {
1270 ret = -1;
1271 goto end;
1272 } else {
1273
1274 }
1275 s->state = 4368;
1276 (s->ctx)->stats.sess_connect += 1;
1277 s->init_num = 0;
1278 goto switch_1_break;
1279 switch_1_4368: ;
1280 switch_1_4369:
1281 s->shutdown = 0;
1282 ret = __VERIFIER_nondet_int();
1283 if (blastFlag == 0) {
1284 blastFlag = 1;
1285 } else {
1286
1287 }
1288 if (ret <= 0) {
1289 goto end;
1290 } else {
1291
1292 }
1293 s->state = 4384;
1294 s->init_num = 0;
1295 if ((unsigned long )s->bbio != (unsigned long )s->wbio) {
1296
1297 } else {
1298
1299 }
1300 goto switch_1_break;
1301 switch_1_4384: ;
1302 switch_1_4385:
1303 ret = __VERIFIER_nondet_int();
1304 if (blastFlag == 1) {
1305 blastFlag = 2;
1306 } else {
1307
1308 }
1309 if (ret <= 0) {
1310 goto end;
1311 } else {
1312
1313 }
1314 if (s->hit) {
1315 s->state = 4560;
1316 } else {
1317 s->state = 4400;
1318 }
1319 s->init_num = 0;
1320 goto switch_1_break;
1321 switch_1_4400: ;
1322 switch_1_4401: ;
1323 if (((s->s3)->tmp.new_cipher)->algorithms & 256UL) {
1324 skip = 1;
1325 } else {
1326 ret = __VERIFIER_nondet_int();
1327 if (blastFlag == 2) {
1328 blastFlag = 3;
1329 } else {
1330 if (blastFlag == 4) {
1331 blastFlag = 5;
1332 } else {
1333
1334 }
1335 }
1336 if (ret <= 0) {
1337 goto end;
1338 } else {
1339
1340 }
1341 }
1342 s->state = 4416;
1343 s->init_num = 0;
1344 goto switch_1_break;
1345 switch_1_4416: ;
1346 switch_1_4417:
1347 ret = __VERIFIER_nondet_int();
1348 if (blastFlag == 3) {
1349 blastFlag = 4;
1350 } else {
1351
1352 }
1353 if (ret <= 0) {
1354 goto end;
1355 } else {
1356
1357 }
1358 s->state = 4432;
1359 s->init_num = 0;
1360 if (! tmp___6) {
1361 ret = -1;
1362 goto end;
1363 } else {
1364
1365 }
1366 goto switch_1_break;
1367 switch_1_4432: ;
1368 switch_1_4433:
1369 ret = __VERIFIER_nondet_int();
1370 if (blastFlag == 4) {
1371 goto ERROR;
1372 } else {
1373
1374 }
1375 if (ret <= 0) {
1376 goto end;
1377 } else {
1378
1379 }
1380 s->state = 4448;
1381 s->init_num = 0;
1382 goto switch_1_break;
1383 switch_1_4448: ;
1384 switch_1_4449:
1385 ret = __VERIFIER_nondet_int();
1386 if (ret <= 0) {
1387 goto end;
1388 } else {
1389
1390 }
1391 if ((s->s3)->tmp.cert_req) {
1392 s->state = 4464;
1393 } else {
1394 s->state = 4480;
1395 }
1396 s->init_num = 0;
1397 goto switch_1_break;
1398 switch_1_4464: ;
1399 switch_1_4465: ;
1400 switch_1_4466: ;
1401 switch_1_4467:
1402 ret = __VERIFIER_nondet_int();
1403 if (ret <= 0) {
1404 goto end;
1405 } else {
1406
1407 }
1408 s->state = 4480;
1409 s->init_num = 0;
1410 goto switch_1_break;
1411 switch_1_4480: ;
1412 switch_1_4481:
1413 ret = __VERIFIER_nondet_int();
1414 if (ret <= 0) {
1415 goto end;
1416 } else {
1417
1418 }
1419 l = ((s->s3)->tmp.new_cipher)->algorithms;
1420 if ((s->s3)->tmp.cert_req == 1) {
1421 s->state = 4496;
1422 } else {
1423 s->state = 4512;
1424 (s->s3)->change_cipher_spec = 0;
1425 }
1426 s->init_num = 0;
1427 goto switch_1_break;
1428 switch_1_4496: ;
1429 switch_1_4497:
1430 ret = __VERIFIER_nondet_int();
1431 if (ret <= 0) {
1432 goto end;
1433 } else {
1434
1435 }
1436 s->state = 4512;
1437 s->init_num = 0;
1438 (s->s3)->change_cipher_spec = 0;
1439 goto switch_1_break;
1440 switch_1_4512: ;
1441 switch_1_4513:
1442 ret = __VERIFIER_nondet_int();
1443 if (ret <= 0) {
1444 goto end;
1445 } else {
1446
1447 }
1448 s->state = 4528;
1449 s->init_num = 0;
1450 (s->session)->cipher = (s->s3)->tmp.new_cipher;
1451 if ((unsigned long )(s->s3)->tmp.new_compression == (unsigned long )((void *)0)) {
1452 (s->session)->compress_meth = 0;
1453 } else {
1454 (s->session)->compress_meth = ((s->s3)->tmp.new_compression)->id;
1455 }
1456 if (! tmp___7) {
1457 ret = -1;
1458 goto end;
1459 } else {
1460
1461 }
1462 if (! tmp___8) {
1463 ret = -1;
1464 goto end;
1465 } else {
1466
1467 }
1468 goto switch_1_break;
1469 switch_1_4528: ;
1470 switch_1_4529:
1471 ret = __VERIFIER_nondet_int();
1472 if (ret <= 0) {
1473 goto end;
1474 } else {
1475
1476 }
1477 s->state = 4352;
1478 (s->s3)->flags &= -5L;
1479 if (s->hit) {
1480 (s->s3)->tmp.next_state = 3;
1481 if ((s->s3)->flags & 2L) {
1482 s->state = 3;
1483 (s->s3)->flags |= 4L;
1484 (s->s3)->delay_buf_pop_ret = 0;
1485 } else {
1486
1487 }
1488 } else {
1489 (s->s3)->tmp.next_state = 4560;
1490 }
1491 s->init_num = 0;
1492 goto switch_1_break;
1493 switch_1_4560: ;
1494 switch_1_4561:
1495 ret = __VERIFIER_nondet_int();
1496 if (ret <= 0) {
1497 goto end;
1498 } else {
1499
1500 }
1501 if (s->hit) {
1502 s->state = 4512;
1503 } else {
1504 s->state = 3;
1505 }
1506 s->init_num = 0;
1507 goto switch_1_break;
1508 switch_1_4352:
1509 if (num1 > 0L) {
1510 s->rwstate = 2;
1511 num1 = (long )((int )tmp___9);
1512 if (num1 <= 0L) {
1513 ret = -1;
1514 goto end;
1515 } else {
1516
1517 }
1518 s->rwstate = 1;
1519 } else {
1520
1521 }
1522 s->state = (s->s3)->tmp.next_state;
1523 goto switch_1_break;
1524 switch_1_3:
1525 if ((unsigned long )s->init_buf != (unsigned long )((void *)0)) {
1526 s->init_buf = (BUF_MEM *)((void *)0);
1527 } else {
1528
1529 }
1530 if (! ((s->s3)->flags & 4L)) {
1531
1532 } else {
1533
1534 }
1535 s->init_num = 0;
1536 s->new_session = 0;
1537 if (s->hit) {
1538 (s->ctx)->stats.sess_hit += 1;
1539 } else {
1540
1541 }
1542 ret = 1;
1543 s->handshake_func = (int (*)())(& ssl3_connect);
1544 (s->ctx)->stats.sess_connect_good += 1;
1545 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1546
1547 } else {
1548
1549 }
1550 goto end;
1551 switch_1_default:
1552 ret = -1;
1553 goto end;
1554 } else {
1555 switch_1_break: ;
1556 }
1557 }
1558 }
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 if (! (s->s3)->tmp.reuse_message) {
1592 if (! skip) {
1593 if (s->debug) {
1594 ret = __VERIFIER_nondet_int();
1595 if (ret <= 0) {
1596 goto end;
1597 } else {
1598
1599 }
1600 } else {
1601
1602 }
1603 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1604 if (s->state != state) {
1605 new_state = s->state;
1606 s->state = state;
1607 s->state = new_state;
1608 } else {
1609
1610 }
1611 } else {
1612
1613 }
1614 } else {
1615
1616 }
1617 } else {
1618
1619 }
1620 skip = 0;
1621 }
1622 while_0_break: ;
1623 }
1624 end:
1625 s->in_handshake -= 1;
1626 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1627
1628 } else {
1629
1630 }
1631 return (ret);
1632 ERROR:
1633 goto ERROR;
1634}
1635}