ClabureDB: Classified Bug-Reports Database

   /* Generated by CIL v. 1.3.7 */
   /* print_CIL_Input is true */
   
   #line 20 "include/asm-generic/int-ll64.h"
   typedef unsigned char __u8;
   #line 23 "include/asm-generic/int-ll64.h"
   typedef unsigned short __u16;
   #line 26 "include/asm-generic/int-ll64.h"
   typedef unsigned int __u32;
  #line 30 "include/asm-generic/int-ll64.h"
  typedef unsigned long long __u64;
  #line 43 "include/asm-generic/int-ll64.h"
  typedef unsigned char u8;
  #line 45 "include/asm-generic/int-ll64.h"
  typedef short s16;
  #line 46 "include/asm-generic/int-ll64.h"
  typedef unsigned short u16;
  #line 49 "include/asm-generic/int-ll64.h"
  typedef unsigned int u32;
  #line 52 "include/asm-generic/int-ll64.h"
  typedef unsigned long long u64;
  #line 14 "include/asm-generic/posix_types.h"
  typedef long __kernel_long_t;
  #line 15 "include/asm-generic/posix_types.h"
  typedef unsigned long __kernel_ulong_t;
  #line 75 "include/asm-generic/posix_types.h"
  typedef __kernel_ulong_t __kernel_size_t;
  #line 76 "include/asm-generic/posix_types.h"
  typedef __kernel_long_t __kernel_ssize_t;
  #line 27 "include/linux/types.h"
  typedef unsigned short umode_t;
  #line 63 "include/linux/types.h"
  typedef __kernel_size_t size_t;
  #line 68 "include/linux/types.h"
  typedef __kernel_ssize_t ssize_t;
  #line 92 "include/linux/types.h"
  typedef unsigned char u_char;
  #line 155 "include/linux/types.h"
  typedef u64 dma_addr_t;
  #line 179 "include/linux/types.h"
  typedef __u16 __be16;
  #line 202 "include/linux/types.h"
  typedef unsigned int gfp_t;
  #line 221 "include/linux/types.h"
  struct __anonstruct_atomic_t_6 {
     int counter ;
  };
  #line 221 "include/linux/types.h"
  typedef struct __anonstruct_atomic_t_6 atomic_t;
  #line 226 "include/linux/types.h"
  struct __anonstruct_atomic64_t_7 {
     long counter ;
  };
  #line 226 "include/linux/types.h"
  typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  #line 227 "include/linux/types.h"
  struct list_head {
     struct list_head *next ;
     struct list_head *prev ;
  };
  #line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  struct module;
  #line 55
  struct module;
  #line 146 "include/linux/init.h"
  typedef void (*ctor_fn_t)(void);
  #line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  struct page;
  #line 58
  struct page;
  #line 26 "include/asm-generic/getorder.h"
  struct task_struct;
  #line 26
  struct task_struct;
  #line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  struct arch_spinlock;
  #line 327
  struct arch_spinlock;
  #line 306 "include/linux/bitmap.h"
  struct bug_entry {
     int bug_addr_disp ;
     int file_disp ;
     unsigned short line ;
     unsigned short flags ;
  };
  #line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
  struct static_key;
  #line 234
  struct static_key;
  #line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  struct kmem_cache;
  #line 23 "include/asm-generic/atomic-long.h"
  typedef atomic64_t atomic_long_t;
  #line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  typedef u16 __ticket_t;
  #line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  typedef u32 __ticketpair_t;
  #line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  struct __raw_tickets {
    __ticket_t head ;
    __ticket_t tail ;
 };
 #line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 union __anonunion_ldv_5907_29 {
    __ticketpair_t head_tail ;
    struct __raw_tickets tickets ;
 };
 #line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 struct arch_spinlock {
    union __anonunion_ldv_5907_29 ldv_5907 ;
 };
 #line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 typedef struct arch_spinlock arch_spinlock_t;
 #line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 struct lockdep_map;
 #line 34
 struct lockdep_map;
 #line 55 "include/linux/debug_locks.h"
 struct stack_trace {
    unsigned int nr_entries ;
    unsigned int max_entries ;
    unsigned long *entries ;
    int skip ;
 };
 #line 26 "include/linux/stacktrace.h"
 struct lockdep_subclass_key {
    char __one_byte ;
 };
 #line 53 "include/linux/lockdep.h"
 struct lock_class_key {
    struct lockdep_subclass_key subkeys[8U] ;
 };
 #line 59 "include/linux/lockdep.h"
 struct lock_class {
    struct list_head hash_entry ;
    struct list_head lock_entry ;
    struct lockdep_subclass_key *key ;
    unsigned int subclass ;
    unsigned int dep_gen_id ;
    unsigned long usage_mask ;
    struct stack_trace usage_traces[13U] ;
    struct list_head locks_after ;
    struct list_head locks_before ;
    unsigned int version ;
    unsigned long ops ;
    char const   *name ;
    int name_version ;
    unsigned long contention_point[4U] ;
    unsigned long contending_point[4U] ;
 };
 #line 144 "include/linux/lockdep.h"
 struct lockdep_map {
    struct lock_class_key *key ;
    struct lock_class *class_cache[2U] ;
    char const   *name ;
    int cpu ;
    unsigned long ip ;
 };
 #line 556 "include/linux/lockdep.h"
 struct raw_spinlock {
    arch_spinlock_t raw_lock ;
    unsigned int magic ;
    unsigned int owner_cpu ;
    void *owner ;
    struct lockdep_map dep_map ;
 };
 #line 33 "include/linux/spinlock_types.h"
 struct __anonstruct_ldv_6122_33 {
    u8 __padding[24U] ;
    struct lockdep_map dep_map ;
 };
 #line 33 "include/linux/spinlock_types.h"
 union __anonunion_ldv_6123_32 {
    struct raw_spinlock rlock ;
    struct __anonstruct_ldv_6122_33 ldv_6122 ;
 };
 #line 33 "include/linux/spinlock_types.h"
 struct spinlock {
    union __anonunion_ldv_6123_32 ldv_6123 ;
 };
 #line 76 "include/linux/spinlock_types.h"
 typedef struct spinlock spinlock_t;
 #line 18 "include/linux/elf.h"
 typedef __u64 Elf64_Addr;
 #line 19 "include/linux/elf.h"
 typedef __u16 Elf64_Half;
 #line 23 "include/linux/elf.h"
 typedef __u32 Elf64_Word;
 #line 24 "include/linux/elf.h"
 typedef __u64 Elf64_Xword;
 #line 193 "include/linux/elf.h"
 struct elf64_sym {
    Elf64_Word st_name ;
    unsigned char st_info ;
    unsigned char st_other ;
    Elf64_Half st_shndx ;
    Elf64_Addr st_value ;
    Elf64_Xword st_size ;
 };
 #line 201 "include/linux/elf.h"
 typedef struct elf64_sym Elf64_Sym;
 #line 445
 struct sock;
 #line 445
 struct sock;
 #line 446
 struct kobject;
 #line 446
 struct kobject;
 #line 447
 enum kobj_ns_type {
     KOBJ_NS_TYPE_NONE = 0,
     KOBJ_NS_TYPE_NET = 1,
     KOBJ_NS_TYPES = 2
 } ;
 #line 453 "include/linux/elf.h"
 struct kobj_ns_type_operations {
    enum kobj_ns_type type ;
    void *(*grab_current_ns)(void) ;
    void const   *(*netlink_ns)(struct sock * ) ;
    void const   *(*initial_ns)(void) ;
    void (*drop_ns)(void * ) ;
 };
 #line 57 "include/linux/kobject_ns.h"
 struct attribute {
    char const   *name ;
    umode_t mode ;
    struct lock_class_key *key ;
    struct lock_class_key skey ;
 };
 #line 98 "include/linux/sysfs.h"
 struct sysfs_ops {
    ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
    ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
    void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 };
 #line 117
 struct sysfs_dirent;
 #line 117
 struct sysfs_dirent;
 #line 182 "include/linux/sysfs.h"
 struct kref {
    atomic_t refcount ;
 };
 #line 49 "include/linux/kobject.h"
 struct kset;
 #line 49
 struct kobj_type;
 #line 49 "include/linux/kobject.h"
 struct kobject {
    char const   *name ;
    struct list_head entry ;
    struct kobject *parent ;
    struct kset *kset ;
    struct kobj_type *ktype ;
    struct sysfs_dirent *sd ;
    struct kref kref ;
    unsigned char state_initialized : 1 ;
    unsigned char state_in_sysfs : 1 ;
    unsigned char state_add_uevent_sent : 1 ;
    unsigned char state_remove_uevent_sent : 1 ;
    unsigned char uevent_suppress : 1 ;
 };
 #line 107 "include/linux/kobject.h"
 struct kobj_type {
    void (*release)(struct kobject * ) ;
    struct sysfs_ops  const  *sysfs_ops ;
    struct attribute **default_attrs ;
    struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
    void const   *(*namespace)(struct kobject * ) ;
 };
 #line 115 "include/linux/kobject.h"
 struct kobj_uevent_env {
    char *envp[32U] ;
    int envp_idx ;
    char buf[2048U] ;
    int buflen ;
 };
 #line 122 "include/linux/kobject.h"
 struct kset_uevent_ops {
    int (* const  filter)(struct kset * , struct kobject * ) ;
    char const   *(* const  name)(struct kset * , struct kobject * ) ;
    int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 };
 #line 139 "include/linux/kobject.h"
 struct kset {
    struct list_head list ;
    spinlock_t list_lock ;
    struct kobject kobj ;
    struct kset_uevent_ops  const  *uevent_ops ;
 };
 #line 215
 struct kernel_param;
 #line 215
 struct kernel_param;
 #line 216 "include/linux/kobject.h"
 struct kernel_param_ops {
    int (*set)(char const   * , struct kernel_param  const  * ) ;
    int (*get)(char * , struct kernel_param  const  * ) ;
    void (*free)(void * ) ;
 };
 #line 49 "include/linux/moduleparam.h"
 struct kparam_string;
 #line 49
 struct kparam_array;
 #line 49 "include/linux/moduleparam.h"
 union __anonunion_ldv_13363_134 {
    void *arg ;
    struct kparam_string  const  *str ;
    struct kparam_array  const  *arr ;
 };
 #line 49 "include/linux/moduleparam.h"
 struct kernel_param {
    char const   *name ;
    struct kernel_param_ops  const  *ops ;
    u16 perm ;
    s16 level ;
    union __anonunion_ldv_13363_134 ldv_13363 ;
 };
 #line 61 "include/linux/moduleparam.h"
 struct kparam_string {
    unsigned int maxlen ;
    char *string ;
 };
 #line 67 "include/linux/moduleparam.h"
 struct kparam_array {
    unsigned int max ;
    unsigned int elemsize ;
    unsigned int *num ;
    struct kernel_param_ops  const  *ops ;
    void *elem ;
 };
 #line 458 "include/linux/moduleparam.h"
 struct static_key {
    atomic_t enabled ;
 };
 #line 225 "include/linux/jump_label.h"
 struct tracepoint;
 #line 225
 struct tracepoint;
 #line 226 "include/linux/jump_label.h"
 struct tracepoint_func {
    void *func ;
    void *data ;
 };
 #line 29 "include/linux/tracepoint.h"
 struct tracepoint {
    char const   *name ;
    struct static_key key ;
    void (*regfunc)(void) ;
    void (*unregfunc)(void) ;
    struct tracepoint_func *funcs ;
 };
 #line 86 "include/linux/tracepoint.h"
 struct kernel_symbol {
    unsigned long value ;
    char const   *name ;
 };
 #line 27 "include/linux/export.h"
 struct mod_arch_specific {
 
 };
 #line 34 "include/linux/module.h"
 struct module_param_attrs;
 #line 34 "include/linux/module.h"
 struct module_kobject {
    struct kobject kobj ;
    struct module *mod ;
    struct kobject *drivers_dir ;
    struct module_param_attrs *mp ;
 };
 #line 43 "include/linux/module.h"
 struct module_attribute {
    struct attribute attr ;
    ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
    ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
                     size_t  ) ;
    void (*setup)(struct module * , char const   * ) ;
    int (*test)(struct module * ) ;
    void (*free)(struct module * ) ;
 };
 #line 69
 struct exception_table_entry;
 #line 69
 struct exception_table_entry;
 #line 198
 enum module_state {
     MODULE_STATE_LIVE = 0,
     MODULE_STATE_COMING = 1,
     MODULE_STATE_GOING = 2
 } ;
 #line 204 "include/linux/module.h"
 struct module_ref {
    unsigned long incs ;
    unsigned long decs ;
 };
 #line 219
 struct module_sect_attrs;
 #line 219
 struct module_notes_attrs;
 #line 219
 struct ftrace_event_call;
 #line 219 "include/linux/module.h"
 struct module {
    enum module_state state ;
    struct list_head list ;
    char name[56U] ;
    struct module_kobject mkobj ;
    struct module_attribute *modinfo_attrs ;
    char const   *version ;
    char const   *srcversion ;
    struct kobject *holders_dir ;
    struct kernel_symbol  const  *syms ;
    unsigned long const   *crcs ;
    unsigned int num_syms ;
    struct kernel_param *kp ;
    unsigned int num_kp ;
    unsigned int num_gpl_syms ;
    struct kernel_symbol  const  *gpl_syms ;
    unsigned long const   *gpl_crcs ;
    struct kernel_symbol  const  *unused_syms ;
    unsigned long const   *unused_crcs ;
    unsigned int num_unused_syms ;
    unsigned int num_unused_gpl_syms ;
    struct kernel_symbol  const  *unused_gpl_syms ;
    unsigned long const   *unused_gpl_crcs ;
    struct kernel_symbol  const  *gpl_future_syms ;
    unsigned long const   *gpl_future_crcs ;
    unsigned int num_gpl_future_syms ;
    unsigned int num_exentries ;
    struct exception_table_entry *extable ;
    int (*init)(void) ;
    void *module_init ;
    void *module_core ;
    unsigned int init_size ;
    unsigned int core_size ;
    unsigned int init_text_size ;
    unsigned int core_text_size ;
    unsigned int init_ro_size ;
    unsigned int core_ro_size ;
    struct mod_arch_specific arch ;
    unsigned int taints ;
    unsigned int num_bugs ;
    struct list_head bug_list ;
    struct bug_entry *bug_table ;
    Elf64_Sym *symtab ;
    Elf64_Sym *core_symtab ;
    unsigned int num_symtab ;
    unsigned int core_num_syms ;
    char *strtab ;
    char *core_strtab ;
    struct module_sect_attrs *sect_attrs ;
    struct module_notes_attrs *notes_attrs ;
    char *args ;
    void *percpu ;
    unsigned int percpu_size ;
    unsigned int num_tracepoints ;
    struct tracepoint * const  *tracepoints_ptrs ;
    unsigned int num_trace_bprintk_fmt ;
    char const   **trace_bprintk_fmt_start ;
    struct ftrace_event_call **trace_events ;
    unsigned int num_trace_events ;
    struct list_head source_list ;
    struct list_head target_list ;
    struct task_struct *waiter ;
    void (*exit)(void) ;
    struct module_ref *refptr ;
    ctor_fn_t (**ctors)(void) ;
    unsigned int num_ctors ;
 };
 #line 88 "include/linux/kmemleak.h"
 struct kmem_cache_cpu {
    void **freelist ;
    unsigned long tid ;
    struct page *page ;
    struct page *partial ;
    int node ;
    unsigned int stat[26U] ;
 };
 #line 55 "include/linux/slub_def.h"
 struct kmem_cache_node {
    spinlock_t list_lock ;
    unsigned long nr_partial ;
    struct list_head partial ;
    atomic_long_t nr_slabs ;
    atomic_long_t total_objects ;
    struct list_head full ;
 };
 #line 66 "include/linux/slub_def.h"
 struct kmem_cache_order_objects {
    unsigned long x ;
 };
 #line 76 "include/linux/slub_def.h"
 struct kmem_cache {
    struct kmem_cache_cpu *cpu_slab ;
    unsigned long flags ;
    unsigned long min_partial ;
    int size ;
    int objsize ;
    int offset ;
    int cpu_partial ;
    struct kmem_cache_order_objects oo ;
    struct kmem_cache_order_objects max ;
    struct kmem_cache_order_objects min ;
    gfp_t allocflags ;
    int refcount ;
    void (*ctor)(void * ) ;
    int inuse ;
    int align ;
    int reserved ;
    char const   *name ;
    struct list_head list ;
    struct kobject kobj ;
    int remote_node_defrag_ratio ;
    struct kmem_cache_node *node[1024U] ;
 };
 #line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
 struct exception_table_entry {
    unsigned long insn ;
    unsigned long fixup ;
 };
 #line 110 "include/linux/uaccess.h"
 struct scatterlist;
 #line 110
 struct scatterlist;
 #line 111
 struct crypto_ablkcipher;
 #line 111
 struct crypto_ablkcipher;
 #line 112
 struct crypto_async_request;
 #line 112
 struct crypto_async_request;
 #line 113
 struct crypto_aead;
 #line 113
 struct crypto_aead;
 #line 114
 struct crypto_blkcipher;
 #line 114
 struct crypto_blkcipher;
 #line 115
 struct crypto_hash;
 #line 115
 struct crypto_hash;
 #line 116
 struct crypto_rng;
 #line 116
 struct crypto_rng;
 #line 117
 struct crypto_tfm;
 #line 117
 struct crypto_tfm;
 #line 118
 struct crypto_type;
 #line 118
 struct crypto_type;
 #line 119
 struct aead_givcrypt_request;
 #line 119
 struct aead_givcrypt_request;
 #line 120
 struct skcipher_givcrypt_request;
 #line 120
 struct skcipher_givcrypt_request;
 #line 129 "include/linux/crypto.h"
 struct crypto_async_request {
    struct list_head list ;
    void (*complete)(struct crypto_async_request * , int  ) ;
    void *data ;
    struct crypto_tfm *tfm ;
    u32 flags ;
 };
 #line 138 "include/linux/crypto.h"
 struct ablkcipher_request {
    struct crypto_async_request base ;
    unsigned int nbytes ;
    void *info ;
    struct scatterlist *src ;
    struct scatterlist *dst ;
    void *__ctx[0U] ;
 };
 #line 151 "include/linux/crypto.h"
 struct aead_request {
    struct crypto_async_request base ;
    unsigned int assoclen ;
    unsigned int cryptlen ;
    u8 *iv ;
    struct scatterlist *assoc ;
    struct scatterlist *src ;
    struct scatterlist *dst ;
    void *__ctx[0U] ;
 };
 #line 177 "include/linux/crypto.h"
 struct blkcipher_desc {
    struct crypto_blkcipher *tfm ;
    void *info ;
    u32 flags ;
 };
 #line 191 "include/linux/crypto.h"
 struct hash_desc {
    struct crypto_hash *tfm ;
    u32 flags ;
 };
 #line 196 "include/linux/crypto.h"
 struct ablkcipher_alg {
    int (*setkey)(struct crypto_ablkcipher * , u8 const   * , unsigned int  ) ;
    int (*encrypt)(struct ablkcipher_request * ) ;
    int (*decrypt)(struct ablkcipher_request * ) ;
    int (*givencrypt)(struct skcipher_givcrypt_request * ) ;
    int (*givdecrypt)(struct skcipher_givcrypt_request * ) ;
    char const   *geniv ;
    unsigned int min_keysize ;
    unsigned int max_keysize ;
    unsigned int ivsize ;
 };
 #line 215 "include/linux/crypto.h"
 struct aead_alg {
    int (*setkey)(struct crypto_aead * , u8 const   * , unsigned int  ) ;
    int (*setauthsize)(struct crypto_aead * , unsigned int  ) ;
    int (*encrypt)(struct aead_request * ) ;
    int (*decrypt)(struct aead_request * ) ;
    int (*givencrypt)(struct aead_givcrypt_request * ) ;
    int (*givdecrypt)(struct aead_givcrypt_request * ) ;
    char const   *geniv ;
    unsigned int ivsize ;
    unsigned int maxauthsize ;
 };
 #line 230 "include/linux/crypto.h"
 struct blkcipher_alg {
    int (*setkey)(struct crypto_tfm * , u8 const   * , unsigned int  ) ;
    int (*encrypt)(struct blkcipher_desc * , struct scatterlist * , struct scatterlist * ,
                   unsigned int  ) ;
    int (*decrypt)(struct blkcipher_desc * , struct scatterlist * , struct scatterlist * ,
                   unsigned int  ) ;
    char const   *geniv ;
    unsigned int min_keysize ;
    unsigned int max_keysize ;
    unsigned int ivsize ;
 };
 #line 247 "include/linux/crypto.h"
 struct cipher_alg {
    unsigned int cia_min_keysize ;
    unsigned int cia_max_keysize ;
    int (*cia_setkey)(struct crypto_tfm * , u8 const   * , unsigned int  ) ;
    void (*cia_encrypt)(struct crypto_tfm * , u8 * , u8 const   * ) ;
    void (*cia_decrypt)(struct crypto_tfm * , u8 * , u8 const   * ) ;
 };
 #line 256 "include/linux/crypto.h"
 struct compress_alg {
    int (*coa_compress)(struct crypto_tfm * , u8 const   * , unsigned int  , u8 * ,
                        unsigned int * ) ;
    int (*coa_decompress)(struct crypto_tfm * , u8 const   * , unsigned int  , u8 * ,
                          unsigned int * ) ;
 };
 #line 262 "include/linux/crypto.h"
 struct rng_alg {
    int (*rng_make_random)(struct crypto_rng * , u8 * , unsigned int  ) ;
    int (*rng_reset)(struct crypto_rng * , u8 * , unsigned int  ) ;
    unsigned int seedsize ;
 };
 #line 271 "include/linux/crypto.h"
 union __anonunion_cra_u_135 {
    struct ablkcipher_alg ablkcipher ;
    struct aead_alg aead ;
    struct blkcipher_alg blkcipher ;
    struct cipher_alg cipher ;
    struct compress_alg compress ;
    struct rng_alg rng ;
 };
 #line 271 "include/linux/crypto.h"
 struct crypto_alg {
    struct list_head cra_list ;
    struct list_head cra_users ;
    u32 cra_flags ;
    unsigned int cra_blocksize ;
    unsigned int cra_ctxsize ;
    unsigned int cra_alignmask ;
    int cra_priority ;
    atomic_t cra_refcnt ;
    char cra_name[64U] ;
    char cra_driver_name[64U] ;
    struct crypto_type  const  *cra_type ;
    union __anonunion_cra_u_135 cra_u ;
    int (*cra_init)(struct crypto_tfm * ) ;
    void (*cra_exit)(struct crypto_tfm * ) ;
    void (*cra_destroy)(struct crypto_alg * ) ;
    struct module *cra_module ;
 };
 #line 325 "include/linux/crypto.h"
 struct ablkcipher_tfm {
    int (*setkey)(struct crypto_ablkcipher * , u8 const   * , unsigned int  ) ;
    int (*encrypt)(struct ablkcipher_request * ) ;
    int (*decrypt)(struct ablkcipher_request * ) ;
    int (*givencrypt)(struct skcipher_givcrypt_request * ) ;
    int (*givdecrypt)(struct skcipher_givcrypt_request * ) ;
    struct crypto_ablkcipher *base ;
    unsigned int ivsize ;
    unsigned int reqsize ;
 };
 #line 345 "include/linux/crypto.h"
 struct aead_tfm {
    int (*setkey)(struct crypto_aead * , u8 const   * , unsigned int  ) ;
    int (*encrypt)(struct aead_request * ) ;
    int (*decrypt)(struct aead_request * ) ;
    int (*givencrypt)(struct aead_givcrypt_request * ) ;
    int (*givdecrypt)(struct aead_givcrypt_request * ) ;
    struct crypto_aead *base ;
    unsigned int ivsize ;
    unsigned int authsize ;
    unsigned int reqsize ;
 };
 #line 360 "include/linux/crypto.h"
 struct blkcipher_tfm {
    void *iv ;
    int (*setkey)(struct crypto_tfm * , u8 const   * , unsigned int  ) ;
    int (*encrypt)(struct blkcipher_desc * , struct scatterlist * , struct scatterlist * ,
                   unsigned int  ) ;
    int (*decrypt)(struct blkcipher_desc * , struct scatterlist * , struct scatterlist * ,
                   unsigned int  ) ;
 };
 #line 369 "include/linux/crypto.h"
 struct cipher_tfm {
    int (*cit_setkey)(struct crypto_tfm * , u8 const   * , unsigned int  ) ;
    void (*cit_encrypt_one)(struct crypto_tfm * , u8 * , u8 const   * ) ;
    void (*cit_decrypt_one)(struct crypto_tfm * , u8 * , u8 const   * ) ;
 };
 #line 377 "include/linux/crypto.h"
 struct hash_tfm {
    int (*init)(struct hash_desc * ) ;
    int (*update)(struct hash_desc * , struct scatterlist * , unsigned int  ) ;
    int (*final)(struct hash_desc * , u8 * ) ;
    int (*digest)(struct hash_desc * , struct scatterlist * , unsigned int  , u8 * ) ;
    int (*setkey)(struct crypto_hash * , u8 const   * , unsigned int  ) ;
    unsigned int digestsize ;
 };
 #line 389 "include/linux/crypto.h"
 struct compress_tfm {
    int (*cot_compress)(struct crypto_tfm * , u8 const   * , unsigned int  , u8 * ,
                        unsigned int * ) ;
    int (*cot_decompress)(struct crypto_tfm * , u8 const   * , unsigned int  , u8 * ,
                          unsigned int * ) ;
 };
 #line 396 "include/linux/crypto.h"
 struct rng_tfm {
    int (*rng_gen_random)(struct crypto_rng * , u8 * , unsigned int  ) ;
    int (*rng_reset)(struct crypto_rng * , u8 * , unsigned int  ) ;
 };
 #line 404 "include/linux/crypto.h"
 union __anonunion_crt_u_136 {
    struct ablkcipher_tfm ablkcipher ;
    struct aead_tfm aead ;
    struct blkcipher_tfm blkcipher ;
    struct cipher_tfm cipher ;
    struct hash_tfm hash ;
    struct compress_tfm compress ;
    struct rng_tfm rng ;
 };
 #line 404 "include/linux/crypto.h"
 struct crypto_tfm {
    u32 crt_flags ;
    union __anonunion_crt_u_136 crt_u ;
    void (*exit)(struct crypto_tfm * ) ;
    struct crypto_alg *__crt_alg ;
    void *__crt_ctx[0U] ;
 };
 #line 433 "include/linux/crypto.h"
 struct crypto_ablkcipher {
    struct crypto_tfm base ;
 };
 #line 437 "include/linux/crypto.h"
 struct crypto_aead {
    struct crypto_tfm base ;
 };
 #line 441 "include/linux/crypto.h"
 struct crypto_blkcipher {
    struct crypto_tfm base ;
 };
 #line 453 "include/linux/crypto.h"
 struct crypto_hash {
    struct crypto_tfm base ;
 };
 #line 457 "include/linux/crypto.h"
 struct crypto_rng {
    struct crypto_tfm base ;
 };
 #line 116 "include/linux/prio_tree.h"
 struct address_space;
 #line 116
 struct address_space;
 #line 117 "include/linux/prio_tree.h"
 union __anonunion_ldv_15229_138 {
    unsigned long index ;
    void *freelist ;
 };
 #line 117 "include/linux/prio_tree.h"
 struct __anonstruct_ldv_15239_142 {
    unsigned short inuse ;
    unsigned short objects : 15 ;
    unsigned char frozen : 1 ;
 };
 #line 117 "include/linux/prio_tree.h"
 union __anonunion_ldv_15240_141 {
    atomic_t _mapcount ;
    struct __anonstruct_ldv_15239_142 ldv_15239 ;
 };
 #line 117 "include/linux/prio_tree.h"
 struct __anonstruct_ldv_15242_140 {
    union __anonunion_ldv_15240_141 ldv_15240 ;
    atomic_t _count ;
 };
 #line 117 "include/linux/prio_tree.h"
 union __anonunion_ldv_15243_139 {
    unsigned long counters ;
    struct __anonstruct_ldv_15242_140 ldv_15242 ;
 };
 #line 117 "include/linux/prio_tree.h"
 struct __anonstruct_ldv_15244_137 {
    union __anonunion_ldv_15229_138 ldv_15229 ;
    union __anonunion_ldv_15243_139 ldv_15243 ;
 };
 #line 117 "include/linux/prio_tree.h"
 struct __anonstruct_ldv_15251_144 {
    struct page *next ;
    int pages ;
    int pobjects ;
 };
 #line 117 "include/linux/prio_tree.h"
 union __anonunion_ldv_15252_143 {
    struct list_head lru ;
    struct __anonstruct_ldv_15251_144 ldv_15251 ;
 };
 #line 117 "include/linux/prio_tree.h"
 union __anonunion_ldv_15257_145 {
    unsigned long private ;
    struct kmem_cache *slab ;
    struct page *first_page ;
 };
 #line 117 "include/linux/prio_tree.h"
 struct page {
    unsigned long flags ;
    struct address_space *mapping ;
    struct __anonstruct_ldv_15244_137 ldv_15244 ;
    union __anonunion_ldv_15252_143 ldv_15252 ;
    union __anonunion_ldv_15257_145 ldv_15257 ;
    unsigned long debug_flags ;
 };
 #line 119 "include/linux/ppp_defs.h"
 struct compstat {
    __u32 unc_bytes ;
    __u32 unc_packets ;
    __u32 comp_bytes ;
    __u32 comp_packets ;
    __u32 inc_bytes ;
    __u32 inc_packets ;
    __u32 in_count ;
    __u32 bytes_out ;
    double ratio ;
 };
 #line 153 "include/linux/ppp_defs.h"
 struct compressor {
    int compress_proto ;
    void *(*comp_alloc)(unsigned char * , int  ) ;
    void (*comp_free)(void * ) ;
    int (*comp_init)(void * , unsigned char * , int  , int  , int  , int  ) ;
    void (*comp_reset)(void * ) ;
    int (*compress)(void * , unsigned char * , unsigned char * , int  , int  ) ;
    void (*comp_stat)(void * , struct compstat * ) ;
    void *(*decomp_alloc)(unsigned char * , int  ) ;
    void (*decomp_free)(void * ) ;
    int (*decomp_init)(void * , unsigned char * , int  , int  , int  , int  , int  ) ;
    void (*decomp_reset)(void * ) ;
    int (*decompress)(void * , unsigned char * , int  , unsigned char * , int  ) ;
    void (*incomp)(void * , unsigned char * , int  ) ;
    void (*decomp_stat)(void * , struct compstat * ) ;
    struct module *owner ;
    unsigned int comp_extra ;
 };
 #line 182 "include/linux/ppp-comp.h"
 struct scatterlist {
    unsigned long sg_magic ;
    unsigned long page_link ;
    unsigned int offset ;
    unsigned int length ;
    dma_addr_t dma_address ;
    unsigned int dma_length ;
 };
 #line 89 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
 struct sha_pad {
    unsigned char sha_pad1[40U] ;
    unsigned char sha_pad2[40U] ;
 };
 #line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
 struct ppp_mppe_state {
    struct crypto_blkcipher *arc4 ;
    struct crypto_hash *sha1 ;
    unsigned char *sha1_digest ;
    unsigned char master_key[16U] ;
    unsigned char session_key[16U] ;
    unsigned int keylen ;
    unsigned char bits ;
    unsigned int ccount ;
    unsigned int stateful ;
    int discard ;
    int sanity_errors ;
    int unit ;
    int debug ;
    struct compstat stats ;
 };
 #line 1 "<compiler builtins>"
 
 #line 1
 long __builtin_expect(long  , long  ) ;
 #line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
 void ldv_spin_lock(void) ;
 #line 3
 void ldv_spin_unlock(void) ;
 #line 4
 int ldv_spin_trylock(void) ;
 #line 46 "include/linux/swab.h"
 __inline static __u16 __fswab16(__u16 val ) 
 { int __cil_tmp2 ;
   int __cil_tmp3 ;
   short __cil_tmp4 ;
   int __cil_tmp5 ;
   int __cil_tmp6 ;
   int __cil_tmp7 ;
   short __cil_tmp8 ;
   int __cil_tmp9 ;
   int __cil_tmp10 ;
 
   {
   {
 #line 51
   __cil_tmp2 = (int )val;
 #line 51
   __cil_tmp3 = __cil_tmp2 >> 8;
 #line 51
   __cil_tmp4 = (short )__cil_tmp3;
 #line 51
   __cil_tmp5 = (int )__cil_tmp4;
 #line 51
   __cil_tmp6 = (int )val;
 #line 51
   __cil_tmp7 = __cil_tmp6 << 8;
 #line 51
   __cil_tmp8 = (short )__cil_tmp7;
 #line 51
   __cil_tmp9 = (int )__cil_tmp8;
 #line 51
   __cil_tmp10 = __cil_tmp9 | __cil_tmp5;
 #line 51
   return ((__u16 )__cil_tmp10);
   }
 }
 }
 #line 101 "include/linux/printk.h"
 extern int printk(char const   *  , ...) ;
 #line 320 "include/linux/kernel.h"
 extern int sprintf(char * , char const   *  , ...) ;
 #line 61 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_64_types.h"
 extern unsigned long __phys_addr(unsigned long  ) ;
 #line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
 extern void *__memcpy(void * , void const   * , size_t  ) ;
 #line 55
 extern void *memset(void * , int  , size_t  ) ;
 #line 32 "include/linux/err.h"
 __inline static long IS_ERR(void const   *ptr ) 
 { long tmp ;
   unsigned long __cil_tmp3 ;
   int __cil_tmp4 ;
   long __cil_tmp5 ;
 
   {
   {
 #line 34
   __cil_tmp3 = (unsigned long )ptr;
 #line 34
   __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;
 #line 34
   __cil_tmp5 = (long )__cil_tmp4;
 #line 34
   tmp = __builtin_expect(__cil_tmp5, 0L);
   }
 #line 34
   return (tmp);
 }
 }
 #line 26 "include/linux/export.h"
 extern struct module __this_module ;
 #line 161 "include/linux/slab.h"
 extern void kfree(void const   * ) ;
 #line 220 "include/linux/slub_def.h"
 extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
 #line 223
 void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
 #line 225
 extern void *__kmalloc(size_t  , gfp_t  ) ;
 #line 268 "include/linux/slub_def.h"
