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