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