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 s->state = 8464;
1076 tmp = ssl3_accept(s);
1077 }
1078 return (tmp);
1079}
1080}
1081int ssl3_accept(SSL *s )
1082{ BUF_MEM *buf ;
1083 unsigned long l ;
1084 unsigned long Time ;
1085 unsigned long tmp ;
1086 void (*cb)() ;
1087 long num1 ;
1088 int ret ;
1089 int new_state ;
1090 int state ;
1091 int skip ;
1092 int got_new_session ;
1093 int tmp___1 = __VERIFIER_nondet_int() ;
1094 int tmp___2 = __VERIFIER_nondet_int() ;
1095 int tmp___3 = __VERIFIER_nondet_int() ;
1096 int tmp___4 = __VERIFIER_nondet_int() ;
1097 int tmp___5 = __VERIFIER_nondet_int() ;
1098 int tmp___6 = __VERIFIER_nondet_int() ;
1099 int tmp___7 ;
1100 long tmp___8 = __VERIFIER_nondet_long() ;
1101 int tmp___9 = __VERIFIER_nondet_int() ;
1102 int tmp___10 = __VERIFIER_nondet_int() ;
1103 int blastFlag ;
1104
1105
1106 {
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 (ret <= 0) {
1367 goto end;
1368 } else {
1369
1370 }
1371 }
1372 s->state = 8528;
1373 s->init_num = 0;
1374 goto switch_1_break;
1375 switch_1_8528: ;
1376 switch_1_8529:
1377 l = ((s->s3)->tmp.new_cipher)->algorithms;
1378 if (s->options & 2097152UL) {
1379 (s->s3)->tmp.use_rsa_tmp = 1;
1380 } else {
1381 (s->s3)->tmp.use_rsa_tmp = 0;
1382 }
1383 if ((s->s3)->tmp.use_rsa_tmp) {
1384 goto _L___0;
1385 } else {
1386 if (l & 30UL) {
1387 goto _L___0;
1388 } else {
1389 if (l & 1UL) {
1390 if ((unsigned long )(s->cert)->pkeys[0].privatekey == (unsigned long )((void *)0)) {
1391 goto _L___0;
1392 } else {
1393 if (((s->s3)->tmp.new_cipher)->algo_strength & 2UL) {
1394 if (((s->s3)->tmp.new_cipher)->algo_strength & 4UL) {
1395 tmp___7 = 512;
1396 } else {
1397 tmp___7 = 1024;
1398 }
1399 if (tmp___6 * 8 > tmp___7) {
1400 _L___0:
1401 ret = __VERIFIER_nondet_int();
1402 if (ret <= 0) {
1403 goto end;
1404 } else {
1405
1406 }
1407 } else {
1408 skip = 1;
1409 }
1410 } else {
1411 skip = 1;
1412 }
1413 }
1414 } else {
1415 skip = 1;
1416 }
1417 }
1418 }
1419 s->state = 8544;
1420 s->init_num = 0;
1421 goto switch_1_break;
1422 switch_1_8544: ;
1423 switch_1_8545: ;
1424 if (s->verify_mode & 1) {
1425 if ((unsigned long )(s->session)->peer != (unsigned long )((void *)0)) {
1426 if (s->verify_mode & 4) {
1427 skip = 1;
1428 (s->s3)->tmp.cert_request = 0;
1429 s->state = 8560;
1430 } else {
1431 goto _L___2;
1432 }
1433 } else {
1434 _L___2:
1435 if (((s->s3)->tmp.new_cipher)->algorithms & 256UL) {
1436 if (s->verify_mode & 2) {
1437 goto _L___1;
1438 } else {
1439 skip = 1;
1440 (s->s3)->tmp.cert_request = 0;
1441 s->state = 8560;
1442 }
1443 } else {
1444 _L___1:
1445 (s->s3)->tmp.cert_request = 1;
1446 ret = __VERIFIER_nondet_int();
1447 if (ret <= 0) {
1448 goto end;
1449 } else {
1450
1451 }
1452 s->state = 8448;
1453 (s->s3)->tmp.next_state = 8576;
1454 s->init_num = 0;
1455 }
1456 }
1457 } else {
1458 skip = 1;
1459 (s->s3)->tmp.cert_request = 0;
1460 s->state = 8560;
1461 }
1462 goto switch_1_break;
1463 switch_1_8560: ;
1464 switch_1_8561:
1465 ret = __VERIFIER_nondet_int();
1466 if (ret <= 0) {
1467 goto end;
1468 } else {
1469
1470 }
1471 (s->s3)->tmp.next_state = 8576;
1472 s->state = 8448;
1473 s->init_num = 0;
1474 goto switch_1_break;
1475 switch_1_8448:
1476 if (num1 > 0L) {
1477 s->rwstate = 2;
1478 num1 = (long )((int )tmp___8);
1479 if (num1 <= 0L) {
1480 ret = -1;
1481 goto end;
1482 } else {
1483
1484 }
1485 s->rwstate = 1;
1486 } else {
1487
1488 }
1489 s->state = (s->s3)->tmp.next_state;
1490 goto switch_1_break;
1491 switch_1_8576: ;
1492 switch_1_8577:
1493 ret = __VERIFIER_nondet_int();
1494 if (ret <= 0) {
1495 goto end;
1496 } else {
1497
1498 }
1499 if (ret == 2) {
1500 s->state = 8466;
1501 } else {
1502 ret = __VERIFIER_nondet_int();
1503 if (ret <= 0) {
1504 goto end;
1505 } else {
1506
1507 }
1508 s->init_num = 0;
1509 s->state = 8592;
1510 }
1511 goto switch_1_break;
1512 switch_1_8592: ;
1513 switch_1_8593:
1514 ret = __VERIFIER_nondet_int();
1515 if (ret <= 0) {
1516 goto end;
1517 } else {
1518
1519 }
1520 s->state = 8608;
1521 s->init_num = 0;
1522 goto switch_1_break;
1523 switch_1_8608: ;
1524 switch_1_8609:
1525 ret = __VERIFIER_nondet_int();
1526 if (ret <= 0) {
1527 goto end;
1528 } else {
1529
1530 }
1531 s->state = 8640;
1532 s->init_num = 0;
1533 goto switch_1_break;
1534 switch_1_8640: ;
1535 switch_1_8641:
1536 ret = __VERIFIER_nondet_int();
1537 if (ret <= 0) {
1538 goto end;
1539 } else {
1540
1541 }
1542 if (s->hit) {
1543 s->state = 3;
1544 } else {
1545 s->state = 8656;
1546 }
1547 s->init_num = 0;
1548 goto switch_1_break;
1549 switch_1_8656: ;
1550 switch_1_8657:
1551 (s->session)->cipher = (s->s3)->tmp.new_cipher;
1552 if (! tmp___9) {
1553 ret = -1;
1554 goto end;
1555 } else {
1556
1557 }
1558 ret = __VERIFIER_nondet_int();
1559 if (blastFlag == 2) {
1560 blastFlag = 4;
1561 } else {
1562 if (blastFlag == 3) {
1563 blastFlag = 4;
1564 } else {
1565
1566 }
1567 }
1568 if (ret <= 0) {
1569 goto end;
1570 } else {
1571
1572 }
1573 s->state = 8672;
1574 s->init_num = 0;
1575 if (! tmp___10) {
1576 ret = -1;
1577 goto end;
1578 } else {
1579
1580 }
1581 goto switch_1_break;
1582 switch_1_8672: ;
1583 switch_1_8673:
1584 ret = __VERIFIER_nondet_int();
1585 if (blastFlag == 4) {
1586 goto ERROR;
1587 } else {
1588
1589 }
1590 if (ret <= 0) {
1591 goto end;
1592 } else {
1593
1594 }
1595 s->state = 8448;
1596 if (s->hit) {
1597 (s->s3)->tmp.next_state = 8640;
1598 } else {
1599 (s->s3)->tmp.next_state = 3;
1600 }
1601 s->init_num = 0;
1602 goto switch_1_break;
1603 switch_1_3:
1604 s->init_buf = (BUF_MEM *)((void *)0);
1605 s->init_num = 0;
1606 if (got_new_session) {
1607 s->new_session = 0;
1608 (s->ctx)->stats.sess_accept_good += 1;
1609 s->handshake_func = (int (*)())(& ssl3_accept);
1610 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1611
1612 } else {
1613
1614 }
1615 } else {
1616
1617 }
1618 ret = 1;
1619 goto end;
1620 switch_1_default:
1621 ret = -1;
1622 goto end;
1623 } else {
1624 switch_1_break: ;
1625 }
1626 }
1627 }
1628 }
1629 }
1630 }
1631 }
1632 }
1633 }
1634 }
1635 }
1636 }
1637 }
1638 }
1639 }
1640 }
1641 }
1642 }
1643 }
1644 }
1645 }
1646 }
1647 }
1648 }
1649 }
1650 }
1651 }
1652 }
1653 }
1654 }
1655 }
1656 }
1657 }
1658 }
1659 }
1660 }
1661 }
1662 if (! (s->s3)->tmp.reuse_message) {
1663 if (! skip) {
1664 if (s->debug) {
1665 ret = __VERIFIER_nondet_int();
1666 if (ret <= 0) {
1667 goto end;
1668 } else {
1669
1670 }
1671 } else {
1672
1673 }
1674 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1675 if (s->state != state) {
1676 new_state = s->state;
1677 s->state = state;
1678 s->state = new_state;
1679 } else {
1680
1681 }
1682 } else {
1683
1684 }
1685 } else {
1686
1687 }
1688 } else {
1689
1690 }
1691 skip = 0;
1692 }
1693 while_0_break: ;
1694 }
1695 end:
1696 s->in_handshake -= 1;
1697 if ((unsigned long )cb != (unsigned long )((void *)0)) {
1698
1699 } else {
1700
1701 }
1702 return (ret);
1703 ERROR:
1704 goto ERROR;
1705}
1706}
1707int ssl3_send_server_certificate(SSL *s )
1708{ unsigned long l ;
1709 X509 *x ;
1710 int tmp ;
1711
1712 {
1713 if (s->state == 8512) {
1714 {
1715 x = ssl_get_server_send_cert(s);
1716 }
1717 if ((unsigned long )x == (unsigned long )((void *)0)) {
1718 {
1719 ERR_put_error(20, 154, 157, "s3_srvr.c", 1844);
1720 }
1721 return (0);
1722 } else {
1723
1724 }
1725 {
1726 l = ssl3_output_cert_chain(s, x);
1727 s->state = 8513;
1728 s->init_num = (int )l;
1729 s->init_off = 0;
1730 }
1731 } else {
1732
1733 }
1734 {
1735 tmp = ssl3_do_write(s, 22);
1736 }
1737 return (tmp);
1738}
1739}