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