1
2
3
4int __VERIFIER_nondet_int() { int x; return x; }
5
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->s3 = malloc(sizeof(struct ssl3_state_st));
1064 s->state = 12292;
1065 ssl3_connect(s);
1066 }
1067 return (0);
1068}
1069}
1070int ssl3_connect(SSL *s )
1071{ BUF_MEM *buf ;
1072 unsigned long tmp ;
1073 unsigned long l ;
1074 long num1 ;
1075 void (*cb)() ;
1076 int ret ;
1077 int new_state ;
1078 int state ;
1079 int skip ;
1080 int *tmp___0 ;
1081 int tmp___1 ;
1082 int tmp___2 ;
1083 int tmp___3 ;
1084 int tmp___4 ;
1085 int tmp___5 ;
1086 int tmp___6 ;
1087 int tmp___7 ;
1088 int tmp___8 ;
1089 long tmp___9 ;
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 buf = __VERIFIER_nondet_int();
1248 if ((unsigned long )buf == (unsigned long )((void *)0)) {
1249 ret = -1;
1250 goto end;
1251 } else {
1252
1253 }
1254 if (! tmp___3) {
1255 ret = -1;
1256 goto end;
1257 } else {
1258
1259 }
1260 s->init_buf = buf;
1261 } else {
1262
1263 }
1264 if (! tmp___4) {
1265 ret = -1;
1266 goto end;
1267 } else {
1268
1269 }
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 if (blastFlag == 4) {
1288 blastFlag = 5;
1289 } else {
1290
1291 }
1292 }
1293 if (ret <= 0) {
1294 goto end;
1295 } else {
1296
1297 }
1298 s->state = 4384;
1299 s->init_num = 0;
1300 if ((unsigned long )s->bbio != (unsigned long )s->wbio) {
1301
1302 } else {
1303
1304 }
1305 goto switch_1_break;
1306 switch_1_4384: ;
1307 switch_1_4385:
1308 ret = __VERIFIER_nondet_int();
1309 if (blastFlag == 1) {
1310 blastFlag = 2;
1311 } else {
1312
1313 }
1314 if (ret <= 0) {
1315 goto end;
1316 } else {
1317
1318 }
1319 if (s->hit) {
1320 s->state = 4560;
1321 } else {
1322 s->state = 4400;
1323 }
1324 s->init_num = 0;
1325 goto switch_1_break;
1326 switch_1_4400: ;
1327 switch_1_4401: ;
1328 if (((s->s3)->tmp.new_cipher)->algorithms & 256UL) {
1329 skip = 1;
1330 } else {
1331 ret = __VERIFIER_nondet_int();
1332 if (blastFlag == 2) {
1333 blastFlag = 3;
1334 } else {
1335
1336 }
1337 if (ret <= 0) {
1338 goto end;
1339 } else {
1340
1341 }
1342 }
1343 s->state = 4416;
1344 s->init_num = 0;
1345 goto switch_1_break;
1346 switch_1_4416: ;
1347 switch_1_4417:
1348 ret = __VERIFIER_nondet_int();
1349 if (blastFlag == 3) {
1350 blastFlag = 4;
1351 } else {
1352
1353 }
1354 if (ret <= 0) {
1355 goto end;
1356 } else {
1357
1358 }
1359 s->state = 4432;
1360 s->init_num = 0;
1361 if (! tmp___6) {
1362 ret = -1;
1363 goto end;
1364 } else {
1365
1366 }
1367 goto switch_1_break;
1368 switch_1_4432: ;
1369 switch_1_4433:
1370 ret = __VERIFIER_nondet_int();
1371 if (blastFlag == 5) {
1372 goto ERROR;
1373 } else {
1374
1375 }
1376 if (ret <= 0) {
1377 goto end;
1378 } else {
1379
1380 }
1381 s->state = 4448;
1382 s->init_num = 0;
1383 goto switch_1_break;
1384 switch_1_4448: ;
1385 switch_1_4449:
1386 ret = __VERIFIER_nondet_int();
1387 if (ret <= 0) {
1388 goto end;
1389 } else {
1390
1391 }
1392 if ((s->s3)->tmp.cert_req) {
1393 s->state = 4464;
1394 } else {
1395 s->state = 4480;
1396 }
1397 s->init_num = 0;
1398 goto switch_1_break;
1399 switch_1_4464: ;
1400 switch_1_4465: ;
1401 switch_1_4466: ;
1402 switch_1_4467:
1403 ret = __VERIFIER_nondet_int();
1404 if (ret <= 0) {
1405 goto end;
1406 } else {
1407
1408 }
1409 s->state = 4480;
1410 s->init_num = 0;
1411 goto switch_1_break;
1412 switch_1_4480: ;
1413 switch_1_4481:
1414 ret = __VERIFIER_nondet_int();
1415 if (ret <= 0) {
1416 goto end;
1417 } else {
1418
1419 }
1420 l = ((s->s3)->tmp.new_cipher)->algorithms;
1421 if ((s->s3)->tmp.cert_req == 1) {
1422 s->state = 4496;
1423 } else {
1424 s->state = 4512;
1425 (s->s3)->change_cipher_spec = 0;
1426 }
1427 s->init_num = 0;
1428 goto switch_1_break;
1429 switch_1_4496: ;
1430 switch_1_4497:
1431 ret = __VERIFIER_nondet_int();
1432 if (ret <= 0) {
1433 goto end;
1434 } else {
1435
1436 }
1437 s->state = 4512;
1438 s->init_num = 0;
1439 (s->s3)->change_cipher_spec = 0;
1440 goto switch_1_break;
1441 switch_1_4512: ;
1442 switch_1_4513:
1443 ret = __VERIFIER_nondet_int();
1444 if (ret <= 0) {
1445 goto end;
1446 } else {
1447
1448 }
1449 s->state = 4528;
1450 s->init_num = 0;
1451 (s->session)->cipher = (s->s3)->tmp.new_cipher;
1452 if ((unsigned long )(s->s3)->tmp.new_compression == (unsigned long )((void *)0)) {
1453 (s->session)->compress_meth = 0;
1454 } else {
1455 (s->session)->compress_meth = ((s->s3)->tmp.new_compression)->id;
1456 }
1457 if (! tmp___7) {
1458 ret = -1;
1459 goto end;
1460 } else {
1461
1462 }
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 if (num1 > 0L) {
1511 s->rwstate = 2;
1512 num1 = (long )((int )tmp___9);
1513 if (num1 <= 0L) {
1514 ret = -1;
1515 goto end;
1516 } else {
1517
1518 }
1519 s->rwstate = 1;
1520 } else {
1521
1522 }
1523 s->state = (s->s3)->tmp.next_state;
1524 goto switch_1_break;
1525 switch_1_3:
1526 if ((unsigned long )s->init_buf != (unsigned long )((void *)0)) {
1527 s->init_buf = (BUF_MEM *)((void *)0);
1528 } else {
1529
1530 }
1531 if (! ((s->s3)->flags & 4L)) {
1532
1533 } else {
1534
1535 }
1536 s->init_num = 0;
1537 s->new_session = 0;
1538 if (s->hit) {
1539 (s->ctx)->stats.sess_hit += 1;
1540 } else {
1541
1542 }
1543 ret = 1;
1544 s->handshake_func = (int (*)())(& ssl3_connect);
1545 (s->ctx)->stats.sess_connect_good += 1;
1546 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1547
1548 } else {
1549
1550 }
1551 goto end;
1552 switch_1_default:
1553 ret = -1;
1554 goto end;
1555 } else {
1556 switch_1_break: ;
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 }
1592 if (! (s->s3)->tmp.reuse_message) {
1593 if (! skip) {
1594 if (s->debug) {
1595 ret = __VERIFIER_nondet_int();
1596 if (ret <= 0) {
1597 goto end;
1598 } else {
1599
1600 }
1601 } else {
1602
1603 }
1604 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1605 if (s->state != state) {
1606 new_state = s->state;
1607 s->state = state;
1608 s->state = new_state;
1609 } else {
1610
1611 }
1612 } else {
1613
1614 }
1615 } else {
1616
1617 }
1618 } else {
1619
1620 }
1621 skip = 0;
1622 }
1623 while_0_break: ;
1624 }
1625 end:
1626 s->in_handshake -= 1;
1627 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1628
1629 } else {
1630
1631 }
1632 return (ret);
1633 ERROR:
1634 goto ERROR;
1635}
1636}