extern void __VERIFIER_error() __attribute__ ((__noreturn__)); extern void *malloc(unsigned int sz ); extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); extern void *__VERIFIER_nondet_pointer(void); /* Generated by CIL v. 1.3.6 */ /* print_CIL_Input is true */ extern int __VERIFIER_nondet_int(); typedef unsigned int size_t; typedef long __time_t; struct buf_mem_st { int length ; char *data ; int max ; }; typedef struct buf_mem_st BUF_MEM; typedef __time_t time_t; struct stack_st { int num ; char **data ; int sorted ; int num_alloc ; int (*comp)(char const * const * , char const * const * ) ; }; typedef struct stack_st STACK; struct bio_st; struct bio_st; struct crypto_ex_data_st { STACK *sk ; int dummy ; }; typedef struct crypto_ex_data_st CRYPTO_EX_DATA; typedef struct bio_st BIO; typedef void bio_info_cb(struct bio_st * , int , char const * , int , long , long ); struct bio_method_st { int type ; char const *name ; int (*bwrite)(BIO * , char const * , int ) ; int (*bread)(BIO * , char * , int ) ; int (*bputs)(BIO * , char const * ) ; int (*bgets)(BIO * , char * , int ) ; long (*ctrl)(BIO * , int , long , void * ) ; int (*create)(BIO * ) ; int (*destroy)(BIO * ) ; long (*callback_ctrl)(BIO * , int , bio_info_cb * ) ; }; typedef struct bio_method_st BIO_METHOD; struct bio_st { BIO_METHOD *method ; long (*callback)(struct bio_st * , int , char const * , int , long , long ) ; char *cb_arg ; int init ; int shutdown ; int flags ; int retry_reason ; int num ; void *ptr ; struct bio_st *next_bio ; struct bio_st *prev_bio ; int references ; unsigned long num_read ; unsigned long num_write ; CRYPTO_EX_DATA ex_data ; }; struct bignum_st { unsigned long *d ; int top ; int dmax ; int neg ; int flags ; }; typedef struct bignum_st BIGNUM; struct bignum_ctx { int tos ; BIGNUM bn[16] ; int flags ; int depth ; int pos[12] ; int too_many ; }; typedef struct bignum_ctx BN_CTX; struct bn_blinding_st { int init ; BIGNUM *A ; BIGNUM *Ai ; BIGNUM *mod ; }; typedef struct bn_blinding_st BN_BLINDING; struct bn_mont_ctx_st { int ri ; BIGNUM RR ; BIGNUM N ; BIGNUM Ni ; unsigned long n0 ; int flags ; }; typedef struct bn_mont_ctx_st BN_MONT_CTX; struct X509_algor_st; struct X509_algor_st; struct X509_algor_st; struct asn1_object_st { char const *sn ; char const *ln ; int nid ; int length ; unsigned char *data ; int flags ; }; typedef struct asn1_object_st ASN1_OBJECT; struct asn1_string_st { int length ; int type ; unsigned char *data ; long flags ; }; typedef struct asn1_string_st ASN1_STRING; typedef struct asn1_string_st ASN1_INTEGER; typedef struct asn1_string_st ASN1_ENUMERATED; typedef struct asn1_string_st ASN1_BIT_STRING; typedef struct asn1_string_st ASN1_OCTET_STRING; typedef struct asn1_string_st ASN1_PRINTABLESTRING; typedef struct asn1_string_st ASN1_T61STRING; typedef struct asn1_string_st ASN1_IA5STRING; typedef struct asn1_string_st ASN1_GENERALSTRING; typedef struct asn1_string_st ASN1_UNIVERSALSTRING; typedef struct asn1_string_st ASN1_BMPSTRING; typedef struct asn1_string_st ASN1_UTCTIME; typedef struct asn1_string_st ASN1_TIME; typedef struct asn1_string_st ASN1_GENERALIZEDTIME; typedef struct asn1_string_st ASN1_VISIBLESTRING; typedef struct asn1_string_st ASN1_UTF8STRING; typedef int ASN1_BOOLEAN; union __anonunion_value_19 { char *ptr ; ASN1_BOOLEAN boolean ; ASN1_STRING *asn1_string ; ASN1_OBJECT *object ; ASN1_INTEGER *integer ; ASN1_ENUMERATED *enumerated ; ASN1_BIT_STRING *bit_string ; ASN1_OCTET_STRING *octet_string ; ASN1_PRINTABLESTRING *printablestring ; ASN1_T61STRING *t61string ; ASN1_IA5STRING *ia5string ; ASN1_GENERALSTRING *generalstring ; ASN1_BMPSTRING *bmpstring ; ASN1_UNIVERSALSTRING *universalstring ; ASN1_UTCTIME *utctime ; ASN1_GENERALIZEDTIME *generalizedtime ; ASN1_VISIBLESTRING *visiblestring ; ASN1_UTF8STRING *utf8string ; ASN1_STRING *set ; ASN1_STRING *sequence ; }; struct asn1_type_st { int type ; union __anonunion_value_19 value ; }; typedef struct asn1_type_st ASN1_TYPE; struct MD5state_st { unsigned int A ; unsigned int B ; unsigned int C ; unsigned int D ; unsigned int Nl ; unsigned int Nh ; unsigned int data[16] ; int num ; }; typedef struct MD5state_st MD5_CTX; struct SHAstate_st { unsigned int h0 ; unsigned int h1 ; unsigned int h2 ; unsigned int h3 ; unsigned int h4 ; unsigned int Nl ; unsigned int Nh ; unsigned int data[16] ; int num ; }; typedef struct SHAstate_st SHA_CTX; struct MD2state_st { int num ; unsigned char data[16] ; unsigned int cksm[16] ; unsigned int state[16] ; }; typedef struct MD2state_st MD2_CTX; struct MD4state_st { unsigned int A ; unsigned int B ; unsigned int C ; unsigned int D ; unsigned int Nl ; unsigned int Nh ; unsigned int data[16] ; int num ; }; typedef struct MD4state_st MD4_CTX; struct RIPEMD160state_st { unsigned int A ; unsigned int B ; unsigned int C ; unsigned int D ; unsigned int E ; unsigned int Nl ; unsigned int Nh ; unsigned int data[16] ; int num ; }; typedef struct RIPEMD160state_st RIPEMD160_CTX; typedef unsigned char des_cblock[8]; union __anonunion_ks_20 { des_cblock cblock ; unsigned long deslong[2] ; }; struct des_ks_struct { union __anonunion_ks_20 ks ; int weak_key ; }; typedef struct des_ks_struct des_key_schedule[16]; struct rc4_key_st { unsigned int x ; unsigned int y ; unsigned int data[256] ; }; typedef struct rc4_key_st RC4_KEY; struct rc2_key_st { unsigned int data[64] ; }; typedef struct rc2_key_st RC2_KEY; struct rc5_key_st { int rounds ; unsigned long data[34] ; }; typedef struct rc5_key_st RC5_32_KEY; struct bf_key_st { unsigned int P[18] ; unsigned int S[1024] ; }; typedef struct bf_key_st BF_KEY; struct cast_key_st { unsigned long data[32] ; int short_key ; }; typedef struct cast_key_st CAST_KEY; struct idea_key_st { unsigned int data[9][6] ; }; typedef struct idea_key_st IDEA_KEY_SCHEDULE; struct mdc2_ctx_st { int num ; unsigned char data[8] ; des_cblock h ; des_cblock hh ; int pad_type ; }; typedef struct mdc2_ctx_st MDC2_CTX; struct rsa_st; struct rsa_st; typedef struct rsa_st RSA; struct rsa_meth_st { char const *name ; int (*rsa_pub_enc)(int flen , unsigned char *from , unsigned char *to , RSA *rsa , int padding ) ; int (*rsa_pub_dec)(int flen , unsigned char *from , unsigned char *to , RSA *rsa , int padding ) ; int (*rsa_priv_enc)(int flen , unsigned char *from , unsigned char *to , RSA *rsa , int padding ) ; int (*rsa_priv_dec)(int flen , unsigned char *from , unsigned char *to , RSA *rsa , int padding ) ; int (*rsa_mod_exp)(BIGNUM *r0 , BIGNUM *I , RSA *rsa ) ; int (*bn_mod_exp)(BIGNUM *r , BIGNUM *a , BIGNUM const *p , BIGNUM const *m , BN_CTX *ctx , BN_MONT_CTX *m_ctx ) ; int (*init)(RSA *rsa ) ; int (*finish)(RSA *rsa ) ; int flags ; char *app_data ; int (*rsa_sign)(int type , unsigned char *m , unsigned int m_len , unsigned char *sigret , unsigned int *siglen , RSA *rsa ) ; int (*rsa_verify)(int dtype , unsigned char *m , unsigned int m_len , unsigned char *sigbuf , unsigned int siglen , RSA *rsa ) ; }; typedef struct rsa_meth_st RSA_METHOD; struct rsa_st { int pad ; int version ; RSA_METHOD *meth ; BIGNUM *n ; BIGNUM *e ; BIGNUM *d ; BIGNUM *p ; BIGNUM *q ; BIGNUM *dmp1 ; BIGNUM *dmq1 ; BIGNUM *iqmp ; CRYPTO_EX_DATA ex_data ; int references ; int flags ; BN_MONT_CTX *_method_mod_n ; BN_MONT_CTX *_method_mod_p ; BN_MONT_CTX *_method_mod_q ; char *bignum_data ; BN_BLINDING *blinding ; }; struct dh_st; struct dh_st; typedef struct dh_st DH; struct dh_method { char const *name ; int (*generate_key)(DH *dh ) ; int (*compute_key)(unsigned char *key , BIGNUM *pub_key , DH *dh ) ; int (*bn_mod_exp)(DH *dh , BIGNUM *r , BIGNUM *a , BIGNUM const *p , BIGNUM const *m , BN_CTX *ctx , BN_MONT_CTX *m_ctx ) ; int (*init)(DH *dh ) ; int (*finish)(DH *dh ) ; int flags ; char *app_data ; }; typedef struct dh_method DH_METHOD; struct dh_st { int pad ; int version ; BIGNUM *p ; BIGNUM *g ; int length ; BIGNUM *pub_key ; BIGNUM *priv_key ; int flags ; char *method_mont_p ; BIGNUM *q ; BIGNUM *j ; unsigned char *seed ; int seedlen ; BIGNUM *counter ; int references ; CRYPTO_EX_DATA ex_data ; DH_METHOD *meth ; }; struct dsa_st; struct dsa_st; typedef struct dsa_st DSA; struct DSA_SIG_st { BIGNUM *r ; BIGNUM *s ; }; typedef struct DSA_SIG_st DSA_SIG; struct dsa_method { char const *name ; DSA_SIG *(*dsa_do_sign)(unsigned char const *dgst , int dlen , DSA *dsa ) ; int (*dsa_sign_setup)(DSA *dsa , BN_CTX *ctx_in , BIGNUM **kinvp , BIGNUM **rp ) ; int (*dsa_do_verify)(unsigned char const *dgst , int dgst_len , DSA_SIG *sig , DSA *dsa ) ; int (*dsa_mod_exp)(DSA *dsa , BIGNUM *rr , BIGNUM *a1 , BIGNUM *p1 , BIGNUM *a2 , BIGNUM *p2 , BIGNUM *m , BN_CTX *ctx , BN_MONT_CTX *in_mont ) ; int (*bn_mod_exp)(DSA *dsa , BIGNUM *r , BIGNUM *a , BIGNUM const *p , BIGNUM const *m , BN_CTX *ctx , BN_MONT_CTX *m_ctx ) ; int (*init)(DSA *dsa ) ; int (*finish)(DSA *dsa ) ; int flags ; char *app_data ; }; typedef struct dsa_method DSA_METHOD; struct dsa_st { int pad ; int version ; int write_params ; BIGNUM *p ; BIGNUM *q ; BIGNUM *g ; BIGNUM *pub_key ; BIGNUM *priv_key ; BIGNUM *kinv ; BIGNUM *r ; int flags ; char *method_mont_p ; int references ; CRYPTO_EX_DATA ex_data ; DSA_METHOD *meth ; }; union __anonunion_pkey_21 { char *ptr ; struct rsa_st *rsa ; struct dsa_st *dsa ; struct dh_st *dh ; }; struct evp_pkey_st { int type ; int save_type ; int references ; union __anonunion_pkey_21 pkey ; int save_parameters ; STACK *attributes ; }; typedef struct evp_pkey_st EVP_PKEY; struct env_md_st { int type ; int pkey_type ; int md_size ; void (*init)() ; void (*update)() ; void (*final)() ; int (*sign)() ; int (*verify)() ; int required_pkey_type[5] ; int block_size ; int ctx_size ; }; typedef struct env_md_st EVP_MD; union __anonunion_md_22 { unsigned char base[4] ; MD2_CTX md2 ; MD5_CTX md5 ; MD4_CTX md4 ; RIPEMD160_CTX ripemd160 ; SHA_CTX sha ; MDC2_CTX mdc2 ; }; struct env_md_ctx_st { EVP_MD const *digest ; union __anonunion_md_22 md ; }; typedef struct env_md_ctx_st EVP_MD_CTX; struct evp_cipher_st; struct evp_cipher_st; typedef struct evp_cipher_st EVP_CIPHER; struct evp_cipher_ctx_st; struct evp_cipher_ctx_st; typedef struct evp_cipher_ctx_st EVP_CIPHER_CTX; struct evp_cipher_st { int nid ; int block_size ; int key_len ; int iv_len ; unsigned long flags ; int (*init)(EVP_CIPHER_CTX *ctx , unsigned char const *key , unsigned char const *iv , int enc ) ; int (*do_cipher)(EVP_CIPHER_CTX *ctx , unsigned char *out , unsigned char const *in , unsigned int inl ) ; int (*cleanup)(EVP_CIPHER_CTX * ) ; int ctx_size ; int (*set_asn1_parameters)(EVP_CIPHER_CTX * , ASN1_TYPE * ) ; int (*get_asn1_parameters)(EVP_CIPHER_CTX * , ASN1_TYPE * ) ; int (*ctrl)(EVP_CIPHER_CTX * , int type , int arg , void *ptr ) ; void *app_data ; }; struct __anonstruct_rc4_24 { unsigned char key[16] ; RC4_KEY ks ; }; struct __anonstruct_desx_cbc_25 { des_key_schedule ks ; des_cblock inw ; des_cblock outw ; }; struct __anonstruct_des_ede_26 { des_key_schedule ks1 ; des_key_schedule ks2 ; des_key_schedule ks3 ; }; struct __anonstruct_rc2_27 { int key_bits ; RC2_KEY ks ; }; struct __anonstruct_rc5_28 { int rounds ; RC5_32_KEY ks ; }; union __anonunion_c_23 { struct __anonstruct_rc4_24 rc4 ; des_key_schedule des_ks ; struct __anonstruct_desx_cbc_25 desx_cbc ; struct __anonstruct_des_ede_26 des_ede ; IDEA_KEY_SCHEDULE idea_ks ; struct __anonstruct_rc2_27 rc2 ; struct __anonstruct_rc5_28 rc5 ; BF_KEY bf_ks ; CAST_KEY cast_ks ; }; struct evp_cipher_ctx_st { EVP_CIPHER const *cipher ; int encrypt ; int buf_len ; unsigned char oiv[8] ; unsigned char iv[8] ; unsigned char buf[8] ; int num ; void *app_data ; int key_len ; union __anonunion_c_23 c ; }; struct X509_algor_st { ASN1_OBJECT *algorithm ; ASN1_TYPE *parameter ; }; typedef struct X509_algor_st X509_ALGOR; struct X509_val_st { ASN1_TIME *notBefore ; ASN1_TIME *notAfter ; }; typedef struct X509_val_st X509_VAL; struct X509_pubkey_st { X509_ALGOR *algor ; ASN1_BIT_STRING *public_key ; EVP_PKEY *pkey ; }; typedef struct X509_pubkey_st X509_PUBKEY; struct X509_name_st { STACK *entries ; int modified ; BUF_MEM *bytes ; unsigned long hash ; }; typedef struct X509_name_st X509_NAME; struct x509_cinf_st { ASN1_INTEGER *version ; ASN1_INTEGER *serialNumber ; X509_ALGOR *signature ; X509_NAME *issuer ; X509_VAL *validity ; X509_NAME *subject ; X509_PUBKEY *key ; ASN1_BIT_STRING *issuerUID ; ASN1_BIT_STRING *subjectUID ; STACK *extensions ; }; typedef struct x509_cinf_st X509_CINF; struct x509_cert_aux_st { STACK *trust ; STACK *reject ; ASN1_UTF8STRING *alias ; ASN1_OCTET_STRING *keyid ; STACK *other ; }; typedef struct x509_cert_aux_st X509_CERT_AUX; struct AUTHORITY_KEYID_st; struct AUTHORITY_KEYID_st; struct x509_st { X509_CINF *cert_info ; X509_ALGOR *sig_alg ; ASN1_BIT_STRING *signature ; int valid ; int references ; char *name ; CRYPTO_EX_DATA ex_data ; long ex_pathlen ; unsigned long ex_flags ; unsigned long ex_kusage ; unsigned long ex_xkusage ; unsigned long ex_nscert ; ASN1_OCTET_STRING *skid ; struct AUTHORITY_KEYID_st *akid ; unsigned char sha1_hash[20] ; X509_CERT_AUX *aux ; }; typedef struct x509_st X509; struct lhash_node_st { void *data ; struct lhash_node_st *next ; unsigned long hash ; }; typedef struct lhash_node_st LHASH_NODE; struct lhash_st { LHASH_NODE **b ; int (*comp)() ; unsigned long (*hash)() ; unsigned int num_nodes ; unsigned int num_alloc_nodes ; unsigned int p ; unsigned int pmax ; unsigned long up_load ; unsigned long down_load ; unsigned long num_items ; unsigned long num_expands ; unsigned long num_expand_reallocs ; unsigned long num_contracts ; unsigned long num_contract_reallocs ; unsigned long num_hash_calls ; unsigned long num_comp_calls ; unsigned long num_insert ; unsigned long num_replace ; unsigned long num_delete ; unsigned long num_no_delete ; unsigned long num_retrieve ; unsigned long num_retrieve_miss ; unsigned long num_hash_comps ; int error ; }; struct x509_store_ctx_st; struct x509_store_ctx_st; typedef struct x509_store_ctx_st X509_STORE_CTX; struct x509_store_st { int cache ; STACK *objs ; STACK *get_cert_methods ; int (*verify)(X509_STORE_CTX *ctx ) ; int (*verify_cb)(int ok , X509_STORE_CTX *ctx ) ; CRYPTO_EX_DATA ex_data ; int references ; int depth ; }; typedef struct x509_store_st X509_STORE; struct x509_store_ctx_st { X509_STORE *ctx ; int current_method ; X509 *cert ; STACK *untrusted ; int purpose ; int trust ; time_t check_time ; unsigned long flags ; void *other_ctx ; int (*verify)(X509_STORE_CTX *ctx ) ; int (*verify_cb)(int ok , X509_STORE_CTX *ctx ) ; int (*get_issuer)(X509 **issuer , X509_STORE_CTX *ctx , X509 *x ) ; int (*check_issued)(X509_STORE_CTX *ctx , X509 *x , X509 *issuer ) ; int (*cleanup)(X509_STORE_CTX *ctx ) ; int depth ; int valid ; int last_untrusted ; STACK *chain ; int error_depth ; int error ; X509 *current_cert ; X509 *current_issuer ; CRYPTO_EX_DATA ex_data ; }; struct comp_method_st { int type ; char const *name ; int (*init)() ; void (*finish)() ; int (*compress)() ; int (*expand)() ; long (*ctrl)() ; long (*callback_ctrl)() ; }; typedef struct comp_method_st COMP_METHOD; struct comp_ctx_st { COMP_METHOD *meth ; unsigned long compress_in ; unsigned long compress_out ; unsigned long expand_in ; unsigned long expand_out ; CRYPTO_EX_DATA ex_data ; }; typedef struct comp_ctx_st COMP_CTX; typedef int pem_password_cb(char *buf , int size , int rwflag , void *userdata ); struct ssl_st; struct ssl_st; struct ssl_cipher_st { int valid ; char const *name ; unsigned long id ; unsigned long algorithms ; unsigned long algo_strength ; unsigned long algorithm2 ; int strength_bits ; int alg_bits ; unsigned long mask ; unsigned long mask_strength ; }; typedef struct ssl_cipher_st SSL_CIPHER; typedef struct ssl_st SSL; struct ssl_ctx_st; struct ssl_ctx_st; typedef struct ssl_ctx_st SSL_CTX; struct ssl3_enc_method; struct ssl3_enc_method; struct ssl_method_st { int version ; int (*ssl_new)(SSL *s ) ; void (*ssl_clear)(SSL *s ) ; void (*ssl_free)(SSL *s ) ; int (*ssl_accept)(SSL *s ) ; int (*ssl_connect)(SSL *s ) ; int (*ssl_read)(SSL *s , void *buf , int len ) ; int (*ssl_peek)(SSL *s , void *buf , int len ) ; int (*ssl_write)(SSL *s , void const *buf , int len ) ; int (*ssl_shutdown)(SSL *s ) ; int (*ssl_renegotiate)(SSL *s ) ; int (*ssl_renegotiate_check)(SSL *s ) ; long (*ssl_ctrl)(SSL *s , int cmd , long larg , char *parg ) ; long (*ssl_ctx_ctrl)(SSL_CTX *ctx , int cmd , long larg , char *parg ) ; SSL_CIPHER *(*get_cipher_by_char)(unsigned char const *ptr ) ; int (*put_cipher_by_char)(SSL_CIPHER const *cipher , unsigned char *ptr ) ; int (*ssl_pending)(SSL *s ) ; int (*num_ciphers)(void) ; SSL_CIPHER *(*get_cipher)(unsigned int ncipher ) ; struct ssl_method_st *(*get_ssl_method)(int version ) ; long (*get_timeout)(void) ; struct ssl3_enc_method *ssl3_enc ; int (*ssl_version)() ; long (*ssl_callback_ctrl)(SSL *s , int cb_id , void (*fp)() ) ; long (*ssl_ctx_callback_ctrl)(SSL_CTX *s , int cb_id , void (*fp)() ) ; }; typedef struct ssl_method_st SSL_METHOD; struct sess_cert_st; struct sess_cert_st; struct ssl_session_st { int ssl_version ; unsigned int key_arg_length ; unsigned char key_arg[8] ; int master_key_length ; unsigned char master_key[48] ; unsigned int session_id_length ; unsigned char session_id[32] ; unsigned int sid_ctx_length ; unsigned char sid_ctx[32] ; int not_resumable ; struct sess_cert_st *sess_cert ; X509 *peer ; long verify_result ; int references ; long timeout ; long time ; int compress_meth ; SSL_CIPHER *cipher ; unsigned long cipher_id ; STACK *ciphers ; CRYPTO_EX_DATA ex_data ; struct ssl_session_st *prev ; struct ssl_session_st *next ; }; typedef struct ssl_session_st SSL_SESSION; struct ssl_comp_st { int id ; char *name ; COMP_METHOD *method ; }; typedef struct ssl_comp_st SSL_COMP; struct __anonstruct_stats_37 { int sess_connect ; int sess_connect_renegotiate ; int sess_connect_good ; int sess_accept ; int sess_accept_renegotiate ; int sess_accept_good ; int sess_miss ; int sess_timeout ; int sess_cache_full ; int sess_hit ; int sess_cb_hit ; }; struct cert_st; struct cert_st; struct ssl_ctx_st { SSL_METHOD *method ; unsigned long options ; unsigned long mode ; STACK *cipher_list ; STACK *cipher_list_by_id ; struct x509_store_st *cert_store ; struct lhash_st *sessions ; unsigned long session_cache_size ; struct ssl_session_st *session_cache_head ; struct ssl_session_st *session_cache_tail ; int session_cache_mode ; long session_timeout ; int (*new_session_cb)(struct ssl_st *ssl , SSL_SESSION *sess ) ; void (*remove_session_cb)(struct ssl_ctx_st *ctx , SSL_SESSION *sess ) ; SSL_SESSION *(*get_session_cb)(struct ssl_st *ssl , unsigned char *data , int len , int *copy ) ; struct __anonstruct_stats_37 stats ; int references ; void (*info_callback)() ; int (*app_verify_callback)() ; char *app_verify_arg ; struct cert_st *cert ; int read_ahead ; int verify_mode ; int verify_depth ; unsigned int sid_ctx_length ; unsigned char sid_ctx[32] ; int (*default_verify_callback)(int ok , X509_STORE_CTX *ctx ) ; int purpose ; int trust ; pem_password_cb *default_passwd_callback ; void *default_passwd_callback_userdata ; int (*client_cert_cb)() ; STACK *client_CA ; int quiet_shutdown ; CRYPTO_EX_DATA ex_data ; EVP_MD const *rsa_md5 ; EVP_MD const *md5 ; EVP_MD const *sha1 ; STACK *extra_certs ; STACK *comp_methods ; }; struct ssl2_state_st; struct ssl2_state_st; struct ssl3_state_st; struct ssl3_state_st; struct ssl_st { int version ; int type ; SSL_METHOD *method ; BIO *rbio ; BIO *wbio ; BIO *bbio ; int rwstate ; int in_handshake ; int (*handshake_func)() ; int server ; int new_session ; int quiet_shutdown ; int shutdown ; int state ; int rstate ; BUF_MEM *init_buf ; int init_num ; int init_off ; unsigned char *packet ; unsigned int packet_length ; struct ssl2_state_st *s2 ; struct ssl3_state_st *s3 ; int read_ahead ; int hit ; int purpose ; int trust ; STACK *cipher_list ; STACK *cipher_list_by_id ; EVP_CIPHER_CTX *enc_read_ctx ; EVP_MD const *read_hash ; COMP_CTX *expand ; EVP_CIPHER_CTX *enc_write_ctx ; EVP_MD const *write_hash ; COMP_CTX *compress ; struct cert_st *cert ; unsigned int sid_ctx_length ; unsigned char sid_ctx[32] ; SSL_SESSION *session ; int verify_mode ; int verify_depth ; int (*verify_callback)(int ok , X509_STORE_CTX *ctx ) ; void (*info_callback)() ; int error ; int error_code ; SSL_CTX *ctx ; int debug ; long verify_result ; CRYPTO_EX_DATA ex_data ; STACK *client_CA ; int references ; unsigned long options ; unsigned long mode ; int first_packet ; int client_version ; }; struct __anonstruct_tmp_38 { unsigned int conn_id_length ; unsigned int cert_type ; unsigned int cert_length ; unsigned int csl ; unsigned int clear ; unsigned int enc ; unsigned char ccl[32] ; unsigned int cipher_spec_length ; unsigned int session_id_length ; unsigned int clen ; unsigned int rlen ; }; struct ssl2_state_st { int three_byte_header ; int clear_text ; int escape ; int ssl2_rollback ; unsigned int wnum ; int wpend_tot ; unsigned char const *wpend_buf ; int wpend_off ; int wpend_len ; int wpend_ret ; int rbuf_left ; int rbuf_offs ; unsigned char *rbuf ; unsigned char *wbuf ; unsigned char *write_ptr ; unsigned int padding ; unsigned int rlength ; int ract_data_length ; unsigned int wlength ; int wact_data_length ; unsigned char *ract_data ; unsigned char *wact_data ; unsigned char *mac_data ; unsigned char *pad_data_UNUSED ; unsigned char *read_key ; unsigned char *write_key ; unsigned int challenge_length ; unsigned char challenge[32] ; unsigned int conn_id_length ; unsigned char conn_id[16] ; unsigned int key_material_length ; unsigned char key_material[48] ; unsigned long read_sequence ; unsigned long write_sequence ; struct __anonstruct_tmp_38 tmp ; }; struct ssl3_record_st { int type ; unsigned int length ; unsigned int off ; unsigned char *data ; unsigned char *input ; unsigned char *comp ; }; typedef struct ssl3_record_st SSL3_RECORD; struct ssl3_buffer_st { unsigned char *buf ; int offset ; int left ; }; typedef struct ssl3_buffer_st SSL3_BUFFER; struct __anonstruct_tmp_39 { unsigned char cert_verify_md[72] ; unsigned char finish_md[72] ; int finish_md_len ; unsigned char peer_finish_md[72] ; int peer_finish_md_len ; unsigned long message_size ; int message_type ; SSL_CIPHER *new_cipher ; DH *dh ; int next_state ; int reuse_message ; int cert_req ; int ctype_num ; char ctype[7] ; STACK *ca_names ; int use_rsa_tmp ; int key_block_length ; unsigned char *key_block ; EVP_CIPHER const *new_sym_enc ; EVP_MD const *new_hash ; SSL_COMP const *new_compression ; int cert_request ; }; struct ssl3_state_st { long flags ; int delay_buf_pop_ret ; unsigned char read_sequence[8] ; unsigned char read_mac_secret[36] ; unsigned char write_sequence[8] ; unsigned char write_mac_secret[36] ; unsigned char server_random[32] ; unsigned char client_random[32] ; SSL3_BUFFER rbuf ; SSL3_BUFFER wbuf ; SSL3_RECORD rrec ; SSL3_RECORD wrec ; unsigned char alert_fragment[2] ; unsigned int alert_fragment_len ; unsigned char handshake_fragment[4] ; unsigned int handshake_fragment_len ; unsigned int wnum ; int wpend_tot ; int wpend_type ; int wpend_ret ; unsigned char const *wpend_buf ; EVP_MD_CTX finish_dgst1 ; EVP_MD_CTX finish_dgst2 ; int change_cipher_spec ; int warn_alert ; int fatal_alert ; int alert_dispatch ; unsigned char send_alert[2] ; int renegotiate ; int total_renegotiations ; int num_renegotiations ; int in_read_app_data ; struct __anonstruct_tmp_39 tmp ; }; struct cert_pkey_st { X509 *x509 ; EVP_PKEY *privatekey ; }; typedef struct cert_pkey_st CERT_PKEY; struct cert_st { CERT_PKEY *key ; int valid ; unsigned long mask ; unsigned long export_mask ; RSA *rsa_tmp ; RSA *(*rsa_tmp_cb)(SSL *ssl , int is_export , int keysize ) ; DH *dh_tmp ; DH *(*dh_tmp_cb)(SSL *ssl , int is_export , int keysize ) ; CERT_PKEY pkeys[5] ; int references ; }; struct sess_cert_st { STACK *cert_chain ; int peer_cert_type ; CERT_PKEY *peer_key ; CERT_PKEY peer_pkeys[5] ; RSA *peer_rsa_tmp ; DH *peer_dh_tmp ; int references ; }; struct ssl3_enc_method { int (*enc)(SSL * , int ) ; int (*mac)(SSL * , unsigned char * , int ) ; int (*setup_key_block)(SSL * ) ; int (*generate_master_secret)(SSL * , unsigned char * , unsigned char * , int ) ; int (*change_cipher_state)(SSL * , int ) ; int (*final_finish_mac)(SSL * , EVP_MD_CTX * , EVP_MD_CTX * , char const * , int , unsigned char * ) ; int finish_mac_length ; int (*cert_verify_mac)(SSL * , EVP_MD_CTX * , unsigned char * ) ; char const *client_finished_label ; int client_finished_label_len ; char const *server_finished_label ; int server_finished_label_len ; int (*alert_value)(int ) ; }; extern void *memcpy(void * __restrict __dest , void const * __restrict __src , size_t __n ) ; extern void ERR_put_error(int lib , int func , int reason , char const *file , int line ) ; SSL_METHOD *SSLv3_server_method(void) ; extern SSL_METHOD *sslv3_base_method(void) ; extern X509 *ssl_get_server_send_cert(SSL * ) ; int ssl3_send_server_certificate(SSL *s ) ; extern int ssl3_do_write(SSL *s , int type ) ; extern unsigned long ssl3_output_cert_chain(SSL *s , X509 *x ) ; int ssl3_accept(SSL *s ) ; static SSL_METHOD *ssl3_get_server_method(int ver ) ; static SSL_METHOD *ssl3_get_server_method(int ver ) { SSL_METHOD *tmp ; { if (ver == 768) { { tmp = SSLv3_server_method(); } return (tmp); } else { return ((SSL_METHOD *)((void *)0)); } } } static int init = 1; static SSL_METHOD SSLv3_server_data ; SSL_METHOD *SSLv3_server_method(void) { char *tmp ; SSL_METHOD *tmp___0 ; { if (init) { { tmp___0 = sslv3_base_method(); tmp = (char *)tmp___0; memcpy((void *)((char *)(& SSLv3_server_data)), (void const *)tmp, sizeof(SSL_METHOD )); SSLv3_server_data.ssl_accept = & ssl3_accept; SSLv3_server_data.get_ssl_method = & ssl3_get_server_method; init = 0; } } else { } return (& SSLv3_server_data); } } int main(void) { SSL *s ; int tmp ; { { s = malloc(sizeof(SSL)); s->s3 = malloc(sizeof(struct ssl3_state_st)); s->ctx = malloc(sizeof(SSL_CTX)); s->session = malloc(sizeof(SSL_SESSION)); tmp = ssl3_accept(s); } return (tmp); } } int ssl3_accept(SSL *s ) { BUF_MEM *buf ; unsigned long l ; unsigned long Time ; unsigned long tmp ; void (*cb)() ; long num1 ; int ret ; int new_state ; int state ; int skip ; int got_new_session ; int tmp___1 = __VERIFIER_nondet_int() ; int tmp___2 = __VERIFIER_nondet_int() ; int tmp___3 = __VERIFIER_nondet_int() ; int tmp___4 = __VERIFIER_nondet_int() ; int tmp___5 = __VERIFIER_nondet_int() ; int tmp___6 = __VERIFIER_nondet_int() ; int tmp___7 ; long tmp___8 = __VERIFIER_nondet_long() ; int tmp___9 = __VERIFIER_nondet_int() ; int tmp___10 = __VERIFIER_nondet_int() ; int blastFlag ; { s->state = 8464; blastFlag = 0; s->hit=__VERIFIER_nondet_int (); s->state = 8464; tmp = __VERIFIER_nondet_int(); Time = tmp; cb = (void (*)())((void *)0); ret = -1; skip = 0; got_new_session = 0; if ((unsigned long )s->info_callback != (unsigned long )((void *)0)) { cb = s->info_callback; } else { } s->in_handshake += 1; if (tmp___1 & 12288) { if (tmp___2 & 16384) { } else { } } else { } if ((unsigned long )s->cert == (unsigned long )((void *)0)) { return (-1); } else { } { while (1) { while_0_continue: /* CIL Label */ ; state = s->state; if (s->state == 12292) { goto switch_1_12292; } else { if (s->state == 16384) { goto switch_1_16384; } else { if (s->state == 8192) { goto switch_1_8192; } else { if (s->state == 24576) { goto switch_1_24576; } else { if (s->state == 8195) { goto switch_1_8195; } else { if (s->state == 8480) { goto switch_1_8480; } else { if (s->state == 8481) { goto switch_1_8481; } else { if (s->state == 8482) { goto switch_1_8482; } else { if (s->state == 8464) { goto switch_1_8464; } else { if (s->state == 8465) { goto switch_1_8465; } else { if (s->state == 8466) { goto switch_1_8466; } else { if (s->state == 8496) { goto switch_1_8496; } else { if (s->state == 8497) { goto switch_1_8497; } else { if (s->state == 8512) { goto switch_1_8512; } else { if (s->state == 8513) { goto switch_1_8513; } else { if (s->state == 8528) { goto switch_1_8528; } else { if (s->state == 8529) { goto switch_1_8529; } else { if (s->state == 8544) { goto switch_1_8544; } else { if (s->state == 8545) { goto switch_1_8545; } else { if (s->state == 8560) { goto switch_1_8560; } else { if (s->state == 8561) { goto switch_1_8561; } else { if (s->state == 8448) { goto switch_1_8448; } else { if (s->state == 8576) { goto switch_1_8576; } else { if (s->state == 8577) { goto switch_1_8577; } else { if (s->state == 8592) { goto switch_1_8592; } else { if (s->state == 8593) { goto switch_1_8593; } else { if (s->state == 8608) { goto switch_1_8608; } else { if (s->state == 8609) { goto switch_1_8609; } else { if (s->state == 8640) { goto switch_1_8640; } else { if (s->state == 8641) { goto switch_1_8641; } else { if (s->state == 8656) { goto switch_1_8656; } else { if (s->state == 8657) { goto switch_1_8657; } else { if (s->state == 8672) { goto switch_1_8672; } else { if (s->state == 8673) { goto switch_1_8673; } else { if (s->state == 3) { goto switch_1_3; } else { { goto switch_1_default; if (0) { switch_1_12292: /* CIL Label */ s->new_session = 1; switch_1_16384: /* CIL Label */ ; switch_1_8192: /* CIL Label */ ; switch_1_24576: /* CIL Label */ ; switch_1_8195: /* CIL Label */ s->server = 1; if ((unsigned long )cb != (unsigned long )((void *)0)) { } else { } if (s->version >> 8 != 3) { return (-1); } else { } s->type = 8192; if ((unsigned long )s->init_buf == (unsigned long )((void *)0)) { buf = __VERIFIER_nondet_pointer(); if ((unsigned long )buf == (unsigned long )((void *)0)) { ret = -1; goto end; } else { } if (! tmp___3) { ret = -1; goto end; } else { } s->init_buf = buf; } else { } if (! tmp___4) { ret = -1; goto end; } else { } s->init_num = 0; if (s->state != 12292) { if (! tmp___5) { ret = -1; goto end; } else { } s->state = 8464; (s->ctx)->stats.sess_accept += 1; } else { (s->ctx)->stats.sess_accept_renegotiate += 1; s->state = 8480; } goto switch_1_break; switch_1_8480: /* CIL Label */ ; switch_1_8481: /* CIL Label */ s->shutdown = 0; ret = __VERIFIER_nondet_int(); if (ret <= 0) { goto end; } else { } (s->s3)->tmp.next_state = 8482; s->state = 8448; s->init_num = 0; goto switch_1_break; switch_1_8482: /* CIL Label */ s->state = 3; goto switch_1_break; switch_1_8464: /* CIL Label */ ; switch_1_8465: /* CIL Label */ ; switch_1_8466: /* CIL Label */ s->shutdown = 0; ret = __VERIFIER_nondet_int(); if (blastFlag == 0) { blastFlag = 1; } else { } if (ret <= 0) { goto end; } else { } got_new_session = 1; s->state = 8496; s->init_num = 0; goto switch_1_break; switch_1_8496: /* CIL Label */ ; switch_1_8497: /* CIL Label */ ret = __VERIFIER_nondet_int(); if (blastFlag == 1) { blastFlag = 2; } else { } if (ret <= 0) { goto end; } else { } if (s->hit) { s->state = 8656; } else { s->state = 8512; } s->init_num = 0; goto switch_1_break; switch_1_8512: /* CIL Label */ ; switch_1_8513: /* CIL Label */ ; if (((s->s3)->tmp.new_cipher)->algorithms & 256UL) { skip = 1; } else { ret = __VERIFIER_nondet_int(); if (blastFlag == 2) { blastFlag = 6; } else { } if (ret <= 0) { goto end; } else { } } s->state = 8528; s->init_num = 0; goto switch_1_break; switch_1_8528: /* CIL Label */ ; switch_1_8529: /* CIL Label */ l = ((s->s3)->tmp.new_cipher)->algorithms; if (s->options & 2097152UL) { (s->s3)->tmp.use_rsa_tmp = 1; } else { (s->s3)->tmp.use_rsa_tmp = 0; } if ((s->s3)->tmp.use_rsa_tmp) { goto _L___0; } else { if (l & 30UL) { goto _L___0; } else { if (l & 1UL) { if ((unsigned long )(s->cert)->pkeys[0].privatekey == (unsigned long )((void *)0)) { goto _L___0; } else { if (((s->s3)->tmp.new_cipher)->algo_strength & 2UL) { if (((s->s3)->tmp.new_cipher)->algo_strength & 4UL) { tmp___7 = 512; } else { tmp___7 = 1024; } if (tmp___6 * 8 > tmp___7) { _L___0: ret = __VERIFIER_nondet_int(); if (blastFlag == 6) { blastFlag = 7; } else { } if (ret <= 0) { goto end; } else { } } else { skip = 1; } } else { skip = 1; } } } else { skip = 1; } } } s->state = 8544; s->init_num = 0; goto switch_1_break; switch_1_8544: /* CIL Label */ ; switch_1_8545: /* CIL Label */ ; if (s->verify_mode & 1) { if ((unsigned long )(s->session)->peer != (unsigned long )((void *)0)) { if (s->verify_mode & 4) { skip = 1; (s->s3)->tmp.cert_request = 0; s->state = 8560; } else { goto _L___2; } } else { _L___2: if (((s->s3)->tmp.new_cipher)->algorithms & 256UL) { if (s->verify_mode & 2) { goto _L___1; } else { skip = 1; (s->s3)->tmp.cert_request = 0; s->state = 8560; } } else { _L___1: (s->s3)->tmp.cert_request = 1; ret = __VERIFIER_nondet_int(); if (blastFlag == 8) { goto ERROR; } else { } if (ret <= 0) { goto end; } else { } s->state = 8448; (s->s3)->tmp.next_state = 8576; s->init_num = 0; } } } else { skip = 1; (s->s3)->tmp.cert_request = 0; s->state = 8560; } goto switch_1_break; switch_1_8560: /* CIL Label */ ; switch_1_8561: /* CIL Label */ ret = __VERIFIER_nondet_int(); if (ret <= 0) { goto end; } else { } (s->s3)->tmp.next_state = 8576; s->state = 8448; s->init_num = 0; goto switch_1_break; switch_1_8448: /* CIL Label */ if (num1 > 0L) { s->rwstate = 2; num1 = (long )((int )tmp___8); if (num1 <= 0L) { ret = -1; goto end; } else { } s->rwstate = 1; } else { } s->state = (s->s3)->tmp.next_state; goto switch_1_break; switch_1_8576: /* CIL Label */ ; switch_1_8577: /* CIL Label */ ret = __VERIFIER_nondet_int(); if (ret <= 0) { goto end; } else { } if (ret == 2) { s->state = 8466; } else { ret = __VERIFIER_nondet_int(); if (ret <= 0) { goto end; } else { } s->init_num = 0; s->state = 8592; } goto switch_1_break; switch_1_8592: /* CIL Label */ ; switch_1_8593: /* CIL Label */ ret = __VERIFIER_nondet_int(); if (ret <= 0) { goto end; } else { } s->state = 8608; s->init_num = 0; goto switch_1_break; switch_1_8608: /* CIL Label */ ; switch_1_8609: /* CIL Label */ ret = __VERIFIER_nondet_int(); if (blastFlag == 4) { blastFlag = 5; } else { if (blastFlag == 7) { blastFlag = 8; } else { } } if (ret <= 0) { goto end; } else { } s->state = 8640; s->init_num = 0; goto switch_1_break; switch_1_8640: /* CIL Label */ ; switch_1_8641: /* CIL Label */ ret = __VERIFIER_nondet_int(); if (blastFlag == 5) { goto ERROR; } else { } if (ret <= 0) { goto end; } else { } if (s->hit) { s->state = 3; } else { s->state = 8656; } s->init_num = 0; goto switch_1_break; switch_1_8656: /* CIL Label */ ; switch_1_8657: /* CIL Label */ (s->session)->cipher = (s->s3)->tmp.new_cipher; if (! tmp___9) { ret = -1; goto end; } else { } ret = __VERIFIER_nondet_int(); if (blastFlag == 2) { blastFlag = 3; } else { } if (ret <= 0) { goto end; } else { } s->state = 8672; s->init_num = 0; if (! tmp___10) { ret = -1; goto end; } else { } goto switch_1_break; switch_1_8672: /* CIL Label */ ; switch_1_8673: /* CIL Label */ ret = __VERIFIER_nondet_int(); if (blastFlag == 3) { blastFlag = 4; } else { } if (ret <= 0) { goto end; } else { } s->state = 8448; if (s->hit) { (s->s3)->tmp.next_state = 8640; } else { (s->s3)->tmp.next_state = 3; } s->init_num = 0; goto switch_1_break; switch_1_3: /* CIL Label */ s->init_buf = (BUF_MEM *)((void *)0); s->init_num = 0; if (got_new_session) { s->new_session = 0; (s->ctx)->stats.sess_accept_good += 1; s->handshake_func = (int (*)())(& ssl3_accept); if ((unsigned long )cb != (unsigned long )((void *)0)) { } else { } } else { } ret = 1; goto end; switch_1_default: /* CIL Label */ ret = -1; goto end; } else { switch_1_break: /* CIL Label */ ; } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } } if (! (s->s3)->tmp.reuse_message) { if (! skip) { if (s->debug) { ret = __VERIFIER_nondet_int(); if (ret <= 0) { goto end; } else { } } else { } if ((unsigned long )cb != (unsigned long )((void *)0)) { if (s->state != state) { new_state = s->state; s->state = state; s->state = new_state; } else { } } else { } } else { } } else { } skip = 0; } while_0_break: /* CIL Label */ ; } end: s->in_handshake -= 1; if ((unsigned long )cb != (unsigned long )((void *)0)) { } else { } return (ret); ERROR: __VERIFIER_error(); } } int ssl3_send_server_certificate(SSL *s ) { unsigned long l ; X509 *x ; int tmp ; { if (s->state == 8512) { { x = ssl_get_server_send_cert(s); } if ((unsigned long )x == (unsigned long )((void *)0)) { { ERR_put_error(20, 154, 157, "s3_srvr.c", 1844); } return (0); } else { } { l = ssl3_output_cert_chain(s, x); s->state = 8513; s->init_num = (int )l; s->init_off = 0; } } else { } { tmp = ssl3_do_write(s, 22); } return (tmp); } }