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 X509_algor_st {
497 ASN1_OBJECT *algorithm ;
498 ASN1_TYPE *parameter ;
499};
500typedef struct X509_algor_st X509_ALGOR;
501struct X509_val_st {
502 ASN1_TIME *notBefore ;
503 ASN1_TIME *notAfter ;
504};
505typedef struct X509_val_st X509_VAL;
506struct X509_pubkey_st {
507 X509_ALGOR *algor ;
508 ASN1_BIT_STRING *public_key ;
509 EVP_PKEY *pkey ;
510};
511typedef struct X509_pubkey_st X509_PUBKEY;
512struct X509_name_st {
513 STACK *entries ;
514 int modified ;
515 BUF_MEM *bytes ;
516 unsigned long hash ;
517};
518typedef struct X509_name_st X509_NAME;
519struct x509_cinf_st {
520 ASN1_INTEGER *version ;
521 ASN1_INTEGER *serialNumber ;
522 X509_ALGOR *signature ;
523 X509_NAME *issuer ;
524 X509_VAL *validity ;
525 X509_NAME *subject ;
526 X509_PUBKEY *key ;
527 ASN1_BIT_STRING *issuerUID ;
528 ASN1_BIT_STRING *subjectUID ;
529 STACK *extensions ;
530};
531typedef struct x509_cinf_st X509_CINF;
532struct x509_cert_aux_st {
533 STACK *trust ;
534 STACK *reject ;
535 ASN1_UTF8STRING *alias ;
536 ASN1_OCTET_STRING *keyid ;
537 STACK *other ;
538};
539typedef struct x509_cert_aux_st X509_CERT_AUX;
540struct AUTHORITY_KEYID_st;
541struct AUTHORITY_KEYID_st;
542struct x509_st {
543 X509_CINF *cert_info ;
544 X509_ALGOR *sig_alg ;
545 ASN1_BIT_STRING *signature ;
546 int valid ;
547 int references ;
548 char *name ;
549 CRYPTO_EX_DATA ex_data ;
550 long ex_pathlen ;
551 unsigned long ex_flags ;
552 unsigned long ex_kusage ;
553 unsigned long ex_xkusage ;
554 unsigned long ex_nscert ;
555 ASN1_OCTET_STRING *skid ;
556 struct AUTHORITY_KEYID_st *akid ;
557 unsigned char sha1_hash[20] ;
558 X509_CERT_AUX *aux ;
559};
560typedef struct x509_st X509;
561struct lhash_node_st {
562 void *data ;
563 struct lhash_node_st *next ;
564 unsigned long hash ;
565};
566typedef struct lhash_node_st LHASH_NODE;
567struct lhash_st {
568 LHASH_NODE **b ;
569 int (*comp)() ;
570 unsigned long (*hash)() ;
571 unsigned int num_nodes ;
572 unsigned int num_alloc_nodes ;
573 unsigned int p ;
574 unsigned int pmax ;
575 unsigned long up_load ;
576 unsigned long down_load ;
577 unsigned long num_items ;
578 unsigned long num_expands ;
579 unsigned long num_expand_reallocs ;
580 unsigned long num_contracts ;
581 unsigned long num_contract_reallocs ;
582 unsigned long num_hash_calls ;
583 unsigned long num_comp_calls ;
584 unsigned long num_insert ;
585 unsigned long num_replace ;
586 unsigned long num_delete ;
587 unsigned long num_no_delete ;
588 unsigned long num_retrieve ;
589 unsigned long num_retrieve_miss ;
590 unsigned long num_hash_comps ;
591 int error ;
592};
593struct x509_store_ctx_st;
594struct x509_store_ctx_st;
595typedef struct x509_store_ctx_st X509_STORE_CTX;
596struct x509_store_st {
597 int cache ;
598 STACK *objs ;
599 STACK *get_cert_methods ;
600 int (*verify)(X509_STORE_CTX *ctx ) ;
601 int (*verify_cb)(int ok , X509_STORE_CTX *ctx ) ;
602 CRYPTO_EX_DATA ex_data ;
603 int references ;
604 int depth ;
605};
606typedef struct x509_store_st X509_STORE;
607struct x509_store_ctx_st {
608 X509_STORE *ctx ;
609 int current_method ;
610 X509 *cert ;
611 STACK *untrusted ;
612 int purpose ;
613 int trust ;
614 time_t check_time ;
615 unsigned long flags ;
616 void *other_ctx ;
617 int (*verify)(X509_STORE_CTX *ctx ) ;
618 int (*verify_cb)(int ok , X509_STORE_CTX *ctx ) ;
619 int (*get_issuer)(X509 **issuer , X509_STORE_CTX *ctx , X509 *x ) ;
620 int (*check_issued)(X509_STORE_CTX *ctx , X509 *x , X509 *issuer ) ;
621 int (*cleanup)(X509_STORE_CTX *ctx ) ;
622 int depth ;
623 int valid ;
624 int last_untrusted ;
625 STACK *chain ;
626 int error_depth ;
627 int error ;
628 X509 *current_cert ;
629 X509 *current_issuer ;
630 CRYPTO_EX_DATA ex_data ;
631};
632struct comp_method_st {
633 int type ;
634 char const *name ;
635 int (*init)() ;
636 void (*finish)() ;
637 int (*compress)() ;
638 int (*expand)() ;
639 long (*ctrl)() ;
640 long (*callback_ctrl)() ;
641};
642typedef struct comp_method_st COMP_METHOD;
643struct comp_ctx_st {
644 COMP_METHOD *meth ;
645 unsigned long compress_in ;
646 unsigned long compress_out ;
647 unsigned long expand_in ;
648 unsigned long expand_out ;
649 CRYPTO_EX_DATA ex_data ;
650};
651typedef struct comp_ctx_st COMP_CTX;
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 ) ;
1022extern void ERR_put_error(int lib , int func , int reason , char const *file , int line ) ;
1023SSL_METHOD *SSLv3_server_method(void) ;
1024extern SSL_METHOD *sslv3_base_method(void) ;
1025extern X509 *ssl_get_server_send_cert(SSL * ) ;
1026int ssl3_send_server_certificate(SSL *s ) ;
1027extern int ssl3_do_write(SSL *s , int type ) ;
1028extern unsigned long ssl3_output_cert_chain(SSL *s , X509 *x ) ;
1029int ssl3_accept(SSL *s ) ;
1030static SSL_METHOD *ssl3_get_server_method(int ver ) ;
1031static SSL_METHOD *ssl3_get_server_method(int ver )
1032{ SSL_METHOD *tmp ;
1033
1034 {
1035 if (ver == 768) {
1036 {
1037 tmp = SSLv3_server_method();
1038 }
1039 return (tmp);
1040 } else {
1041 return ((SSL_METHOD *)((void *)0));
1042 }
1043}
1044}
1045static int init = 1;
1046static SSL_METHOD SSLv3_server_data ;
1047SSL_METHOD *SSLv3_server_method(void)
1048{ char *tmp ;
1049 SSL_METHOD *tmp___0 ;
1050
1051 {
1052 if (init) {
1053 {
1054 tmp___0 = sslv3_base_method();
1055 tmp = (char *)tmp___0;
1056 memcpy((void *)((char *)(& SSLv3_server_data)), (void const *)tmp, sizeof(SSL_METHOD ));
1057 SSLv3_server_data.ssl_accept = & ssl3_accept;
1058 SSLv3_server_data.get_ssl_method = & ssl3_get_server_method;
1059 init = 0;
1060 }
1061 } else {
1062
1063 }
1064 return (& SSLv3_server_data);
1065}
1066}
1067int main(void)
1068{ SSL *s ;
1069 int tmp ;
1070
1071 {
1072 {
1073 s = malloc(sizeof(SSL));
1074 s->s3 = malloc(sizeof(struct ssl3_state_st));
1075 tmp = ssl3_accept(s);
1076 }
1077 return (tmp);
1078}
1079}
1080int ssl3_accept(SSL *s )
1081{ BUF_MEM *buf ;
1082 unsigned long l ;
1083 unsigned long Time ;
1084 unsigned long tmp ;
1085 void (*cb)() ;
1086 long num1 ;
1087 int ret ;
1088 int new_state ;
1089 int state ;
1090 int skip ;
1091 int got_new_session ;
1092 int tmp___1 = __VERIFIER_nondet_int() ;
1093 int tmp___2 = __VERIFIER_nondet_int() ;
1094 int tmp___3 = __VERIFIER_nondet_int() ;
1095 int tmp___4 = __VERIFIER_nondet_int() ;
1096 int tmp___5 = __VERIFIER_nondet_int() ;
1097 int tmp___6 = __VERIFIER_nondet_int() ;
1098 int tmp___7 ;
1099 long tmp___8 = __VERIFIER_nondet_long() ;
1100 int tmp___9 = __VERIFIER_nondet_int() ;
1101 int tmp___10 = __VERIFIER_nondet_int() ;
1102 int blastFlag ;
1103
1104
1105 {
1106 s->state = 8464;
1107 blastFlag = 0;
1108 s->hit=__VERIFIER_nondet_int ();
1109 s->state = 8464;
1110 tmp = __VERIFIER_nondet_int();
1111 Time = tmp;
1112 cb = (void (*)())((void *)0);
1113 ret = -1;
1114 skip = 0;
1115 got_new_session = 0;
1116 if ((unsigned long )s->info_callback != (unsigned long )((void *)0)) {
1117 cb = s->info_callback;
1118 } else {
1119
1120 }
1121 s->in_handshake += 1;
1122 if (tmp___1 & 12288) {
1123 if (tmp___2 & 16384) {
1124
1125 } else {
1126
1127 }
1128 } else {
1129
1130 }
1131 if ((unsigned long )s->cert == (unsigned long )((void *)0)) {
1132 return (-1);
1133 } else {
1134
1135 }
1136 {
1137 while (1) {
1138 while_0_continue: ;
1139 state = s->state;
1140 if (s->state == 12292) {
1141 goto switch_1_12292;
1142 } else {
1143 if (s->state == 16384) {
1144 goto switch_1_16384;
1145 } else {
1146 if (s->state == 8192) {
1147 goto switch_1_8192;
1148 } else {
1149 if (s->state == 24576) {
1150 goto switch_1_24576;
1151 } else {
1152 if (s->state == 8195) {
1153 goto switch_1_8195;
1154 } else {
1155 if (s->state == 8480) {
1156 goto switch_1_8480;
1157 } else {
1158 if (s->state == 8481) {
1159 goto switch_1_8481;
1160 } else {
1161 if (s->state == 8482) {
1162 goto switch_1_8482;
1163 } else {
1164 if (s->state == 8464) {
1165 goto switch_1_8464;
1166 } else {
1167 if (s->state == 8465) {
1168 goto switch_1_8465;
1169 } else {
1170 if (s->state == 8466) {
1171 goto switch_1_8466;
1172 } else {
1173 if (s->state == 8496) {
1174 goto switch_1_8496;
1175 } else {
1176 if (s->state == 8497) {
1177 goto switch_1_8497;
1178 } else {
1179 if (s->state == 8512) {
1180 goto switch_1_8512;
1181 } else {
1182 if (s->state == 8513) {
1183 goto switch_1_8513;
1184 } else {
1185 if (s->state == 8528) {
1186 goto switch_1_8528;
1187 } else {
1188 if (s->state == 8529) {
1189 goto switch_1_8529;
1190 } else {
1191 if (s->state == 8544) {
1192 goto switch_1_8544;
1193 } else {
1194 if (s->state == 8545) {
1195 goto switch_1_8545;
1196 } else {
1197 if (s->state == 8560) {
1198 goto switch_1_8560;
1199 } else {
1200 if (s->state == 8561) {
1201 goto switch_1_8561;
1202 } else {
1203 if (s->state == 8448) {
1204 goto switch_1_8448;
1205 } else {
1206 if (s->state == 8576) {
1207 goto switch_1_8576;
1208 } else {
1209 if (s->state == 8577) {
1210 goto switch_1_8577;
1211 } else {
1212 if (s->state == 8592) {
1213 goto switch_1_8592;
1214 } else {
1215 if (s->state == 8593) {
1216 goto switch_1_8593;
1217 } else {
1218 if (s->state == 8608) {
1219 goto switch_1_8608;
1220 } else {
1221 if (s->state == 8609) {
1222 goto switch_1_8609;
1223 } else {
1224 if (s->state == 8640) {
1225 goto switch_1_8640;
1226 } else {
1227 if (s->state == 8641) {
1228 goto switch_1_8641;
1229 } else {
1230 if (s->state == 8656) {
1231 goto switch_1_8656;
1232 } else {
1233 if (s->state == 8657) {
1234 goto switch_1_8657;
1235 } else {
1236 if (s->state == 8672) {
1237 goto switch_1_8672;
1238 } else {
1239 if (s->state == 8673) {
1240 goto switch_1_8673;
1241 } else {
1242 if (s->state == 3) {
1243 goto switch_1_3;
1244 } else {
1245 {
1246 goto switch_1_default;
1247 if (0) {
1248 switch_1_12292:
1249 s->new_session = 1;
1250 switch_1_16384: ;
1251 switch_1_8192: ;
1252 switch_1_24576: ;
1253 switch_1_8195:
1254 s->server = 1;
1255 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1256
1257 } else {
1258
1259 }
1260 if (s->version >> 8 != 3) {
1261 return (-1);
1262 } else {
1263
1264 }
1265 s->type = 8192;
1266 if ((unsigned long )s->init_buf == (unsigned long )((void *)0)) {
1267 buf = __VERIFIER_nondet_pointer();
1268 if ((unsigned long )buf == (unsigned long )((void *)0)) {
1269 ret = -1;
1270 goto end;
1271 } else {
1272
1273 }
1274 if (! tmp___3) {
1275 ret = -1;
1276 goto end;
1277 } else {
1278
1279 }
1280 s->init_buf = buf;
1281 } else {
1282
1283 }
1284 if (! tmp___4) {
1285 ret = -1;
1286 goto end;
1287 } else {
1288
1289 }
1290 s->init_num = 0;
1291 if (s->state != 12292) {
1292 if (! tmp___5) {
1293 ret = -1;
1294 goto end;
1295 } else {
1296
1297 }
1298 s->state = 8464;
1299 (s->ctx)->stats.sess_accept += 1;
1300 } else {
1301 (s->ctx)->stats.sess_accept_renegotiate += 1;
1302 s->state = 8480;
1303 }
1304 goto switch_1_break;
1305 switch_1_8480: ;
1306 switch_1_8481:
1307 s->shutdown = 0;
1308 ret = __VERIFIER_nondet_int();
1309 if (ret <= 0) {
1310 goto end;
1311 } else {
1312
1313 }
1314 (s->s3)->tmp.next_state = 8482;
1315 s->state = 8448;
1316 s->init_num = 0;
1317 goto switch_1_break;
1318 switch_1_8482:
1319 s->state = 3;
1320 goto switch_1_break;
1321 switch_1_8464: ;
1322 switch_1_8465: ;
1323 switch_1_8466:
1324 s->shutdown = 0;
1325 ret = __VERIFIER_nondet_int();
1326 if (blastFlag == 0) {
1327 blastFlag = 1;
1328 } else {
1329
1330 }
1331 if (ret <= 0) {
1332 goto end;
1333 } else {
1334
1335 }
1336 got_new_session = 1;
1337 s->state = 8496;
1338 s->init_num = 0;
1339 goto switch_1_break;
1340 switch_1_8496: ;
1341 switch_1_8497:
1342 ret = __VERIFIER_nondet_int();
1343 if (blastFlag == 1) {
1344 blastFlag = 2;
1345 } else {
1346
1347 }
1348 if (ret <= 0) {
1349 goto end;
1350 } else {
1351
1352 }
1353 if (s->hit) {
1354 s->state = 8656;
1355 } else {
1356 s->state = 8512;
1357 }
1358 s->init_num = 0;
1359 goto switch_1_break;
1360 switch_1_8512: ;
1361 switch_1_8513: ;
1362 if (((s->s3)->tmp.new_cipher)->algorithms & 256UL) {
1363 skip = 1;
1364 } else {
1365 ret = __VERIFIER_nondet_int();
1366 if (blastFlag == 2) {
1367 blastFlag = 3;
1368 } else {
1369
1370 }
1371 if (ret <= 0) {
1372 goto end;
1373 } else {
1374
1375 }
1376 }
1377 s->state = 8528;
1378 s->init_num = 0;
1379 goto switch_1_break;
1380 switch_1_8528: ;
1381 switch_1_8529:
1382 l = ((s->s3)->tmp.new_cipher)->algorithms;
1383 if (s->options & 2097152UL) {
1384 (s->s3)->tmp.use_rsa_tmp = 1;
1385 } else {
1386 (s->s3)->tmp.use_rsa_tmp = 0;
1387 }
1388 if ((s->s3)->tmp.use_rsa_tmp) {
1389 goto _L___0;
1390 } else {
1391 if (l & 30UL) {
1392 goto _L___0;
1393 } else {
1394 if (l & 1UL) {
1395 if ((unsigned long )(s->cert)->pkeys[0].privatekey == (unsigned long )((void *)0)) {
1396 goto _L___0;
1397 } else {
1398 if (((s->s3)->tmp.new_cipher)->algo_strength & 2UL) {
1399 if (((s->s3)->tmp.new_cipher)->algo_strength & 4UL) {
1400 tmp___7 = 512;
1401 } else {
1402 tmp___7 = 1024;
1403 }
1404 if (tmp___6 * 8 > tmp___7) {
1405 _L___0:
1406 ret = __VERIFIER_nondet_int();
1407 if (blastFlag == 3) {
1408 blastFlag = 4;
1409 } else {
1410
1411 }
1412 if (ret <= 0) {
1413 goto end;
1414 } else {
1415
1416 }
1417 } else {
1418 skip = 1;
1419 }
1420 } else {
1421 skip = 1;
1422 }
1423 }
1424 } else {
1425 skip = 1;
1426 }
1427 }
1428 }
1429 s->state = 8544;
1430 s->init_num = 0;
1431 goto switch_1_break;
1432 switch_1_8544: ;
1433 switch_1_8545: ;
1434 if (s->verify_mode & 1) {
1435 if ((unsigned long )(s->session)->peer != (unsigned long )((void *)0)) {
1436 if (s->verify_mode & 4) {
1437 skip = 1;
1438 (s->s3)->tmp.cert_request = 0;
1439 s->state = 8560;
1440 } else {
1441 goto _L___2;
1442 }
1443 } else {
1444 _L___2:
1445 if (((s->s3)->tmp.new_cipher)->algorithms & 256UL) {
1446 if (s->verify_mode & 2) {
1447 goto _L___1;
1448 } else {
1449 skip = 1;
1450 (s->s3)->tmp.cert_request = 0;
1451 s->state = 8560;
1452 }
1453 } else {
1454 _L___1:
1455 (s->s3)->tmp.cert_request = 1;
1456 ret = __VERIFIER_nondet_int();
1457 if (blastFlag == 4) {
1458 blastFlag = 5;
1459 } else {
1460
1461 }
1462 if (ret <= 0) {
1463 goto end;
1464 } else {
1465
1466 }
1467 s->state = 8448;
1468 (s->s3)->tmp.next_state = 8576;
1469 s->init_num = 0;
1470 }
1471 }
1472 } else {
1473 skip = 1;
1474 (s->s3)->tmp.cert_request = 0;
1475 s->state = 8560;
1476 }
1477 goto switch_1_break;
1478 switch_1_8560: ;
1479 switch_1_8561:
1480 ret = __VERIFIER_nondet_int();
1481 if (ret <= 0) {
1482 goto end;
1483 } else {
1484
1485 }
1486 (s->s3)->tmp.next_state = 8576;
1487 s->state = 8448;
1488 s->init_num = 0;
1489 goto switch_1_break;
1490 switch_1_8448:
1491 if (num1 > 0L) {
1492 s->rwstate = 2;
1493 num1 = (long )((int )tmp___8);
1494 if (num1 <= 0L) {
1495 ret = -1;
1496 goto end;
1497 } else {
1498
1499 }
1500 s->rwstate = 1;
1501 } else {
1502
1503 }
1504 s->state = (s->s3)->tmp.next_state;
1505 goto switch_1_break;
1506 switch_1_8576: ;
1507 switch_1_8577:
1508 ret = __VERIFIER_nondet_int();
1509 if (blastFlag == 5) {
1510 blastFlag = 6;
1511 } else {
1512
1513 }
1514 if (ret <= 0) {
1515 goto end;
1516 } else {
1517
1518 }
1519 if (ret == 2) {
1520 s->state = 8466;
1521 } else {
1522 ret = __VERIFIER_nondet_int();
1523 if (blastFlag == 6) {
1524 blastFlag = 7;
1525 } else {
1526
1527 }
1528 if (ret <= 0) {
1529 goto end;
1530 } else {
1531
1532 }
1533 s->init_num = 0;
1534 s->state = 8592;
1535 }
1536 goto switch_1_break;
1537 switch_1_8592: ;
1538 switch_1_8593:
1539 ret = __VERIFIER_nondet_int();
1540 if (blastFlag == 7) {
1541 blastFlag = 8;
1542 } else {
1543
1544 }
1545 if (ret <= 0) {
1546 goto end;
1547 } else {
1548
1549 }
1550 s->state = 8608;
1551 s->init_num = 0;
1552 goto switch_1_break;
1553 switch_1_8608: ;
1554 switch_1_8609:
1555 ret = __VERIFIER_nondet_int();
1556 if (blastFlag == 8) {
1557 blastFlag = 9;
1558 } else {
1559
1560 }
1561 if (ret <= 0) {
1562 goto end;
1563 } else {
1564
1565 }
1566 s->state = 8640;
1567 s->init_num = 0;
1568 goto switch_1_break;
1569 switch_1_8640: ;
1570 switch_1_8641:
1571 ret = __VERIFIER_nondet_int();
1572 if (blastFlag == 9) {
1573 blastFlag = 10;
1574 } else {
1575 if (blastFlag == 12) {
1576 blastFlag = 13;
1577 } else {
1578 if (blastFlag == 15) {
1579 blastFlag = 16;
1580 } else {
1581 if (blastFlag == 18) {
1582 blastFlag = 19;
1583 } else {
1584 goto ERROR;
1585 }
1586 }
1587 }
1588 }
1589 if (ret <= 0) {
1590 goto end;
1591 } else {
1592
1593 }
1594 if (s->hit) {
1595 s->state = 3;
1596 } else {
1597 s->state = 8656;
1598 }
1599 s->init_num = 0;
1600 goto switch_1_break;
1601 switch_1_8656: ;
1602 switch_1_8657:
1603 (s->session)->cipher = (s->s3)->tmp.new_cipher;
1604 if (! tmp___9) {
1605 ret = -1;
1606 goto end;
1607 } else {
1608
1609 }
1610 ret = __VERIFIER_nondet_int();
1611 if (blastFlag == 10) {
1612 blastFlag = 11;
1613 } else {
1614 if (blastFlag == 13) {
1615 blastFlag = 14;
1616 } else {
1617 if (blastFlag == 16) {
1618 blastFlag = 17;
1619 } else {
1620 if (blastFlag == 19) {
1621 blastFlag = 20;
1622 } else {
1623
1624 }
1625 }
1626 }
1627 }
1628 if (ret <= 0) {
1629 goto end;
1630 } else {
1631
1632 }
1633 s->state = 8672;
1634 s->init_num = 0;
1635 if (! tmp___10) {
1636 ret = -1;
1637 goto end;
1638 } else {
1639
1640 }
1641 goto switch_1_break;
1642 switch_1_8672: ;
1643 switch_1_8673:
1644 ret = __VERIFIER_nondet_int();
1645 if (blastFlag == 11) {
1646 blastFlag = 12;
1647 } else {
1648 if (blastFlag == 14) {
1649 blastFlag = 15;
1650 } else {
1651 if (blastFlag == 17) {
1652 blastFlag = 18;
1653 } else {
1654 if (blastFlag == 20) {
1655 blastFlag = 21;
1656 } else {
1657
1658 }
1659 }
1660 }
1661 }
1662 if (ret <= 0) {
1663 goto end;
1664 } else {
1665
1666 }
1667 s->state = 8448;
1668 if (s->hit) {
1669 (s->s3)->tmp.next_state = 8640;
1670 } else {
1671 (s->s3)->tmp.next_state = 3;
1672 }
1673 s->init_num = 0;
1674 goto switch_1_break;
1675 switch_1_3:
1676 s->init_buf = (BUF_MEM *)((void *)0);
1677 s->init_num = 0;
1678 if (got_new_session) {
1679 s->new_session = 0;
1680 (s->ctx)->stats.sess_accept_good += 1;
1681 s->handshake_func = (int (*)())(& ssl3_accept);
1682 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1683
1684 } else {
1685
1686 }
1687 } else {
1688
1689 }
1690 ret = 1;
1691 goto end;
1692 switch_1_default:
1693 ret = -1;
1694 goto end;
1695 } else {
1696 switch_1_break: ;
1697 }
1698 }
1699 }
1700 }
1701 }
1702 }
1703 }
1704 }
1705 }
1706 }
1707 }
1708 }
1709 }
1710 }
1711 }
1712 }
1713 }
1714 }
1715 }
1716 }
1717 }
1718 }
1719 }
1720 }
1721 }
1722 }
1723 }
1724 }
1725 }
1726 }
1727 }
1728 }
1729 }
1730 }
1731 }
1732 }
1733 }
1734 if (! (s->s3)->tmp.reuse_message) {
1735 if (! skip) {
1736 if (s->debug) {
1737 ret = __VERIFIER_nondet_int();
1738 if (ret <= 0) {
1739 goto end;
1740 } else {
1741
1742 }
1743 } else {
1744
1745 }
1746 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1747 if (s->state != state) {
1748 new_state = s->state;
1749 s->state = state;
1750 s->state = new_state;
1751 } else {
1752
1753 }
1754 } else {
1755
1756 }
1757 } else {
1758
1759 }
1760 } else {
1761
1762 }
1763 skip = 0;
1764 }
1765 while_0_break: ;
1766 }
1767 end:
1768 s->in_handshake -= 1;
1769 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1770
1771 } else {
1772
1773 }
1774 return (ret);
1775 ERROR:
1776 goto ERROR;
1777}
1778}
1779int ssl3_send_server_certificate(SSL *s )
1780{ unsigned long l ;
1781 X509 *x ;
1782 int tmp ;
1783
1784 {
1785 if (s->state == 8512) {
1786 {
1787 x = ssl_get_server_send_cert(s);
1788 }
1789 if ((unsigned long )x == (unsigned long )((void *)0)) {
1790 {
1791 ERR_put_error(20, 154, 157, "s3_srvr.c", 1844);
1792 }
1793 return (0);
1794 } else {
1795
1796 }
1797 {
1798 l = ssl3_output_cert_chain(s, x);
1799 s->state = 8513;
1800 s->init_num = (int )l;
1801 s->init_off = 0;
1802 }
1803 } else {
1804
1805 }
1806 {
1807 tmp = ssl3_do_write(s, 22);
1808 }
1809 return (tmp);
1810}
1811}