__inline static void *ldv_kmalloc_12(size_t size , gfp_t flags ) 
{ void *tmp___2 ;

  {
  {
#line 283
  tmp___2 = __kmalloc(size, flags);
  }
#line 283
  return (tmp___2);
}
}
#line 268
__inline static void *kmalloc(size_t size , gfp_t flags ) ;
#line 353 "include/linux/slab.h"
__inline static void *kzalloc(size_t size , gfp_t flags ) ;
#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
extern void *__VERIFIER_nondet_pointer(void) ;
#line 11
void ldv_check_alloc_flags(gfp_t flags ) ;
#line 12
void ldv_check_alloc_nonatomic(void) ;
#line 14
struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
#line 324 "include/linux/crypto.h"
extern int crypto_has_alg(char const   * , u32  , u32  ) ;
#line 492
extern struct crypto_tfm *crypto_alloc_base(char const   * , u32  , u32  ) ;
#line 495 "include/linux/crypto.h"
__inline static void crypto_free_tfm(struct crypto_tfm *tfm ) 
{ 

  {
#line 497
  return;
}
}
#line 871 "include/linux/crypto.h"
__inline static struct crypto_blkcipher *__crypto_blkcipher_cast(struct crypto_tfm *tfm ) 
{ 

  {
#line 874
  return ((struct crypto_blkcipher *)tfm);
}
}
#line 884 "include/linux/crypto.h"
__inline static struct crypto_blkcipher *crypto_alloc_blkcipher(char const   *alg_name ,
                                                                u32 type , u32 mask ) 
{ struct crypto_tfm *tmp ;
  struct crypto_blkcipher *tmp___0 ;

  {
  {
#line 887
  type = type & 4294967280U;
#line 888
  type = type | 4U;
#line 889
  mask = mask | 15U;
#line 891
  tmp = crypto_alloc_base(alg_name, type, mask);
#line 891
  tmp___0 = __crypto_blkcipher_cast(tmp);
  }
#line 891
  return (tmp___0);
}
}
#line 894 "include/linux/crypto.h"
__inline static struct crypto_tfm *crypto_blkcipher_tfm(struct crypto_blkcipher *tfm ) 
{ 

  {
#line 897
  return ((struct crypto_tfm *)tfm);
}
}
#line 900 "include/linux/crypto.h"
__inline static void crypto_free_blkcipher(struct crypto_blkcipher *tfm ) 
{ struct crypto_tfm *tmp ;

  {
  {
#line 902
  tmp = crypto_blkcipher_tfm(tfm);
#line 902
  crypto_free_tfm(tmp);
  }
#line 903
  return;
}
}
#line 905 "include/linux/crypto.h"
__inline static int crypto_has_blkcipher(char const   *alg_name , u32 type , u32 mask ) 
{ int tmp ;

  {
  {
#line 907
  type = type & 4294967280U;
#line 908
  type = type | 4U;
#line 909
  mask = mask | 15U;
#line 911
  tmp = crypto_has_alg(alg_name, type, mask);
  }
#line 911
  return (tmp);
}
}
#line 919 "include/linux/crypto.h"
__inline static struct blkcipher_tfm *crypto_blkcipher_crt(struct crypto_blkcipher *tfm ) 
{ struct crypto_tfm *tmp ;
  unsigned long __cil_tmp3 ;
  unsigned long __cil_tmp4 ;

  {
  {
#line 922
  tmp = crypto_blkcipher_tfm(tfm);
  }
  {
#line 922
  __cil_tmp3 = (unsigned long )tmp;
#line 922
  __cil_tmp4 = __cil_tmp3 + 8;
#line 922
  return ((struct blkcipher_tfm *)__cil_tmp4);
  }
}
}
#line 965 "include/linux/crypto.h"
__inline static int crypto_blkcipher_setkey(struct crypto_blkcipher *tfm , u8 const   *key ,
                                            unsigned int keylen ) 
{ struct blkcipher_tfm *tmp ;
  struct crypto_tfm *tmp___0 ;
  int tmp___1 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  int (*__cil_tmp9)(struct crypto_tfm * , u8 const   * , unsigned int  ) ;

  {
  {
#line 968
  tmp = crypto_blkcipher_crt(tfm);
#line 968
  tmp___0 = crypto_blkcipher_tfm(tfm);
#line 968
  __cil_tmp7 = (unsigned long )tmp;
#line 968
  __cil_tmp8 = __cil_tmp7 + 8;
#line 968
  __cil_tmp9 = *((int (**)(struct crypto_tfm * , u8 const   * , unsigned int  ))__cil_tmp8);
#line 968
  tmp___1 = (*__cil_tmp9)(tmp___0, key, keylen);
  }
#line 968
  return (tmp___1);
}
}
#line 972 "include/linux/crypto.h"
__inline static int crypto_blkcipher_encrypt(struct blkcipher_desc *desc , struct scatterlist *dst ,
                                             struct scatterlist *src , unsigned int nbytes ) 
{ struct blkcipher_tfm *tmp ;
  struct blkcipher_tfm *tmp___0 ;
  int tmp___1 ;
  struct crypto_blkcipher *__cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  struct crypto_blkcipher *__cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  int (*__cil_tmp14)(struct blkcipher_desc * , struct scatterlist * , struct scatterlist * ,
                     unsigned int  ) ;

