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 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 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_13371_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_13371_134 ldv_13371 ;
 };
 #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 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 __anonstruct_hs_136 {
    unsigned short prefix ;
    unsigned char suffix ;
    unsigned char pad ;
 };
 #line 182 "include/linux/ppp-comp.h"
 union __anonunion_f_135 {
    unsigned long fcode ;
    struct __anonstruct_hs_136 hs ;
 };
 #line 182 "include/linux/ppp-comp.h"
 struct bsd_dict {
    union __anonunion_f_135 f ;
    unsigned short codem1 ;
    unsigned short cptr ;
 };
 #line 150 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
 struct bsd_db {
    int totlen ;
    unsigned int hsize ;
    unsigned char hshift ;
    unsigned char n_bits ;
    unsigned char maxbits ;
    unsigned char debug ;
    unsigned char unit ;
    unsigned short seqno ;
    unsigned int mru ;
    unsigned int maxmaxcode ;
    unsigned int max_ent ;
    unsigned int in_count ;
    unsigned int bytes_out ;
    unsigned int ratio ;
    unsigned int checkpoint ;
    unsigned int clear_count ;
    unsigned int incomp_count ;
    unsigned int incomp_bytes ;
    unsigned int uncomp_count ;
    unsigned int uncomp_bytes ;
    unsigned int comp_count ;
    unsigned int comp_bytes ;
    unsigned short *lens ;
    struct bsd_dict *dict ;
 };
 #line 2
 void ldv_spin_lock(void) ;
 #line 3
 void ldv_spin_unlock(void) ;
 #line 4
 int ldv_spin_trylock(void) ;
 #line 101 "include/linux/printk.h"
 extern int printk(char const   *  , ...) ;
 #line 54 "include/linux/vmalloc.h"
 extern void *vmalloc(unsigned long  ) ;
 #line 57
 void *ldv_vmalloc_19(unsigned long ldv_func_arg1 ) ;
 #line 61
 void *ldv_vmalloc_20(unsigned long ldv_func_arg1 ) ;
 #line 74
 extern void vfree(void const   * ) ;
 #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 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/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.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 180 "include/linux/ppp-comp.h"
 extern int ppp_register_compressor(struct compressor * ) ;
 #line 181
 extern void ppp_unregister_compressor(struct compressor * ) ;
 #line 183 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
 static void bsd_free(void *state ) ;
 #line 184
 static void *bsd_alloc(unsigned char *options , int opt_len , int decomp ) ;
 #line 185
 static void *bsd_comp_alloc(unsigned char *options , int opt_len ) ;
 #line 186
 static void *bsd_decomp_alloc(unsigned char *options , int opt_len ) ;
 #line 188
 static int bsd_init(void *state , unsigned char *options , int opt_len , int unit ,
                     int debug , int decomp ) ;
 #line 190
 static int bsd_comp_init(void *state , unsigned char *options , int opt_len , int unit ,
                          int opthdr , int debug ) ;
 #line 192
 static int bsd_decomp_init(void *state , unsigned char *options , int opt_len , int unit ,
                            int opthdr , int mru , int debug ) ;
 #line 196
 static void bsd_reset(void *state ) ;
 #line 197
 static void bsd_comp_stats(void *state , struct compstat *stats ) ;
 #line 199
 static int bsd_compress(void *state , unsigned char *rptr , unsigned char *obuf ,
                         int isize , int osize ) ;
 #line 201
 static void bsd_incomp(void *state , unsigned char *ibuf , int icnt ) ;
 #line 203
 static int bsd_decompress(void *state , unsigned char *ibuf , int isize , unsigned char *obuf ,
                           int osize ) ;
 #line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
 static void bsd_clear(struct bsd_db *db ) 
 { unsigned long __cil_tmp2 ;
   unsigned long __cil_tmp3 ;
   unsigned long __cil_tmp4 ;
   unsigned long __cil_tmp5 ;
   unsigned int __cil_tmp6 ;
   unsigned long __cil_tmp7 ;
   unsigned long __cil_tmp8 ;
   unsigned long __cil_tmp9 ;
   unsigned long __cil_tmp10 ;
   unsigned long __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   unsigned long __cil_tmp15 ;
   unsigned long __cil_tmp16 ;
   unsigned long __cil_tmp17 ;
   unsigned long __cil_tmp18 ;
 
   {
 #line 239
   __cil_tmp2 = (unsigned long )db;
 #line 239
   __cil_tmp3 = __cil_tmp2 + 44;
 #line 239
   __cil_tmp4 = (unsigned long )db;
 #line 239
   __cil_tmp5 = __cil_tmp4 + 44;
 #line 239
   __cil_tmp6 = *((unsigned int *)__cil_tmp5);
 #line 239
   *((unsigned int *)__cil_tmp3) = __cil_tmp6 + 1U;
 #line 240
   __cil_tmp7 = (unsigned long )db;
 #line 240
   __cil_tmp8 = __cil_tmp7 + 24;
 #line 240
   *((unsigned int *)__cil_tmp8) = 256U;
 #line 241
   __cil_tmp9 = (unsigned long )db;
 #line 241
   __cil_tmp10 = __cil_tmp9 + 9;
 #line 241
   *((unsigned char *)__cil_tmp10) = (unsigned char)9;
 #line 242
   __cil_tmp11 = (unsigned long )db;
 #line 242
   __cil_tmp12 = __cil_tmp11 + 32;
 #line 242
   *((unsigned int *)__cil_tmp12) = 0U;
 #line 243
   __cil_tmp13 = (unsigned long )db;
 #line 243
   __cil_tmp14 = __cil_tmp13 + 28;
 #line 243
   *((unsigned int *)__cil_tmp14) = 0U;
 #line 244
   __cil_tmp15 = (unsigned long )db;
 #line 244
   __cil_tmp16 = __cil_tmp15 + 36;
 #line 244
   *((unsigned int *)__cil_tmp16) = 0U;
 #line 245
   __cil_tmp17 = (unsigned long )db;
 #line 245
   __cil_tmp18 = __cil_tmp17 + 40;
 #line 245
   *((unsigned int *)__cil_tmp18) = 10000U;
 #line 246
   return;
 }
 }
 #line 262 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
 static int bsd_check(struct bsd_db *db ) 
 { unsigned int new_ratio ;
   unsigned long __cil_tmp3 ;
   unsigned long __cil_tmp4 ;
   unsigned int __cil_tmp5 ;
   unsigned long __cil_tmp6 ;
   unsigned long __cil_tmp7 ;
   unsigned int __cil_tmp8 ;
   unsigned long __cil_tmp9 ;
   unsigned long __cil_tmp10 ;
   unsigned int __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   unsigned long __cil_tmp15 ;
   unsigned int __cil_tmp16 ;
   unsigned int __cil_tmp17 ;
   unsigned long __cil_tmp18 ;
   unsigned long __cil_tmp19 ;
   unsigned int __cil_tmp20 ;
   unsigned long __cil_tmp21 ;
   unsigned long __cil_tmp22 ;
   unsigned long __cil_tmp23 ;
   unsigned long __cil_tmp24 ;
   unsigned int __cil_tmp25 ;
   unsigned int __cil_tmp26 ;
   unsigned long __cil_tmp27 ;
   unsigned long __cil_tmp28 ;
   unsigned int __cil_tmp29 ;
   unsigned long __cil_tmp30 ;
   unsigned long __cil_tmp31 ;
   unsigned int __cil_tmp32 ;
   unsigned long __cil_tmp33 ;
   unsigned long __cil_tmp34 ;
   unsigned long __cil_tmp35 ;
   unsigned long __cil_tmp36 ;
   unsigned int __cil_tmp37 ;
   unsigned int __cil_tmp38 ;
   unsigned long __cil_tmp39 ;
   unsigned long __cil_tmp40 ;
   unsigned int __cil_tmp41 ;
   unsigned long __cil_tmp42 ;
   unsigned long __cil_tmp43 ;
   unsigned long __cil_tmp44 ;
   unsigned long __cil_tmp45 ;
   unsigned int __cil_tmp46 ;
   unsigned int __cil_tmp47 ;
   unsigned long __cil_tmp48 ;
   unsigned long __cil_tmp49 ;
   unsigned int __cil_tmp50 ;
   unsigned long __cil_tmp51 ;
   unsigned long __cil_tmp52 ;
   unsigned long __cil_tmp53 ;
   unsigned long __cil_tmp54 ;
   unsigned int __cil_tmp55 ;
   unsigned long __cil_tmp56 ;
   unsigned long __cil_tmp57 ;
   unsigned int __cil_tmp58 ;
   unsigned long __cil_tmp59 ;
   unsigned long __cil_tmp60 ;
   unsigned int __cil_tmp61 ;
   unsigned long __cil_tmp62 ;
   unsigned long __cil_tmp63 ;
   unsigned int __cil_tmp64 ;
   unsigned long __cil_tmp65 ;
   unsigned long __cil_tmp66 ;
   unsigned int __cil_tmp67 ;
   unsigned long __cil_tmp68 ;
   unsigned long __cil_tmp69 ;
   unsigned int __cil_tmp70 ;
   unsigned long __cil_tmp71 ;
   unsigned long __cil_tmp72 ;
   unsigned int __cil_tmp73 ;
   unsigned long __cil_tmp74 ;
   unsigned long __cil_tmp75 ;
 
   {
   {
 #line 266
   __cil_tmp3 = (unsigned long )db;
 #line 266
   __cil_tmp4 = __cil_tmp3 + 40;
 #line 266
   __cil_tmp5 = *((unsigned int *)__cil_tmp4);
 #line 266
   __cil_tmp6 = (unsigned long )db;
 #line 266
   __cil_tmp7 = __cil_tmp6 + 28;
 #line 266
   __cil_tmp8 = *((unsigned int *)__cil_tmp7);
 #line 266
   if (__cil_tmp8 >= __cil_tmp5) {
     {
 #line 269
     __cil_tmp9 = (unsigned long )db;
 #line 269
     __cil_tmp10 = __cil_tmp9 + 28;
 #line 269
     __cil_tmp11 = *((unsigned int *)__cil_tmp10);
 #line 269
     if (__cil_tmp11 > 8388606U) {
 #line 271
       __cil_tmp12 = (unsigned long )db;
 #line 271
       __cil_tmp13 = __cil_tmp12 + 28;
 #line 271
       __cil_tmp14 = (unsigned long )db;
 #line 271
       __cil_tmp15 = __cil_tmp14 + 28;
 #line 271
       __cil_tmp16 = *((unsigned int *)__cil_tmp15);
 #line 271
       __cil_tmp17 = __cil_tmp16 >> 2;
 #line 271
       __cil_tmp18 = (unsigned long )db;
 #line 271
       __cil_tmp19 = __cil_tmp18 + 28;
 #line 271
       __cil_tmp20 = *((unsigned int *)__cil_tmp19);
 #line 271
       *((unsigned int *)__cil_tmp13) = __cil_tmp20 - __cil_tmp17;
 #line 272
       __cil_tmp21 = (unsigned long )db;
 #line 272
       __cil_tmp22 = __cil_tmp21 + 32;
 #line 272
       __cil_tmp23 = (unsigned long )db;
 #line 272
       __cil_tmp24 = __cil_tmp23 + 32;
 #line 272
       __cil_tmp25 = *((unsigned int *)__cil_tmp24);
 #line 272
       __cil_tmp26 = __cil_tmp25 >> 2;
 #line 272
       __cil_tmp27 = (unsigned long )db;
 #line 272
       __cil_tmp28 = __cil_tmp27 + 32;
 #line 272
       __cil_tmp29 = *((unsigned int *)__cil_tmp28);
 #line 272
       *((unsigned int *)__cil_tmp22) = __cil_tmp29 - __cil_tmp26;
     } else {
       {
 #line 269
       __cil_tmp30 = (unsigned long )db;
 #line 269
       __cil_tmp31 = __cil_tmp30 + 32;
 #line 269
       __cil_tmp32 = *((unsigned int *)__cil_tmp31);
 #line 269
       if (__cil_tmp32 > 8388606U) {
 #line 271
         __cil_tmp33 = (unsigned long )db;
 #line 271
         __cil_tmp34 = __cil_tmp33 + 28;
 #line 271
         __cil_tmp35 = (unsigned long )db;
 #line 271
         __cil_tmp36 = __cil_tmp35 + 28;
 #line 271
         __cil_tmp37 = *((unsigned int *)__cil_tmp36);
 #line 271
         __cil_tmp38 = __cil_tmp37 >> 2;
 #line 271
         __cil_tmp39 = (unsigned long )db;
 #line 271
         __cil_tmp40 = __cil_tmp39 + 28;
 #line 271
         __cil_tmp41 = *((unsigned int *)__cil_tmp40);
 #line 271
         *((unsigned int *)__cil_tmp34) = __cil_tmp41 - __cil_tmp38;
 #line 272
         __cil_tmp42 = (unsigned long )db;
 #line 272
         __cil_tmp43 = __cil_tmp42 + 32;
 #line 272
         __cil_tmp44 = (unsigned long )db;
 #line 272
         __cil_tmp45 = __cil_tmp44 + 32;
 #line 272
         __cil_tmp46 = *((unsigned int *)__cil_tmp45);
 #line 272
         __cil_tmp47 = __cil_tmp46 >> 2;
 #line 272
         __cil_tmp48 = (unsigned long )db;
 #line 272
         __cil_tmp49 = __cil_tmp48 + 32;
 #line 272
         __cil_tmp50 = *((unsigned int *)__cil_tmp49);
 #line 272
         *((unsigned int *)__cil_tmp43) = __cil_tmp50 - __cil_tmp47;
       } else {
 
       }
       }
     }
     }
 #line 275
     __cil_tmp51 = (unsigned long )db;
 #line 275
     __cil_tmp52 = __cil_tmp51 + 40;
 #line 275
     __cil_tmp53 = (unsigned long )db;
 #line 275
     __cil_tmp54 = __cil_tmp53 + 28;
 #line 275
     __cil_tmp55 = *((unsigned int *)__cil_tmp54);
 #line 275
     *((unsigned int *)__cil_tmp52) = __cil_tmp55 + 10000U;
     {
 #line 277
     __cil_tmp56 = (unsigned long )db;
 #line 277
     __cil_tmp57 = __cil_tmp56 + 20;
 #line 277
     __cil_tmp58 = *((unsigned int *)__cil_tmp57);
 #line 277
     __cil_tmp59 = (unsigned long )db;
 #line 277
     __cil_tmp60 = __cil_tmp59 + 24;
 #line 277
     __cil_tmp61 = *((unsigned int *)__cil_tmp60);
 #line 277
     if (__cil_tmp61 >= __cil_tmp58) {
 #line 287
       __cil_tmp62 = (unsigned long )db;
 #line 287
       __cil_tmp63 = __cil_tmp62 + 28;
 #line 287
       __cil_tmp64 = *((unsigned int *)__cil_tmp63);
 #line 287
       new_ratio = __cil_tmp64 << 8;
       {
 #line 288
       __cil_tmp65 = (unsigned long )db;
 #line 288
       __cil_tmp66 = __cil_tmp65 + 32;
 #line 288
       __cil_tmp67 = *((unsigned int *)__cil_tmp66);
 #line 288
       if (__cil_tmp67 != 0U) {
 #line 290
         __cil_tmp68 = (unsigned long )db;
 #line 290
         __cil_tmp69 = __cil_tmp68 + 32;
 #line 290
         __cil_tmp70 = *((unsigned int *)__cil_tmp69);
 #line 290
         new_ratio = new_ratio / __cil_tmp70;
       } else {
 
       }
       }
       {
 #line 293
       __cil_tmp71 = (unsigned long )db;
 #line 293
       __cil_tmp72 = __cil_tmp71 + 36;
 #line 293
       __cil_tmp73 = *((unsigned int *)__cil_tmp72);
 #line 293
       if (__cil_tmp73 > new_ratio) {
         {
 #line 295
         bsd_clear(db);
         }
 #line 296
         return (1);
       } else
 #line 293
       if (new_ratio <= 255U) {
         {
 #line 295
         bsd_clear(db);
         }
#line 296
        return (1);
      } else {

      }
      }
#line 298
      __cil_tmp74 = (unsigned long )db;
#line 298
      __cil_tmp75 = __cil_tmp74 + 36;
#line 298
      *((unsigned int *)__cil_tmp75) = new_ratio;
    } else {

    }
    }
  } else {

  }
  }
#line 301
  return (0);
}
}
#line 308 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static void bsd_comp_stats(void *state , struct compstat *stats ) 
{ struct bsd_db *db ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;

  {
#line 310
  db = (struct bsd_db *)state;
#line 312
  __cil_tmp4 = (unsigned long )db;
#line 312
  __cil_tmp5 = __cil_tmp4 + 60;
#line 312
  *((__u32 *)stats) = *((unsigned int *)__cil_tmp5);
#line 313
  __cil_tmp6 = (unsigned long )stats;
#line 313
  __cil_tmp7 = __cil_tmp6 + 4;
#line 313
  __cil_tmp8 = (unsigned long )db;
#line 313
  __cil_tmp9 = __cil_tmp8 + 56;
#line 313
  *((__u32 *)__cil_tmp7) = *((unsigned int *)__cil_tmp9);
#line 314
  __cil_tmp10 = (unsigned long )stats;
#line 314
  __cil_tmp11 = __cil_tmp10 + 8;
#line 314
  __cil_tmp12 = (unsigned long )db;
#line 314
  __cil_tmp13 = __cil_tmp12 + 68;
#line 314
  *((__u32 *)__cil_tmp11) = *((unsigned int *)__cil_tmp13);
#line 315
  __cil_tmp14 = (unsigned long )stats;
#line 315
  __cil_tmp15 = __cil_tmp14 + 12;
#line 315
  __cil_tmp16 = (unsigned long )db;
#line 315
  __cil_tmp17 = __cil_tmp16 + 64;
#line 315
  *((__u32 *)__cil_tmp15) = *((unsigned int *)__cil_tmp17);
#line 316
  __cil_tmp18 = (unsigned long )stats;
#line 316
  __cil_tmp19 = __cil_tmp18 + 16;
#line 316
  __cil_tmp20 = (unsigned long )db;
#line 316
  __cil_tmp21 = __cil_tmp20 + 52;
#line 316
  *((__u32 *)__cil_tmp19) = *((unsigned int *)__cil_tmp21);
#line 317
  __cil_tmp22 = (unsigned long )stats;
#line 317
  __cil_tmp23 = __cil_tmp22 + 20;
#line 317
  __cil_tmp24 = (unsigned long )db;
#line 317
  __cil_tmp25 = __cil_tmp24 + 48;
#line 317
  *((__u32 *)__cil_tmp23) = *((unsigned int *)__cil_tmp25);
#line 318
  __cil_tmp26 = (unsigned long )stats;
#line 318
  __cil_tmp27 = __cil_tmp26 + 24;
#line 318
  __cil_tmp28 = (unsigned long )db;
#line 318
  __cil_tmp29 = __cil_tmp28 + 28;
#line 318
  *((__u32 *)__cil_tmp27) = *((unsigned int *)__cil_tmp29);
#line 319
  __cil_tmp30 = (unsigned long )stats;
#line 319
  __cil_tmp31 = __cil_tmp30 + 28;
#line 319
  __cil_tmp32 = (unsigned long )db;
#line 319
  __cil_tmp33 = __cil_tmp32 + 32;
#line 319
  *((__u32 *)__cil_tmp31) = *((unsigned int *)__cil_tmp33);
#line 320
  return;
}
}
#line 326 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static void bsd_reset(void *state ) 
{ struct bsd_db *db ;
  unsigned long __cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;

  {
  {
#line 328
  db = (struct bsd_db *)state;
#line 330
  bsd_clear(db);
#line 332
  __cil_tmp3 = (unsigned long )db;
#line 332
  __cil_tmp4 = __cil_tmp3 + 14;
#line 332
  *((unsigned short *)__cil_tmp4) = (unsigned short)0;
#line 333
  __cil_tmp5 = (unsigned long )db;
#line 333
  __cil_tmp6 = __cil_tmp5 + 44;
#line 333
  *((unsigned int *)__cil_tmp6) = 0U;
  }
#line 334
  return;
}
}
#line 340 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static void bsd_free(void *state ) 
{ struct bsd_db *db ;
  struct bsd_db *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  struct bsd_dict *__cil_tmp8 ;
  void const   *__cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned short *__cil_tmp14 ;
  void const   *__cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  void const   *__cil_tmp18 ;

  {
#line 342
  db = (struct bsd_db *)state;
  {
#line 344
  __cil_tmp3 = (struct bsd_db *)0;
#line 344
  __cil_tmp4 = (unsigned long )__cil_tmp3;
#line 344
  __cil_tmp5 = (unsigned long )db;
#line 344
  if (__cil_tmp5 == __cil_tmp4) {
#line 345
    return;
  } else {

  }
  }
  {
#line 350
  __cil_tmp6 = (unsigned long )db;
#line 350
  __cil_tmp7 = __cil_tmp6 + 80;
#line 350
  __cil_tmp8 = *((struct bsd_dict **)__cil_tmp7);
#line 350
  __cil_tmp9 = (void const   *)__cil_tmp8;
#line 350
  vfree(__cil_tmp9);
#line 351
  __cil_tmp10 = (unsigned long )db;
#line 351
  __cil_tmp11 = __cil_tmp10 + 80;
#line 351
  *((struct bsd_dict **)__cil_tmp11) = (struct bsd_dict *)0;
#line 355
  __cil_tmp12 = (unsigned long )db;
#line 355
  __cil_tmp13 = __cil_tmp12 + 72;
#line 355
  __cil_tmp14 = *((unsigned short **)__cil_tmp13);
#line 355
  __cil_tmp15 = (void const   *)__cil_tmp14;
#line 355
  vfree(__cil_tmp15);
#line 356
  __cil_tmp16 = (unsigned long )db;
#line 356
  __cil_tmp17 = __cil_tmp16 + 72;
#line 356
  *((unsigned short **)__cil_tmp17) = (unsigned short *)0;
#line 360
  __cil_tmp18 = (void const   *)db;
#line 360
  kfree(__cil_tmp18);
  }
#line 361
  return;
}
}
#line 367 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static void *bsd_alloc(unsigned char *options , int opt_len , int decomp ) 
{ int bits ;
  unsigned int hsize ;
  unsigned int hshift ;
  unsigned int maxmaxcode ;
  struct bsd_db *db ;
  void *tmp ;
  void *tmp___0 ;
  void *tmp___1 ;
  unsigned char __cil_tmp12 ;
  unsigned int __cil_tmp13 ;
  unsigned char *__cil_tmp14 ;
  unsigned char __cil_tmp15 ;
  unsigned int __cil_tmp16 ;
  unsigned char *__cil_tmp17 ;
  unsigned char __cil_tmp18 ;
  int __cil_tmp19 ;
  int __cil_tmp20 ;
  unsigned int __cil_tmp21 ;
  unsigned char *__cil_tmp22 ;
  unsigned char __cil_tmp23 ;
  int __cil_tmp24 ;
  int __cil_tmp25 ;
  int __cil_tmp26 ;
  struct bsd_db *__cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  struct bsd_dict *__cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  struct bsd_dict *__cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  void *__cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned int __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned short *__cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned short *__cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  void *__cil_tmp54 ;
  unsigned int __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 ;

  {
#line 373
  if (opt_len != 3) {
#line 376
    return ((void *)0);
  } else {
    {
#line 373
    __cil_tmp12 = *options;
#line 373
    __cil_tmp13 = (unsigned int )__cil_tmp12;
#line 373
    if (__cil_tmp13 != 21U) {
#line 376
      return ((void *)0);
    } else {
      {
#line 373
      __cil_tmp14 = options + 1UL;
#line 373
      __cil_tmp15 = *__cil_tmp14;
#line 373
      __cil_tmp16 = (unsigned int )__cil_tmp15;
#line 373
      if (__cil_tmp16 != 3U) {
#line 376
        return ((void *)0);
      } else {
        {
#line 373
        __cil_tmp17 = options + 2UL;
#line 373
        __cil_tmp18 = *__cil_tmp17;
#line 373
        __cil_tmp19 = (int )__cil_tmp18;
#line 373
        __cil_tmp20 = __cil_tmp19 >> 5;
#line 373
        __cil_tmp21 = (unsigned int )__cil_tmp20;
#line 373
        if (__cil_tmp21 != 1U) {
#line 376
          return ((void *)0);
        } else {

        }
        }
      }
      }
    }
    }
  }
#line 379
  __cil_tmp22 = options + 2UL;
#line 379
  __cil_tmp23 = *__cil_tmp22;
#line 379
  __cil_tmp24 = (int )__cil_tmp23;
#line 379
  bits = __cil_tmp24 & 31;
#line 383
  if (bits == 9) {
#line 383
    goto case_9;
  } else
#line 384
  if (bits == 10) {
#line 384
    goto case_10;
  } else
#line 385
  if (bits == 11) {
#line 385
    goto case_11;
  } else
#line 386
  if (bits == 12) {
#line 386
    goto case_12;
  } else
#line 390
  if (bits == 13) {
#line 390
    goto case_13;
  } else
#line 394
  if (bits == 14) {
#line 394
    goto case_14;
  } else
#line 398
  if (bits == 15) {
#line 398
    goto case_15;
  } else
#line 402
  if (bits == 16) {
#line 402
    goto case_16;
  } else {
    {
#line 406
    goto switch_default;
#line 381
    if (0) {
      case_9: /* CIL Label */ ;
      case_10: /* CIL Label */ ;
      case_11: /* CIL Label */ ;
      case_12: /* CIL Label */ 
#line 387
      hsize = 5003U;
#line 388
      hshift = 4U;
#line 389
      goto ldv_14405;
      case_13: /* CIL Label */ 
#line 391
      hsize = 9001U;
#line 392
      hshift = 5U;
#line 393
      goto ldv_14405;
      case_14: /* CIL Label */ 
#line 395
      hsize = 18013U;
#line 396
      hshift = 6U;
#line 397
      goto ldv_14405;
      case_15: /* CIL Label */ 
#line 399
      hsize = 35023U;
#line 400
      hshift = 7U;
#line 401
      goto ldv_14405;
      case_16: /* CIL Label */ ;
      switch_default: /* CIL Label */ ;
#line 407
      return ((void *)0);
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
  ldv_14405: 
  {
#line 412
  __cil_tmp25 = 1 << bits;
#line 412
  __cil_tmp26 = __cil_tmp25 + -1;
#line 412
  maxmaxcode = (unsigned int )__cil_tmp26;
#line 413
  tmp = kzalloc(88UL, 208U);
#line 413
  db = (struct bsd_db *)tmp;
  }
  {
#line 415
  __cil_tmp27 = (struct bsd_db *)0;
#line 415
  __cil_tmp28 = (unsigned long )__cil_tmp27;
#line 415
  __cil_tmp29 = (unsigned long )db;
#line 415
  if (__cil_tmp29 == __cil_tmp28) {
#line 417
    return ((void *)0);
  } else {

  }
  }
  {
#line 424
  __cil_tmp30 = (unsigned long )hsize;
#line 424
  __cil_tmp31 = __cil_tmp30 * 16UL;
#line 424
  tmp___0 = ldv_vmalloc_19(__cil_tmp31);
#line 424
  __cil_tmp32 = (unsigned long )db;
#line 424
  __cil_tmp33 = __cil_tmp32 + 80;
#line 424
  *((struct bsd_dict **)__cil_tmp33) = (struct bsd_dict *)tmp___0;
  }
  {
#line 425
  __cil_tmp34 = (struct bsd_dict *)0;
#line 425
  __cil_tmp35 = (unsigned long )__cil_tmp34;
#line 425
  __cil_tmp36 = (unsigned long )db;
#line 425
  __cil_tmp37 = __cil_tmp36 + 80;
#line 425
  __cil_tmp38 = *((struct bsd_dict **)__cil_tmp37);
#line 425
  __cil_tmp39 = (unsigned long )__cil_tmp38;
#line 425
  if (__cil_tmp39 == __cil_tmp35) {
    {
#line 427
    __cil_tmp40 = (void *)db;
#line 427
    bsd_free(__cil_tmp40);
    }
#line 428
    return ((void *)0);
  } else {

  }
  }
#line 434
  if (decomp == 0) {
#line 436
    __cil_tmp41 = (unsigned long )db;
#line 436
    __cil_tmp42 = __cil_tmp41 + 72;
#line 436
    *((unsigned short **)__cil_tmp42) = (unsigned short *)0;
  } else {
    {
#line 443
    __cil_tmp43 = maxmaxcode + 1U;
#line 443
    __cil_tmp44 = (unsigned long )__cil_tmp43;
#line 443
    __cil_tmp45 = __cil_tmp44 * 2UL;
#line 443
    tmp___1 = ldv_vmalloc_20(__cil_tmp45);
#line 443
    __cil_tmp46 = (unsigned long )db;
#line 443
    __cil_tmp47 = __cil_tmp46 + 72;
#line 443
    *((unsigned short **)__cil_tmp47) = (unsigned short *)tmp___1;
    }
    {
#line 444
    __cil_tmp48 = (unsigned short *)0;
#line 444
    __cil_tmp49 = (unsigned long )__cil_tmp48;
#line 444
    __cil_tmp50 = (unsigned long )db;
#line 444
    __cil_tmp51 = __cil_tmp50 + 72;
#line 444
    __cil_tmp52 = *((unsigned short **)__cil_tmp51);
#line 444
    __cil_tmp53 = (unsigned long )__cil_tmp52;
#line 444
    if (__cil_tmp53 == __cil_tmp49) {
      {
#line 446
      __cil_tmp54 = (void *)db;
#line 446
      bsd_free(__cil_tmp54);
      }
#line 447
      return ((void *)0);
    } else {

    }
    }
  }
#line 453
  __cil_tmp55 = hsize * 16U;
#line 453
  __cil_tmp56 = __cil_tmp55 + 88U;
#line 453
  *((int *)db) = (int )__cil_tmp56;
#line 456
  __cil_tmp57 = (unsigned long )db;
#line 456
  __cil_tmp58 = __cil_tmp57 + 4;
#line 456
  *((unsigned int *)__cil_tmp58) = hsize;
#line 457
  __cil_tmp59 = (unsigned long )db;
#line 457
  __cil_tmp60 = __cil_tmp59 + 8;
#line 457
  *((unsigned char *)__cil_tmp60) = (unsigned char )hshift;
#line 458
  __cil_tmp61 = (unsigned long )db;
#line 458
  __cil_tmp62 = __cil_tmp61 + 20;
#line 458
  *((unsigned int *)__cil_tmp62) = maxmaxcode;
#line 459
  __cil_tmp63 = (unsigned long )db;
#line 459
  __cil_tmp64 = __cil_tmp63 + 10;
#line 459
  *((unsigned char *)__cil_tmp64) = (unsigned char )bits;
#line 461
  return ((void *)db);
}
}
#line 464 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static void *bsd_comp_alloc(unsigned char *options , int opt_len ) 
{ void *tmp ;

  {
  {
#line 466
  tmp = bsd_alloc(options, opt_len, 0);
  }
#line 466
  return (tmp);
}
}
#line 469 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static void *bsd_decomp_alloc(unsigned char *options , int opt_len ) 
{ void *tmp ;

  {
  {
#line 471
  tmp = bsd_alloc(options, opt_len, 1);
  }
#line 471
  return (tmp);
}
}
#line 478 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static int bsd_init(void *state , unsigned char *options , int opt_len , int unit ,
                    int debug , int decomp ) 
{ struct bsd_db *db ;
  int indx ;
  int tmp ;
  int tmp___0 ;
  unsigned char __cil_tmp11 ;
  unsigned int __cil_tmp12 ;
  unsigned char *__cil_tmp13 ;
  unsigned char __cil_tmp14 ;
  unsigned int __cil_tmp15 ;
  unsigned char *__cil_tmp16 ;
  unsigned char __cil_tmp17 ;
  int __cil_tmp18 ;
  int __cil_tmp19 ;
  unsigned int __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned char __cil_tmp23 ;
  int __cil_tmp24 ;
  unsigned char *__cil_tmp25 ;
  unsigned char __cil_tmp26 ;
  int __cil_tmp27 ;
  int __cil_tmp28 ;
  unsigned short *__cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned short *__cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned short *__cil_tmp38 ;
  unsigned short *__cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned int __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  struct bsd_dict *__cil_tmp46 ;
  struct bsd_dict *__cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  struct bsd_dict *__cil_tmp53 ;
  struct bsd_dict *__cil_tmp54 ;
  unsigned long __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 ;
  unsigned long __cil_tmp62 ;
  void *__cil_tmp63 ;

  {
#line 481
  db = (struct bsd_db *)state;
#line 484
  if (opt_len != 3) {
#line 489
    return (0);
  } else {
    {
#line 484
    __cil_tmp11 = *options;
#line 484
    __cil_tmp12 = (unsigned int )__cil_tmp11;
#line 484
    if (__cil_tmp12 != 21U) {
#line 489
      return (0);
    } else {
      {
#line 484
      __cil_tmp13 = options + 1UL;
#line 484
      __cil_tmp14 = *__cil_tmp13;
#line 484
      __cil_tmp15 = (unsigned int )__cil_tmp14;
#line 484
      if (__cil_tmp15 != 3U) {
#line 489
        return (0);
      } else {
        {
#line 484
        __cil_tmp16 = options + 2UL;
#line 484
        __cil_tmp17 = *__cil_tmp16;
#line 484
        __cil_tmp18 = (int )__cil_tmp17;
#line 484
        __cil_tmp19 = __cil_tmp18 >> 5;
#line 484
        __cil_tmp20 = (unsigned int )__cil_tmp19;
#line 484
        if (__cil_tmp20 != 1U) {
#line 489
          return (0);
        } else {
          {
#line 484
          __cil_tmp21 = (unsigned long )db;
#line 484
          __cil_tmp22 = __cil_tmp21 + 10;
#line 484
          __cil_tmp23 = *((unsigned char *)__cil_tmp22);
#line 484
          __cil_tmp24 = (int )__cil_tmp23;
#line 484
          __cil_tmp25 = options + 2UL;
#line 484
          __cil_tmp26 = *__cil_tmp25;
#line 484
          __cil_tmp27 = (int )__cil_tmp26;
#line 484
          __cil_tmp28 = __cil_tmp27 & 31;
#line 484
          if (__cil_tmp28 != __cil_tmp24) {
#line 489
            return (0);
          } else
#line 484
          if (decomp != 0) {
            {
#line 484
            __cil_tmp29 = (unsigned short *)0;
#line 484
            __cil_tmp30 = (unsigned long )__cil_tmp29;
#line 484
            __cil_tmp31 = (unsigned long )db;
#line 484
            __cil_tmp32 = __cil_tmp31 + 72;
#line 484
            __cil_tmp33 = *((unsigned short **)__cil_tmp32);
#line 484
            __cil_tmp34 = (unsigned long )__cil_tmp33;
#line 484
            if (__cil_tmp34 == __cil_tmp30) {
#line 489
              return (0);
            } else {

            }
            }
          } else {

          }
          }
        }
        }
      }
      }
    }
    }
  }
#line 492
  if (decomp != 0) {
#line 494
    indx = 255;
    ldv_14429: 
#line 497
    __cil_tmp35 = (unsigned long )indx;
#line 497
    __cil_tmp36 = (unsigned long )db;
#line 497
    __cil_tmp37 = __cil_tmp36 + 72;
#line 497
    __cil_tmp38 = *((unsigned short **)__cil_tmp37);
#line 497
    __cil_tmp39 = __cil_tmp38 + __cil_tmp35;
#line 497
    *__cil_tmp39 = (unsigned short)1;
#line 499
    tmp = indx;
#line 499
    indx = indx - 1;
#line 499
    if (tmp > 0) {
#line 500
      goto ldv_14429;
    } else {
#line 502
      goto ldv_14430;
    }
    ldv_14430: ;
  } else {

  }
#line 502
  __cil_tmp40 = (unsigned long )db;
#line 502
  __cil_tmp41 = __cil_tmp40 + 4;
#line 502
  __cil_tmp42 = *((unsigned int *)__cil_tmp41);
#line 502
  indx = (int )__cil_tmp42;
#line 503
  goto ldv_14432;
  ldv_14431: 
#line 505
  __cil_tmp43 = (unsigned long )indx;
#line 505
  __cil_tmp44 = (unsigned long )db;
#line 505
  __cil_tmp45 = __cil_tmp44 + 80;
#line 505
  __cil_tmp46 = *((struct bsd_dict **)__cil_tmp45);
#line 505
  __cil_tmp47 = __cil_tmp46 + __cil_tmp43;
#line 505
  __cil_tmp48 = (unsigned long )__cil_tmp47;
#line 505
  __cil_tmp49 = __cil_tmp48 + 8;
#line 505
  *((unsigned short *)__cil_tmp49) = (unsigned short)32767;
#line 506
  __cil_tmp50 = (unsigned long )indx;
#line 506
  __cil_tmp51 = (unsigned long )db;
#line 506
  __cil_tmp52 = __cil_tmp51 + 80;
#line 506
  __cil_tmp53 = *((struct bsd_dict **)__cil_tmp52);
#line 506
  __cil_tmp54 = __cil_tmp53 + __cil_tmp50;
#line 506
  __cil_tmp55 = (unsigned long )__cil_tmp54;
#line 506
  __cil_tmp56 = __cil_tmp55 + 10;
#line 506
  *((unsigned short *)__cil_tmp56) = (unsigned short)0;
  ldv_14432: 
#line 503
  tmp___0 = indx;
#line 503
  indx = indx - 1;
#line 503
  if (tmp___0 != 0) {
#line 504
    goto ldv_14431;
  } else {
#line 506
    goto ldv_14433;
  }
  ldv_14433: 
#line 509
  __cil_tmp57 = (unsigned long )db;
#line 509
  __cil_tmp58 = __cil_tmp57 + 12;
#line 509
  *((unsigned char *)__cil_tmp58) = (unsigned char )unit;
#line 510
  __cil_tmp59 = (unsigned long )db;
#line 510
  __cil_tmp60 = __cil_tmp59 + 16;
#line 510
  *((unsigned int *)__cil_tmp60) = 0U;
#line 512
  if (debug != 0) {
#line 514
    __cil_tmp61 = (unsigned long )db;
#line 514
    __cil_tmp62 = __cil_tmp61 + 11;
#line 514
    *((unsigned char *)__cil_tmp62) = (unsigned char)1;
  } else {

  }
  {
#line 516
  __cil_tmp63 = (void *)db;
#line 516
  bsd_reset(__cil_tmp63);
  }
#line 518
  return (1);
}
}
#line 521 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static int bsd_comp_init(void *state , unsigned char *options , int opt_len , int unit ,
                         int opthdr , int debug ) 
{ int tmp ;

  {
  {
#line 524
  tmp = bsd_init(state, options, opt_len, unit, debug, 0);
  }
#line 524
  return (tmp);
}
}
#line 527 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static int bsd_decomp_init(void *state , unsigned char *options , int opt_len , int unit ,
                           int opthdr , int mru , int debug ) 
{ int tmp ;

  {
  {
#line 531
  tmp = bsd_init(state, options, opt_len, unit, debug, 1);
  }
#line 531
  return (tmp);
}
}
#line 578 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static int bsd_compress(void *state , unsigned char *rptr , unsigned char *obuf ,
                        int isize , int osize ) 
{ struct bsd_db *db ;
  int hshift ;
  unsigned int max_ent ;
  unsigned int n_bits ;
  unsigned int bitno ;
  unsigned long accm ;
  int ent ;
  unsigned long fcode ;
  struct bsd_dict *dictp ;
  unsigned char c ;
  int hval ;
  int disp ;
  int ilen ;
  int mxcode ;
  unsigned char *wptr ;
  int olen ;
  unsigned char *tmp ;
  unsigned char *tmp___0 ;
  unsigned char *tmp___1 ;
  unsigned char *tmp___2 ;
  unsigned char *tmp___3 ;
  unsigned char *tmp___4 ;
  unsigned char *tmp___5 ;
  unsigned char *tmp___6 ;
  struct bsd_dict *dictp2 ;
  struct bsd_dict *dictp3 ;
  int indx ;
  unsigned short *len1 ;
  unsigned short *len2 ;
  unsigned char *tmp___7 ;
  unsigned char *tmp___8 ;
  int tmp___9 ;
  unsigned char *tmp___10 ;
  __u8 *__cil_tmp39 ;
  __u8 __cil_tmp40 ;
  int __cil_tmp41 ;
  __u8 *__cil_tmp42 ;
  __u8 __cil_tmp43 ;
  int __cil_tmp44 ;
  int __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned char __cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned char __cil_tmp53 ;
  int __cil_tmp54 ;
  int __cil_tmp55 ;
  unsigned char *__cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  __u8 *__cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned short __cil_tmp62 ;
  int __cil_tmp63 ;
  int __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned short __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  unsigned long __cil_tmp69 ;
  unsigned long __cil_tmp70 ;
  unsigned int __cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  unsigned int __cil_tmp74 ;
  unsigned int __cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  struct bsd_dict *__cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  unsigned long __cil_tmp81 ;
  unsigned short __cil_tmp82 ;
  unsigned int __cil_tmp83 ;
  unsigned long __cil_tmp84 ;
  unsigned long __cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  unsigned short __cil_tmp87 ;
  int __cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  unsigned long __cil_tmp90 ;
  unsigned int __cil_tmp91 ;
  unsigned int __cil_tmp92 ;
  unsigned long __cil_tmp93 ;
  unsigned long __cil_tmp94 ;
  unsigned int __cil_tmp95 ;
  unsigned int __cil_tmp96 ;
  unsigned int __cil_tmp97 ;
  unsigned long __cil_tmp98 ;
  unsigned long __cil_tmp99 ;
  unsigned long __cil_tmp100 ;
  struct bsd_dict *__cil_tmp101 ;
  unsigned long __cil_tmp102 ;
  unsigned long __cil_tmp103 ;
  unsigned short __cil_tmp104 ;
  unsigned int __cil_tmp105 ;
  unsigned long __cil_tmp106 ;
  unsigned long __cil_tmp107 ;
  unsigned long __cil_tmp108 ;
  unsigned short __cil_tmp109 ;
  int __cil_tmp110 ;
  int __cil_tmp111 ;
  int __cil_tmp112 ;
  unsigned long __cil_tmp113 ;
  unsigned char *__cil_tmp114 ;
  unsigned long __cil_tmp115 ;
  unsigned long __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  unsigned long __cil_tmp119 ;
  unsigned int __cil_tmp120 ;
  unsigned int __cil_tmp121 ;
  unsigned long __cil_tmp122 ;
  unsigned long __cil_tmp123 ;
  int __cil_tmp124 ;
  int __cil_tmp125 ;
  unsigned int __cil_tmp126 ;
  unsigned long __cil_tmp127 ;
  unsigned long __cil_tmp128 ;
  unsigned long __cil_tmp129 ;
  struct bsd_dict *__cil_tmp130 ;
  unsigned long __cil_tmp131 ;
  unsigned long __cil_tmp132 ;
  unsigned short __cil_tmp133 ;
  unsigned long __cil_tmp134 ;
  unsigned long __cil_tmp135 ;
  unsigned long __cil_tmp136 ;
  struct bsd_dict *__cil_tmp137 ;
  unsigned long __cil_tmp138 ;
  unsigned long __cil_tmp139 ;
  unsigned short __cil_tmp140 ;
  unsigned int __cil_tmp141 ;
  unsigned long __cil_tmp142 ;
  unsigned long __cil_tmp143 ;
  unsigned long __cil_tmp144 ;
  unsigned long __cil_tmp145 ;
  unsigned long __cil_tmp146 ;
  unsigned long __cil_tmp147 ;
  unsigned long __cil_tmp148 ;
  unsigned long __cil_tmp149 ;
  unsigned short *__cil_tmp150 ;
  unsigned long __cil_tmp151 ;
  unsigned long __cil_tmp152 ;
  unsigned long __cil_tmp153 ;
  unsigned short *__cil_tmp154 ;
  unsigned long __cil_tmp155 ;
  unsigned long __cil_tmp156 ;
  unsigned long __cil_tmp157 ;
  unsigned long __cil_tmp158 ;
  unsigned short *__cil_tmp159 ;
  unsigned long __cil_tmp160 ;
  unsigned long __cil_tmp161 ;
  unsigned long __cil_tmp162 ;
  unsigned short *__cil_tmp163 ;
  unsigned short __cil_tmp164 ;
  unsigned int __cil_tmp165 ;
  unsigned int __cil_tmp166 ;
  int __cil_tmp167 ;
  int __cil_tmp168 ;
  unsigned long __cil_tmp169 ;
  unsigned char *__cil_tmp170 ;
  unsigned long __cil_tmp171 ;
  unsigned long __cil_tmp172 ;
  unsigned long __cil_tmp173 ;
  unsigned long __cil_tmp174 ;
  unsigned long __cil_tmp175 ;
  unsigned int __cil_tmp176 ;
  unsigned long __cil_tmp177 ;
  unsigned long __cil_tmp178 ;
  unsigned int __cil_tmp179 ;
  unsigned int __cil_tmp180 ;
  unsigned long __cil_tmp181 ;
  unsigned long __cil_tmp182 ;
  unsigned int __cil_tmp183 ;
  unsigned long __cil_tmp184 ;
  unsigned long __cil_tmp185 ;
  unsigned int __cil_tmp186 ;
  unsigned long __cil_tmp187 ;
  unsigned long __cil_tmp188 ;
  unsigned int __cil_tmp189 ;
  unsigned long __cil_tmp190 ;
  unsigned long __cil_tmp191 ;
  unsigned int __cil_tmp192 ;
  unsigned long __cil_tmp193 ;
  unsigned long __cil_tmp194 ;
  unsigned long __cil_tmp195 ;
  unsigned long __cil_tmp196 ;
  unsigned int __cil_tmp197 ;
  unsigned long __cil_tmp198 ;
  unsigned long __cil_tmp199 ;
  unsigned long __cil_tmp200 ;
  unsigned long __cil_tmp201 ;
  unsigned short __cil_tmp202 ;
  int __cil_tmp203 ;
  int __cil_tmp204 ;
  unsigned long __cil_tmp205 ;
  unsigned long __cil_tmp206 ;
  unsigned long __cil_tmp207 ;
  unsigned long __cil_tmp208 ;
  unsigned int __cil_tmp209 ;
  int __cil_tmp210 ;
  int __cil_tmp211 ;
  unsigned long __cil_tmp212 ;
  unsigned char *__cil_tmp213 ;
  unsigned long __cil_tmp214 ;
  unsigned long __cil_tmp215 ;
  unsigned long __cil_tmp216 ;
  unsigned char *__cil_tmp217 ;
  unsigned long __cil_tmp218 ;
  unsigned long __cil_tmp219 ;
  unsigned int __cil_tmp220 ;
  int __cil_tmp221 ;
  int __cil_tmp222 ;
  unsigned long __cil_tmp223 ;
  unsigned long __cil_tmp224 ;
  unsigned long __cil_tmp225 ;
  unsigned int __cil_tmp226 ;
  unsigned long __cil_tmp227 ;
  unsigned long __cil_tmp228 ;
  unsigned int __cil_tmp229 ;
  unsigned long __cil_tmp230 ;
  unsigned long __cil_tmp231 ;
  unsigned long __cil_tmp232 ;
  unsigned long __cil_tmp233 ;
  unsigned char __cil_tmp234 ;
  int __cil_tmp235 ;
  int __cil_tmp236 ;
  unsigned char *__cil_tmp237 ;
  unsigned long __cil_tmp238 ;
  unsigned long __cil_tmp239 ;
  unsigned long __cil_tmp240 ;
  unsigned long __cil_tmp241 ;
  unsigned long __cil_tmp242 ;
  unsigned long __cil_tmp243 ;
  unsigned int __cil_tmp244 ;
  unsigned long __cil_tmp245 ;
  unsigned long __cil_tmp246 ;
  unsigned int __cil_tmp247 ;
  unsigned long __cil_tmp248 ;
  unsigned long __cil_tmp249 ;
  unsigned int __cil_tmp250 ;
  unsigned long __cil_tmp251 ;
  unsigned long __cil_tmp252 ;
  unsigned long __cil_tmp253 ;
  unsigned long __cil_tmp254 ;
  unsigned int __cil_tmp255 ;
  unsigned long __cil_tmp256 ;
  unsigned long __cil_tmp257 ;
  unsigned int __cil_tmp258 ;
  unsigned long __cil_tmp259 ;
  unsigned long __cil_tmp260 ;
  unsigned int __cil_tmp261 ;

  {
#line 630
  __cil_tmp39 = rptr + 3UL;
#line 630
  __cil_tmp40 = *__cil_tmp39;
#line 630
  __cil_tmp41 = (int )__cil_tmp40;
#line 630
  __cil_tmp42 = rptr + 2UL;
#line 630
  __cil_tmp43 = *__cil_tmp42;
#line 630
  __cil_tmp44 = (int )__cil_tmp43;
#line 630
  __cil_tmp45 = __cil_tmp44 << 8;
#line 630
  ent = __cil_tmp45 + __cil_tmp41;
#line 631
  if (ent <= 32) {
#line 633
    return (0);
  } else
#line 631
  if (ent > 249) {
#line 633
    return (0);
  } else {

  }
#line 636
  db = (struct bsd_db *)state;
#line 637
  __cil_tmp46 = (unsigned long )db;
#line 637
  __cil_tmp47 = __cil_tmp46 + 8;
#line 637
  __cil_tmp48 = *((unsigned char *)__cil_tmp47);
#line 637
  hshift = (int )__cil_tmp48;
#line 638
  __cil_tmp49 = (unsigned long )db;
#line 638
  __cil_tmp50 = __cil_tmp49 + 24;
#line 638
  max_ent = *((unsigned int *)__cil_tmp50);
#line 639
  __cil_tmp51 = (unsigned long )db;
#line 639
  __cil_tmp52 = __cil_tmp51 + 9;
#line 639
  __cil_tmp53 = *((unsigned char *)__cil_tmp52);
#line 639
  n_bits = (unsigned int )__cil_tmp53;
#line 640
  bitno = 32U;
#line 641
  accm = 0UL;
#line 642
  __cil_tmp54 = (int )n_bits;
#line 642
  __cil_tmp55 = 1 << __cil_tmp54;
#line 642
  mxcode = __cil_tmp55 + -1;
#line 645
  wptr = obuf;
#line 646
  olen = 6;
#line 648
  if (osize > isize) {
#line 650
    osize = isize;
  } else {

  }
  {
#line 654
  __cil_tmp56 = (unsigned char *)0;
#line 654
  __cil_tmp57 = (unsigned long )__cil_tmp56;
#line 654
  __cil_tmp58 = (unsigned long )wptr;
#line 654
  if (__cil_tmp58 != __cil_tmp57) {
#line 656
    tmp = wptr;
#line 656
    wptr = wptr + 1;
#line 656
    *tmp = *rptr;
#line 657
    tmp___0 = wptr;
#line 657
    wptr = wptr + 1;
#line 657
    __cil_tmp59 = rptr + 1UL;
#line 657
    *tmp___0 = *__cil_tmp59;
#line 658
    tmp___1 = wptr;
#line 658
    wptr = wptr + 1;
#line 658
    *tmp___1 = (unsigned char)0;
#line 659
    tmp___2 = wptr;
#line 659
    wptr = wptr + 1;
#line 659
    *tmp___2 = (unsigned char)253;
#line 660
    tmp___3 = wptr;
#line 660
    wptr = wptr + 1;
#line 660
    __cil_tmp60 = (unsigned long )db;
#line 660
    __cil_tmp61 = __cil_tmp60 + 14;
#line 660
    __cil_tmp62 = *((unsigned short *)__cil_tmp61);
#line 660
    __cil_tmp63 = (int )__cil_tmp62;
#line 660
    __cil_tmp64 = __cil_tmp63 >> 8;
#line 660
    *tmp___3 = (unsigned char )__cil_tmp64;
#line 661
    tmp___4 = wptr;
#line 661
    wptr = wptr + 1;
#line 661
    __cil_tmp65 = (unsigned long )db;
#line 661
    __cil_tmp66 = __cil_tmp65 + 14;
#line 661
    __cil_tmp67 = *((unsigned short *)__cil_tmp66);
#line 661
    *tmp___4 = (unsigned char )__cil_tmp67;
  } else {

  }
  }
#line 665
  rptr = rptr + 4UL;
#line 666
  isize = isize + -4;
#line 667
  isize = isize + 1;
#line 667
  ilen = isize;
#line 669
  goto ldv_14475;
  ldv_14485: 
#line 671
  tmp___5 = rptr;
#line 671
  rptr = rptr + 1;
#line 671
  c = *tmp___5;
#line 672
  __cil_tmp68 = (unsigned long )ent;
#line 672
  __cil_tmp69 = (unsigned long )c;
#line 672
  __cil_tmp70 = __cil_tmp69 << 16;
#line 672
  fcode = __cil_tmp70 + __cil_tmp68;
#line 673
  __cil_tmp71 = (unsigned int )ent;
#line 673
  __cil_tmp72 = (unsigned long )c;
#line 673
  __cil_tmp73 = __cil_tmp72 << hshift;
#line 673
  __cil_tmp74 = (unsigned int )__cil_tmp73;
#line 673
  __cil_tmp75 = __cil_tmp74 ^ __cil_tmp71;
#line 673
  hval = (int )__cil_tmp75;
#line 674
  __cil_tmp76 = (unsigned long )hval;
#line 674
  __cil_tmp77 = (unsigned long )db;
#line 674
  __cil_tmp78 = __cil_tmp77 + 80;
#line 674
  __cil_tmp79 = *((struct bsd_dict **)__cil_tmp78);
#line 674
  dictp = __cil_tmp79 + __cil_tmp76;
  {
#line 677
  __cil_tmp80 = (unsigned long )dictp;
#line 677
  __cil_tmp81 = __cil_tmp80 + 8;
#line 677
  __cil_tmp82 = *((unsigned short *)__cil_tmp81);
#line 677
  __cil_tmp83 = (unsigned int )__cil_tmp82;
#line 677
  if (__cil_tmp83 >= max_ent) {
#line 679
    goto nomatch;
  } else {

  }
  }
  {
#line 682
  __cil_tmp84 = *((unsigned long *)dictp);
#line 682
  if (__cil_tmp84 == fcode) {
#line 684
    __cil_tmp85 = (unsigned long )dictp;
#line 684
    __cil_tmp86 = __cil_tmp85 + 8;
#line 684
    __cil_tmp87 = *((unsigned short *)__cil_tmp86);
#line 684
    __cil_tmp88 = (int )__cil_tmp87;
#line 684
    ent = __cil_tmp88 + 1;
#line 685
    goto ldv_14475;
  } else {

  }
  }
#line 689
  if (hval != 0) {
#line 689
    disp = hval;
  } else {
#line 689
    disp = 1;
  }
  ldv_14476: 
#line 693
  hval = hval + disp;
  {
#line 694
  __cil_tmp89 = (unsigned long )db;
#line 694
  __cil_tmp90 = __cil_tmp89 + 4;
#line 694
  __cil_tmp91 = *((unsigned int *)__cil_tmp90);
#line 694
  __cil_tmp92 = (unsigned int )hval;
#line 694
  if (__cil_tmp92 >= __cil_tmp91) {
#line 696
    __cil_tmp93 = (unsigned long )db;
#line 696
    __cil_tmp94 = __cil_tmp93 + 4;
#line 696
    __cil_tmp95 = *((unsigned int *)__cil_tmp94);
#line 696
    __cil_tmp96 = (unsigned int )hval;
#line 696
    __cil_tmp97 = __cil_tmp96 - __cil_tmp95;
#line 696
    hval = (int )__cil_tmp97;
  } else {

  }
  }
#line 698
  __cil_tmp98 = (unsigned long )hval;
#line 698
  __cil_tmp99 = (unsigned long )db;
#line 698
  __cil_tmp100 = __cil_tmp99 + 80;
#line 698
  __cil_tmp101 = *((struct bsd_dict **)__cil_tmp100);
#line 698
  dictp = __cil_tmp101 + __cil_tmp98;
  {
#line 699
  __cil_tmp102 = (unsigned long )dictp;
#line 699
  __cil_tmp103 = __cil_tmp102 + 8;
#line 699
  __cil_tmp104 = *((unsigned short *)__cil_tmp103);
#line 699
  __cil_tmp105 = (unsigned int )__cil_tmp104;
#line 699
  if (__cil_tmp105 >= max_ent) {
#line 701
    goto nomatch;
  } else {

  }
  }
  {
#line 704
  __cil_tmp106 = *((unsigned long *)dictp);
#line 704
  if (__cil_tmp106 != fcode) {
#line 705
    goto ldv_14476;
  } else {
#line 707
    goto ldv_14477;
  }
  }
  ldv_14477: 
#line 706
  __cil_tmp107 = (unsigned long )dictp;
#line 706
  __cil_tmp108 = __cil_tmp107 + 8;
#line 706
  __cil_tmp109 = *((unsigned short *)__cil_tmp108);
#line 706
  __cil_tmp110 = (int )__cil_tmp109;
#line 706
  ent = __cil_tmp110 + 1;
#line 707
  goto ldv_14475;
  nomatch: 
#line 710
  bitno = bitno - n_bits;
#line 710
  __cil_tmp111 = (int )bitno;
#line 710
  __cil_tmp112 = ent << __cil_tmp111;
#line 710
  __cil_tmp113 = (unsigned long )__cil_tmp112;
#line 710
  accm = __cil_tmp113 | accm;
  ldv_14478: 
#line 710
  olen = olen + 1;
  {
#line 710
  __cil_tmp114 = (unsigned char *)0;
#line 710
  __cil_tmp115 = (unsigned long )__cil_tmp114;
#line 710
  __cil_tmp116 = (unsigned long )wptr;
#line 710
  if (__cil_tmp116 != __cil_tmp115) {
#line 710
    tmp___6 = wptr;
#line 710
    wptr = wptr + 1;
#line 710
    __cil_tmp117 = accm >> 24;
#line 710
    *tmp___6 = (unsigned char )__cil_tmp117;
#line 710
    if (olen >= osize) {
#line 710
      wptr = (unsigned char *)0;
    } else {

    }
  } else {

  }
  }
#line 710
  accm = accm << 8;
#line 710
  bitno = bitno + 8U;
#line 710
  if (bitno <= 24U) {
#line 711
    goto ldv_14478;
  } else {
#line 713
    goto ldv_14479;
  }
  ldv_14479: ;
  {
#line 713
  __cil_tmp118 = (unsigned long )db;
#line 713
  __cil_tmp119 = __cil_tmp118 + 20;
#line 713
  __cil_tmp120 = *((unsigned int *)__cil_tmp119);
#line 713
  if (__cil_tmp120 > max_ent) {
    {
#line 720
    __cil_tmp121 = (unsigned int )mxcode;
#line 720
    if (__cil_tmp121 <= max_ent) {
#line 722
      n_bits = n_bits + 1U;
#line 722
      __cil_tmp122 = (unsigned long )db;
#line 722
      __cil_tmp123 = __cil_tmp122 + 9;
#line 722
      *((unsigned char *)__cil_tmp123) = (unsigned char )n_bits;
#line 723
      __cil_tmp124 = (int )n_bits;
#line 723
      __cil_tmp125 = 1 << __cil_tmp124;
#line 723
      mxcode = __cil_tmp125 + -1;
    } else {

    }
    }
#line 730
    __cil_tmp126 = max_ent + 1U;
#line 730
    __cil_tmp127 = (unsigned long )__cil_tmp126;
#line 730
    __cil_tmp128 = (unsigned long )db;
#line 730
    __cil_tmp129 = __cil_tmp128 + 80;
#line 730
    __cil_tmp130 = *((struct bsd_dict **)__cil_tmp129);
#line 730
    dictp2 = __cil_tmp130 + __cil_tmp127;
#line 731
    __cil_tmp131 = (unsigned long )dictp2;
#line 731
    __cil_tmp132 = __cil_tmp131 + 10;
#line 731
    __cil_tmp133 = *((unsigned short *)__cil_tmp132);
#line 731
    indx = (int )__cil_tmp133;
#line 732
    __cil_tmp134 = (unsigned long )indx;
#line 732
    __cil_tmp135 = (unsigned long )db;
#line 732
    __cil_tmp136 = __cil_tmp135 + 80;
#line 732
    __cil_tmp137 = *((struct bsd_dict **)__cil_tmp136);
#line 732
    dictp3 = __cil_tmp137 + __cil_tmp134;
    {
#line 734
    __cil_tmp138 = (unsigned long )dictp3;
#line 734
    __cil_tmp139 = __cil_tmp138 + 8;
#line 734
    __cil_tmp140 = *((unsigned short *)__cil_tmp139);
#line 734
    __cil_tmp141 = (unsigned int )__cil_tmp140;
#line 734
    if (__cil_tmp141 == max_ent) {
#line 736
      __cil_tmp142 = (unsigned long )dictp3;
#line 736
      __cil_tmp143 = __cil_tmp142 + 8;
#line 736
      *((unsigned short *)__cil_tmp143) = (unsigned short)32767;
    } else {

    }
    }
#line 739
    __cil_tmp144 = (unsigned long )dictp2;
#line 739
    __cil_tmp145 = __cil_tmp144 + 10;
#line 739
    *((unsigned short *)__cil_tmp145) = (unsigned short )hval;
#line 740
    __cil_tmp146 = (unsigned long )dictp;
#line 740
    __cil_tmp147 = __cil_tmp146 + 8;
#line 740
    *((unsigned short *)__cil_tmp147) = (unsigned short )max_ent;
#line 741
    *((unsigned long *)dictp) = fcode;
#line 742
    max_ent = max_ent + 1U;
#line 742
    __cil_tmp148 = (unsigned long )db;
#line 742
    __cil_tmp149 = __cil_tmp148 + 24;
#line 742
    *((unsigned int *)__cil_tmp149) = max_ent;
    {
#line 744
    __cil_tmp150 = (unsigned short *)0;
#line 744
    __cil_tmp151 = (unsigned long )__cil_tmp150;
#line 744
    __cil_tmp152 = (unsigned long )db;
#line 744
    __cil_tmp153 = __cil_tmp152 + 72;
#line 744
    __cil_tmp154 = *((unsigned short **)__cil_tmp153);
#line 744
    __cil_tmp155 = (unsigned long )__cil_tmp154;
#line 744
    if (__cil_tmp155 != __cil_tmp151) {
#line 746
      __cil_tmp156 = (unsigned long )max_ent;
#line 746
      __cil_tmp157 = (unsigned long )db;
#line 746
      __cil_tmp158 = __cil_tmp157 + 72;
#line 746
      __cil_tmp159 = *((unsigned short **)__cil_tmp158);
#line 746
      len1 = __cil_tmp159 + __cil_tmp156;
#line 747
      __cil_tmp160 = (unsigned long )ent;
#line 747
      __cil_tmp161 = (unsigned long )db;
#line 747
      __cil_tmp162 = __cil_tmp161 + 72;
#line 747
      __cil_tmp163 = *((unsigned short **)__cil_tmp162);
#line 747
      len2 = __cil_tmp163 + __cil_tmp160;
#line 748
      __cil_tmp164 = *len2;
#line 748
      __cil_tmp165 = (unsigned int )__cil_tmp164;
#line 748
      __cil_tmp166 = __cil_tmp165 + 1U;
#line 748
      *len1 = (unsigned short )__cil_tmp166;
    } else {

    }
    }
  } else {

  }
  }
#line 751
  ent = (int )c;
  ldv_14475: 
#line 669
  ilen = ilen - 1;
#line 669
  if (ilen > 0) {
#line 670
    goto ldv_14485;
  } else {
#line 672
    goto ldv_14486;
  }
  ldv_14486: 
#line 754
  bitno = bitno - n_bits;
#line 754
  __cil_tmp167 = (int )bitno;
#line 754
  __cil_tmp168 = ent << __cil_tmp167;
#line 754
  __cil_tmp169 = (unsigned long )__cil_tmp168;
#line 754
  accm = __cil_tmp169 | accm;
  ldv_14487: 
#line 754
  olen = olen + 1;
  {
#line 754
  __cil_tmp170 = (unsigned char *)0;
#line 754
  __cil_tmp171 = (unsigned long )__cil_tmp170;
#line 754
  __cil_tmp172 = (unsigned long )wptr;
#line 754
  if (__cil_tmp172 != __cil_tmp171) {
#line 754
    tmp___7 = wptr;
#line 754
    wptr = wptr + 1;
#line 754
    __cil_tmp173 = accm >> 24;
#line 754
    *tmp___7 = (unsigned char )__cil_tmp173;
#line 754
    if (olen >= osize) {
#line 754
      wptr = (unsigned char *)0;
    } else {

    }
  } else {

  }
  }
#line 754
  accm = accm << 8;
#line 754
  bitno = bitno + 8U;
#line 754
  if (bitno <= 24U) {
#line 755
    goto ldv_14487;
  } else {
#line 757
    goto ldv_14488;
  }
  ldv_14488: 
#line 756
  __cil_tmp174 = (unsigned long )db;
#line 756
  __cil_tmp175 = __cil_tmp174 + 32;
#line 756
  __cil_tmp176 = (unsigned int )olen;
#line 756
  __cil_tmp177 = (unsigned long )db;
#line 756
  __cil_tmp178 = __cil_tmp177 + 32;
#line 756
  __cil_tmp179 = *((unsigned int *)__cil_tmp178);
#line 756
  __cil_tmp180 = __cil_tmp179 + __cil_tmp176;
#line 756
  *((unsigned int *)__cil_tmp175) = __cil_tmp180 + 4294967290U;
#line 757
  __cil_tmp181 = (unsigned long )db;
#line 757
  __cil_tmp182 = __cil_tmp181 + 60;
#line 757
  __cil_tmp183 = (unsigned int )isize;
#line 757
  __cil_tmp184 = (unsigned long )db;
#line 757
  __cil_tmp185 = __cil_tmp184 + 60;
#line 757
  __cil_tmp186 = *((unsigned int *)__cil_tmp185);
#line 757
  *((unsigned int *)__cil_tmp182) = __cil_tmp186 + __cil_tmp183;
#line 758
  __cil_tmp187 = (unsigned long )db;
#line 758
  __cil_tmp188 = __cil_tmp187 + 28;
#line 758
  __cil_tmp189 = (unsigned int )isize;
#line 758
  __cil_tmp190 = (unsigned long )db;
#line 758
  __cil_tmp191 = __cil_tmp190 + 28;
#line 758
  __cil_tmp192 = *((unsigned int *)__cil_tmp191);
#line 758
  *((unsigned int *)__cil_tmp188) = __cil_tmp192 + __cil_tmp189;
#line 759
  __cil_tmp193 = (unsigned long )db;
#line 759
  __cil_tmp194 = __cil_tmp193 + 56;
#line 759
  __cil_tmp195 = (unsigned long )db;
#line 759
  __cil_tmp196 = __cil_tmp195 + 56;
#line 759
  __cil_tmp197 = *((unsigned int *)__cil_tmp196);
#line 759
  *((unsigned int *)__cil_tmp194) = __cil_tmp197 + 1U;
#line 760
  __cil_tmp198 = (unsigned long )db;
#line 760
  __cil_tmp199 = __cil_tmp198 + 14;
#line 760
  __cil_tmp200 = (unsigned long )db;
#line 760
  __cil_tmp201 = __cil_tmp200 + 14;
#line 760
  __cil_tmp202 = *((unsigned short *)__cil_tmp201);
#line 760
  __cil_tmp203 = (int )__cil_tmp202;
#line 760
  __cil_tmp204 = __cil_tmp203 + 1;
#line 760
  *((unsigned short *)__cil_tmp199) = (unsigned short )__cil_tmp204;
#line 762
  if (bitno <= 31U) {
#line 764
    __cil_tmp205 = (unsigned long )db;
#line 764
    __cil_tmp206 = __cil_tmp205 + 32;
#line 764
    __cil_tmp207 = (unsigned long )db;
#line 764
    __cil_tmp208 = __cil_tmp207 + 32;
#line 764
    __cil_tmp209 = *((unsigned int *)__cil_tmp208);
#line 764
    *((unsigned int *)__cil_tmp206) = __cil_tmp209 + 1U;
  } else {

  }
  {
#line 771
  tmp___9 = bsd_check(db);
  }
#line 771
  if (tmp___9 != 0) {
#line 773
    bitno = bitno - n_bits;
#line 773
    __cil_tmp210 = (int )bitno;
#line 773
    __cil_tmp211 = 256 << __cil_tmp210;
#line 773
    __cil_tmp212 = (unsigned long )__cil_tmp211;
#line 773
    accm = __cil_tmp212 | accm;
    ldv_14489: 
#line 773
    olen = olen + 1;
    {
#line 773
    __cil_tmp213 = (unsigned char *)0;
#line 773
    __cil_tmp214 = (unsigned long )__cil_tmp213;
#line 773
    __cil_tmp215 = (unsigned long )wptr;
#line 773
    if (__cil_tmp215 != __cil_tmp214) {
#line 773
      tmp___8 = wptr;
#line 773
      wptr = wptr + 1;
#line 773
      __cil_tmp216 = accm >> 24;
#line 773
      *tmp___8 = (unsigned char )__cil_tmp216;
#line 773
      if (olen >= osize) {
#line 773
        wptr = (unsigned char *)0;
      } else {

      }
    } else {

    }
    }
#line 773
    accm = accm << 8;
#line 773
    bitno = bitno + 8U;
#line 773
    if (bitno <= 24U) {
#line 774
      goto ldv_14489;
    } else {
#line 776
      goto ldv_14490;
    }
    ldv_14490: ;
  } else {

  }
#line 781
  if (bitno != 32U) {
#line 783
    olen = olen + 1;
    {
#line 783
    __cil_tmp217 = (unsigned char *)0;
#line 783
    __cil_tmp218 = (unsigned long )__cil_tmp217;
#line 783
    __cil_tmp219 = (unsigned long )wptr;
#line 783
    if (__cil_tmp219 != __cil_tmp218) {
#line 783
      tmp___10 = wptr;
#line 783
      wptr = wptr + 1;
#line 783
      __cil_tmp220 = bitno - 8U;
#line 783
      __cil_tmp221 = (int )__cil_tmp220;
#line 783
      __cil_tmp222 = 255 << __cil_tmp221;
#line 783
      __cil_tmp223 = (unsigned long )__cil_tmp222;
#line 783
      __cil_tmp224 = __cil_tmp223 | accm;
#line 783
      __cil_tmp225 = __cil_tmp224 >> 24;
#line 783
      *tmp___10 = (unsigned char )__cil_tmp225;
#line 783
      if (olen >= osize) {
#line 783
        wptr = (unsigned char *)0;
      } else {

      }
    } else {

    }
    }
  } else {

  }
  {
#line 791
  __cil_tmp226 = (unsigned int )mxcode;
#line 791
  if (__cil_tmp226 <= max_ent) {
    {
#line 791
    __cil_tmp227 = (unsigned long )db;
#line 791
    __cil_tmp228 = __cil_tmp227 + 20;
#line 791
    __cil_tmp229 = *((unsigned int *)__cil_tmp228);
#line 791
    if (__cil_tmp229 > max_ent) {
#line 793
      __cil_tmp230 = (unsigned long )db;
#line 793
      __cil_tmp231 = __cil_tmp230 + 9;
#line 793
      __cil_tmp232 = (unsigned long )db;
#line 793
      __cil_tmp233 = __cil_tmp232 + 9;
#line 793
      __cil_tmp234 = *((unsigned char *)__cil_tmp233);
#line 793
      __cil_tmp235 = (int )__cil_tmp234;
#line 793
      __cil_tmp236 = __cil_tmp235 + 1;
#line 793
      *((unsigned char *)__cil_tmp231) = (unsigned char )__cil_tmp236;
    } else {

    }
    }
  } else {

  }
  }
  {
#line 797
  __cil_tmp237 = (unsigned char *)0;
#line 797
  __cil_tmp238 = (unsigned long )__cil_tmp237;
#line 797
  __cil_tmp239 = (unsigned long )wptr;
#line 797
  if (__cil_tmp239 == __cil_tmp238) {
#line 799
    __cil_tmp240 = (unsigned long )db;
#line 799
    __cil_tmp241 = __cil_tmp240 + 48;
#line 799
    __cil_tmp242 = (unsigned long )db;
#line 799
    __cil_tmp243 = __cil_tmp242 + 48;
#line 799
    __cil_tmp244 = *((unsigned int *)__cil_tmp243);
#line 799
    *((unsigned int *)__cil_tmp241) = __cil_tmp244 + 1U;
#line 800
    __cil_tmp245 = (unsigned long )db;
#line 800
    __cil_tmp246 = __cil_tmp245 + 52;
#line 800
    __cil_tmp247 = (unsigned int )isize;
#line 800
    __cil_tmp248 = (unsigned long )db;
#line 800
    __cil_tmp249 = __cil_tmp248 + 52;
#line 800
    __cil_tmp250 = *((unsigned int *)__cil_tmp249);
#line 800
    *((unsigned int *)__cil_tmp246) = __cil_tmp250 + __cil_tmp247;
#line 801
    olen = 0;
  } else {
#line 805
    __cil_tmp251 = (unsigned long )db;
#line 805
    __cil_tmp252 = __cil_tmp251 + 64;
#line 805
    __cil_tmp253 = (unsigned long )db;
#line 805
    __cil_tmp254 = __cil_tmp253 + 64;
#line 805
    __cil_tmp255 = *((unsigned int *)__cil_tmp254);
#line 805
    *((unsigned int *)__cil_tmp252) = __cil_tmp255 + 1U;
#line 806
    __cil_tmp256 = (unsigned long )db;
#line 806
    __cil_tmp257 = __cil_tmp256 + 68;
#line 806
    __cil_tmp258 = (unsigned int )olen;
#line 806
    __cil_tmp259 = (unsigned long )db;
#line 806
    __cil_tmp260 = __cil_tmp259 + 68;
#line 806
    __cil_tmp261 = *((unsigned int *)__cil_tmp260);
#line 806
    *((unsigned int *)__cil_tmp257) = __cil_tmp261 + __cil_tmp258;
  }
  }
#line 810
  return (olen);
}
}
#line 820 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static void bsd_incomp(void *state , unsigned char *ibuf , int icnt ) 
{ unsigned char *__cil_tmp4 ;

  {
  {
#line 822
  __cil_tmp4 = (unsigned char *)0;
#line 822
  bsd_compress(state, ibuf, __cil_tmp4, icnt, 0);
  }
#line 823
  return;
}
}
#line 842 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static int bsd_decompress(void *state , unsigned char *ibuf , int isize , unsigned char *obuf ,
                          int osize ) 
{ struct bsd_db *db ;
  unsigned int max_ent ;
  unsigned long accm ;
  unsigned int bitno ;
  unsigned int n_bits ;
  unsigned int tgtbitno ;
  struct bsd_dict *dictp ;
  int explen ;
  int seq ;
  unsigned int incode ;
  unsigned int oldcode ;
  unsigned int finchar ;
  unsigned char *p ;
  unsigned char *wptr ;
  int adrs ;
  int ctrl ;
  int ilen ;
  int codelen ;
  int extra ;
  unsigned char *tmp ;
  unsigned char *tmp___0 ;
  unsigned char *tmp___1 ;
  int tmp___2 ;
  unsigned char *tmp___3 ;
  struct bsd_dict *dictp2 ;
  unsigned char *tmp___4 ;
  struct bsd_dict *dictp2___0 ;
  struct bsd_dict *dictp3 ;
  unsigned short *lens1 ;
  unsigned short *lens2 ;
  unsigned long fcode ;
  int hval ;
  int disp ;
  int indx ;
  int tmp___5 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned char __cil_tmp45 ;
  unsigned char __cil_tmp46 ;
  __u8 *__cil_tmp47 ;
  __u8 __cil_tmp48 ;
  unsigned char *__cil_tmp49 ;
  unsigned char __cil_tmp50 ;
  int __cil_tmp51 ;
  unsigned char *__cil_tmp52 ;
  unsigned char __cil_tmp53 ;
  int __cil_tmp54 ;
  int __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned short __cil_tmp58 ;
  int __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned char __cil_tmp62 ;
  unsigned int __cil_tmp63 ;
  unsigned long __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  unsigned char __cil_tmp66 ;
  int __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  unsigned long __cil_tmp69 ;
  unsigned short __cil_tmp70 ;
  int __cil_tmp71 ;
  int __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned short __cil_tmp77 ;
  int __cil_tmp78 ;
  int __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  unsigned long __cil_tmp81 ;
  unsigned int __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  unsigned long __cil_tmp84 ;
  unsigned int __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 ;
  unsigned int __cil_tmp92 ;
  int __cil_tmp93 ;
  unsigned char __cil_tmp94 ;
  int __cil_tmp95 ;
  int __cil_tmp96 ;
  unsigned long __cil_tmp97 ;
  int __cil_tmp98 ;
  unsigned long __cil_tmp99 ;
  int __cil_tmp100 ;
  unsigned long __cil_tmp101 ;
  unsigned long __cil_tmp102 ;
  unsigned char __cil_tmp103 ;
  unsigned int __cil_tmp104 ;
  unsigned long __cil_tmp105 ;
  unsigned long __cil_tmp106 ;
  unsigned char __cil_tmp107 ;
  int __cil_tmp108 ;
  unsigned int __cil_tmp109 ;
  unsigned long __cil_tmp110 ;
  unsigned long __cil_tmp111 ;
  unsigned int __cil_tmp112 ;
  unsigned long __cil_tmp113 ;
  unsigned long __cil_tmp114 ;
  unsigned char __cil_tmp115 ;
  unsigned int __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  unsigned char __cil_tmp119 ;
  int __cil_tmp120 ;
  unsigned long __cil_tmp121 ;
  unsigned long __cil_tmp122 ;
  unsigned short __cil_tmp123 ;
  int __cil_tmp124 ;
  unsigned long __cil_tmp125 ;
  unsigned long __cil_tmp126 ;
  unsigned long __cil_tmp127 ;
  unsigned short *__cil_tmp128 ;
  unsigned short *__cil_tmp129 ;
  unsigned short __cil_tmp130 ;
  int __cil_tmp131 ;
  unsigned long __cil_tmp132 ;
  unsigned long __cil_tmp133 ;
  unsigned char __cil_tmp134 ;
  unsigned int __cil_tmp135 ;
  unsigned long __cil_tmp136 ;
  unsigned long __cil_tmp137 ;
  unsigned char __cil_tmp138 ;
  int __cil_tmp139 ;
  unsigned long __cil_tmp140 ;
  unsigned long __cil_tmp141 ;
  unsigned long __cil_tmp142 ;
  unsigned long __cil_tmp143 ;
  struct bsd_dict *__cil_tmp144 ;
  unsigned long __cil_tmp145 ;
  unsigned long __cil_tmp146 ;
  unsigned short __cil_tmp147 ;
  unsigned long __cil_tmp148 ;
  unsigned long __cil_tmp149 ;
  unsigned long __cil_tmp150 ;
  struct bsd_dict *__cil_tmp151 ;
  unsigned long __cil_tmp152 ;
  unsigned long __cil_tmp153 ;
  unsigned long __cil_tmp154 ;
  unsigned long __cil_tmp155 ;
  unsigned short __cil_tmp156 ;
  unsigned long __cil_tmp157 ;
  unsigned long __cil_tmp158 ;
  unsigned int __cil_tmp159 ;
  unsigned long __cil_tmp160 ;
  unsigned long __cil_tmp161 ;
  unsigned long __cil_tmp162 ;
  unsigned long __cil_tmp163 ;
  unsigned long __cil_tmp164 ;
  unsigned char __cil_tmp165 ;
  int __cil_tmp166 ;
  unsigned long __cil_tmp167 ;
  unsigned long __cil_tmp168 ;
  unsigned int __cil_tmp169 ;
  unsigned int __cil_tmp170 ;
  unsigned long __cil_tmp171 ;
  unsigned long __cil_tmp172 ;
  unsigned long __cil_tmp173 ;
  struct bsd_dict *__cil_tmp174 ;
  unsigned long __cil_tmp175 ;
  unsigned long __cil_tmp176 ;
  unsigned short __cil_tmp177 ;
  unsigned int __cil_tmp178 ;
  unsigned long __cil_tmp179 ;
  unsigned long __cil_tmp180 ;
  unsigned int __cil_tmp181 ;
  unsigned int __cil_tmp182 ;
  unsigned long __cil_tmp183 ;
  unsigned long __cil_tmp184 ;
  unsigned int __cil_tmp185 ;
  unsigned int __cil_tmp186 ;
  unsigned int __cil_tmp187 ;
  unsigned long __cil_tmp188 ;
  unsigned long __cil_tmp189 ;
  unsigned long __cil_tmp190 ;
  struct bsd_dict *__cil_tmp191 ;
  unsigned long __cil_tmp192 ;
  unsigned long __cil_tmp193 ;
  unsigned short __cil_tmp194 ;
  unsigned int __cil_tmp195 ;
  unsigned int __cil_tmp196 ;
  unsigned long __cil_tmp197 ;
  unsigned long __cil_tmp198 ;
  unsigned long __cil_tmp199 ;
  struct bsd_dict *__cil_tmp200 ;
  unsigned long __cil_tmp201 ;
  unsigned long __cil_tmp202 ;
  unsigned short __cil_tmp203 ;
  unsigned long __cil_tmp204 ;
  unsigned long __cil_tmp205 ;
  unsigned long __cil_tmp206 ;
  struct bsd_dict *__cil_tmp207 ;
  unsigned long __cil_tmp208 ;
  unsigned long __cil_tmp209 ;
  unsigned short __cil_tmp210 ;
  unsigned int __cil_tmp211 ;
  unsigned long __cil_tmp212 ;
  unsigned long __cil_tmp213 ;
  unsigned long __cil_tmp214 ;
  unsigned long __cil_tmp215 ;
  unsigned long __cil_tmp216 ;
  unsigned long __cil_tmp217 ;
  unsigned long __cil_tmp218 ;
  unsigned long __cil_tmp219 ;
  unsigned long __cil_tmp220 ;
  unsigned long __cil_tmp221 ;
  unsigned long __cil_tmp222 ;
  unsigned short *__cil_tmp223 ;
  unsigned long __cil_tmp224 ;
  unsigned long __cil_tmp225 ;
  unsigned long __cil_tmp226 ;
  unsigned short *__cil_tmp227 ;
  unsigned short __cil_tmp228 ;
  unsigned int __cil_tmp229 ;
  unsigned int __cil_tmp230 ;
  int __cil_tmp231 ;
  int __cil_tmp232 ;
  int __cil_tmp233 ;
  unsigned int __cil_tmp234 ;
  unsigned long __cil_tmp235 ;
  unsigned long __cil_tmp236 ;
  unsigned int __cil_tmp237 ;
  unsigned long __cil_tmp238 ;
  unsigned long __cil_tmp239 ;
  unsigned long __cil_tmp240 ;
  unsigned long __cil_tmp241 ;
  unsigned long __cil_tmp242 ;
  unsigned long __cil_tmp243 ;
  unsigned int __cil_tmp244 ;
  unsigned long __cil_tmp245 ;
  unsigned long __cil_tmp246 ;
  unsigned long __cil_tmp247 ;
  unsigned long __cil_tmp248 ;
  unsigned int __cil_tmp249 ;
  unsigned long __cil_tmp250 ;
  unsigned long __cil_tmp251 ;
  unsigned int __cil_tmp252 ;
  unsigned long __cil_tmp253 ;
  unsigned long __cil_tmp254 ;
  unsigned int __cil_tmp255 ;
  unsigned int __cil_tmp256 ;
  unsigned long __cil_tmp257 ;
  unsigned long __cil_tmp258 ;
  unsigned int __cil_tmp259 ;
  unsigned long __cil_tmp260 ;
  unsigned long __cil_tmp261 ;
  unsigned int __cil_tmp262 ;
  unsigned long __cil_tmp263 ;
  unsigned long __cil_tmp264 ;
  unsigned char __cil_tmp265 ;
  unsigned int __cil_tmp266 ;
  unsigned long __cil_tmp267 ;
  unsigned long __cil_tmp268 ;
  unsigned char __cil_tmp269 ;
  int __cil_tmp270 ;
  unsigned long __cil_tmp271 ;
  unsigned long __cil_tmp272 ;
  unsigned short __cil_tmp273 ;
  int __cil_tmp274 ;
  int __cil_tmp275 ;

  {
#line 865
  db = (struct bsd_db *)state;
#line 866
  __cil_tmp41 = (unsigned long )db;
#line 866
  __cil_tmp42 = __cil_tmp41 + 24;
#line 866
  max_ent = *((unsigned int *)__cil_tmp42);
#line 867
  accm = 0UL;
#line 868
  bitno = 32U;
#line 869
  __cil_tmp43 = (unsigned long )db;
#line 869
  __cil_tmp44 = __cil_tmp43 + 9;
#line 869
  __cil_tmp45 = *((unsigned char *)__cil_tmp44);
#line 869
  n_bits = (unsigned int )__cil_tmp45;
#line 870
  tgtbitno = 32U - n_bits;
#line 877
  __cil_tmp46 = *ibuf;
#line 877
  adrs = (int )__cil_tmp46;
#line 878
  __cil_tmp47 = ibuf + 1UL;
#line 878
  __cil_tmp48 = *__cil_tmp47;
#line 878
  ctrl = (int )__cil_tmp48;
#line 880
  __cil_tmp49 = ibuf + 5UL;
#line 880
  __cil_tmp50 = *__cil_tmp49;
#line 880
  __cil_tmp51 = (int )__cil_tmp50;
#line 880
  __cil_tmp52 = ibuf + 4UL;
#line 880
  __cil_tmp53 = *__cil_tmp52;
#line 880
  __cil_tmp54 = (int )__cil_tmp53;
#line 880
  __cil_tmp55 = __cil_tmp54 << 8;
#line 880
  seq = __cil_tmp55 + __cil_tmp51;
#line 882
  ibuf = ibuf + 6UL;
#line 883
  ilen = isize + -6;
  {
#line 890
  __cil_tmp56 = (unsigned long )db;
#line 890
  __cil_tmp57 = __cil_tmp56 + 14;
#line 890
  __cil_tmp58 = *((unsigned short *)__cil_tmp57);
#line 890
  __cil_tmp59 = (int )__cil_tmp58;
#line 890
  if (__cil_tmp59 != seq) {
    {
#line 892
    __cil_tmp60 = (unsigned long )db;
#line 892
    __cil_tmp61 = __cil_tmp60 + 11;
#line 892
    __cil_tmp62 = *((unsigned char *)__cil_tmp61);
#line 892
    __cil_tmp63 = (unsigned int )__cil_tmp62;
#line 892
    if (__cil_tmp63 != 0U) {
      {
#line 894
      __cil_tmp64 = (unsigned long )db;
#line 894
      __cil_tmp65 = __cil_tmp64 + 12;
#line 894
      __cil_tmp66 = *((unsigned char *)__cil_tmp65);
#line 894
      __cil_tmp67 = (int )__cil_tmp66;
#line 894
      __cil_tmp68 = (unsigned long )db;
#line 894
      __cil_tmp69 = __cil_tmp68 + 14;
#line 894
      __cil_tmp70 = *((unsigned short *)__cil_tmp69);
#line 894
      __cil_tmp71 = (int )__cil_tmp70;
#line 894
      __cil_tmp72 = __cil_tmp71 + -1;
#line 894
      printk("bsd_decomp%d: bad sequence # %d, expected %d\n", __cil_tmp67, seq, __cil_tmp72);
      }
    } else {

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

  }
  }
#line 900
  __cil_tmp73 = (unsigned long )db;
#line 900
  __cil_tmp74 = __cil_tmp73 + 14;
#line 900
  __cil_tmp75 = (unsigned long )db;
#line 900
  __cil_tmp76 = __cil_tmp75 + 14;
#line 900
  __cil_tmp77 = *((unsigned short *)__cil_tmp76);
#line 900
  __cil_tmp78 = (int )__cil_tmp77;
#line 900
  __cil_tmp79 = __cil_tmp78 + 1;
#line 900
  *((unsigned short *)__cil_tmp74) = (unsigned short )__cil_tmp79;
#line 901
  __cil_tmp80 = (unsigned long )db;
#line 901
  __cil_tmp81 = __cil_tmp80 + 32;
#line 901
  __cil_tmp82 = (unsigned int )ilen;
#line 901
  __cil_tmp83 = (unsigned long )db;
#line 901
  __cil_tmp84 = __cil_tmp83 + 32;
#line 901
  __cil_tmp85 = *((unsigned int *)__cil_tmp84);
#line 901
  *((unsigned int *)__cil_tmp81) = __cil_tmp85 + __cil_tmp82;
#line 908
  wptr = obuf;
#line 909
  tmp = wptr;
#line 909
  wptr = wptr + 1;
#line 909
  *tmp = (unsigned char )adrs;
#line 910
  tmp___0 = wptr;
#line 910
  wptr = wptr + 1;
#line 910
  *tmp___0 = (unsigned char )ctrl;
#line 911
  tmp___1 = wptr;
#line 911
  wptr = wptr + 1;
#line 911
  *tmp___1 = (unsigned char)0;
#line 913
  oldcode = 256U;
#line 914
  explen = 3;
  ldv_14538: 
#line 923
  tmp___2 = ilen;
#line 923
  ilen = ilen - 1;
#line 923
  if (tmp___2 <= 0) {
#line 925
    __cil_tmp86 = (unsigned long )db;
#line 925
    __cil_tmp87 = __cil_tmp86 + 28;
#line 925
    __cil_tmp88 = (unsigned int )explen;
#line 925
    __cil_tmp89 = (unsigned long )db;
#line 925
    __cil_tmp90 = __cil_tmp89 + 28;
#line 925
    __cil_tmp91 = *((unsigned int *)__cil_tmp90);
#line 925
    __cil_tmp92 = __cil_tmp91 + __cil_tmp88;
#line 925
    *((unsigned int *)__cil_tmp87) = __cil_tmp92 + 4294967293U;
#line 926
    goto ldv_14522;
  } else {

  }
#line 935
  bitno = bitno - 8U;
#line 936
  tmp___3 = ibuf;
#line 936
  ibuf = ibuf + 1;
#line 936
  __cil_tmp93 = (int )bitno;
#line 936
  __cil_tmp94 = *tmp___3;
#line 936
  __cil_tmp95 = (int )__cil_tmp94;
#line 936
  __cil_tmp96 = __cil_tmp95 << __cil_tmp93;
#line 936
  __cil_tmp97 = (unsigned long )__cil_tmp96;
#line 936
  accm = __cil_tmp97 | accm;
#line 937
  if (tgtbitno < bitno) {
#line 939
    goto ldv_14523;
  } else {

  }
#line 942
  __cil_tmp98 = (int )tgtbitno;
#line 942
  __cil_tmp99 = accm >> __cil_tmp98;
#line 942
  incode = (unsigned int )__cil_tmp99;
#line 943
  __cil_tmp100 = (int )n_bits;
#line 943
  accm = accm << __cil_tmp100;
#line 944
  bitno = bitno + n_bits;
#line 950
  if (incode == 256U) {
#line 952
    if (ilen > 0) {
      {
#line 954
      __cil_tmp101 = (unsigned long )db;
#line 954
      __cil_tmp102 = __cil_tmp101 + 11;
#line 954
      __cil_tmp103 = *((unsigned char *)__cil_tmp102);
#line 954
      __cil_tmp104 = (unsigned int )__cil_tmp103;
#line 954
      if (__cil_tmp104 != 0U) {
        {
#line 956
        __cil_tmp105 = (unsigned long )db;
#line 956
        __cil_tmp106 = __cil_tmp105 + 12;
#line 956
        __cil_tmp107 = *((unsigned char *)__cil_tmp106);
#line 956
        __cil_tmp108 = (int )__cil_tmp107;
#line 956
        printk("bsd_decomp%d: bad CLEAR\n", __cil_tmp108);
        }
      } else {

      }
      }
#line 958
      return (-2);
    } else {

    }
    {
#line 961
    bsd_clear(db);
    }
#line 962
    goto ldv_14522;
  } else {

  }
  {
#line 965
  __cil_tmp109 = max_ent + 2U;
#line 965
  if (__cil_tmp109 < incode) {
#line 965
    goto _L;
  } else {
    {
#line 965
    __cil_tmp110 = (unsigned long )db;
#line 965
    __cil_tmp111 = __cil_tmp110 + 20;
#line 965
    __cil_tmp112 = *((unsigned int *)__cil_tmp111);
#line 965
    if (__cil_tmp112 < incode) {
#line 965
      goto _L;
    } else
#line 965
    if (incode > max_ent) {
#line 965
      if (oldcode == 256U) {
        _L: /* CIL Label */ 
        {
#line 968
        __cil_tmp113 = (unsigned long )db;
#line 968
        __cil_tmp114 = __cil_tmp113 + 11;
#line 968
        __cil_tmp115 = *((unsigned char *)__cil_tmp114);
#line 968
        __cil_tmp116 = (unsigned int )__cil_tmp115;
#line 968
        if (__cil_tmp116 != 0U) {
          {
#line 970
          __cil_tmp117 = (unsigned long )db;
#line 970
          __cil_tmp118 = __cil_tmp117 + 12;
#line 970
          __cil_tmp119 = *((unsigned char *)__cil_tmp118);
#line 970
          __cil_tmp120 = (int )__cil_tmp119;
#line 970
          printk("bsd_decomp%d: bad code 0x%x oldcode=0x%x ", __cil_tmp120, incode,
                 oldcode);
#line 972
          __cil_tmp121 = (unsigned long )db;
#line 972
          __cil_tmp122 = __cil_tmp121 + 14;
#line 972
          __cil_tmp123 = *((unsigned short *)__cil_tmp122);
#line 972
          __cil_tmp124 = (int )__cil_tmp123;
#line 972
          printk("max_ent=0x%x explen=%d seqno=%d\n", max_ent, explen, __cil_tmp124);
          }
        } else {

        }
        }
#line 975
        return (-2);
      } else {

      }
    } else {

    }
    }
  }
  }
#line 979
  if (incode > max_ent) {
#line 981
    finchar = oldcode;
#line 982
    extra = 1;
  } else {
#line 986
    finchar = incode;
#line 987
    extra = 0;
  }
#line 990
  __cil_tmp125 = (unsigned long )finchar;
#line 990
  __cil_tmp126 = (unsigned long )db;
#line 990
  __cil_tmp127 = __cil_tmp126 + 72;
#line 990
  __cil_tmp128 = *((unsigned short **)__cil_tmp127);
#line 990
  __cil_tmp129 = __cil_tmp128 + __cil_tmp125;
#line 990
  __cil_tmp130 = *__cil_tmp129;
#line 990
  codelen = (int )__cil_tmp130;
#line 991
  __cil_tmp131 = codelen + extra;
#line 991
  explen = __cil_tmp131 + explen;
#line 992
  if (explen > osize) {
    {
#line 994
    __cil_tmp132 = (unsigned long )db;
#line 994
    __cil_tmp133 = __cil_tmp132 + 11;
#line 994
    __cil_tmp134 = *((unsigned char *)__cil_tmp133);
#line 994
    __cil_tmp135 = (unsigned int )__cil_tmp134;
#line 994
    if (__cil_tmp135 != 0U) {
      {
#line 996
      __cil_tmp136 = (unsigned long )db;
#line 996
      __cil_tmp137 = __cil_tmp136 + 12;
#line 996
      __cil_tmp138 = *((unsigned char *)__cil_tmp137);
#line 996
      __cil_tmp139 = (int )__cil_tmp138;
#line 996
      printk("bsd_decomp%d: ran out of mru\n", __cil_tmp139);
      }
    } else {

    }
    }
#line 1002
    return (-2);
  } else {

  }
#line 1009
  __cil_tmp140 = (unsigned long )codelen;
#line 1009
  wptr = wptr + __cil_tmp140;
#line 1010
  p = wptr;
#line 1011
  goto ldv_14526;
  ldv_14525: 
#line 1013
  __cil_tmp141 = (unsigned long )finchar;
#line 1013
  __cil_tmp142 = (unsigned long )db;
#line 1013
  __cil_tmp143 = __cil_tmp142 + 80;
#line 1013
  __cil_tmp144 = *((struct bsd_dict **)__cil_tmp143);
#line 1013
  dictp2 = __cil_tmp144 + __cil_tmp141;
#line 1015
  __cil_tmp145 = (unsigned long )dictp2;
#line 1015
  __cil_tmp146 = __cil_tmp145 + 10;
#line 1015
  __cil_tmp147 = *((unsigned short *)__cil_tmp146);
#line 1015
  __cil_tmp148 = (unsigned long )__cil_tmp147;
#line 1015
  __cil_tmp149 = (unsigned long )db;
#line 1015
  __cil_tmp150 = __cil_tmp149 + 80;
#line 1015
  __cil_tmp151 = *((struct bsd_dict **)__cil_tmp150);
#line 1015
  dictp = __cil_tmp151 + __cil_tmp148;
#line 1040
  p = p - 1;
#line 1040
  __cil_tmp152 = 0 + 2;
#line 1040
  __cil_tmp153 = 0 + __cil_tmp152;
#line 1040
  __cil_tmp154 = (unsigned long )dictp;
#line 1040
  __cil_tmp155 = __cil_tmp154 + __cil_tmp153;
#line 1040
  *p = *((unsigned char *)__cil_tmp155);
#line 1041
  __cil_tmp156 = *((unsigned short *)dictp);
#line 1041
  finchar = (unsigned int )__cil_tmp156;
  ldv_14526: ;
#line 1011
  if (finchar > 255U) {
#line 1012
    goto ldv_14525;
  } else {
#line 1014
    goto ldv_14527;
  }
  ldv_14527: 
#line 1043
  p = p - 1;
#line 1043
  *p = (unsigned char )finchar;
#line 1053
  if (extra != 0) {
#line 1055
    tmp___4 = wptr;
#line 1055
    wptr = wptr + 1;
#line 1055
    *tmp___4 = (unsigned char )finchar;
  } else {

  }
#line 1066
  if (oldcode != 256U) {
    {
#line 1066
    __cil_tmp157 = (unsigned long )db;
#line 1066
    __cil_tmp158 = __cil_tmp157 + 20;
#line 1066
    __cil_tmp159 = *((unsigned int *)__cil_tmp158);
#line 1066
    if (__cil_tmp159 > max_ent) {
#line 1073
      __cil_tmp160 = (unsigned long )oldcode;
#line 1073
      __cil_tmp161 = (unsigned long )finchar;
#line 1073
      __cil_tmp162 = __cil_tmp161 << 16;
#line 1073
      fcode = __cil_tmp162 + __cil_tmp160;
#line 1074
      __cil_tmp163 = (unsigned long )db;
#line 1074
      __cil_tmp164 = __cil_tmp163 + 8;
#line 1074
      __cil_tmp165 = *((unsigned char *)__cil_tmp164);
#line 1074
      __cil_tmp166 = (int )__cil_tmp165;
#line 1074
      __cil_tmp167 = (unsigned long )finchar;
#line 1074
      __cil_tmp168 = __cil_tmp167 << __cil_tmp166;
#line 1074
      __cil_tmp169 = (unsigned int )__cil_tmp168;
#line 1074
      __cil_tmp170 = __cil_tmp169 ^ oldcode;
#line 1074
      hval = (int )__cil_tmp170;
#line 1075
      __cil_tmp171 = (unsigned long )hval;
#line 1075
      __cil_tmp172 = (unsigned long )db;
#line 1075
      __cil_tmp173 = __cil_tmp172 + 80;
#line 1075
      __cil_tmp174 = *((struct bsd_dict **)__cil_tmp173);
#line 1075
      dictp = __cil_tmp174 + __cil_tmp171;
      {
#line 1078
      __cil_tmp175 = (unsigned long )dictp;
#line 1078
      __cil_tmp176 = __cil_tmp175 + 8;
#line 1078
      __cil_tmp177 = *((unsigned short *)__cil_tmp176);
#line 1078
      __cil_tmp178 = (unsigned int )__cil_tmp177;
#line 1078
      if (__cil_tmp178 < max_ent) {
#line 1080
        if (hval != 0) {
#line 1080
          disp = hval;
        } else {
#line 1080
          disp = 1;
        }
        ldv_14536: 
#line 1083
        hval = hval + disp;
        {
#line 1084
        __cil_tmp179 = (unsigned long )db;
#line 1084
        __cil_tmp180 = __cil_tmp179 + 4;
#line 1084
        __cil_tmp181 = *((unsigned int *)__cil_tmp180);
#line 1084
        __cil_tmp182 = (unsigned int )hval;
#line 1084
        if (__cil_tmp182 >= __cil_tmp181) {
#line 1086
          __cil_tmp183 = (unsigned long )db;
#line 1086
          __cil_tmp184 = __cil_tmp183 + 4;
#line 1086
          __cil_tmp185 = *((unsigned int *)__cil_tmp184);
#line 1086
          __cil_tmp186 = (unsigned int )hval;
#line 1086
          __cil_tmp187 = __cil_tmp186 - __cil_tmp185;
#line 1086
          hval = (int )__cil_tmp187;
        } else {

        }
        }
#line 1088
        __cil_tmp188 = (unsigned long )hval;
#line 1088
        __cil_tmp189 = (unsigned long )db;
#line 1088
        __cil_tmp190 = __cil_tmp189 + 80;
#line 1088
        __cil_tmp191 = *((struct bsd_dict **)__cil_tmp190);
#line 1088
        dictp = __cil_tmp191 + __cil_tmp188;
        {
#line 1090
        __cil_tmp192 = (unsigned long )dictp;
#line 1090
        __cil_tmp193 = __cil_tmp192 + 8;
#line 1090
        __cil_tmp194 = *((unsigned short *)__cil_tmp193);
#line 1090
        __cil_tmp195 = (unsigned int )__cil_tmp194;
#line 1090
        if (__cil_tmp195 < max_ent) {
#line 1091
          goto ldv_14536;
        } else {
#line 1093
          goto ldv_14537;
        }
        }
        ldv_14537: ;
      } else {

      }
      }
#line 1098
      __cil_tmp196 = max_ent + 1U;
#line 1098
      __cil_tmp197 = (unsigned long )__cil_tmp196;
#line 1098
      __cil_tmp198 = (unsigned long )db;
#line 1098
      __cil_tmp199 = __cil_tmp198 + 80;
#line 1098
      __cil_tmp200 = *((struct bsd_dict **)__cil_tmp199);
#line 1098
      dictp2___0 = __cil_tmp200 + __cil_tmp197;
#line 1099
      __cil_tmp201 = (unsigned long )dictp2___0;
#line 1099
      __cil_tmp202 = __cil_tmp201 + 10;
#line 1099
      __cil_tmp203 = *((unsigned short *)__cil_tmp202);
#line 1099
      indx = (int )__cil_tmp203;
#line 1100
      __cil_tmp204 = (unsigned long )indx;
#line 1100
      __cil_tmp205 = (unsigned long )db;
#line 1100
      __cil_tmp206 = __cil_tmp205 + 80;
#line 1100
      __cil_tmp207 = *((struct bsd_dict **)__cil_tmp206);
#line 1100
      dictp3 = __cil_tmp207 + __cil_tmp204;
      {
#line 1102
      __cil_tmp208 = (unsigned long )dictp3;
#line 1102
      __cil_tmp209 = __cil_tmp208 + 8;
#line 1102
      __cil_tmp210 = *((unsigned short *)__cil_tmp209);
#line 1102
      __cil_tmp211 = (unsigned int )__cil_tmp210;
#line 1102
      if (__cil_tmp211 == max_ent) {
#line 1104
        __cil_tmp212 = (unsigned long )dictp3;
#line 1104
        __cil_tmp213 = __cil_tmp212 + 8;
#line 1104
        *((unsigned short *)__cil_tmp213) = (unsigned short)32767;
      } else {

      }
      }
#line 1107
      __cil_tmp214 = (unsigned long )dictp2___0;
#line 1107
      __cil_tmp215 = __cil_tmp214 + 10;
#line 1107
      *((unsigned short *)__cil_tmp215) = (unsigned short )hval;
#line 1108
      __cil_tmp216 = (unsigned long )dictp;
#line 1108
      __cil_tmp217 = __cil_tmp216 + 8;
#line 1108
      *((unsigned short *)__cil_tmp217) = (unsigned short )max_ent;
#line 1109
      *((unsigned long *)dictp) = fcode;
#line 1110
      max_ent = max_ent + 1U;
#line 1110
      __cil_tmp218 = (unsigned long )db;
#line 1110
      __cil_tmp219 = __cil_tmp218 + 24;
#line 1110
      *((unsigned int *)__cil_tmp219) = max_ent;
#line 1113
      __cil_tmp220 = (unsigned long )max_ent;
#line 1113
      __cil_tmp221 = (unsigned long )db;
#line 1113
      __cil_tmp222 = __cil_tmp221 + 72;
#line 1113
      __cil_tmp223 = *((unsigned short **)__cil_tmp222);
#line 1113
      lens1 = __cil_tmp223 + __cil_tmp220;
#line 1114
      __cil_tmp224 = (unsigned long )oldcode;
#line 1114
      __cil_tmp225 = (unsigned long )db;
#line 1114
      __cil_tmp226 = __cil_tmp225 + 72;
#line 1114
      __cil_tmp227 = *((unsigned short **)__cil_tmp226);
#line 1114
      lens2 = __cil_tmp227 + __cil_tmp224;
#line 1115
      __cil_tmp228 = *lens2;
#line 1115
      __cil_tmp229 = (unsigned int )__cil_tmp228;
#line 1115
      __cil_tmp230 = __cil_tmp229 + 1U;
#line 1115
      *lens1 = (unsigned short )__cil_tmp230;
      {
#line 1118
      __cil_tmp231 = (int )n_bits;
#line 1118
      __cil_tmp232 = 1 << __cil_tmp231;
#line 1118
      __cil_tmp233 = __cil_tmp232 + -1;
#line 1118
      __cil_tmp234 = (unsigned int )__cil_tmp233;
#line 1118
      if (__cil_tmp234 <= max_ent) {
        {
#line 1118
        __cil_tmp235 = (unsigned long )db;
#line 1118
        __cil_tmp236 = __cil_tmp235 + 20;
#line 1118
        __cil_tmp237 = *((unsigned int *)__cil_tmp236);
#line 1118
        if (__cil_tmp237 > max_ent) {
#line 1120
          n_bits = n_bits + 1U;
#line 1120
          __cil_tmp238 = (unsigned long )db;
#line 1120
          __cil_tmp239 = __cil_tmp238 + 9;
#line 1120
          *((unsigned char *)__cil_tmp239) = (unsigned char )n_bits;
#line 1121
          tgtbitno = 32U - n_bits;
        } else {

        }
        }
      } else {

      }
      }
    } else {

    }
    }
  } else {

  }
#line 1124
  oldcode = incode;
  ldv_14523: ;
#line 1125
  goto ldv_14538;
  ldv_14522: 
  {
#line 1127
  __cil_tmp240 = (unsigned long )db;
#line 1127
  __cil_tmp241 = __cil_tmp240 + 64;
#line 1127
  __cil_tmp242 = (unsigned long )db;
#line 1127
  __cil_tmp243 = __cil_tmp242 + 64;
#line 1127
  __cil_tmp244 = *((unsigned int *)__cil_tmp243);
#line 1127
  *((unsigned int *)__cil_tmp241) = __cil_tmp244 + 1U;
#line 1128
  __cil_tmp245 = (unsigned long )db;
#line 1128
  __cil_tmp246 = __cil_tmp245 + 56;
#line 1128
  __cil_tmp247 = (unsigned long )db;
#line 1128
  __cil_tmp248 = __cil_tmp247 + 56;
#line 1128
  __cil_tmp249 = *((unsigned int *)__cil_tmp248);
#line 1128
  *((unsigned int *)__cil_tmp246) = __cil_tmp249 + 1U;
#line 1129
  __cil_tmp250 = (unsigned long )db;
#line 1129
  __cil_tmp251 = __cil_tmp250 + 68;
#line 1129
  __cil_tmp252 = (unsigned int )isize;
#line 1129
  __cil_tmp253 = (unsigned long )db;
#line 1129
  __cil_tmp254 = __cil_tmp253 + 68;
#line 1129
  __cil_tmp255 = *((unsigned int *)__cil_tmp254);
#line 1129
  __cil_tmp256 = __cil_tmp255 + __cil_tmp252;
#line 1129
  *((unsigned int *)__cil_tmp251) = __cil_tmp256 + 4294967290U;
#line 1130
  __cil_tmp257 = (unsigned long )db;
#line 1130
  __cil_tmp258 = __cil_tmp257 + 60;
#line 1130
  __cil_tmp259 = (unsigned int )explen;
#line 1130
  __cil_tmp260 = (unsigned long )db;
#line 1130
  __cil_tmp261 = __cil_tmp260 + 60;
#line 1130
  __cil_tmp262 = *((unsigned int *)__cil_tmp261);
#line 1130
  *((unsigned int *)__cil_tmp258) = __cil_tmp262 + __cil_tmp259;
#line 1132
  tmp___5 = bsd_check(db);
  }
#line 1132
  if (tmp___5 != 0) {
    {
#line 1134
    __cil_tmp263 = (unsigned long )db;
#line 1134
    __cil_tmp264 = __cil_tmp263 + 11;
#line 1134
    __cil_tmp265 = *((unsigned char *)__cil_tmp264);
#line 1134
    __cil_tmp266 = (unsigned int )__cil_tmp265;
#line 1134
    if (__cil_tmp266 != 0U) {
      {
#line 1136
      __cil_tmp267 = (unsigned long )db;
#line 1136
      __cil_tmp268 = __cil_tmp267 + 12;
#line 1136
      __cil_tmp269 = *((unsigned char *)__cil_tmp268);
#line 1136
      __cil_tmp270 = (int )__cil_tmp269;
#line 1136
      __cil_tmp271 = (unsigned long )db;
#line 1136
      __cil_tmp272 = __cil_tmp271 + 14;
#line 1136
      __cil_tmp273 = *((unsigned short *)__cil_tmp272);
#line 1136
      __cil_tmp274 = (int )__cil_tmp273;
#line 1136
      __cil_tmp275 = __cil_tmp274 + -1;
#line 1136
      printk("bsd_decomp%d: peer should have cleared dictionary on %d\n", __cil_tmp270,
             __cil_tmp275);
      }
    } else {

    }
    }
  } else {

  }
#line 1140
  return (explen);
}
}
#line 1147 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static struct compressor ppp_bsd_compress  = 
#line 1147
     {21, & bsd_comp_alloc, & bsd_free, & bsd_comp_init, & bsd_reset, & bsd_compress,
    & bsd_comp_stats, & bsd_decomp_alloc, & bsd_free, & bsd_decomp_init, & bsd_reset,
    & bsd_decompress, & bsd_incomp, & bsd_comp_stats, & __this_module, 0U};
#line 1169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static int bsdcomp_init(void) 
{ int answer ;
  int tmp ;

  {
  {
#line 1171
  tmp = ppp_register_compressor(& ppp_bsd_compress);
#line 1171
  answer = tmp;
  }
#line 1172
  if (answer == 0) {
    {
#line 1173
    printk("<6>PPP BSD Compression module registered\n");
    }
  } else {

  }
#line 1174
  return (answer);
}
}
#line 1177 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
static void bsdcomp_cleanup(void) 
{ 

  {
  {
#line 1179
  ppp_unregister_compressor(& ppp_bsd_compress);
  }
#line 1180
  return;
}
}
#line 1203
extern void ldv_check_final_state(void) ;
#line 1209
extern void ldv_initialize(void) ;
#line 1212
extern int __VERIFIER_nondet_int(void) ;
#line 1215 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
int LDV_IN_INTERRUPT  ;
#line 1218 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
void main(void) 
{ unsigned char *var_bsd_comp_alloc_6_p0 ;
  int var_bsd_comp_alloc_6_p1 ;
  void *var_bsd_free_4_p0 ;
  void *var_bsd_comp_init_9_p0 ;
  unsigned char *var_bsd_comp_init_9_p1 ;
  int var_bsd_comp_init_9_p2 ;
  int var_bsd_comp_init_9_p3 ;
  int var_bsd_comp_init_9_p4 ;
  int var_bsd_comp_init_9_p5 ;
  void *var_bsd_reset_3_p0 ;
  void *var_bsd_compress_13_p0 ;
  unsigned char *var_bsd_compress_13_p1 ;
  unsigned char *var_bsd_compress_13_p2 ;
  int var_bsd_compress_13_p3 ;
  int var_bsd_compress_13_p4 ;
  void *var_bsd_comp_stats_2_p0 ;
  struct compstat *var_group1 ;
  unsigned char *var_bsd_decomp_alloc_7_p0 ;
  int var_bsd_decomp_alloc_7_p1 ;
  void *var_bsd_decomp_init_10_p0 ;
  unsigned char *var_bsd_decomp_init_10_p1 ;
  int var_bsd_decomp_init_10_p2 ;
  int var_bsd_decomp_init_10_p3 ;
  int var_bsd_decomp_init_10_p4 ;
  int var_bsd_decomp_init_10_p5 ;
  int var_bsd_decomp_init_10_p6 ;
  void *var_bsd_decompress_15_p0 ;
  unsigned char *var_bsd_decompress_15_p1 ;
  int var_bsd_decompress_15_p2 ;
  unsigned char *var_bsd_decompress_15_p3 ;
  int var_bsd_decompress_15_p4 ;
  void *var_bsd_incomp_14_p0 ;
  unsigned char *var_bsd_incomp_14_p1 ;
  int var_bsd_incomp_14_p2 ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
  {
#line 2006
  LDV_IN_INTERRUPT = 1;
#line 2015
  ldv_initialize();
#line 2091
  tmp = bsdcomp_init();
  }
#line 2091
  if (tmp != 0) {
#line 2092
    goto ldv_final;
  } else {

  }
#line 2096
  goto ldv_14619;
  ldv_14618: 
  {
#line 2099
  tmp___0 = __VERIFIER_nondet_int();
  }
#line 2101
  if (tmp___0 == 0) {
#line 2101
    goto case_0;
  } else
#line 2189
  if (tmp___0 == 1) {
#line 2189
    goto case_1;
  } else
#line 2277
  if (tmp___0 == 2) {
#line 2277
    goto case_2;
  } else
#line 2365
  if (tmp___0 == 3) {
#line 2365
    goto case_3;
  } else
#line 2453
  if (tmp___0 == 4) {
#line 2453
    goto case_4;
  } else
#line 2515
  if (tmp___0 == 5) {
#line 2515
    goto case_5;
  } else
#line 2603
  if (tmp___0 == 6) {
#line 2603
    goto case_6;
  } else
#line 2691
  if (tmp___0 == 7) {
#line 2691
    goto case_7;
  } else
#line 2779
  if (tmp___0 == 8) {
#line 2779
    goto case_8;
  } else
#line 2859
  if (tmp___0 == 9) {
#line 2859
    goto case_9;
  } else {
    {
#line 2947
    goto switch_default;
#line 2099
    if (0) {
      case_0: /* CIL Label */ 
      {
#line 2138
      bsd_comp_alloc(var_bsd_comp_alloc_6_p0, var_bsd_comp_alloc_6_p1);
      }
#line 2188
      goto ldv_14607;
      case_1: /* CIL Label */ 
      {
#line 2226
      bsd_free(var_bsd_free_4_p0);
      }
#line 2276
      goto ldv_14607;
      case_2: /* CIL Label */ 
      {
#line 2316
      bsd_comp_init(var_bsd_comp_init_9_p0, var_bsd_comp_init_9_p1, var_bsd_comp_init_9_p2,
                    var_bsd_comp_init_9_p3, var_bsd_comp_init_9_p4, var_bsd_comp_init_9_p5);
      }
#line 2364
      goto ldv_14607;
      case_3: /* CIL Label */ 
      {
#line 2402
      bsd_reset(var_bsd_reset_3_p0);
      }
#line 2452
      goto ldv_14607;
      case_4: /* CIL Label */ 
      {
#line 2499
      bsd_compress(var_bsd_compress_13_p0, var_bsd_compress_13_p1, var_bsd_compress_13_p2,
                   var_bsd_compress_13_p3, var_bsd_compress_13_p4);
      }
#line 2514
      goto ldv_14607;
      case_5: /* CIL Label */ 
      {
#line 2552
      bsd_comp_stats(var_bsd_comp_stats_2_p0, var_group1);
      }
#line 2602
      goto ldv_14607;
      case_6: /* CIL Label */ 
      {
#line 2640
      bsd_decomp_alloc(var_bsd_decomp_alloc_7_p0, var_bsd_decomp_alloc_7_p1);
      }
#line 2690
      goto ldv_14607;
      case_7: /* CIL Label */ 
      {
#line 2730
      bsd_decomp_init(var_bsd_decomp_init_10_p0, var_bsd_decomp_init_10_p1, var_bsd_decomp_init_10_p2,
                      var_bsd_decomp_init_10_p3, var_bsd_decomp_init_10_p4, var_bsd_decomp_init_10_p5,
                      var_bsd_decomp_init_10_p6);
      }
#line 2778
      goto ldv_14607;
      case_8: /* CIL Label */ 
      {
#line 2851
      bsd_decompress(var_bsd_decompress_15_p0, var_bsd_decompress_15_p1, var_bsd_decompress_15_p2,
                     var_bsd_decompress_15_p3, var_bsd_decompress_15_p4);
      }
#line 2858
      goto ldv_14607;
      case_9: /* CIL Label */ 
      {
#line 2931
      bsd_incomp(var_bsd_incomp_14_p0, var_bsd_incomp_14_p1, var_bsd_incomp_14_p2);
      }
#line 2946
      goto ldv_14607;
      switch_default: /* CIL Label */ ;
#line 2947
      goto ldv_14607;
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
  ldv_14607: ;
  ldv_14619: 
  {
#line 2096
  tmp___1 = __VERIFIER_nondet_int();
  }
#line 2096
  if (tmp___1 != 0) {
#line 2097
    goto ldv_14618;
  } else {
#line 2099
    goto ldv_14620;
  }
  ldv_14620: ;
  {
#line 3029
  bsdcomp_cleanup();
  }
  ldv_final: 
  {
#line 3032
  ldv_check_final_state();
  }
#line 3035
  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/15261/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/15261/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
extern int __VERIFIER_nondet_int(void) ;
#line 3056 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
int ldv_spin  =    0;
#line 3060 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
void ldv_check_alloc_flags(gfp_t flags ) 
{ 

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

    }
  } else {

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

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

    }
  } else {

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

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

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

  {
#line 3088
  ldv_spin = 1;
#line 3089
  return;
}
}
#line 3092 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
void ldv_spin_unlock(void) 
{ 

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

  {
  {
#line 3104
  is_lock = __VERIFIER_nondet_int();
  }
#line 3106
  if (is_lock != 0) {
#line 3109
    return (0);
  } else {
#line 3114
    ldv_spin = 1;
#line 3116
    return (1);
  }
}
}
#line 3283 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
{ 

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

  {
  {
#line 3300
  ldv_check_alloc_flags(flags);
#line 3301
  tmp = __VERIFIER_nondet_pointer();
  }
#line 3301
  return (tmp);
}
}
#line 3315 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
void *ldv_vmalloc_19(unsigned long ldv_func_arg1 ) 
{ 

  {
  {
#line 3320
  ldv_check_alloc_nonatomic();
#line 3322
  vmalloc(ldv_func_arg1);
  }
#line 3323
  return ((void *)0);
}
}
#line 3325 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
void *ldv_vmalloc_20(unsigned long ldv_func_arg1 ) 
{ 

  {
  {
#line 3330
  ldv_check_alloc_nonatomic();
#line 3332
  vmalloc(ldv_func_arg1);
  }
#line 3333
  return ((void *)0);
}
}