  {
  {
#line 977
  __cil_tmp8 = *((struct crypto_blkcipher **)desc);
#line 977
  tmp = crypto_blkcipher_crt(__cil_tmp8);
#line 977
  __cil_tmp9 = (unsigned long )desc;
#line 977
  __cil_tmp10 = __cil_tmp9 + 8;
#line 977
  *((void **)__cil_tmp10) = *((void **)tmp);
#line 978
  __cil_tmp11 = *((struct crypto_blkcipher **)desc);
#line 978
  tmp___0 = crypto_blkcipher_crt(__cil_tmp11);
#line 978
  __cil_tmp12 = (unsigned long )tmp___0;
#line 978
  __cil_tmp13 = __cil_tmp12 + 16;
#line 978
  __cil_tmp14 = *((int (**)(struct blkcipher_desc * , struct scatterlist * , struct scatterlist * ,
                            unsigned int  ))__cil_tmp13);
#line 978
  tmp___1 = (*__cil_tmp14)(desc, dst, src, nbytes);
  }
#line 978
  return (tmp___1);
}
}
#line 989 "include/linux/crypto.h"
__inline static int crypto_blkcipher_decrypt(struct blkcipher_desc *desc , struct scatterlist *dst ,
                                             struct scatterlist *src , unsigned int nbytes ) 
{ struct blkcipher_tfm *tmp ;
  struct blkcipher_tfm *tmp___0 ;
  int tmp___1 ;
  struct crypto_blkcipher *__cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  struct crypto_blkcipher *__cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  int (*__cil_tmp14)(struct blkcipher_desc * , struct scatterlist * , struct scatterlist * ,
                     unsigned int  ) ;

  {
  {
#line 994
  __cil_tmp8 = *((struct crypto_blkcipher **)desc);
#line 994
  tmp = crypto_blkcipher_crt(__cil_tmp8);
#line 994
  __cil_tmp9 = (unsigned long )desc;
#line 994
  __cil_tmp10 = __cil_tmp9 + 8;
#line 994
  *((void **)__cil_tmp10) = *((void **)tmp);
#line 995
  __cil_tmp11 = *((struct crypto_blkcipher **)desc);
#line 995
  tmp___0 = crypto_blkcipher_crt(__cil_tmp11);
#line 995
  __cil_tmp12 = (unsigned long )tmp___0;
#line 995
  __cil_tmp13 = __cil_tmp12 + 24;
#line 995
  __cil_tmp14 = *((int (**)(struct blkcipher_desc * , struct scatterlist * , struct scatterlist * ,
                            unsigned int  ))__cil_tmp13);
#line 995
  tmp___1 = (*__cil_tmp14)(desc, dst, src, nbytes);
  }
#line 995
  return (tmp___1);
}
}
#line 1111 "include/linux/crypto.h"
__inline static struct crypto_hash *__crypto_hash_cast(struct crypto_tfm *tfm ) 
{ 

  {
#line 1113
  return ((struct crypto_hash *)tfm);
}
}
#line 1123 "include/linux/crypto.h"
__inline static struct crypto_hash *crypto_alloc_hash(char const   *alg_name , u32 type ,
                                                      u32 mask ) 
{ struct crypto_tfm *tmp ;
  struct crypto_hash *tmp___0 ;

  {
  {
#line 1126
  type = type & 4294967280U;
#line 1127
  mask = mask & 4294967280U;
#line 1128
  type = type | 8U;
#line 1129
  mask = mask | 14U;
#line 1131
  tmp = crypto_alloc_base(alg_name, type, mask);
#line 1131
  tmp___0 = __crypto_hash_cast(tmp);
  }
#line 1131
  return (tmp___0);
}
}
#line 1134 "include/linux/crypto.h"
__inline static struct crypto_tfm *crypto_hash_tfm(struct crypto_hash *tfm ) 
{ 

  {
#line 1136
  return ((struct crypto_tfm *)tfm);
}
}
#line 1139 "include/linux/crypto.h"
__inline static void crypto_free_hash(struct crypto_hash *tfm ) 
{ struct crypto_tfm *tmp ;

  {
  {
#line 1141
  tmp = crypto_hash_tfm(tfm);
#line 1141
  crypto_free_tfm(tmp);
  }
#line 1142
  return;
}
}
#line 1144 "include/linux/crypto.h"
__inline static int crypto_has_hash(char const   *alg_name , u32 type , u32 mask ) 
{ int tmp ;

  {
  {
#line 1146
  type = type & 4294967280U;
#line 1147
  mask = mask & 4294967280U;
#line 1148
  type = type | 8U;
#line 1149
  mask = mask | 14U;
#line 1151
  tmp = crypto_has_alg(alg_name, type, mask);
  }
#line 1151
  return (tmp);
}
}
#line 1154 "include/linux/crypto.h"
__inline static struct hash_tfm *crypto_hash_crt(struct crypto_hash *tfm ) 
{ struct crypto_tfm *tmp ;
  unsigned long __cil_tmp3 ;
  unsigned long __cil_tmp4 ;

  {
  {
#line 1156
  tmp = crypto_hash_tfm(tfm);
  }
  {
#line 1156
  __cil_tmp3 = (unsigned long )tmp;
#line 1156
  __cil_tmp4 = __cil_tmp3 + 8;
#line 1156
  return ((struct hash_tfm *)__cil_tmp4);
  }
}
}
#line 1169 "include/linux/crypto.h"
__inline static unsigned int crypto_hash_digestsize(struct crypto_hash *tfm ) 
{ struct hash_tfm *tmp ;
  unsigned long __cil_tmp3 ;
  unsigned long __cil_tmp4 ;

  {
  {
#line 1171
  tmp = crypto_hash_crt(tfm);
  }
  {
#line 1171
  __cil_tmp3 = (unsigned long )tmp;
#line 1171
  __cil_tmp4 = __cil_tmp3 + 40;
#line 1171
  return (*((unsigned int *)__cil_tmp4));
  }
}
}
#line 1206 "include/linux/crypto.h"
__inline static int crypto_hash_digest(struct hash_desc *desc , struct scatterlist *sg ,
                                       unsigned int nbytes , u8 *out ) 
{ struct hash_tfm *tmp ;
  int tmp___0 ;
  struct crypto_hash *__cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  int (*__cil_tmp10)(struct hash_desc * , struct scatterlist * , unsigned int  , u8 * ) ;

  {
  {
#line 1210
  __cil_tmp7 = *((struct crypto_hash **)desc);
#line 1210
  tmp = crypto_hash_crt(__cil_tmp7);
#line 1210
  __cil_tmp8 = (unsigned long )tmp;
#line 1210
  __cil_tmp9 = __cil_tmp8 + 24;
#line 1210
  __cil_tmp10 = *((int (**)(struct hash_desc * , struct scatterlist * , unsigned int  ,
                            u8 * ))__cil_tmp9);
#line 1210
  tmp___0 = (*__cil_tmp10)(desc, sg, nbytes, out);
  }
#line 1210
  return (tmp___0);
}
}
#line 180 "include/linux/ppp-comp.h"
extern int ppp_register_compressor(struct compressor * ) ;
#line 181
extern void ppp_unregister_compressor(struct compressor * ) ;
#line 57 "include/linux/scatterlist.h"
__inline static void sg_assign_page(struct scatterlist *sg , struct page *page ) 
{ unsigned long page_link ;
  long tmp ;
  long tmp___0 ;
  long tmp___1 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  int __cil_tmp12 ;
  long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  int __cil_tmp15 ;
  long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  int __cil_tmp20 ;
  long __cil_tmp21 ;
  long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;

  {
  {
#line 59
  __cil_tmp7 = (unsigned long )sg;
#line 59
  __cil_tmp8 = __cil_tmp7 + 8;
#line 59
  __cil_tmp9 = *((unsigned long *)__cil_tmp8);
#line 59
  page_link = __cil_tmp9 & 3UL;
#line 65
  __cil_tmp10 = (unsigned long )page;
#line 65
  __cil_tmp11 = __cil_tmp10 & 3UL;
#line 65
  __cil_tmp12 = __cil_tmp11 != 0UL;
#line 65
  __cil_tmp13 = (long )__cil_tmp12;
#line 65
  tmp = __builtin_expect(__cil_tmp13, 0L);
  }
#line 65
  if (tmp != 0L) {
#line 65
    __asm__  volatile   ("1:\tud2\n.pushsection __bug_table,\"a\"\n2:\t.long 1b - 2b, %c0 - 2b\n\t.word %c1, 0\n\t.org 2b+%c2\n.popsection": : "i" ((char *)"include/linux/scatterlist.h"),
                         "i" (65), "i" (12UL));
    ldv_17922: ;
#line 65
    goto ldv_17922;
  } else {

  }
  {
#line 67
  __cil_tmp14 = *((unsigned long *)sg);
#line 67
  __cil_tmp15 = __cil_tmp14 != 2271560481UL;
#line 67
  __cil_tmp16 = (long )__cil_tmp15;
#line 67
  tmp___0 = __builtin_expect(__cil_tmp16, 0L);
  }
#line 67
  if (tmp___0 != 0L) {
#line 67
    __asm__  volatile   ("1:\tud2\n.pushsection __bug_table,\"a\"\n2:\t.long 1b - 2b, %c0 - 2b\n\t.word %c1, 0\n\t.org 2b+%c2\n.popsection": : "i" ((char *)"include/linux/scatterlist.h"),
                         "i" (67), "i" (12UL));
    ldv_17923: ;
#line 67
    goto ldv_17923;
  } else {

  }
  {
#line 68
  __cil_tmp17 = (unsigned long )sg;
#line 68
  __cil_tmp18 = __cil_tmp17 + 8;
#line 68
  __cil_tmp19 = *((unsigned long *)__cil_tmp18);
#line 68
  __cil_tmp20 = (int )__cil_tmp19;
#line 68
  __cil_tmp21 = (long )__cil_tmp20;
#line 68
  __cil_tmp22 = __cil_tmp21 & 1L;
#line 68
  tmp___1 = __builtin_expect(__cil_tmp22, 0L);
  }
#line 68
  if (tmp___1 != 0L) {
#line 68
    __asm__  volatile   ("1:\tud2\n.pushsection __bug_table,\"a\"\n2:\t.long 1b - 2b, %c0 - 2b\n\t.word %c1, 0\n\t.org 2b+%c2\n.popsection": : "i" ((char *)"include/linux/scatterlist.h"),
                         "i" (68), "i" (12UL));
    ldv_17924: ;
#line 68
    goto ldv_17924;
  } else {

  }
#line 70
  __cil_tmp23 = (unsigned long )sg;
#line 70
  __cil_tmp24 = __cil_tmp23 + 8;
#line 70
  __cil_tmp25 = (unsigned long )page;
#line 70
  *((unsigned long *)__cil_tmp24) = page_link | __cil_tmp25;
#line 71
  return;
}
}
#line 87 "include/linux/scatterlist.h"
__inline static void sg_set_page(struct scatterlist *sg , struct page *page , unsigned int len ,
                                 unsigned int offset ) 
{ unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;

  {
  {
#line 90
  sg_assign_page(sg, page);
#line 91
  __cil_tmp5 = (unsigned long )sg;
#line 91
  __cil_tmp6 = __cil_tmp5 + 16;
#line 91
  *((unsigned int *)__cil_tmp6) = offset;
#line 92
  __cil_tmp7 = (unsigned long )sg;
#line 92
  __cil_tmp8 = __cil_tmp7 + 20;
#line 92
  *((unsigned int *)__cil_tmp8) = len;
  }
#line 93
  return;
}
}
#line 111 "include/linux/scatterlist.h"
__inline static void sg_set_buf(struct scatterlist *sg , void const   *buf , unsigned int buflen ) 
{ unsigned long tmp ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  struct page *__cil_tmp8 ;
  long __cil_tmp9 ;
  unsigned int __cil_tmp10 ;
  unsigned int __cil_tmp11 ;

  {
  {
#line 114
  __cil_tmp5 = (unsigned long )buf;
#line 114
  tmp = __phys_addr(__cil_tmp5);
#line 114
  __cil_tmp6 = tmp >> 12;
#line 114
  __cil_tmp7 = 0xffffea0000000000UL + __cil_tmp6;
#line 114
  __cil_tmp8 = (struct page *)__cil_tmp7;
#line 114
  __cil_tmp9 = (long )buf;
#line 114
  __cil_tmp10 = (unsigned int )__cil_tmp9;
#line 114
  __cil_tmp11 = __cil_tmp10 & 4095U;
#line 114
  sg_set_page(sg, __cil_tmp8, buflen, __cil_tmp11);
  }
#line 115
  return;
}
}
#line 206
extern void sg_init_table(struct scatterlist * , unsigned int  ) ;
#line 52 "include/linux/unaligned/access_ok.h"
__inline static void put_unaligned_be16(u16 val , void *p ) 
{ __u16 tmp ;
  int __cil_tmp4 ;
  __u16 __cil_tmp5 ;
  __be16 *__cil_tmp6 ;

  {
  {
#line 54
  __cil_tmp4 = (int )val;
#line 54
  __cil_tmp5 = (__u16 )__cil_tmp4;
#line 54
  tmp = __fswab16(__cil_tmp5);
#line 54
  __cil_tmp6 = (__be16 *)p;
#line 54
  *__cil_tmp6 = tmp;
  }
#line 55
  return;
}
}
#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static unsigned int setup_sg(struct scatterlist *sg , void const   *address , unsigned int length ) 
{ 

  {
  {
#line 86
  sg_set_buf(sg, address, length);
  }
#line 87
  return (length);
}
}
#line 101 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static struct sha_pad *sha_pad  ;
#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
__inline static void sha_pad_init(struct sha_pad *shapad ) 
{ unsigned char (*__cil_tmp2)[40U] ;
  void *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned char (*__cil_tmp6)[40U] ;
  void *__cil_tmp7 ;

  {
  {
#line 105
  __cil_tmp2 = (unsigned char (*)[40U])shapad;
#line 105
  __cil_tmp3 = (void *)__cil_tmp2;
#line 105
  memset(__cil_tmp3, 0, 40UL);
#line 106
  __cil_tmp4 = (unsigned long )shapad;
#line 106
  __cil_tmp5 = __cil_tmp4 + 40;
#line 106
  __cil_tmp6 = (unsigned char (*)[40U])__cil_tmp5;
#line 106
  __cil_tmp7 = (void *)__cil_tmp6;
#line 106
  memset(__cil_tmp7, 242, 40UL);
  }
#line 107
  return;
}
}
#line 152 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void get_new_key_from_sha(struct ppp_mppe_state *state ) 
{ struct hash_desc desc ;
  struct scatterlist sg[4U] ;
  unsigned int nbytes ;
  unsigned int tmp ;
  unsigned int tmp___0 ;
  unsigned int tmp___1 ;
  struct scatterlist *__cil_tmp8 ;
  struct scatterlist *__cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned char (*__cil_tmp12)[16U] ;
  void const   *__cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned int __cil_tmp16 ;
  struct scatterlist *__cil_tmp17 ;
  struct scatterlist *__cil_tmp18 ;
  unsigned char (*__cil_tmp19)[40U] ;
  void const   *__cil_tmp20 ;
  struct scatterlist *__cil_tmp21 ;
  struct scatterlist *__cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned char (*__cil_tmp25)[16U] ;
  void const   *__cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  unsigned int __cil_tmp29 ;
  struct scatterlist *__cil_tmp30 ;
  struct scatterlist *__cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  unsigned char (*__cil_tmp34)[40U] ;
  void const   *__cil_tmp35 ;
  struct hash_desc *__cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  struct scatterlist *__cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned char *__cil_tmp43 ;

  {
  {
#line 158
  __cil_tmp8 = (struct scatterlist *)(& sg);
#line 158
  sg_init_table(__cil_tmp8, 4U);
#line 160
  __cil_tmp9 = (struct scatterlist *)(& sg);
#line 160
  __cil_tmp10 = (unsigned long )state;
#line 160
  __cil_tmp11 = __cil_tmp10 + 24;
#line 160
  __cil_tmp12 = (unsigned char (*)[16U])__cil_tmp11;
#line 160
  __cil_tmp13 = (void const   *)__cil_tmp12;
#line 160
  __cil_tmp14 = (unsigned long )state;
#line 160
  __cil_tmp15 = __cil_tmp14 + 56;
#line 160
  __cil_tmp16 = *((unsigned int *)__cil_tmp15);
#line 160
  nbytes = setup_sg(__cil_tmp9, __cil_tmp13, __cil_tmp16);
#line 161
  __cil_tmp17 = (struct scatterlist *)(& sg);
#line 161
  __cil_tmp18 = __cil_tmp17 + 1UL;
#line 161
  __cil_tmp19 = (unsigned char (*)[40U])sha_pad;
#line 161
  __cil_tmp20 = (void const   *)__cil_tmp19;
#line 161
  tmp = setup_sg(__cil_tmp18, __cil_tmp20, 40U);
#line 161
  nbytes = tmp + nbytes;
#line 163
  __cil_tmp21 = (struct scatterlist *)(& sg);
#line 163
  __cil_tmp22 = __cil_tmp21 + 2UL;
#line 163
  __cil_tmp23 = (unsigned long )state;
#line 163
  __cil_tmp24 = __cil_tmp23 + 40;
#line 163
  __cil_tmp25 = (unsigned char (*)[16U])__cil_tmp24;
#line 163
  __cil_tmp26 = (void const   *)__cil_tmp25;
#line 163
  __cil_tmp27 = (unsigned long )state;
#line 163
  __cil_tmp28 = __cil_tmp27 + 56;
#line 163
  __cil_tmp29 = *((unsigned int *)__cil_tmp28);
#line 163
  tmp___0 = setup_sg(__cil_tmp22, __cil_tmp26, __cil_tmp29);
#line 163
  nbytes = tmp___0 + nbytes;
#line 164
  __cil_tmp30 = (struct scatterlist *)(& sg);
#line 164
  __cil_tmp31 = __cil_tmp30 + 3UL;
#line 164
  __cil_tmp32 = (unsigned long )sha_pad;
#line 164
  __cil_tmp33 = __cil_tmp32 + 40;
#line 164
  __cil_tmp34 = (unsigned char (*)[40U])__cil_tmp33;
#line 164
  __cil_tmp35 = (void const   *)__cil_tmp34;
#line 164
  tmp___1 = setup_sg(__cil_tmp31, __cil_tmp35, 40U);
#line 164
  nbytes = tmp___1 + nbytes;
#line 167
  __cil_tmp36 = & desc;
#line 167
  __cil_tmp37 = (unsigned long )state;
#line 167
  __cil_tmp38 = __cil_tmp37 + 8;
#line 167
  *((struct crypto_hash **)__cil_tmp36) = *((struct crypto_hash **)__cil_tmp38);
#line 168
  __cil_tmp39 = (unsigned long )(& desc) + 8;
#line 168
  *((u32 *)__cil_tmp39) = 0U;
#line 170
  __cil_tmp40 = (struct scatterlist *)(& sg);
#line 170
  __cil_tmp41 = (unsigned long )state;
#line 170
  __cil_tmp42 = __cil_tmp41 + 16;
#line 170
  __cil_tmp43 = *((unsigned char **)__cil_tmp42);
#line 170
  crypto_hash_digest(& desc, __cil_tmp40, nbytes, __cil_tmp43);
  }
#line 171
  return;
}
}
#line 177 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void mppe_rekey(struct ppp_mppe_state *state , int initial_key ) 
{ struct scatterlist sg_in[1U] ;
  struct scatterlist sg_out[1U] ;
  struct blkcipher_desc desc ;
  int tmp ;
  size_t __len ;
  void *__ret ;
  struct blkcipher_desc *__cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  struct crypto_blkcipher *__cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned char *__cil_tmp15 ;
  u8 const   *__cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned int __cil_tmp19 ;
  struct scatterlist *__cil_tmp20 ;
  struct scatterlist *__cil_tmp21 ;
  struct scatterlist *__cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned char *__cil_tmp25 ;
  void const   *__cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  unsigned int __cil_tmp29 ;
  struct scatterlist *__cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned char (*__cil_tmp33)[16U] ;
  void const   *__cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned int __cil_tmp37 ;
  struct scatterlist *__cil_tmp38 ;
  struct scatterlist *__cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned int __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned int __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned char (*__cil_tmp48)[16U] ;
  void *__cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned char *__cil_tmp52 ;
  void const   *__cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  unsigned int __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  unsigned long __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  unsigned long __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  struct crypto_blkcipher *__cil_tmp69 ;
  unsigned long __cil_tmp70 ;
  unsigned long __cil_tmp71 ;
  unsigned char (*__cil_tmp72)[16U] ;
  u8 const   *__cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  unsigned int __cil_tmp76 ;

  {
  {
#line 180
  __cil_tmp9 = & desc;
#line 180
  *((struct crypto_blkcipher **)__cil_tmp9) = *((struct crypto_blkcipher **)state);
#line 180
  __cil_tmp10 = (unsigned long )(& desc) + 8;
#line 180
  *((void **)__cil_tmp10) = (void *)0;
#line 180
  __cil_tmp11 = (unsigned long )(& desc) + 16;
#line 180
  *((u32 *)__cil_tmp11) = 0U;
#line 182
  get_new_key_from_sha(state);
  }
#line 183
  if (initial_key == 0) {
    {
#line 184
    __cil_tmp12 = *((struct crypto_blkcipher **)state);
#line 184
    __cil_tmp13 = (unsigned long )state;
#line 184
    __cil_tmp14 = __cil_tmp13 + 16;
#line 184
    __cil_tmp15 = *((unsigned char **)__cil_tmp14);
#line 184
    __cil_tmp16 = (u8 const   *)__cil_tmp15;
#line 184
    __cil_tmp17 = (unsigned long )state;
#line 184
    __cil_tmp18 = __cil_tmp17 + 56;
#line 184
    __cil_tmp19 = *((unsigned int *)__cil_tmp18);
#line 184
    crypto_blkcipher_setkey(__cil_tmp12, __cil_tmp16, __cil_tmp19);
#line 186
    __cil_tmp20 = (struct scatterlist *)(& sg_in);
#line 186
    sg_init_table(__cil_tmp20, 1U);
#line 187
    __cil_tmp21 = (struct scatterlist *)(& sg_out);
#line 187
    sg_init_table(__cil_tmp21, 1U);
#line 188
    __cil_tmp22 = (struct scatterlist *)(& sg_in);
#line 188
    __cil_tmp23 = (unsigned long )state;
#line 188
    __cil_tmp24 = __cil_tmp23 + 16;
#line 188
    __cil_tmp25 = *((unsigned char **)__cil_tmp24);
#line 188
    __cil_tmp26 = (void const   *)__cil_tmp25;
#line 188
    __cil_tmp27 = (unsigned long )state;
#line 188
    __cil_tmp28 = __cil_tmp27 + 56;
#line 188
    __cil_tmp29 = *((unsigned int *)__cil_tmp28);
#line 188
    setup_sg(__cil_tmp22, __cil_tmp26, __cil_tmp29);
#line 189
    __cil_tmp30 = (struct scatterlist *)(& sg_out);
#line 189
    __cil_tmp31 = (unsigned long )state;
#line 189
    __cil_tmp32 = __cil_tmp31 + 40;
#line 189
    __cil_tmp33 = (unsigned char (*)[16U])__cil_tmp32;
#line 189
    __cil_tmp34 = (void const   *)__cil_tmp33;
#line 189
    __cil_tmp35 = (unsigned long )state;
#line 189
    __cil_tmp36 = __cil_tmp35 + 56;
#line 189
    __cil_tmp37 = *((unsigned int *)__cil_tmp36);
#line 189
    setup_sg(__cil_tmp30, __cil_tmp34, __cil_tmp37);
#line 190
    __cil_tmp38 = (struct scatterlist *)(& sg_out);
#line 190
    __cil_tmp39 = (struct scatterlist *)(& sg_in);
#line 190
    __cil_tmp40 = (unsigned long )state;
#line 190
    __cil_tmp41 = __cil_tmp40 + 56;
#line 190
    __cil_tmp42 = *((unsigned int *)__cil_tmp41);
#line 190
    tmp = crypto_blkcipher_encrypt(& desc, __cil_tmp38, __cil_tmp39, __cil_tmp42);
    }
#line 190
    if (tmp != 0) {
      {
#line 192
      printk("<4>mppe_rekey: cipher_encrypt failed\n");
      }
    } else {

    }
  } else {
    {
#line 195
    __cil_tmp43 = (unsigned long )state;
#line 195
    __cil_tmp44 = __cil_tmp43 + 56;
#line 195
    __cil_tmp45 = *((unsigned int *)__cil_tmp44);
#line 195
    __len = (size_t )__cil_tmp45;
#line 195
    __cil_tmp46 = (unsigned long )state;
#line 195
    __cil_tmp47 = __cil_tmp46 + 40;
#line 195
    __cil_tmp48 = (unsigned char (*)[16U])__cil_tmp47;
#line 195
    __cil_tmp49 = (void *)__cil_tmp48;
#line 195
    __cil_tmp50 = (unsigned long )state;
#line 195
    __cil_tmp51 = __cil_tmp50 + 16;
#line 195
    __cil_tmp52 = *((unsigned char **)__cil_tmp51);
#line 195
    __cil_tmp53 = (void const   *)__cil_tmp52;
#line 195
    __ret = __builtin_memcpy(__cil_tmp49, __cil_tmp53, __len);
    }
  }
  {
#line 197
  __cil_tmp54 = (unsigned long )state;
#line 197
  __cil_tmp55 = __cil_tmp54 + 56;
#line 197
  __cil_tmp56 = *((unsigned int *)__cil_tmp55);
#line 197
  if (__cil_tmp56 == 8U) {
#line 199
    __cil_tmp57 = 0 * 1UL;
#line 199
    __cil_tmp58 = 40 + __cil_tmp57;
#line 199
    __cil_tmp59 = (unsigned long )state;
#line 199
    __cil_tmp60 = __cil_tmp59 + __cil_tmp58;
#line 199
    *((unsigned char *)__cil_tmp60) = (unsigned char)209;
#line 200
    __cil_tmp61 = 1 * 1UL;
#line 200
    __cil_tmp62 = 40 + __cil_tmp61;
#line 200
    __cil_tmp63 = (unsigned long )state;
#line 200
    __cil_tmp64 = __cil_tmp63 + __cil_tmp62;
#line 200
    *((unsigned char *)__cil_tmp64) = (unsigned char)38;
#line 201
    __cil_tmp65 = 2 * 1UL;
#line 201
    __cil_tmp66 = 40 + __cil_tmp65;
#line 201
    __cil_tmp67 = (unsigned long )state;
#line 201
    __cil_tmp68 = __cil_tmp67 + __cil_tmp66;
#line 201
    *((unsigned char *)__cil_tmp68) = (unsigned char)158;
  } else {

  }
  }
  {
#line 203
  __cil_tmp69 = *((struct crypto_blkcipher **)state);
#line 203
  __cil_tmp70 = (unsigned long )state;
#line 203
  __cil_tmp71 = __cil_tmp70 + 40;
#line 203
  __cil_tmp72 = (unsigned char (*)[16U])__cil_tmp71;
#line 203
  __cil_tmp73 = (u8 const   *)__cil_tmp72;
#line 203
  __cil_tmp74 = (unsigned long )state;
#line 203
  __cil_tmp75 = __cil_tmp74 + 56;
#line 203
  __cil_tmp76 = *((unsigned int *)__cil_tmp75);
#line 203
  crypto_blkcipher_setkey(__cil_tmp69, __cil_tmp73, __cil_tmp76);
  }
#line 204
  return;
}
}
#line 209 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void *mppe_alloc(unsigned char *options , int optlen ) 
{ struct ppp_mppe_state *state ;
  unsigned int digestsize ;
  void *tmp ;
  long tmp___0 ;
  long tmp___1 ;
  void *tmp___2 ;
  size_t __len ;
  void *__ret ;
  size_t __len___0 ;
  void *__ret___0 ;
  unsigned char __cil_tmp13 ;
  unsigned int __cil_tmp14 ;
  unsigned char *__cil_tmp15 ;
  unsigned char __cil_tmp16 ;
  unsigned int __cil_tmp17 ;
  struct ppp_mppe_state *__cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  struct crypto_blkcipher *__cil_tmp21 ;
  void const   *__cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  struct crypto_hash *__cil_tmp27 ;
  void const   *__cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  struct crypto_hash *__cil_tmp33 ;
  size_t __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned char *__cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned char *__cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned char (*__cil_tmp45)[16U] ;
  void *__cil_tmp46 ;
  void const   *__cil_tmp47 ;
  void const   *__cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned char (*__cil_tmp51)[16U] ;
  void *__cil_tmp52 ;
  void const   *__cil_tmp53 ;
  void const   *__cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned char (*__cil_tmp57)[16U] ;
  void *__cil_tmp58 ;
  unsigned long __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned char (*__cil_tmp61)[16U] ;
  void const   *__cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  unsigned long __cil_tmp64 ;
  unsigned char (*__cil_tmp65)[16U] ;
  void *__cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  unsigned char (*__cil_tmp69)[16U] ;
  void const   *__cil_tmp70 ;
  unsigned char *__cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  unsigned char *__cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  unsigned char *__cil_tmp79 ;
  void const   *__cil_tmp80 ;
  struct crypto_hash *__cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  unsigned long __cil_tmp84 ;
  struct crypto_hash *__cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  unsigned long __cil_tmp87 ;
  unsigned long __cil_tmp88 ;
  struct crypto_hash *__cil_tmp89 ;
  struct crypto_blkcipher *__cil_tmp90 ;
  unsigned long __cil_tmp91 ;
  struct crypto_blkcipher *__cil_tmp92 ;
  unsigned long __cil_tmp93 ;
  struct crypto_blkcipher *__cil_tmp94 ;
  void const   *__cil_tmp95 ;

  {
#line 214
  if (optlen != 22) {
#line 216
    goto out;
  } else {
    {
#line 214
    __cil_tmp13 = *options;
#line 214
    __cil_tmp14 = (unsigned int )__cil_tmp13;
#line 214
    if (__cil_tmp14 != 18U) {
#line 216
      goto out;
    } else {
      {
#line 214
      __cil_tmp15 = options + 1UL;
#line 214
      __cil_tmp16 = *__cil_tmp15;
#line 214
      __cil_tmp17 = (unsigned int )__cil_tmp16;
#line 214
      if (__cil_tmp17 != 6U) {
#line 216
        goto out;
      } else {

      }
      }
    }
    }
  }
  {
#line 218
  tmp = kzalloc(128UL, 208U);
#line 218
  state = (struct ppp_mppe_state *)tmp;
  }
  {
#line 219
  __cil_tmp18 = (struct ppp_mppe_state *)0;
#line 219
  __cil_tmp19 = (unsigned long )__cil_tmp18;
#line 219
  __cil_tmp20 = (unsigned long )state;
#line 219
  if (__cil_tmp20 == __cil_tmp19) {
#line 220
    goto out;
  } else {

  }
  }
  {
#line 223
  *((struct crypto_blkcipher **)state) = crypto_alloc_blkcipher("ecb(arc4)", 0U, 128U);
#line 224
  __cil_tmp21 = *((struct crypto_blkcipher **)state);
#line 224
  __cil_tmp22 = (void const   *)__cil_tmp21;
#line 224
  tmp___0 = IS_ERR(__cil_tmp22);
  }
#line 224
  if (tmp___0 != 0L) {
#line 225
    *((struct crypto_blkcipher **)state) = (struct crypto_blkcipher *)0;
#line 226
    goto out_free;
  } else {

  }
  {
#line 229
  __cil_tmp23 = (unsigned long )state;
#line 229
  __cil_tmp24 = __cil_tmp23 + 8;
#line 229
  *((struct crypto_hash **)__cil_tmp24) = crypto_alloc_hash("sha1", 0U, 128U);
#line 230
  __cil_tmp25 = (unsigned long )state;
#line 230
  __cil_tmp26 = __cil_tmp25 + 8;
#line 230
  __cil_tmp27 = *((struct crypto_hash **)__cil_tmp26);
#line 230
  __cil_tmp28 = (void const   *)__cil_tmp27;
#line 230
  tmp___1 = IS_ERR(__cil_tmp28);
  }
#line 230
  if (tmp___1 != 0L) {
#line 231
    __cil_tmp29 = (unsigned long )state;
#line 231
    __cil_tmp30 = __cil_tmp29 + 8;
#line 231
    *((struct crypto_hash **)__cil_tmp30) = (struct crypto_hash *)0;
#line 232
    goto out_free;
  } else {

  }
  {
#line 235
  __cil_tmp31 = (unsigned long )state;
#line 235
  __cil_tmp32 = __cil_tmp31 + 8;
#line 235
  __cil_tmp33 = *((struct crypto_hash **)__cil_tmp32);
#line 235
  digestsize = crypto_hash_digestsize(__cil_tmp33);
  }
#line 236
  if (digestsize <= 15U) {
#line 237
    goto out_free;
  } else {

  }
  {
#line 239
  __cil_tmp34 = (size_t )digestsize;
#line 239
  tmp___2 = kmalloc(__cil_tmp34, 208U);
#line 239
  __cil_tmp35 = (unsigned long )state;
#line 239
  __cil_tmp36 = __cil_tmp35 + 16;
#line 239
  *((unsigned char **)__cil_tmp36) = (unsigned char *)tmp___2;
  }
  {
#line 240
  __cil_tmp37 = (unsigned char *)0;
#line 240
  __cil_tmp38 = (unsigned long )__cil_tmp37;
#line 240
  __cil_tmp39 = (unsigned long )state;
#line 240
  __cil_tmp40 = __cil_tmp39 + 16;
#line 240
  __cil_tmp41 = *((unsigned char **)__cil_tmp40);
#line 240
  __cil_tmp42 = (unsigned long )__cil_tmp41;
#line 240
  if (__cil_tmp42 == __cil_tmp38) {
#line 241
    goto out_free;
  } else {

  }
  }
#line 244
  __len = 16UL;
#line 244
  if (__len > 63UL) {
    {
#line 244
    __cil_tmp43 = (unsigned long )state;
#line 244
    __cil_tmp44 = __cil_tmp43 + 24;
#line 244
    __cil_tmp45 = (unsigned char (*)[16U])__cil_tmp44;
#line 244
    __cil_tmp46 = (void *)__cil_tmp45;
#line 244
    __cil_tmp47 = (void const   *)options;
#line 244
    __cil_tmp48 = __cil_tmp47 + 6U;
#line 244
    __ret = __memcpy(__cil_tmp46, __cil_tmp48, __len);
    }
  } else {
    {
#line 244
    __cil_tmp49 = (unsigned long )state;
#line 244
    __cil_tmp50 = __cil_tmp49 + 24;
#line 244
    __cil_tmp51 = (unsigned char (*)[16U])__cil_tmp50;
#line 244
    __cil_tmp52 = (void *)__cil_tmp51;
#line 244
    __cil_tmp53 = (void const   *)options;
#line 244
    __cil_tmp54 = __cil_tmp53 + 6U;
#line 244
    __ret = __builtin_memcpy(__cil_tmp52, __cil_tmp54, __len);
    }
  }
#line 246
  __len___0 = 16UL;
#line 246
  if (__len___0 > 63UL) {
    {
#line 246
    __cil_tmp55 = (unsigned long )state;
#line 246
    __cil_tmp56 = __cil_tmp55 + 40;
#line 246
    __cil_tmp57 = (unsigned char (*)[16U])__cil_tmp56;
#line 246
    __cil_tmp58 = (void *)__cil_tmp57;
#line 246
    __cil_tmp59 = (unsigned long )state;
#line 246
    __cil_tmp60 = __cil_tmp59 + 24;
#line 246
    __cil_tmp61 = (unsigned char (*)[16U])__cil_tmp60;
#line 246
    __cil_tmp62 = (void const   *)__cil_tmp61;
#line 246
    __ret___0 = __memcpy(__cil_tmp58, __cil_tmp62, __len___0);
    }
  } else {
    {
#line 246
    __cil_tmp63 = (unsigned long )state;
#line 246
    __cil_tmp64 = __cil_tmp63 + 40;
#line 246
    __cil_tmp65 = (unsigned char (*)[16U])__cil_tmp64;
#line 246
    __cil_tmp66 = (void *)__cil_tmp65;
#line 246
    __cil_tmp67 = (unsigned long )state;
#line 246
    __cil_tmp68 = __cil_tmp67 + 24;
#line 246
    __cil_tmp69 = (unsigned char (*)[16U])__cil_tmp68;
#line 246
    __cil_tmp70 = (void const   *)__cil_tmp69;
#line 246
    __ret___0 = __builtin_memcpy(__cil_tmp66, __cil_tmp70, __len___0);
    }
  }
#line 254
  return ((void *)state);
  out_free: ;
  {
#line 257
  __cil_tmp71 = (unsigned char *)0;
#line 257
  __cil_tmp72 = (unsigned long )__cil_tmp71;
#line 257
  __cil_tmp73 = (unsigned long )state;
#line 257
  __cil_tmp74 = __cil_tmp73 + 16;
#line 257
  __cil_tmp75 = *((unsigned char **)__cil_tmp74);
#line 257
  __cil_tmp76 = (unsigned long )__cil_tmp75;
#line 257
  if (__cil_tmp76 != __cil_tmp72) {
    {
#line 258
    __cil_tmp77 = (unsigned long )state;
#line 258
    __cil_tmp78 = __cil_tmp77 + 16;
#line 258
    __cil_tmp79 = *((unsigned char **)__cil_tmp78);
#line 258
    __cil_tmp80 = (void const   *)__cil_tmp79;
#line 258
    kfree(__cil_tmp80);
    }
  } else {

  }
  }
  {
#line 259
  __cil_tmp81 = (struct crypto_hash *)0;
#line 259
  __cil_tmp82 = (unsigned long )__cil_tmp81;
#line 259
  __cil_tmp83 = (unsigned long )state;
#line 259
  __cil_tmp84 = __cil_tmp83 + 8;
#line 259
  __cil_tmp85 = *((struct crypto_hash **)__cil_tmp84);
#line 259
  __cil_tmp86 = (unsigned long )__cil_tmp85;
#line 259
  if (__cil_tmp86 != __cil_tmp82) {
    {
#line 260
    __cil_tmp87 = (unsigned long )state;
#line 260
    __cil_tmp88 = __cil_tmp87 + 8;
#line 260
    __cil_tmp89 = *((struct crypto_hash **)__cil_tmp88);
#line 260
    crypto_free_hash(__cil_tmp89);
    }
  } else {

  }
  }
  {
#line 261
  __cil_tmp90 = (struct crypto_blkcipher *)0;
#line 261
  __cil_tmp91 = (unsigned long )__cil_tmp90;
#line 261
  __cil_tmp92 = *((struct crypto_blkcipher **)state);
#line 261
  __cil_tmp93 = (unsigned long )__cil_tmp92;
#line 261
  if (__cil_tmp93 != __cil_tmp91) {
    {
#line 262
    __cil_tmp94 = *((struct crypto_blkcipher **)state);
#line 262
    crypto_free_blkcipher(__cil_tmp94);
    }
  } else {

  }
  }
  {
#line 263
  __cil_tmp95 = (void const   *)state;
#line 263
  kfree(__cil_tmp95);
  }
  out: ;
#line 265
  return ((void *)0);
}
}
#line 271 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void mppe_free(void *arg ) 
{ struct ppp_mppe_state *state ;
  struct ppp_mppe_state *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned char *__cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned char *__cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned char *__cil_tmp14 ;
  void const   *__cil_tmp15 ;
  struct crypto_hash *__cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  struct crypto_hash *__cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  struct crypto_hash *__cil_tmp24 ;
  struct crypto_blkcipher *__cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  struct crypto_blkcipher *__cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  struct crypto_blkcipher *__cil_tmp29 ;
  void const   *__cil_tmp30 ;

  {
#line 273
  state = (struct ppp_mppe_state *)arg;
  {
#line 274
  __cil_tmp3 = (struct ppp_mppe_state *)0;
#line 274
  __cil_tmp4 = (unsigned long )__cil_tmp3;
#line 274
  __cil_tmp5 = (unsigned long )state;
#line 274
  if (__cil_tmp5 != __cil_tmp4) {
    {
#line 275
    __cil_tmp6 = (unsigned char *)0;
#line 275
    __cil_tmp7 = (unsigned long )__cil_tmp6;
#line 275
    __cil_tmp8 = (unsigned long )state;
#line 275
    __cil_tmp9 = __cil_tmp8 + 16;
#line 275
    __cil_tmp10 = *((unsigned char **)__cil_tmp9);
#line 275
    __cil_tmp11 = (unsigned long )__cil_tmp10;
#line 275
    if (__cil_tmp11 != __cil_tmp7) {
      {
#line 276
      __cil_tmp12 = (unsigned long )state;
#line 276
      __cil_tmp13 = __cil_tmp12 + 16;
#line 276
      __cil_tmp14 = *((unsigned char **)__cil_tmp13);
#line 276
      __cil_tmp15 = (void const   *)__cil_tmp14;
#line 276
      kfree(__cil_tmp15);
      }
    } else {

    }
    }
    {
#line 277
    __cil_tmp16 = (struct crypto_hash *)0;
#line 277
    __cil_tmp17 = (unsigned long )__cil_tmp16;
#line 277
    __cil_tmp18 = (unsigned long )state;
#line 277
    __cil_tmp19 = __cil_tmp18 + 8;
#line 277
    __cil_tmp20 = *((struct crypto_hash **)__cil_tmp19);
#line 277
    __cil_tmp21 = (unsigned long )__cil_tmp20;
#line 277
    if (__cil_tmp21 != __cil_tmp17) {
      {
#line 278
      __cil_tmp22 = (unsigned long )state;
#line 278
      __cil_tmp23 = __cil_tmp22 + 8;
#line 278
      __cil_tmp24 = *((struct crypto_hash **)__cil_tmp23);
#line 278
      crypto_free_hash(__cil_tmp24);
      }
    } else {

    }
    }
    {
#line 279
    __cil_tmp25 = (struct crypto_blkcipher *)0;
#line 279
    __cil_tmp26 = (unsigned long )__cil_tmp25;
#line 279
    __cil_tmp27 = *((struct crypto_blkcipher **)state);
#line 279
    __cil_tmp28 = (unsigned long )__cil_tmp27;
#line 279
    if (__cil_tmp28 != __cil_tmp26) {
      {
#line 280
      __cil_tmp29 = *((struct crypto_blkcipher **)state);
#line 280
      crypto_free_blkcipher(__cil_tmp29);
      }
    } else {

    }
    }
    {
#line 281
    __cil_tmp30 = (void const   *)state;
#line 281
    kfree(__cil_tmp30);
    }
  } else {

  }
  }
#line 283
  return;
}
}
#line 289 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static int mppe_init(void *arg , unsigned char *options , int optlen , int unit ,
                     int debug , char const   *debugstr ) 
{ struct ppp_mppe_state *state ;
  unsigned char mppe_opts ;
  u_char *ptr ;
  int i ;
  char mkey[33U] ;
  char skey[33U] ;
  char *tmp ;
  int tmp___0 ;
  unsigned char __cil_tmp15 ;
  unsigned int __cil_tmp16 ;
  unsigned char *__cil_tmp17 ;
  unsigned char __cil_tmp18 ;
  unsigned int __cil_tmp19 ;
  u_char __cil_tmp20 ;
  int __cil_tmp21 ;
  int __cil_tmp22 ;
  unsigned int __cil_tmp23 ;
  unsigned int __cil_tmp24 ;
  u_char *__cil_tmp25 ;
  u_char __cil_tmp26 ;
  int __cil_tmp27 ;
  int __cil_tmp28 ;
  unsigned int __cil_tmp29 ;
  unsigned int __cil_tmp30 ;
  u_char *__cil_tmp31 ;
  u_char __cil_tmp32 ;
  int __cil_tmp33 ;
  int __cil_tmp34 ;
  unsigned int __cil_tmp35 ;
  unsigned int __cil_tmp36 ;
  u_char *__cil_tmp37 ;
  u_char __cil_tmp38 ;
  signed char __cil_tmp39 ;
  int __cil_tmp40 ;
  unsigned int __cil_tmp41 ;
  unsigned int __cil_tmp42 ;
  u_char *__cil_tmp43 ;
  u_char __cil_tmp44 ;
  int __cil_tmp45 ;
  int __cil_tmp46 ;
  unsigned int __cil_tmp47 ;
  unsigned int __cil_tmp48 ;
  u_char *__cil_tmp49 ;
  u_char __cil_tmp50 ;
  int __cil_tmp51 ;
  unsigned int __cil_tmp52 ;
  unsigned int __cil_tmp53 ;
  u_char __cil_tmp54 ;
  int __cil_tmp55 ;
  int __cil_tmp56 ;
  unsigned int __cil_tmp57 ;
  unsigned int __cil_tmp58 ;
  u_char *__cil_tmp59 ;
  u_char __cil_tmp60 ;
  unsigned int __cil_tmp61 ;
  unsigned int __cil_tmp62 ;
  unsigned int __cil_tmp63 ;
  u_char *__cil_tmp64 ;
  u_char __cil_tmp65 ;
  unsigned int __cil_tmp66 ;
  unsigned int __cil_tmp67 ;
  unsigned int __cil_tmp68 ;
  u_char *__cil_tmp69 ;
  u_char __cil_tmp70 ;
  int __cil_tmp71 ;
  int __cil_tmp72 ;
  unsigned int __cil_tmp73 ;
  unsigned int __cil_tmp74 ;
  int __cil_tmp75 ;
  int __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  int __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  unsigned long __cil_tmp81 ;
  int __cil_tmp82 ;
  int __cil_tmp83 ;
  unsigned long __cil_tmp84 ;
  unsigned long __cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  unsigned long __cil_tmp87 ;
  unsigned int __cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  unsigned long __cil_tmp90 ;
  unsigned int __cil_tmp91 ;
  int __cil_tmp92 ;
  unsigned long __cil_tmp93 ;
  char *__cil_tmp94 ;
  char *__cil_tmp95 ;
  unsigned long __cil_tmp96 ;
  unsigned long __cil_tmp97 ;
  unsigned long __cil_tmp98 ;
  unsigned long __cil_tmp99 ;
  unsigned char __cil_tmp100 ;
  int __cil_tmp101 ;
  unsigned int __cil_tmp102 ;
  int __cil_tmp103 ;
  unsigned long __cil_tmp104 ;
  char *__cil_tmp105 ;
  char *__cil_tmp106 ;
  unsigned long __cil_tmp107 ;
  unsigned long __cil_tmp108 ;
  unsigned long __cil_tmp109 ;
  unsigned long __cil_tmp110 ;
  unsigned char __cil_tmp111 ;
  int __cil_tmp112 ;
  unsigned int __cil_tmp113 ;
  char *__cil_tmp114 ;
  char *__cil_tmp115 ;
  unsigned long __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  unsigned long __cil_tmp119 ;
  unsigned long __cil_tmp120 ;
  unsigned long __cil_tmp121 ;
  unsigned long __cil_tmp122 ;
  unsigned long __cil_tmp123 ;

  {
#line 292
  state = (struct ppp_mppe_state *)arg;
#line 295
  if (optlen != 6) {
#line 297
    return (0);
  } else {
    {
#line 295
    __cil_tmp15 = *options;
#line 295
    __cil_tmp16 = (unsigned int )__cil_tmp15;
#line 295
    if (__cil_tmp16 != 18U) {
#line 297
      return (0);
    } else {
      {
#line 295
      __cil_tmp17 = options + 1UL;
#line 295
      __cil_tmp18 = *__cil_tmp17;
#line 295
      __cil_tmp19 = (unsigned int )__cil_tmp18;
#line 295
      if (__cil_tmp19 != 6U) {
#line 297
        return (0);
      } else {

      }
      }
    }
    }
  }
#line 299
  ptr = options + 2U;
#line 299
  mppe_opts = (unsigned char)0;
  {
#line 299
  __cil_tmp20 = *ptr;
#line 299
  __cil_tmp21 = (int )__cil_tmp20;
#line 299
  __cil_tmp22 = __cil_tmp21 & 1;
#line 299
  if (__cil_tmp22 == 0) {
#line 299
    __cil_tmp23 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp24 = __cil_tmp23 | 4U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp24;
  } else {

  }
  }
  {
#line 299
  __cil_tmp25 = ptr + 3UL;
#line 299
  __cil_tmp26 = *__cil_tmp25;
#line 299
  __cil_tmp27 = (int )__cil_tmp26;
#line 299
  __cil_tmp28 = __cil_tmp27 & 64;
#line 299
  if (__cil_tmp28 != 0) {
#line 299
    __cil_tmp29 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp30 = __cil_tmp29 | 2U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp30;
  } else {

  }
  }
  {
#line 299
  __cil_tmp31 = ptr + 3UL;
#line 299
  __cil_tmp32 = *__cil_tmp31;
#line 299
  __cil_tmp33 = (int )__cil_tmp32;
#line 299
  __cil_tmp34 = __cil_tmp33 & 32;
#line 299
  if (__cil_tmp34 != 0) {
#line 299
    __cil_tmp35 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp36 = __cil_tmp35 | 1U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp36;
  } else {

  }
  }
  {
#line 299
  __cil_tmp37 = ptr + 3UL;
#line 299
  __cil_tmp38 = *__cil_tmp37;
#line 299
  __cil_tmp39 = (signed char )__cil_tmp38;
#line 299
  __cil_tmp40 = (int )__cil_tmp39;
#line 299
  if (__cil_tmp40 < 0) {
#line 299
    __cil_tmp41 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp42 = __cil_tmp41 | 8U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp42;
  } else {

  }
  }
  {
#line 299
  __cil_tmp43 = ptr + 3UL;
#line 299
  __cil_tmp44 = *__cil_tmp43;
#line 299
  __cil_tmp45 = (int )__cil_tmp44;
#line 299
  __cil_tmp46 = __cil_tmp45 & 16;
#line 299
  if (__cil_tmp46 != 0) {
#line 299
    __cil_tmp47 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp48 = __cil_tmp47 | 32U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp48;
  } else {

  }
  }
  {
#line 299
  __cil_tmp49 = ptr + 3UL;
#line 299
  __cil_tmp50 = *__cil_tmp49;
#line 299
  __cil_tmp51 = (int )__cil_tmp50;
#line 299
  if (__cil_tmp51 & 1) {
#line 299
    __cil_tmp52 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp53 = __cil_tmp52 | 16U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp53;
  } else {

  }
  }
  {
#line 299
  __cil_tmp54 = *ptr;
#line 299
  __cil_tmp55 = (int )__cil_tmp54;
#line 299
  __cil_tmp56 = __cil_tmp55 & -2;
#line 299
  if (__cil_tmp56 != 0) {
#line 299
    __cil_tmp57 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp58 = __cil_tmp57 | 64U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp58;
  } else {

  }
  }
  {
#line 299
  __cil_tmp59 = ptr + 1UL;
#line 299
  __cil_tmp60 = *__cil_tmp59;
#line 299
  __cil_tmp61 = (unsigned int )__cil_tmp60;
#line 299
  if (__cil_tmp61 != 0U) {
#line 299
    __cil_tmp62 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp63 = __cil_tmp62 | 64U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp63;
  } else {
    {
#line 299
    __cil_tmp64 = ptr + 2UL;
#line 299
    __cil_tmp65 = *__cil_tmp64;
#line 299
    __cil_tmp66 = (unsigned int )__cil_tmp65;
#line 299
    if (__cil_tmp66 != 0U) {
#line 299
      __cil_tmp67 = (unsigned int )mppe_opts;
#line 299
      __cil_tmp68 = __cil_tmp67 | 64U;
#line 299
      mppe_opts = (unsigned char )__cil_tmp68;
    } else {

    }
    }
  }
  }
  {
#line 299
  __cil_tmp69 = ptr + 3UL;
#line 299
  __cil_tmp70 = *__cil_tmp69;
#line 299
  __cil_tmp71 = (int )__cil_tmp70;
#line 299
  __cil_tmp72 = __cil_tmp71 & -242;
#line 299
  if (__cil_tmp72 != 0) {
#line 299
    __cil_tmp73 = (unsigned int )mppe_opts;
#line 299
    __cil_tmp74 = __cil_tmp73 | 64U;
#line 299
    mppe_opts = (unsigned char )__cil_tmp74;
  } else {

  }
  }
  {
#line 300
  __cil_tmp75 = (int )mppe_opts;
#line 300
  __cil_tmp76 = __cil_tmp75 & 2;
#line 300
  if (__cil_tmp76 != 0) {
#line 301
    __cil_tmp77 = (unsigned long )state;
#line 301
    __cil_tmp78 = __cil_tmp77 + 56;
#line 301
    *((unsigned int *)__cil_tmp78) = 16U;
  } else {
    {
#line 302
    __cil_tmp79 = (int )mppe_opts;
#line 302
    if (__cil_tmp79 & 1) {
#line 303
      __cil_tmp80 = (unsigned long )state;
#line 303
      __cil_tmp81 = __cil_tmp80 + 56;
#line 303
      *((unsigned int *)__cil_tmp81) = 8U;
    } else {
      {
#line 305
      printk("<4>%s[%d]: unknown key length\n", debugstr, unit);
      }
#line 307
      return (0);
    }
    }
  }
  }
  {
#line 309
  __cil_tmp82 = (int )mppe_opts;
#line 309
  __cil_tmp83 = __cil_tmp82 & 4;
#line 309
  if (__cil_tmp83 != 0) {
#line 310
    __cil_tmp84 = (unsigned long )state;
#line 310
    __cil_tmp85 = __cil_tmp84 + 68;
#line 310
    *((unsigned int *)__cil_tmp85) = 1U;
  } else {

  }
  }
  {
#line 313
  mppe_rekey(state, 1);
  }
#line 315
  if (debug != 0) {
    {
#line 320
    __cil_tmp86 = (unsigned long )state;
#line 320
    __cil_tmp87 = __cil_tmp86 + 68;
#line 320
    __cil_tmp88 = *((unsigned int *)__cil_tmp87);
#line 320
    if (__cil_tmp88 != 0U) {
#line 320
      tmp = (char *)"stateful";
    } else {
#line 320
      tmp = (char *)"stateless";
    }
    }
    {
#line 320
    __cil_tmp89 = (unsigned long )state;
#line 320
    __cil_tmp90 = __cil_tmp89 + 56;
#line 320
    __cil_tmp91 = *((unsigned int *)__cil_tmp90);
#line 320
    if (__cil_tmp91 == 16U) {
#line 320
      tmp___0 = 128;
    } else {
#line 320
      tmp___0 = 40;
    }
    }
    {
#line 320
    printk("<7>%s[%d]: initialized with %d-bit %s mode\n", debugstr, unit, tmp___0,
           tmp);
#line 324
    i = 0;
    }
#line 324
    goto ldv_18143;
    ldv_18142: 
    {
#line 325
    __cil_tmp92 = i * 2;
#line 325
    __cil_tmp93 = (unsigned long )__cil_tmp92;
#line 325
    __cil_tmp94 = (char *)(& mkey);
#line 325
    __cil_tmp95 = __cil_tmp94 + __cil_tmp93;
#line 325
    __cil_tmp96 = i * 1UL;
#line 325
    __cil_tmp97 = 24 + __cil_tmp96;
#line 325
    __cil_tmp98 = (unsigned long )state;
#line 325
    __cil_tmp99 = __cil_tmp98 + __cil_tmp97;
#line 325
    __cil_tmp100 = *((unsigned char *)__cil_tmp99);
#line 325
    __cil_tmp101 = (int )__cil_tmp100;
#line 325
    sprintf(__cil_tmp95, "%02x", __cil_tmp101);
#line 324
    i = i + 1;
    }
    ldv_18143: ;
    {
#line 324
    __cil_tmp102 = (unsigned int )i;
#line 324
    if (__cil_tmp102 <= 15U) {
#line 325
      goto ldv_18142;
    } else {
#line 327
      goto ldv_18144;
    }
    }
    ldv_18144: 
#line 326
    i = 0;
#line 326
    goto ldv_18146;
    ldv_18145: 
    {
#line 327
    __cil_tmp103 = i * 2;
#line 327
    __cil_tmp104 = (unsigned long )__cil_tmp103;
#line 327
    __cil_tmp105 = (char *)(& skey);
#line 327
    __cil_tmp106 = __cil_tmp105 + __cil_tmp104;
#line 327
    __cil_tmp107 = i * 1UL;
#line 327
    __cil_tmp108 = 40 + __cil_tmp107;
#line 327
    __cil_tmp109 = (unsigned long )state;
#line 327
    __cil_tmp110 = __cil_tmp109 + __cil_tmp108;
#line 327
    __cil_tmp111 = *((unsigned char *)__cil_tmp110);
#line 327
    __cil_tmp112 = (int )__cil_tmp111;
#line 327
    sprintf(__cil_tmp106, "%02x", __cil_tmp112);
#line 326
    i = i + 1;
    }
    ldv_18146: ;
    {
#line 326
    __cil_tmp113 = (unsigned int )i;
#line 326
    if (__cil_tmp113 <= 15U) {
#line 327
      goto ldv_18145;
    } else {
#line 329
      goto ldv_18147;
    }
    }
    ldv_18147: 
    {
#line 328
    __cil_tmp114 = (char *)(& mkey);
#line 328
    __cil_tmp115 = (char *)(& skey);
#line 328
    printk("<7>%s[%d]: keys: master: %s initial session: %s\n", debugstr, unit, __cil_tmp114,
           __cil_tmp115);
    }
  } else {

  }
#line 339
  __cil_tmp116 = (unsigned long )state;
#line 339
  __cil_tmp117 = __cil_tmp116 + 64;
#line 339
  *((unsigned int *)__cil_tmp117) = 4095U;
#line 345
  __cil_tmp118 = (unsigned long )state;
#line 345
  __cil_tmp119 = __cil_tmp118 + 60;
#line 345
  *((unsigned char *)__cil_tmp119) = (unsigned char)16;
#line 347
  __cil_tmp120 = (unsigned long )state;
#line 347
  __cil_tmp121 = __cil_tmp120 + 80;
#line 347
  *((int *)__cil_tmp121) = unit;
#line 348
  __cil_tmp122 = (unsigned long )state;
#line 348
  __cil_tmp123 = __cil_tmp122 + 84;
#line 348
  *((int *)__cil_tmp123) = debug;
#line 350
  return (1);
}
}
#line 354 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static int mppe_comp_init(void *arg , unsigned char *options , int optlen , int unit ,
                          int hdrlen , int debug ) 
{ int tmp ;

  {
  {
#line 358
  tmp = mppe_init(arg, options, optlen, unit, debug, "mppe_comp_init");
  }
#line 358
  return (tmp);
}
}
#line 370 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void mppe_comp_reset(void *arg ) 
{ struct ppp_mppe_state *state ;
  unsigned long __cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned char __cil_tmp7 ;
  unsigned int __cil_tmp8 ;
  unsigned int __cil_tmp9 ;

  {
#line 372
  state = (struct ppp_mppe_state *)arg;
#line 374
  __cil_tmp3 = (unsigned long )state;
#line 374
  __cil_tmp4 = __cil_tmp3 + 60;
#line 374
  __cil_tmp5 = (unsigned long )state;
#line 374
  __cil_tmp6 = __cil_tmp5 + 60;
#line 374
  __cil_tmp7 = *((unsigned char *)__cil_tmp6);
#line 374
  __cil_tmp8 = (unsigned int )__cil_tmp7;
#line 374
  __cil_tmp9 = __cil_tmp8 | 128U;
#line 374
  *((unsigned char *)__cil_tmp4) = (unsigned char )__cil_tmp9;
#line 375
  return;
}
}
#line 383 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static int mppe_compress(void *arg , unsigned char *ibuf , unsigned char *obuf , int isize ,
                         int osize ) 
{ struct ppp_mppe_state *state ;
  struct blkcipher_desc desc ;
  int proto ;
  struct scatterlist sg_in[1U] ;
  struct scatterlist sg_out[1U] ;
  int tmp ;
  struct blkcipher_desc *__cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  __u8 *__cil_tmp15 ;
  __u8 __cil_tmp16 ;
  int __cil_tmp17 ;
  __u8 *__cil_tmp18 ;
  __u8 __cil_tmp19 ;
  int __cil_tmp20 ;
  int __cil_tmp21 ;
  int __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  int __cil_tmp25 ;
  int __cil_tmp26 ;
  unsigned char *__cil_tmp27 ;
  __u8 *__cil_tmp28 ;
  u16 __cil_tmp29 ;
  void *__cil_tmp30 ;
  void *__cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned int __cil_tmp36 ;
  unsigned int __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  int __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  int __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  unsigned int __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  unsigned int __cil_tmp49 ;
  u16 __cil_tmp50 ;
  int __cil_tmp51 ;
  u16 __cil_tmp52 ;
  void *__cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  unsigned int __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  unsigned int __cil_tmp59 ;
  unsigned int __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  unsigned char __cil_tmp63 ;
  signed char __cil_tmp64 ;
  int __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  int __cil_tmp68 ;
  unsigned long __cil_tmp69 ;
  unsigned long __cil_tmp70 ;
  unsigned int __cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  int __cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  unsigned char __cil_tmp79 ;
  unsigned int __cil_tmp80 ;
  unsigned int __cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  unsigned char __cil_tmp84 ;
  int __cil_tmp85 ;
  unsigned char __cil_tmp86 ;
  int __cil_tmp87 ;
  int __cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  unsigned long __cil_tmp90 ;
  unsigned long __cil_tmp91 ;
  unsigned long __cil_tmp92 ;
  unsigned char __cil_tmp93 ;
  unsigned int __cil_tmp94 ;
  unsigned int __cil_tmp95 ;
  struct scatterlist *__cil_tmp96 ;
  struct scatterlist *__cil_tmp97 ;
  struct scatterlist *__cil_tmp98 ;
  void const   *__cil_tmp99 ;
  unsigned int __cil_tmp100 ;
  struct scatterlist *__cil_tmp101 ;
  void const   *__cil_tmp102 ;
  unsigned int __cil_tmp103 ;
  struct scatterlist *__cil_tmp104 ;
  struct scatterlist *__cil_tmp105 ;
  unsigned int __cil_tmp106 ;
  unsigned long __cil_tmp107 ;
  unsigned long __cil_tmp108 ;
  __u32 __cil_tmp109 ;
  unsigned long __cil_tmp110 ;
  unsigned long __cil_tmp111 ;
  __u32 __cil_tmp112 ;
  unsigned long __cil_tmp113 ;
  unsigned long __cil_tmp114 ;
  unsigned long __cil_tmp115 ;
  unsigned long __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  __u32 __cil_tmp119 ;
  unsigned long __cil_tmp120 ;
  unsigned long __cil_tmp121 ;
  unsigned long __cil_tmp122 ;
  __u32 __cil_tmp123 ;
  unsigned long __cil_tmp124 ;
  unsigned long __cil_tmp125 ;
  unsigned long __cil_tmp126 ;
  __u32 __cil_tmp127 ;
  unsigned long __cil_tmp128 ;
  unsigned long __cil_tmp129 ;
  unsigned long __cil_tmp130 ;
  unsigned long __cil_tmp131 ;
  unsigned long __cil_tmp132 ;
  unsigned long __cil_tmp133 ;
  __u32 __cil_tmp134 ;

  {
#line 386
  state = (struct ppp_mppe_state *)arg;
#line 387
  __cil_tmp12 = & desc;
#line 387
  *((struct crypto_blkcipher **)__cil_tmp12) = *((struct crypto_blkcipher **)state);
#line 387
  __cil_tmp13 = (unsigned long )(& desc) + 8;
#line 387
  *((void **)__cil_tmp13) = (void *)0;
#line 387
  __cil_tmp14 = (unsigned long )(& desc) + 16;
#line 387
  *((u32 *)__cil_tmp14) = 0U;
#line 394
  __cil_tmp15 = ibuf + 3UL;
#line 394
  __cil_tmp16 = *__cil_tmp15;
#line 394
  __cil_tmp17 = (int )__cil_tmp16;
#line 394
  __cil_tmp18 = ibuf + 2UL;
#line 394
  __cil_tmp19 = *__cil_tmp18;
#line 394
  __cil_tmp20 = (int )__cil_tmp19;
#line 394
  __cil_tmp21 = __cil_tmp20 << 8;
#line 394
  proto = __cil_tmp21 + __cil_tmp17;
#line 395
  if (proto <= 32) {
#line 396
    return (0);
  } else
#line 395
  if (proto > 250) {
#line 396
    return (0);
  } else {

  }
  {
#line 399
  __cil_tmp22 = isize + 4;
#line 399
  if (__cil_tmp22 > osize) {
    {
#line 401
    __cil_tmp23 = (unsigned long )state;
#line 401
    __cil_tmp24 = __cil_tmp23 + 80;
#line 401
    __cil_tmp25 = *((int *)__cil_tmp24);
#line 401
    __cil_tmp26 = osize + 4;
#line 401
    printk("<7>mppe_compress[%d]: osize too small! (have: %d need: %d)\n", __cil_tmp25,
           osize, __cil_tmp26);
    }
#line 404
    return (-1);
  } else {

  }
  }
  {
#line 407
  osize = isize + 4;
#line 412
  *obuf = *ibuf;
#line 413
  __cil_tmp27 = obuf + 1UL;
#line 413
  __cil_tmp28 = ibuf + 1UL;
#line 413
  *__cil_tmp27 = *__cil_tmp28;
#line 414
  __cil_tmp29 = (u16 )253;
#line 414
  __cil_tmp30 = (void *)obuf;
#line 414
  __cil_tmp31 = __cil_tmp30 + 2U;
#line 414
  put_unaligned_be16(__cil_tmp29, __cil_tmp31);
#line 415
  obuf = obuf + 4UL;
#line 417
  __cil_tmp32 = (unsigned long )state;
#line 417
  __cil_tmp33 = __cil_tmp32 + 64;
#line 417
  __cil_tmp34 = (unsigned long )state;
#line 417
  __cil_tmp35 = __cil_tmp34 + 64;
#line 417
  __cil_tmp36 = *((unsigned int *)__cil_tmp35);
#line 417
  __cil_tmp37 = __cil_tmp36 + 1U;
#line 417
  *((unsigned int *)__cil_tmp33) = __cil_tmp37 & 4095U;
  }
  {
#line 418
  __cil_tmp38 = (unsigned long )state;
#line 418
  __cil_tmp39 = __cil_tmp38 + 84;
#line 418
  __cil_tmp40 = *((int *)__cil_tmp39);
#line 418
  if (__cil_tmp40 > 6) {
    {
#line 419
    __cil_tmp41 = (unsigned long )state;
#line 419
    __cil_tmp42 = __cil_tmp41 + 80;
#line 419
    __cil_tmp43 = *((int *)__cil_tmp42);
#line 419
    __cil_tmp44 = (unsigned long )state;
#line 419
    __cil_tmp45 = __cil_tmp44 + 64;
#line 419
    __cil_tmp46 = *((unsigned int *)__cil_tmp45);
#line 419
    printk("<7>mppe_compress[%d]: ccount %d\n", __cil_tmp43, __cil_tmp46);
    }
  } else {

  }
  }
  {
#line 421
  __cil_tmp47 = (unsigned long )state;
#line 421
  __cil_tmp48 = __cil_tmp47 + 64;
#line 421
  __cil_tmp49 = *((unsigned int *)__cil_tmp48);
#line 421
  __cil_tmp50 = (u16 )__cil_tmp49;
#line 421
  __cil_tmp51 = (int )__cil_tmp50;
#line 421
  __cil_tmp52 = (u16 )__cil_tmp51;
#line 421
  __cil_tmp53 = (void *)obuf;
#line 421
  put_unaligned_be16(__cil_tmp52, __cil_tmp53);
  }
  {
#line 423
  __cil_tmp54 = (unsigned long )state;
#line 423
  __cil_tmp55 = __cil_tmp54 + 68;
#line 423
  __cil_tmp56 = *((unsigned int *)__cil_tmp55);
#line 423
  if (__cil_tmp56 == 0U) {
#line 423
    goto _L;
  } else {
    {
#line 423
    __cil_tmp57 = (unsigned long )state;
#line 423
    __cil_tmp58 = __cil_tmp57 + 64;
#line 423
    __cil_tmp59 = *((unsigned int *)__cil_tmp58);
#line 423
    __cil_tmp60 = __cil_tmp59 & 255U;
#line 423
    if (__cil_tmp60 == 255U) {
#line 423
      goto _L;
    } else {
      {
#line 423
      __cil_tmp61 = (unsigned long )state;
#line 423
      __cil_tmp62 = __cil_tmp61 + 60;
#line 423
      __cil_tmp63 = *((unsigned char *)__cil_tmp62);
#line 423
      __cil_tmp64 = (signed char )__cil_tmp63;
#line 423
      __cil_tmp65 = (int )__cil_tmp64;
#line 423
      if (__cil_tmp65 < 0) {
        _L: /* CIL Label */ 
        {
#line 427
        __cil_tmp66 = (unsigned long )state;
#line 427
        __cil_tmp67 = __cil_tmp66 + 84;
#line 427
        __cil_tmp68 = *((int *)__cil_tmp67);
#line 427
        if (__cil_tmp68 != 0) {
          {
#line 427
          __cil_tmp69 = (unsigned long )state;
#line 427
          __cil_tmp70 = __cil_tmp69 + 68;
#line 427
          __cil_tmp71 = *((unsigned int *)__cil_tmp70);
#line 427
          if (__cil_tmp71 != 0U) {
            {
#line 428
            __cil_tmp72 = (unsigned long )state;
#line 428
            __cil_tmp73 = __cil_tmp72 + 80;
#line 428
            __cil_tmp74 = *((int *)__cil_tmp73);
#line 428
            printk("<7>mppe_compress[%d]: rekeying\n", __cil_tmp74);
            }
          } else {

          }
          }
        } else {

        }
        }
        {
#line 430
        mppe_rekey(state, 0);
#line 431
        __cil_tmp75 = (unsigned long )state;
#line 431
        __cil_tmp76 = __cil_tmp75 + 60;
#line 431
        __cil_tmp77 = (unsigned long )state;
#line 431
        __cil_tmp78 = __cil_tmp77 + 60;
#line 431
        __cil_tmp79 = *((unsigned char *)__cil_tmp78);
#line 431
        __cil_tmp80 = (unsigned int )__cil_tmp79;
#line 431
        __cil_tmp81 = __cil_tmp80 | 128U;
#line 431
        *((unsigned char *)__cil_tmp76) = (unsigned char )__cil_tmp81;
        }
      } else {

      }
      }
    }
    }
  }
  }
  {
#line 433
  __cil_tmp82 = (unsigned long )state;
#line 433
  __cil_tmp83 = __cil_tmp82 + 60;
#line 433
  __cil_tmp84 = *((unsigned char *)__cil_tmp83);
#line 433
  __cil_tmp85 = (int )__cil_tmp84;
#line 433
  __cil_tmp86 = *obuf;
#line 433
  __cil_tmp87 = (int )__cil_tmp86;
#line 433
  __cil_tmp88 = __cil_tmp87 | __cil_tmp85;
#line 433
  *obuf = (unsigned char )__cil_tmp88;
#line 434
  __cil_tmp89 = (unsigned long )state;
#line 434
  __cil_tmp90 = __cil_tmp89 + 60;
#line 434
  __cil_tmp91 = (unsigned long )state;
#line 434
  __cil_tmp92 = __cil_tmp91 + 60;
#line 434
  __cil_tmp93 = *((unsigned char *)__cil_tmp92);
#line 434
  __cil_tmp94 = (unsigned int )__cil_tmp93;
#line 434
  __cil_tmp95 = __cil_tmp94 & 127U;
#line 434
  *((unsigned char *)__cil_tmp90) = (unsigned char )__cil_tmp95;
#line 436
  obuf = obuf + 2UL;
#line 437
  ibuf = ibuf + 2UL;
#line 438
  isize = isize + -2;
#line 441
  __cil_tmp96 = (struct scatterlist *)(& sg_in);
#line 441
  sg_init_table(__cil_tmp96, 1U);
#line 442
  __cil_tmp97 = (struct scatterlist *)(& sg_out);
#line 442
  sg_init_table(__cil_tmp97, 1U);
#line 443
  __cil_tmp98 = (struct scatterlist *)(& sg_in);
#line 443
  __cil_tmp99 = (void const   *)ibuf;
#line 443
  __cil_tmp100 = (unsigned int )isize;
#line 443
  setup_sg(__cil_tmp98, __cil_tmp99, __cil_tmp100);
#line 444
  __cil_tmp101 = (struct scatterlist *)(& sg_out);
#line 444
  __cil_tmp102 = (void const   *)obuf;
#line 444
  __cil_tmp103 = (unsigned int )osize;
#line 444
  setup_sg(__cil_tmp101, __cil_tmp102, __cil_tmp103);
#line 445
  __cil_tmp104 = (struct scatterlist *)(& sg_out);
#line 445
  __cil_tmp105 = (struct scatterlist *)(& sg_in);
#line 445
  __cil_tmp106 = (unsigned int )isize;
#line 445
  tmp = crypto_blkcipher_encrypt(& desc, __cil_tmp104, __cil_tmp105, __cil_tmp106);
  }
#line 445
  if (tmp != 0) {
    {
#line 446
    printk("<7>crypto_cypher_encrypt failed\n");
    }
#line 447
    return (-1);
  } else {

  }
#line 450
  __cil_tmp107 = (unsigned long )state;
#line 450
  __cil_tmp108 = __cil_tmp107 + 88;
#line 450
  __cil_tmp109 = (__u32 )isize;
#line 450
  __cil_tmp110 = (unsigned long )state;
#line 450
  __cil_tmp111 = __cil_tmp110 + 88;
#line 450
  __cil_tmp112 = *((__u32 *)__cil_tmp111);
#line 450
  *((__u32 *)__cil_tmp108) = __cil_tmp112 + __cil_tmp109;
#line 451
  __cil_tmp113 = 88 + 4;
#line 451
  __cil_tmp114 = (unsigned long )state;
#line 451
  __cil_tmp115 = __cil_tmp114 + __cil_tmp113;
#line 451
  __cil_tmp116 = 88 + 4;
#line 451
  __cil_tmp117 = (unsigned long )state;
#line 451
  __cil_tmp118 = __cil_tmp117 + __cil_tmp116;
#line 451
  __cil_tmp119 = *((__u32 *)__cil_tmp118);
#line 451
  *((__u32 *)__cil_tmp115) = __cil_tmp119 + 1U;
#line 452
  __cil_tmp120 = 88 + 8;
#line 452
  __cil_tmp121 = (unsigned long )state;
#line 452
  __cil_tmp122 = __cil_tmp121 + __cil_tmp120;
#line 452
  __cil_tmp123 = (__u32 )osize;
#line 452
  __cil_tmp124 = 88 + 8;
#line 452
  __cil_tmp125 = (unsigned long )state;
#line 452
  __cil_tmp126 = __cil_tmp125 + __cil_tmp124;
#line 452
  __cil_tmp127 = *((__u32 *)__cil_tmp126);
#line 452
  *((__u32 *)__cil_tmp122) = __cil_tmp127 + __cil_tmp123;
#line 453
  __cil_tmp128 = 88 + 12;
#line 453
  __cil_tmp129 = (unsigned long )state;
#line 453
  __cil_tmp130 = __cil_tmp129 + __cil_tmp128;
#line 453
  __cil_tmp131 = 88 + 12;
#line 453
  __cil_tmp132 = (unsigned long )state;
#line 453
  __cil_tmp133 = __cil_tmp132 + __cil_tmp131;
#line 453
  __cil_tmp134 = *((__u32 *)__cil_tmp133);
#line 453
  *((__u32 *)__cil_tmp130) = __cil_tmp134 + 1U;
#line 455
  return (osize);
}
}
#line 462 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void mppe_comp_stats(void *arg , struct compstat *stats ) 
{ struct ppp_mppe_state *state ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;

  {
#line 464
  state = (struct ppp_mppe_state *)arg;
#line 466
  __cil_tmp4 = (unsigned long )state;
#line 466
  __cil_tmp5 = __cil_tmp4 + 88;
#line 466
  *stats = *((struct compstat *)__cil_tmp5);
#line 467
  return;
}
}
#line 470 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static int mppe_decomp_init(void *arg , unsigned char *options , int optlen , int unit ,
                            int hdrlen , int mru , int debug ) 
{ int tmp ;

  {
  {
#line 474
  tmp = mppe_init(arg, options, optlen, unit, debug, "mppe_decomp_init");
  }
#line 474
  return (tmp);
}
}
#line 480 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void mppe_decomp_reset(void *arg ) 
{ 

  {
#line 483
  return;
}
}
#line 490 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static int mppe_decompress(void *arg , unsigned char *ibuf , int isize , unsigned char *obuf ,
                           int osize ) 
{ struct ppp_mppe_state *state ;
  struct blkcipher_desc desc ;
  unsigned int ccount ;
  int flushed ;
  int sanity ;
  struct scatterlist sg_in[1U] ;
  struct scatterlist sg_out[1U] ;
  int tmp ;
  int tmp___0 ;
  struct blkcipher_desc *__cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned char *__cil_tmp18 ;
  unsigned char __cil_tmp19 ;
  int __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  int __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  int __cil_tmp26 ;
  int __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  int __cil_tmp30 ;
  int __cil_tmp31 ;
  unsigned char *__cil_tmp32 ;
  unsigned char __cil_tmp33 ;
  int __cil_tmp34 ;
  unsigned char *__cil_tmp35 ;
  unsigned char __cil_tmp36 ;
  int __cil_tmp37 ;
  int __cil_tmp38 ;
  int __cil_tmp39 ;
  int __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  int __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  int __cil_tmp46 ;
  unsigned char *__cil_tmp47 ;
  unsigned char __cil_tmp48 ;
  int __cil_tmp49 ;
  int __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  int __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  int __cil_tmp58 ;
  unsigned long __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned int __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  int __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  int __cil_tmp69 ;
  unsigned long __cil_tmp70 ;
  unsigned long __cil_tmp71 ;
  unsigned int __cil_tmp72 ;
  unsigned int __cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  int __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  unsigned long __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  int __cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  int __cil_tmp84 ;
  unsigned long __cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  unsigned int __cil_tmp87 ;
  unsigned long __cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  unsigned long __cil_tmp90 ;
  unsigned long __cil_tmp91 ;
  unsigned int __cil_tmp92 ;
  unsigned int __cil_tmp93 ;
  unsigned long __cil_tmp94 ;
  unsigned long __cil_tmp95 ;
  unsigned int __cil_tmp96 ;
  unsigned long __cil_tmp97 ;
  unsigned long __cil_tmp98 ;
  int __cil_tmp99 ;
  unsigned long __cil_tmp100 ;
  unsigned long __cil_tmp101 ;
  unsigned long __cil_tmp102 ;
  unsigned long __cil_tmp103 ;
  unsigned int __cil_tmp104 ;
  unsigned int __cil_tmp105 ;
  unsigned long __cil_tmp106 ;
  unsigned long __cil_tmp107 ;
  unsigned int __cil_tmp108 ;
  unsigned long __cil_tmp109 ;
  unsigned long __cil_tmp110 ;
  unsigned long __cil_tmp111 ;
  unsigned long __cil_tmp112 ;
  unsigned long __cil_tmp113 ;
  unsigned long __cil_tmp114 ;
  unsigned int __cil_tmp115 ;
  unsigned int __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  unsigned int __cil_tmp119 ;
  unsigned int __cil_tmp120 ;
  unsigned int __cil_tmp121 ;
  unsigned long __cil_tmp122 ;
  unsigned long __cil_tmp123 ;
  unsigned long __cil_tmp124 ;
  unsigned long __cil_tmp125 ;
  unsigned char *__cil_tmp126 ;
  __u8 *__cil_tmp127 ;
  struct scatterlist *__cil_tmp128 ;
  struct scatterlist *__cil_tmp129 ;
  struct scatterlist *__cil_tmp130 ;
  void const   *__cil_tmp131 ;
  struct scatterlist *__cil_tmp132 ;
  void const   *__cil_tmp133 ;
  struct scatterlist *__cil_tmp134 ;
  struct scatterlist *__cil_tmp135 ;
  unsigned char __cil_tmp136 ;
  int __cil_tmp137 ;
  unsigned char *__cil_tmp138 ;
  struct scatterlist *__cil_tmp139 ;
  void const   *__cil_tmp140 ;
  void const   *__cil_tmp141 ;
  int __cil_tmp142 ;
  unsigned int __cil_tmp143 ;
  struct scatterlist *__cil_tmp144 ;
  void const   *__cil_tmp145 ;
  void const   *__cil_tmp146 ;
  int __cil_tmp147 ;
  unsigned int __cil_tmp148 ;
  struct scatterlist *__cil_tmp149 ;
  struct scatterlist *__cil_tmp150 ;
  int __cil_tmp151 ;
  unsigned int __cil_tmp152 ;
  unsigned long __cil_tmp153 ;
  unsigned long __cil_tmp154 ;
  __u32 __cil_tmp155 ;
  unsigned long __cil_tmp156 ;
  unsigned long __cil_tmp157 ;
  __u32 __cil_tmp158 ;
  unsigned long __cil_tmp159 ;
  unsigned long __cil_tmp160 ;
  unsigned long __cil_tmp161 ;
  unsigned long __cil_tmp162 ;
  unsigned long __cil_tmp163 ;
  unsigned long __cil_tmp164 ;
  __u32 __cil_tmp165 ;
  unsigned long __cil_tmp166 ;
  unsigned long __cil_tmp167 ;
  unsigned long __cil_tmp168 ;
  __u32 __cil_tmp169 ;
  unsigned long __cil_tmp170 ;
  unsigned long __cil_tmp171 ;
  unsigned long __cil_tmp172 ;
  __u32 __cil_tmp173 ;
  unsigned long __cil_tmp174 ;
  unsigned long __cil_tmp175 ;
  unsigned long __cil_tmp176 ;
  unsigned long __cil_tmp177 ;
  unsigned long __cil_tmp178 ;
  unsigned long __cil_tmp179 ;
  __u32 __cil_tmp180 ;
  unsigned long __cil_tmp181 ;
  unsigned long __cil_tmp182 ;
  unsigned long __cil_tmp183 ;
  unsigned long __cil_tmp184 ;
  int __cil_tmp185 ;

  {
#line 493
  state = (struct ppp_mppe_state *)arg;
#line 494
  __cil_tmp15 = & desc;
#line 494
  *((struct crypto_blkcipher **)__cil_tmp15) = *((struct crypto_blkcipher **)state);
#line 494
  __cil_tmp16 = (unsigned long )(& desc) + 8;
#line 494
  *((void **)__cil_tmp16) = (void *)0;
#line 494
  __cil_tmp17 = (unsigned long )(& desc) + 16;
#line 494
  *((u32 *)__cil_tmp17) = 0U;
#line 496
  __cil_tmp18 = ibuf + 4UL;
#line 496
  __cil_tmp19 = *__cil_tmp18;
#line 496
  __cil_tmp20 = (int )__cil_tmp19;
#line 496
  flushed = __cil_tmp20 & 128;
#line 497
  sanity = 0;
#line 500
  if (isize <= 6) {
    {
#line 501
    __cil_tmp21 = (unsigned long )state;
#line 501
    __cil_tmp22 = __cil_tmp21 + 84;
#line 501
    __cil_tmp23 = *((int *)__cil_tmp22);
#line 501
    if (__cil_tmp23 != 0) {
      {
#line 502
      __cil_tmp24 = (unsigned long )state;
#line 502
      __cil_tmp25 = __cil_tmp24 + 80;
#line 502
      __cil_tmp26 = *((int *)__cil_tmp25);
#line 502
      printk("<7>mppe_decompress[%d]: short pkt (%d)\n", __cil_tmp26, isize);
      }
    } else {

    }
    }
#line 505
    return (-1);
  } else {

  }
  {
#line 514
  __cil_tmp27 = isize + -3;
#line 514
  if (__cil_tmp27 > osize) {
    {
#line 515
    __cil_tmp28 = (unsigned long )state;
#line 515
    __cil_tmp29 = __cil_tmp28 + 80;
#line 515
    __cil_tmp30 = *((int *)__cil_tmp29);
#line 515
    __cil_tmp31 = isize + -3;
#line 515
    printk("<7>mppe_decompress[%d]: osize too small! (have: %d need: %d)\n", __cil_tmp30,
           osize, __cil_tmp31);
    }
#line 518
    return (-1);
  } else {

  }
  }
#line 520
  osize = isize + -4;
#line 522
  __cil_tmp32 = ibuf + 5UL;
#line 522
  __cil_tmp33 = *__cil_tmp32;
#line 522
  __cil_tmp34 = (int )__cil_tmp33;
#line 522
  __cil_tmp35 = ibuf + 4UL;
#line 522
  __cil_tmp36 = *__cil_tmp35;
#line 522
  __cil_tmp37 = (int )__cil_tmp36;
#line 522
  __cil_tmp38 = __cil_tmp37 & 15;
#line 522
  __cil_tmp39 = __cil_tmp38 << 8;
#line 522
  __cil_tmp40 = __cil_tmp39 + __cil_tmp34;
#line 522
  ccount = (unsigned int )__cil_tmp40;
  {
#line 523
  __cil_tmp41 = (unsigned long )state;
#line 523
  __cil_tmp42 = __cil_tmp41 + 84;
#line 523
  __cil_tmp43 = *((int *)__cil_tmp42);
#line 523
  if (__cil_tmp43 > 6) {
    {
#line 524
    __cil_tmp44 = (unsigned long )state;
#line 524
    __cil_tmp45 = __cil_tmp44 + 80;
#line 524
    __cil_tmp46 = *((int *)__cil_tmp45);
#line 524
    printk("<7>mppe_decompress[%d]: ccount %d\n", __cil_tmp46, ccount);
    }
  } else {

  }
  }
  {
#line 528
  __cil_tmp47 = ibuf + 4UL;
#line 528
  __cil_tmp48 = *__cil_tmp47;
#line 528
  __cil_tmp49 = (int )__cil_tmp48;
#line 528
  __cil_tmp50 = __cil_tmp49 & 16;
#line 528
  if (__cil_tmp50 == 0) {
    {
#line 529
    __cil_tmp51 = (unsigned long )state;
#line 529
    __cil_tmp52 = __cil_tmp51 + 80;
#line 529
    __cil_tmp53 = *((int *)__cil_tmp52);
#line 529
    printk("<7>mppe_decompress[%d]: ENCRYPTED bit not set!\n", __cil_tmp53);
#line 532
    __cil_tmp54 = (unsigned long )state;
#line 532
    __cil_tmp55 = __cil_tmp54 + 76;
#line 532
    __cil_tmp56 = (unsigned long )state;
#line 532
    __cil_tmp57 = __cil_tmp56 + 76;
#line 532
    __cil_tmp58 = *((int *)__cil_tmp57);
#line 532
    *((int *)__cil_tmp55) = __cil_tmp58 + 100;
#line 533
    sanity = 1;
    }
  } else {

  }
  }
  {
#line 535
  __cil_tmp59 = (unsigned long )state;
#line 535
  __cil_tmp60 = __cil_tmp59 + 68;
#line 535
  __cil_tmp61 = *((unsigned int *)__cil_tmp60);
#line 535
  if (__cil_tmp61 == 0U) {
#line 535
    if (flushed == 0) {
      {
#line 536
      __cil_tmp62 = (unsigned long )state;
#line 536
      __cil_tmp63 = __cil_tmp62 + 80;
#line 536
      __cil_tmp64 = *((int *)__cil_tmp63);
#line 536
      printk("<7>mppe_decompress[%d]: FLUSHED bit not set in stateless mode!\n", __cil_tmp64);
#line 538
      __cil_tmp65 = (unsigned long )state;
#line 538
      __cil_tmp66 = __cil_tmp65 + 76;
#line 538
      __cil_tmp67 = (unsigned long )state;
#line 538
      __cil_tmp68 = __cil_tmp67 + 76;
#line 538
      __cil_tmp69 = *((int *)__cil_tmp68);
#line 538
      *((int *)__cil_tmp66) = __cil_tmp69 + 100;
#line 539
      sanity = 1;
      }
    } else {

    }
  } else {

  }
  }
  {
#line 541
  __cil_tmp70 = (unsigned long )state;
#line 541
  __cil_tmp71 = __cil_tmp70 + 68;
#line 541
  __cil_tmp72 = *((unsigned int *)__cil_tmp71);
#line 541
  if (__cil_tmp72 != 0U) {
    {
#line 541
    __cil_tmp73 = ccount & 255U;
#line 541
    if (__cil_tmp73 == 255U) {
#line 541
      if (flushed == 0) {
        {
#line 542
        __cil_tmp74 = (unsigned long )state;
#line 542
        __cil_tmp75 = __cil_tmp74 + 80;
#line 542
        __cil_tmp76 = *((int *)__cil_tmp75);
#line 542
        printk("<7>mppe_decompress[%d]: FLUSHED bit not set on flag packet!\n", __cil_tmp76);
#line 544
        __cil_tmp77 = (unsigned long )state;
#line 544
        __cil_tmp78 = __cil_tmp77 + 76;
#line 544
        __cil_tmp79 = (unsigned long )state;
#line 544
        __cil_tmp80 = __cil_tmp79 + 76;
#line 544
        __cil_tmp81 = *((int *)__cil_tmp80);
#line 544
        *((int *)__cil_tmp78) = __cil_tmp81 + 100;
#line 545
        sanity = 1;
        }
      } else {

      }
    } else {

    }
    }
  } else {

  }
  }
#line 548
  if (sanity != 0) {
    {
#line 549
    __cil_tmp82 = (unsigned long )state;
#line 549
    __cil_tmp83 = __cil_tmp82 + 76;
#line 549
    __cil_tmp84 = *((int *)__cil_tmp83);
#line 549
    if (__cil_tmp84 <= 1599) {
#line 550
      return (-1);
    } else {
#line 557
      return (-2);
    }
    }
  } else {

  }
  {
#line 564
  __cil_tmp85 = (unsigned long )state;
#line 564
  __cil_tmp86 = __cil_tmp85 + 68;
#line 564
  __cil_tmp87 = *((unsigned int *)__cil_tmp86);
#line 564
  if (__cil_tmp87 == 0U) {
#line 566
    goto ldv_18204;
    ldv_18203: 
    {
#line 567
    mppe_rekey(state, 0);
#line 568
    __cil_tmp88 = (unsigned long )state;
#line 568
    __cil_tmp89 = __cil_tmp88 + 64;
#line 568
    __cil_tmp90 = (unsigned long )state;
#line 568
    __cil_tmp91 = __cil_tmp90 + 64;
#line 568
    __cil_tmp92 = *((unsigned int *)__cil_tmp91);
#line 568
    __cil_tmp93 = __cil_tmp92 + 1U;
#line 568
    *((unsigned int *)__cil_tmp89) = __cil_tmp93 & 4095U;
    }
    ldv_18204: ;
    {
#line 566
    __cil_tmp94 = (unsigned long )state;
#line 566
    __cil_tmp95 = __cil_tmp94 + 64;
#line 566
    __cil_tmp96 = *((unsigned int *)__cil_tmp95);
#line 566
    if (__cil_tmp96 != ccount) {
#line 567
      goto ldv_18203;
    } else {
#line 569
      goto ldv_18205;
    }
    }
    ldv_18205: ;
  } else {
    {
#line 572
    __cil_tmp97 = (unsigned long )state;
#line 572
    __cil_tmp98 = __cil_tmp97 + 72;
#line 572
    __cil_tmp99 = *((int *)__cil_tmp98);
#line 572
    if (__cil_tmp99 == 0) {
#line 574
      __cil_tmp100 = (unsigned long )state;
#line 574
      __cil_tmp101 = __cil_tmp100 + 64;
#line 574
      __cil_tmp102 = (unsigned long )state;
#line 574
      __cil_tmp103 = __cil_tmp102 + 64;
#line 574
      __cil_tmp104 = *((unsigned int *)__cil_tmp103);
#line 574
      __cil_tmp105 = __cil_tmp104 + 1U;
#line 574
      *((unsigned int *)__cil_tmp101) = __cil_tmp105 & 4095U;
      {
#line 575
      __cil_tmp106 = (unsigned long )state;
#line 575
      __cil_tmp107 = __cil_tmp106 + 64;
#line 575
      __cil_tmp108 = *((unsigned int *)__cil_tmp107);
#line 575
      if (__cil_tmp108 != ccount) {
#line 581
        __cil_tmp109 = (unsigned long )state;
#line 581
        __cil_tmp110 = __cil_tmp109 + 72;
#line 581
        *((int *)__cil_tmp110) = 1;
#line 582
        return (-1);
      } else {

      }
      }
    } else
#line 586
    if (flushed == 0) {
#line 588
      return (-1);
    } else {
#line 591
      goto ldv_18207;
      ldv_18206: 
      {
#line 593
      mppe_rekey(state, 0);
#line 594
      __cil_tmp111 = (unsigned long )state;
#line 594
      __cil_tmp112 = __cil_tmp111 + 64;
#line 594
      __cil_tmp113 = (unsigned long )state;
#line 594
      __cil_tmp114 = __cil_tmp113 + 64;
#line 594
      __cil_tmp115 = *((unsigned int *)__cil_tmp114);
#line 594
      __cil_tmp116 = __cil_tmp115 + 256U;
#line 594
      *((unsigned int *)__cil_tmp112) = __cil_tmp116 & 4095U;
      }
      ldv_18207: ;
      {
#line 591
      __cil_tmp117 = (unsigned long )state;
#line 591
      __cil_tmp118 = __cil_tmp117 + 64;
#line 591
      __cil_tmp119 = *((unsigned int *)__cil_tmp118);
#line 591
      __cil_tmp120 = __cil_tmp119 ^ ccount;
#line 591
      __cil_tmp121 = __cil_tmp120 & 4294967040U;
#line 591
      if (__cil_tmp121 != 0U) {
#line 592
        goto ldv_18206;
      } else {
#line 594
        goto ldv_18208;
      }
      }
      ldv_18208: 
#line 600
      __cil_tmp122 = (unsigned long )state;
#line 600
      __cil_tmp123 = __cil_tmp122 + 72;
#line 600
      *((int *)__cil_tmp123) = 0;
#line 601
      __cil_tmp124 = (unsigned long )state;
#line 601
      __cil_tmp125 = __cil_tmp124 + 64;
#line 601
      *((unsigned int *)__cil_tmp125) = ccount;
    }
    }
#line 611
    if (flushed != 0) {
      {
#line 612
      mppe_rekey(state, 0);
      }
    } else {

    }
  }
  }
  {
#line 619
  *obuf = *ibuf;
#line 620
  __cil_tmp126 = obuf + 1UL;
#line 620
  __cil_tmp127 = ibuf + 1UL;
#line 620
  *__cil_tmp126 = *__cil_tmp127;
#line 621
  obuf = obuf + 2UL;
#line 622
  ibuf = ibuf + 6UL;
#line 623
  isize = isize + -6;
#line 630
  __cil_tmp128 = (struct scatterlist *)(& sg_in);
#line 630
  sg_init_table(__cil_tmp128, 1U);
#line 631
  __cil_tmp129 = (struct scatterlist *)(& sg_out);
#line 631
  sg_init_table(__cil_tmp129, 1U);
#line 632
  __cil_tmp130 = (struct scatterlist *)(& sg_in);
#line 632
  __cil_tmp131 = (void const   *)ibuf;
#line 632
  setup_sg(__cil_tmp130, __cil_tmp131, 1U);
#line 633
  __cil_tmp132 = (struct scatterlist *)(& sg_out);
#line 633
  __cil_tmp133 = (void const   *)obuf;
#line 633
  setup_sg(__cil_tmp132, __cil_tmp133, 1U);
#line 634
  __cil_tmp134 = (struct scatterlist *)(& sg_out);
#line 634
  __cil_tmp135 = (struct scatterlist *)(& sg_in);
#line 634
  tmp = crypto_blkcipher_decrypt(& desc, __cil_tmp134, __cil_tmp135, 1U);
  }
#line 634
  if (tmp != 0) {
    {
#line 635
    printk("<7>crypto_cypher_decrypt failed\n");
    }
#line 636
    return (-1);
  } else {

  }
  {
#line 644
  __cil_tmp136 = *obuf;
#line 644
  __cil_tmp137 = (int )__cil_tmp136;
#line 644
  if (__cil_tmp137 & 1) {
#line 645
    __cil_tmp138 = obuf + 1UL;
#line 645
    *__cil_tmp138 = *obuf;
#line 646
    *obuf = (unsigned char)0;
#line 647
    obuf = obuf + 1;
#line 648
    osize = osize + 1;
  } else {

  }
  }
  {
#line 652
  __cil_tmp139 = (struct scatterlist *)(& sg_in);
#line 652
  __cil_tmp140 = (void const   *)ibuf;
#line 652
  __cil_tmp141 = __cil_tmp140 + 1U;
#line 652
  __cil_tmp142 = isize + -1;
#line 652
  __cil_tmp143 = (unsigned int )__cil_tmp142;
#line 652
  setup_sg(__cil_tmp139, __cil_tmp141, __cil_tmp143);
#line 653
  __cil_tmp144 = (struct scatterlist *)(& sg_out);
#line 653
  __cil_tmp145 = (void const   *)obuf;
#line 653
  __cil_tmp146 = __cil_tmp145 + 1U;
#line 653
  __cil_tmp147 = osize + -1;
#line 653
  __cil_tmp148 = (unsigned int )__cil_tmp147;
#line 653
  setup_sg(__cil_tmp144, __cil_tmp146, __cil_tmp148);
#line 654
  __cil_tmp149 = (struct scatterlist *)(& sg_out);
#line 654
  __cil_tmp150 = (struct scatterlist *)(& sg_in);
#line 654
  __cil_tmp151 = isize + -1;
#line 654
  __cil_tmp152 = (unsigned int )__cil_tmp151;
#line 654
  tmp___0 = crypto_blkcipher_decrypt(& desc, __cil_tmp149, __cil_tmp150, __cil_tmp152);
  }
#line 654
  if (tmp___0 != 0) {
    {
#line 655
    printk("<7>crypto_cypher_decrypt failed\n");
    }
#line 656
    return (-1);
  } else {

  }
#line 659
  __cil_tmp153 = (unsigned long )state;
#line 659
  __cil_tmp154 = __cil_tmp153 + 88;
#line 659
  __cil_tmp155 = (__u32 )osize;
#line 659
  __cil_tmp156 = (unsigned long )state;
#line 659
  __cil_tmp157 = __cil_tmp156 + 88;
#line 659
  __cil_tmp158 = *((__u32 *)__cil_tmp157);
#line 659
  *((__u32 *)__cil_tmp154) = __cil_tmp158 + __cil_tmp155;
#line 660
  __cil_tmp159 = 88 + 4;
#line 660
  __cil_tmp160 = (unsigned long )state;
#line 660
  __cil_tmp161 = __cil_tmp160 + __cil_tmp159;
#line 660
  __cil_tmp162 = 88 + 4;
#line 660
  __cil_tmp163 = (unsigned long )state;
#line 660
  __cil_tmp164 = __cil_tmp163 + __cil_tmp162;
#line 660
  __cil_tmp165 = *((__u32 *)__cil_tmp164);
#line 660
  *((__u32 *)__cil_tmp161) = __cil_tmp165 + 1U;
#line 661
  __cil_tmp166 = 88 + 8;
#line 661
  __cil_tmp167 = (unsigned long )state;
#line 661
  __cil_tmp168 = __cil_tmp167 + __cil_tmp166;
#line 661
  __cil_tmp169 = (__u32 )isize;
#line 661
  __cil_tmp170 = 88 + 8;
#line 661
  __cil_tmp171 = (unsigned long )state;
#line 661
  __cil_tmp172 = __cil_tmp171 + __cil_tmp170;
#line 661
  __cil_tmp173 = *((__u32 *)__cil_tmp172);
#line 661
  *((__u32 *)__cil_tmp168) = __cil_tmp173 + __cil_tmp169;
#line 662
  __cil_tmp174 = 88 + 12;
#line 662
  __cil_tmp175 = (unsigned long )state;
#line 662
  __cil_tmp176 = __cil_tmp175 + __cil_tmp174;
#line 662
  __cil_tmp177 = 88 + 12;
#line 662
  __cil_tmp178 = (unsigned long )state;
#line 662
  __cil_tmp179 = __cil_tmp178 + __cil_tmp177;
#line 662
  __cil_tmp180 = *((__u32 *)__cil_tmp179);
#line 662
  *((__u32 *)__cil_tmp176) = __cil_tmp180 + 1U;
#line 665
  __cil_tmp181 = (unsigned long )state;
#line 665
  __cil_tmp182 = __cil_tmp181 + 76;
#line 665
  __cil_tmp183 = (unsigned long )state;
#line 665
  __cil_tmp184 = __cil_tmp183 + 76;
#line 665
  __cil_tmp185 = *((int *)__cil_tmp184);
#line 665
  *((int *)__cil_tmp182) = __cil_tmp185 >> 1;
#line 667
  return (osize);
}
}
#line 676 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void mppe_incomp(void *arg , unsigned char *ibuf , int icnt ) 
{ struct ppp_mppe_state *state ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  int __cil_tmp7 ;
  __u8 *__cil_tmp8 ;
  __u8 __cil_tmp9 ;
  int __cil_tmp10 ;
  __u8 *__cil_tmp11 ;
  __u8 __cil_tmp12 ;
  int __cil_tmp13 ;
  int __cil_tmp14 ;
  int __cil_tmp15 ;
  __u8 *__cil_tmp16 ;
  __u8 __cil_tmp17 ;
  int __cil_tmp18 ;
  __u8 *__cil_tmp19 ;
  __u8 __cil_tmp20 ;
  int __cil_tmp21 ;
  int __cil_tmp22 ;
  int __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  int __cil_tmp26 ;
  __u8 *__cil_tmp27 ;
  __u8 __cil_tmp28 ;
  int __cil_tmp29 ;
  __u8 *__cil_tmp30 ;
  __u8 __cil_tmp31 ;
  int __cil_tmp32 ;
  int __cil_tmp33 ;
  int __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  __u32 __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  __u32 __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  __u32 __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  __u32 __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  __u32 __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  unsigned long __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  __u32 __cil_tmp62 ;

  {
#line 678
  state = (struct ppp_mppe_state *)arg;
  {
#line 680
  __cil_tmp5 = (unsigned long )state;
#line 680
  __cil_tmp6 = __cil_tmp5 + 84;
#line 680
  __cil_tmp7 = *((int *)__cil_tmp6);
#line 680
  if (__cil_tmp7 != 0) {
    {
#line 680
    __cil_tmp8 = ibuf + 3UL;
#line 680
    __cil_tmp9 = *__cil_tmp8;
#line 680
    __cil_tmp10 = (int )__cil_tmp9;
#line 680
    __cil_tmp11 = ibuf + 2UL;
#line 680
    __cil_tmp12 = *__cil_tmp11;
#line 680
    __cil_tmp13 = (int )__cil_tmp12;
#line 680
    __cil_tmp14 = __cil_tmp13 << 8;
#line 680
    __cil_tmp15 = __cil_tmp14 + __cil_tmp10;
#line 680
    if (__cil_tmp15 > 32) {
      {
#line 680
      __cil_tmp16 = ibuf + 3UL;
#line 680
      __cil_tmp17 = *__cil_tmp16;
#line 680
      __cil_tmp18 = (int )__cil_tmp17;
#line 680
      __cil_tmp19 = ibuf + 2UL;
#line 680
      __cil_tmp20 = *__cil_tmp19;
#line 680
      __cil_tmp21 = (int )__cil_tmp20;
#line 680
      __cil_tmp22 = __cil_tmp21 << 8;
#line 680
      __cil_tmp23 = __cil_tmp22 + __cil_tmp18;
#line 680
      if (__cil_tmp23 <= 250) {
        {
#line 682
        __cil_tmp24 = (unsigned long )state;
#line 682
        __cil_tmp25 = __cil_tmp24 + 80;
#line 682
        __cil_tmp26 = *((int *)__cil_tmp25);
#line 682
        __cil_tmp27 = ibuf + 3UL;
#line 682
        __cil_tmp28 = *__cil_tmp27;
#line 682
        __cil_tmp29 = (int )__cil_tmp28;
#line 682
        __cil_tmp30 = ibuf + 2UL;
#line 682
        __cil_tmp31 = *__cil_tmp30;
#line 682
        __cil_tmp32 = (int )__cil_tmp31;
#line 682
        __cil_tmp33 = __cil_tmp32 << 8;
#line 682
        __cil_tmp34 = __cil_tmp33 + __cil_tmp29;
#line 682
        printk("<7>mppe_incomp[%d]: incompressible (unencrypted) data! (proto %04x)\n",
               __cil_tmp26, __cil_tmp34);
        }
      } else {

      }
      }
    } else {

    }
    }
  } else {

  }
  }
#line 686
  __cil_tmp35 = 88 + 16;
#line 686
  __cil_tmp36 = (unsigned long )state;
#line 686
  __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
#line 686
  __cil_tmp38 = (__u32 )icnt;
#line 686
  __cil_tmp39 = 88 + 16;
#line 686
  __cil_tmp40 = (unsigned long )state;
#line 686
  __cil_tmp41 = __cil_tmp40 + __cil_tmp39;
#line 686
  __cil_tmp42 = *((__u32 *)__cil_tmp41);
#line 686
  *((__u32 *)__cil_tmp37) = __cil_tmp42 + __cil_tmp38;
#line 687
  __cil_tmp43 = 88 + 20;
#line 687
  __cil_tmp44 = (unsigned long )state;
#line 687
  __cil_tmp45 = __cil_tmp44 + __cil_tmp43;
#line 687
  __cil_tmp46 = 88 + 20;
#line 687
  __cil_tmp47 = (unsigned long )state;
#line 687
  __cil_tmp48 = __cil_tmp47 + __cil_tmp46;
#line 687
  __cil_tmp49 = *((__u32 *)__cil_tmp48);
#line 687
  *((__u32 *)__cil_tmp45) = __cil_tmp49 + 1U;
#line 688
  __cil_tmp50 = (unsigned long )state;
#line 688
  __cil_tmp51 = __cil_tmp50 + 88;
#line 688
  __cil_tmp52 = (__u32 )icnt;
#line 688
  __cil_tmp53 = (unsigned long )state;
#line 688
  __cil_tmp54 = __cil_tmp53 + 88;
#line 688
  __cil_tmp55 = *((__u32 *)__cil_tmp54);
#line 688
  *((__u32 *)__cil_tmp51) = __cil_tmp55 + __cil_tmp52;
#line 689
  __cil_tmp56 = 88 + 4;
#line 689
  __cil_tmp57 = (unsigned long )state;
#line 689
  __cil_tmp58 = __cil_tmp57 + __cil_tmp56;
#line 689
  __cil_tmp59 = 88 + 4;
#line 689
  __cil_tmp60 = (unsigned long )state;
#line 689
  __cil_tmp61 = __cil_tmp60 + __cil_tmp59;
#line 689
  __cil_tmp62 = *((__u32 *)__cil_tmp61);
#line 689
  *((__u32 *)__cil_tmp58) = __cil_tmp62 + 1U;
#line 690
  return;
}
}
#line 699 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static struct compressor ppp_mppe  = 
#line 699
     {18, & mppe_alloc, & mppe_free, & mppe_comp_init, & mppe_comp_reset, & mppe_compress,
    & mppe_comp_stats, & mppe_alloc, & mppe_free, & mppe_decomp_init, & mppe_decomp_reset,
    & mppe_decompress, & mppe_incomp, & mppe_comp_stats, & __this_module, 4U};
#line 726 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static int ppp_mppe_init(void) 
{ int answer ;
  int tmp ;
  int tmp___0 ;
  void *tmp___1 ;
  struct sha_pad *__cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  void const   *__cil_tmp8 ;

  {
  {
#line 729
  tmp = crypto_has_blkcipher("ecb(arc4)", 0U, 128U);
  }
#line 729
  if (tmp == 0) {
#line 731
    return (-19);
  } else {
    {
#line 729
    tmp___0 = crypto_has_hash("sha1", 0U, 128U);
    }
#line 729
    if (tmp___0 == 0) {
#line 731
      return (-19);
    } else {

    }
  }
  {
#line 733
  tmp___1 = kmalloc(80UL, 208U);
#line 733
  sha_pad = (struct sha_pad *)tmp___1;
  }
  {
#line 734
  __cil_tmp5 = (struct sha_pad *)0;
#line 734
  __cil_tmp6 = (unsigned long )__cil_tmp5;
#line 734
  __cil_tmp7 = (unsigned long )sha_pad;
#line 734
  if (__cil_tmp7 == __cil_tmp6) {
#line 735
    return (-12);
  } else {

  }
  }
  {
#line 736
  sha_pad_init(sha_pad);
#line 738
  answer = ppp_register_compressor(& ppp_mppe);
  }
#line 740
  if (answer == 0) {
    {
#line 741
    printk("<6>PPP MPPE Compression module registered\n");
    }
  } else {
    {
#line 743
    __cil_tmp8 = (void const   *)sha_pad;
#line 743
    kfree(__cil_tmp8);
    }
  }
#line 745
  return (answer);
}
}
#line 748 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
static void ppp_mppe_cleanup(void) 
{ void const   *__cil_tmp1 ;

  {
  {
#line 750
  ppp_unregister_compressor(& ppp_mppe);
#line 751
  __cil_tmp1 = (void const   *)sha_pad;
#line 751
  kfree(__cil_tmp1);
  }
#line 752
  return;
}
}
#line 773
extern void ldv_check_final_state(void) ;
#line 779
extern void ldv_initialize(void) ;
#line 782
extern int __VERIFIER_nondet_int(void) ;
#line 785 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
int LDV_IN_INTERRUPT  ;
#line 788 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
void main(void) 
{ unsigned char *var_mppe_alloc_4_p0 ;
  int var_mppe_alloc_4_p1 ;
  void *var_mppe_free_5_p0 ;
  void *var_mppe_comp_init_7_p0 ;
  unsigned char *var_mppe_comp_init_7_p1 ;
  int var_mppe_comp_init_7_p2 ;
  int var_mppe_comp_init_7_p3 ;
  int var_mppe_comp_init_7_p4 ;
  int var_mppe_comp_init_7_p5 ;
  void *var_mppe_comp_reset_8_p0 ;
  void *var_mppe_compress_9_p0 ;
  unsigned char *var_mppe_compress_9_p1 ;
  unsigned char *var_mppe_compress_9_p2 ;
  int var_mppe_compress_9_p3 ;
  int var_mppe_compress_9_p4 ;
  void *var_mppe_comp_stats_10_p0 ;
  struct compstat *var_group1 ;
  void *var_mppe_decomp_init_11_p0 ;
  unsigned char *var_mppe_decomp_init_11_p1 ;
  int var_mppe_decomp_init_11_p2 ;
  int var_mppe_decomp_init_11_p3 ;
  int var_mppe_decomp_init_11_p4 ;
  int var_mppe_decomp_init_11_p5 ;
  int var_mppe_decomp_init_11_p6 ;
  void *var_mppe_decomp_reset_12_p0 ;
  void *var_mppe_decompress_13_p0 ;
  unsigned char *var_mppe_decompress_13_p1 ;
  int var_mppe_decompress_13_p2 ;
  unsigned char *var_mppe_decompress_13_p3 ;
  int var_mppe_decompress_13_p4 ;
  void *var_mppe_incomp_14_p0 ;
  unsigned char *var_mppe_incomp_14_p1 ;
  int var_mppe_incomp_14_p2 ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
  {
#line 1018
  LDV_IN_INTERRUPT = 1;
#line 1027
  ldv_initialize();
#line 1046
  tmp = ppp_mppe_init();
  }
#line 1046
  if (tmp != 0) {
#line 1047
    goto ldv_final;
  } else {

  }
#line 1051
  goto ldv_18292;
  ldv_18291: 
  {
#line 1054
  tmp___0 = __VERIFIER_nondet_int();
  }
#line 1056
  if (tmp___0 == 0) {
#line 1056
    goto case_0;
  } else
#line 1085
  if (tmp___0 == 1) {
#line 1085
    goto case_1;
  } else
#line 1114
  if (tmp___0 == 2) {
#line 1114
    goto case_2;
  } else
#line 1143
  if (tmp___0 == 3) {
#line 1143
    goto case_3;
  } else
#line 1172
  if (tmp___0 == 4) {
#line 1172
    goto case_4;
  } else
#line 1201
  if (tmp___0 == 5) {
#line 1201
    goto case_5;
  } else
#line 1230
  if (tmp___0 == 6) {
#line 1230
    goto case_6;
  } else
#line 1259
  if (tmp___0 == 7) {
#line 1259
    goto case_7;
  } else
#line 1288
  if (tmp___0 == 8) {
#line 1288
    goto case_8;
  } else
#line 1317
  if (tmp___0 == 9) {
#line 1317
    goto case_9;
  } else {
    {
#line 1346
    goto switch_default;
#line 1054
    if (0) {
      case_0: /* CIL Label */ 
      {
#line 1077
      mppe_alloc(var_mppe_alloc_4_p0, var_mppe_alloc_4_p1);
      }
#line 1084
      goto ldv_18280;
      case_1: /* CIL Label */ 
      {
#line 1106
      mppe_free(var_mppe_free_5_p0);
      }
#line 1113
      goto ldv_18280;
      case_2: /* CIL Label */ 
      {
#line 1135
      mppe_comp_init(var_mppe_comp_init_7_p0, var_mppe_comp_init_7_p1, var_mppe_comp_init_7_p2,
                     var_mppe_comp_init_7_p3, var_mppe_comp_init_7_p4, var_mppe_comp_init_7_p5);
      }
#line 1142
      goto ldv_18280;
      case_3: /* CIL Label */ 
      {
#line 1164
      mppe_comp_reset(var_mppe_comp_reset_8_p0);
      }
#line 1171
      goto ldv_18280;
      case_4: /* CIL Label */ 
      {
#line 1193
      mppe_compress(var_mppe_compress_9_p0, var_mppe_compress_9_p1, var_mppe_compress_9_p2,
                    var_mppe_compress_9_p3, var_mppe_compress_9_p4);
      }
#line 1200
      goto ldv_18280;
      case_5: /* CIL Label */ 
      {
#line 1222
      mppe_comp_stats(var_mppe_comp_stats_10_p0, var_group1);
      }
#line 1229
      goto ldv_18280;
      case_6: /* CIL Label */ 
      {
#line 1251
      mppe_decomp_init(var_mppe_decomp_init_11_p0, var_mppe_decomp_init_11_p1, var_mppe_decomp_init_11_p2,
                       var_mppe_decomp_init_11_p3, var_mppe_decomp_init_11_p4, var_mppe_decomp_init_11_p5,
                       var_mppe_decomp_init_11_p6);
      }
#line 1258
      goto ldv_18280;
      case_7: /* CIL Label */ 
      {
#line 1280
      mppe_decomp_reset(var_mppe_decomp_reset_12_p0);
      }
#line 1287
      goto ldv_18280;
      case_8: /* CIL Label */ 
      {
#line 1309
      mppe_decompress(var_mppe_decompress_13_p0, var_mppe_decompress_13_p1, var_mppe_decompress_13_p2,
                      var_mppe_decompress_13_p3, var_mppe_decompress_13_p4);
      }
#line 1316
      goto ldv_18280;
      case_9: /* CIL Label */ 
      {
#line 1338
      mppe_incomp(var_mppe_incomp_14_p0, var_mppe_incomp_14_p1, var_mppe_incomp_14_p2);
      }
#line 1345
      goto ldv_18280;
      switch_default: /* CIL Label */ ;
#line 1346
      goto ldv_18280;
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
  ldv_18280: ;
  ldv_18292: 
  {
#line 1051
  tmp___1 = __VERIFIER_nondet_int();
  }
#line 1051
  if (tmp___1 != 0) {
#line 1052
    goto ldv_18291;
  } else {
#line 1054
    goto ldv_18293;
  }
  ldv_18293: ;
  {
#line 1371
  ppp_mppe_cleanup();
  }
  ldv_final: 
  {
#line 1374
  ldv_check_final_state();
  }
#line 1377
  return;
}
}
#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
void ldv_blast_assert(void) 
{ 

  {
  ERROR: ;
#line 6
  goto ERROR;
}
}
#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
extern int __VERIFIER_nondet_int(void) ;
#line 1398 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
int ldv_spin  =    0;
#line 1402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
void ldv_check_alloc_flags(gfp_t flags ) 
{ 

  {
#line 1405
  if (ldv_spin != 0) {
#line 1405
    if (flags != 32U) {
      {
#line 1405
      ldv_blast_assert();
      }
    } else {

    }
  } else {

  }
#line 1408
  return;
}
}
#line 1408
extern struct page *ldv_some_page(void) ;
#line 1411 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
{ struct page *tmp ;

  {
#line 1414
  if (ldv_spin != 0) {
#line 1414
    if (flags != 32U) {
      {
#line 1414
      ldv_blast_assert();
      }
    } else {

    }
  } else {

  }
  {
#line 1416
  tmp = ldv_some_page();
  }
#line 1416
  return (tmp);
}
}
#line 1420 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
void ldv_check_alloc_nonatomic(void) 
{ 

  {
#line 1423
  if (ldv_spin != 0) {
    {
#line 1423
    ldv_blast_assert();
    }
  } else {

  }
#line 1426
  return;
}
}
#line 1427 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
void ldv_spin_lock(void) 
{ 

  {
#line 1430
  ldv_spin = 1;
#line 1431
  return;
}
}
#line 1434 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
void ldv_spin_unlock(void) 
{ 

  {
#line 1437
  ldv_spin = 0;
#line 1438
  return;
}
}
#line 1441 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
int ldv_spin_trylock(void) 
{ int is_lock ;

  {
  {
#line 1446
  is_lock = __VERIFIER_nondet_int();
  }
#line 1448
  if (is_lock != 0) {
#line 1451
    return (0);
  } else {
#line 1456
    ldv_spin = 1;
#line 1458
    return (1);
  }
}
}
#line 1580 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
__inline static void *kmalloc(size_t size , gfp_t flags ) 
{ 

  {
  {
#line 1586
  ldv_check_alloc_flags(flags);
#line 1588
  ldv_kmalloc_12(size, flags);
  }
#line 1589
  return ((void *)0);
}
}
#line 1625 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
{ 

  {
  {
#line 1631
  ldv_check_alloc_flags(ldv_func_arg2);
#line 1633
  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
  }
#line 1634
  return ((void *)0);
}
}
#line 1636 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15265/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/ppp_mppe.c.p"
__inline static void *kzalloc(size_t size , gfp_t flags ) 
{ void *tmp ;

  {
  {
#line 1642
  ldv_check_alloc_flags(flags);
#line 1643
  tmp = __VERIFIER_nondet_pointer();
  }
#line 1643
  return (tmp);
}
}