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 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 219 "include/linux/types.h"
  struct __anonstruct_atomic_t_7 {
     int counter ;
  };
  #line 219 "include/linux/types.h"
  typedef struct __anonstruct_atomic_t_7 atomic_t;
  #line 224 "include/linux/types.h"
  struct __anonstruct_atomic64_t_8 {
     long counter ;
  };
  #line 224 "include/linux/types.h"
  typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  #line 229 "include/linux/types.h"
  struct list_head {
     struct list_head *next ;
     struct list_head *prev ;
  };
  #line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  struct module;
  #line 56
  struct module;
  #line 146 "include/linux/init.h"
  typedef void (*ctor_fn_t)(void);
  #line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
  struct page;
  #line 18
  struct page;
  #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
  struct task_struct;
  #line 20
  struct task_struct;
  #line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  struct task_struct;
  #line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  struct page;
  #line 52
  struct task_struct;
  #line 329
  struct arch_spinlock;
  #line 329
  struct arch_spinlock;
  #line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  struct task_struct;
  #line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
  struct task_struct;
  #line 10 "include/asm-generic/bug.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 20 "/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 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 union __anonunion____missing_field_name_36 {
    __ticketpair_t head_tail ;
    struct __raw_tickets tickets ;
 };
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 struct arch_spinlock {
    union __anonunion____missing_field_name_36 __annonCompField17 ;
 };
 #line 20 "/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 12 "include/linux/lockdep.h"
 struct task_struct;
 #line 20 "include/linux/spinlock_types.h"
 struct raw_spinlock {
    arch_spinlock_t raw_lock ;
    unsigned int magic ;
    unsigned int owner_cpu ;
    void *owner ;
 };
 #line 64 "include/linux/spinlock_types.h"
 union __anonunion____missing_field_name_39 {
    struct raw_spinlock rlock ;
 };
 #line 64 "include/linux/spinlock_types.h"
 struct spinlock {
    union __anonunion____missing_field_name_39 __annonCompField19 ;
 };
 #line 64 "include/linux/spinlock_types.h"
 typedef struct spinlock spinlock_t;
 #line 55 "include/linux/wait.h"
 struct task_struct;
 #line 60 "include/linux/pageblock-flags.h"
 struct page;
 #line 48 "include/linux/mutex.h"
 struct mutex {
    atomic_t count ;
    spinlock_t wait_lock ;
    struct list_head wait_list ;
    struct task_struct *owner ;
    char const   *name ;
    void *magic ;
 };
 #line 9 "include/linux/memory_hotplug.h"
 struct page;
 #line 994 "include/linux/mmzone.h"
 struct page;
 #line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 struct task_struct;
 #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 194 "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 194 "include/linux/elf.h"
 typedef struct elf64_sym Elf64_Sym;
 #line 20 "include/linux/kobject_ns.h"
 struct sock;
 #line 20
 struct sock;
 #line 21
 struct kobject;
 #line 21
 struct kobject;
 #line 27
 enum kobj_ns_type {
     KOBJ_NS_TYPE_NONE = 0,
     KOBJ_NS_TYPE_NET = 1,
     KOBJ_NS_TYPES = 2
 } ;
 #line 40 "include/linux/kobject_ns.h"
 struct kobj_ns_type_operations {
    enum kobj_ns_type type ;
    void *(*grab_current_ns)(void) ;
    void const   *(*netlink_ns)(struct sock *sk ) ;
    void const   *(*initial_ns)(void) ;
    void (*drop_ns)(void * ) ;
 };
 #line 22 "include/linux/sysfs.h"
 struct kobject;
 #line 23
 struct module;
 #line 24
 enum kobj_ns_type;
 #line 26 "include/linux/sysfs.h"
 struct attribute {
    char const   *name ;
    umode_t mode ;
 };
 #line 112 "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 118
 struct sysfs_dirent;
 #line 118
 struct sysfs_dirent;
 #line 22 "include/linux/kref.h"
 struct kref {
    atomic_t refcount ;
 };
 #line 60 "include/linux/kobject.h"
 struct kset;
 #line 60
 struct kobj_type;
 #line 60 "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 int state_initialized : 1 ;
    unsigned int state_in_sysfs : 1 ;
    unsigned int state_add_uevent_sent : 1 ;
    unsigned int state_remove_uevent_sent : 1 ;
    unsigned int uevent_suppress : 1 ;
 };
 #line 108 "include/linux/kobject.h"
 struct kobj_type {
    void (*release)(struct kobject *kobj ) ;
    struct sysfs_ops  const  *sysfs_ops ;
    struct attribute **default_attrs ;
    struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
    void const   *(*namespace)(struct kobject *kobj ) ;
 };
 #line 116 "include/linux/kobject.h"
 struct kobj_uevent_env {
    char *envp[32] ;
    int envp_idx ;
    char buf[2048] ;
    int buflen ;
 };
 #line 123 "include/linux/kobject.h"
 struct kset_uevent_ops {
    int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
    char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
    int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 };
 #line 140
 struct sock;
 #line 159 "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 39 "include/linux/moduleparam.h"
 struct kernel_param;
 #line 39
 struct kernel_param;
 #line 41 "include/linux/moduleparam.h"
 struct kernel_param_ops {
    int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
    int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
    void (*free)(void *arg ) ;
 };
 #line 50
 struct kparam_string;
 #line 50
 struct kparam_array;
 #line 50 "include/linux/moduleparam.h"
 union __anonunion____missing_field_name_199 {
    void *arg ;
    struct kparam_string  const  *str ;
    struct kparam_array  const  *arr ;
 };
 #line 50 "include/linux/moduleparam.h"
 struct kernel_param {
    char const   *name ;
    struct kernel_param_ops  const  *ops ;
    u16 perm ;
    s16 level ;
    union __anonunion____missing_field_name_199 __annonCompField32 ;
 };
 #line 63 "include/linux/moduleparam.h"
 struct kparam_string {
    unsigned int maxlen ;
    char *string ;
 };
 #line 69 "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 445
 struct module;
 #line 80 "include/linux/jump_label.h"
 struct module;
 #line 143 "include/linux/jump_label.h"
 struct static_key {
    atomic_t enabled ;
 };
 #line 22 "include/linux/tracepoint.h"
 struct module;
 #line 23
 struct tracepoint;
 #line 23
 struct tracepoint;
 #line 25 "include/linux/tracepoint.h"
 struct tracepoint_func {
    void *func ;
    void *data ;
 };
 #line 30 "include/linux/tracepoint.h"
 struct tracepoint {
    char const   *name ;
    struct static_key key ;
    void (*regfunc)(void) ;
    void (*unregfunc)(void) ;
    struct tracepoint_func *funcs ;
 };
 #line 19 "include/linux/export.h"
 struct kernel_symbol {
    unsigned long value ;
    char const   *name ;
 };
 #line 8 "include/asm-generic/module.h"
 struct mod_arch_specific {
 
 };
 #line 35 "include/linux/module.h"
 struct module;
 #line 37
 struct module_param_attrs;
 #line 37 "include/linux/module.h"
 struct module_kobject {
    struct kobject kobj ;
    struct module *mod ;
    struct kobject *drivers_dir ;
    struct module_param_attrs *mp ;
 };
 #line 44 "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 count ) ;
    void (*setup)(struct module * , char const   * ) ;
    int (*test)(struct module * ) ;
    void (*free)(struct module * ) ;
 };
 #line 71
 struct exception_table_entry;
 #line 71
 struct exception_table_entry;
 #line 199
 enum module_state {
     MODULE_STATE_LIVE = 0,
     MODULE_STATE_COMING = 1,
     MODULE_STATE_GOING = 2
 } ;
 #line 215 "include/linux/module.h"
 struct module_ref {
    unsigned long incs ;
    unsigned long decs ;
 } __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 #line 220
 struct module_sect_attrs;
 #line 220
 struct module_notes_attrs;
 #line 220
 struct ftrace_event_call;
 #line 220 "include/linux/module.h"
 struct module {
    enum module_state state ;
    struct list_head list ;
    char name[64UL - sizeof(unsigned long )] ;
    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 ;
    unsigned int num_ctors ;
 };
 #line 46 "include/linux/slub_def.h"
 struct kmem_cache_cpu {
    void **freelist ;
    unsigned long tid ;
    struct page *page ;
    struct page *partial ;
    int node ;
    unsigned int stat[26] ;
 };
 #line 57 "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 73 "include/linux/slub_def.h"
 struct kmem_cache_order_objects {
    unsigned long x ;
 };
 #line 80 "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[1 << 10] ;
 };
 #line 120 "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 13 "include/linux/ppp-comp.h"
 struct module;
 #line 33 "include/linux/ppp-comp.h"
 struct compressor {
    int compress_proto ;
    void *(*comp_alloc)(unsigned char *options , int opt_len ) ;
    void (*comp_free)(void *state ) ;
    int (*comp_init)(void *state , unsigned char *options , int opt_len , int unit ,
                     int opthdr , int debug ) ;
    void (*comp_reset)(void *state ) ;
    int (*compress)(void *state , unsigned char *rptr , unsigned char *obuf , int isize ,
                    int osize ) ;
    void (*comp_stat)(void *state , struct compstat *stats ) ;
    void *(*decomp_alloc)(unsigned char *options , int opt_len ) ;
    void (*decomp_free)(void *state ) ;
    int (*decomp_init)(void *state , unsigned char *options , int opt_len , int unit ,
                       int opthdr , int mru , int debug ) ;
    void (*decomp_reset)(void *state ) ;
    int (*decompress)(void *state , unsigned char *ibuf , int isize , unsigned char *obuf ,
                      int osize ) ;
    void (*incomp)(void *state , unsigned char *ibuf , int icnt ) ;
    void (*decomp_stat)(void *state , struct compstat *stats ) ;
    struct module *owner ;
    unsigned int comp_extra ;
 };
 #line 116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
 struct __anonstruct_hs_202 {
    unsigned short prefix ;
    unsigned char suffix ;
    unsigned char pad ;
 };
 #line 116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
 union __anonunion_f_201 {
    unsigned long fcode ;
    struct __anonstruct_hs_202 hs ;
 };
 #line 116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
 struct bsd_dict {
    union __anonunion_f_201 f ;
    unsigned short codem1 ;
    unsigned short cptr ;
 };
 #line 137 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
 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 1 "<compiler builtins>"
 long __builtin_expect(long val , long res ) ;
 #line 100 "include/linux/printk.h"
 extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
 #line 152 "include/linux/mutex.h"
 void mutex_lock(struct mutex *lock ) ;
 #line 153
 int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
 #line 154
 int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
 #line 168
 int mutex_trylock(struct mutex *lock ) ;
 #line 169
 void mutex_unlock(struct mutex *lock ) ;
 #line 170
 int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
 #line 54 "include/linux/vmalloc.h"
 extern void *vmalloc(unsigned long size ) ;
 #line 66
 extern void vfree(void const   *addr ) ;
 #line 26 "include/linux/export.h"
 extern struct module __this_module ;
 #line 67 "include/linux/module.h"
 int init_module(void) ;
 #line 68
 void cleanup_module(void) ;
 #line 161 "include/linux/slab.h"
 extern void kfree(void const   * ) ;
 #line 221 "include/linux/slub_def.h"
 extern void *__kmalloc(size_t size , gfp_t flags ) ;
 #line 268
 __inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
                                                                     gfp_t flags )  __attribute__((__no_instrument_function__)) ;
 #line 268 "include/linux/slub_def.h"
 __inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
                                                                     gfp_t flags ) 
 { void *tmp___2 ;
 
   {
   {
 #line 283
   tmp___2 = __kmalloc(size, flags);
   }
 #line 283
   return (tmp___2);
 }
 }
 #line 349 "include/linux/slab.h"
 __inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
 #line 349 "include/linux/slab.h"
 __inline static void *kzalloc(size_t size , gfp_t flags ) 
 { void *tmp ;
   unsigned int __cil_tmp4 ;
 
   {
   {
 #line 351
   __cil_tmp4 = flags | 32768U;
 #line 351
   tmp = kmalloc(size, __cil_tmp4);
   }
 #line 351
   return (tmp);
 }
 }
 #line 180 "include/linux/ppp-comp.h"
 extern int ppp_register_compressor(struct compressor *cp ) ;
 #line 181
 extern void ppp_unregister_compressor(struct compressor *cp ) ;
 #line 169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
 static void bsd_free(void *state ) ;
 #line 170
 static void *bsd_alloc(unsigned char *options , int opt_len , int decomp ) ;
 #line 171
 static void *bsd_comp_alloc(unsigned char *options , int opt_len ) ;
 #line 172
 static void *bsd_decomp_alloc(unsigned char *options , int opt_len ) ;
 #line 174
 static int bsd_init(void *state , unsigned char *options , int opt_len , int unit ,
                     int debug , int decomp ) ;
 #line 176
 static int bsd_comp_init(void *state , unsigned char *options , int opt_len , int unit ,
                          int opthdr , int debug ) ;
 #line 178
 static int bsd_decomp_init(void *state , unsigned char *options , int opt_len , int unit ,
                            int opthdr , int mru , int debug ) ;
 #line 182
 static void bsd_reset(void *state ) ;
 #line 183
 static void bsd_comp_stats(void *state , struct compstat *stats ) ;
 #line 185
 static int bsd_compress(void *state , unsigned char *rptr , unsigned char *obuf ,
                         int isize , int osize ) ;
 #line 187
 static void bsd_incomp(void *state , unsigned char *ibuf , int icnt ) ;
 #line 189
 static int bsd_decompress(void *state , unsigned char *ibuf , int isize , unsigned char *obuf ,
                           int osize ) ;
 #line 222 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
 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 225
   __cil_tmp2 = (unsigned long )db;
 #line 225
   __cil_tmp3 = __cil_tmp2 + 44;
 #line 225
   __cil_tmp4 = (unsigned long )db;
 #line 225
   __cil_tmp5 = __cil_tmp4 + 44;
 #line 225
   __cil_tmp6 = *((unsigned int *)__cil_tmp5);
 #line 225
   *((unsigned int *)__cil_tmp3) = __cil_tmp6 + 1U;
 #line 226
   __cil_tmp7 = (unsigned long )db;
 #line 226
   __cil_tmp8 = __cil_tmp7 + 24;
 #line 226
   *((unsigned int *)__cil_tmp8) = 256U;
 #line 227
   __cil_tmp9 = (unsigned long )db;
 #line 227
   __cil_tmp10 = __cil_tmp9 + 9;
 #line 227
   *((unsigned char *)__cil_tmp10) = (unsigned char)9;
 #line 228
   __cil_tmp11 = (unsigned long )db;
 #line 228
   __cil_tmp12 = __cil_tmp11 + 32;
 #line 228
   *((unsigned int *)__cil_tmp12) = 0U;
 #line 229
   __cil_tmp13 = (unsigned long )db;
 #line 229
   __cil_tmp14 = __cil_tmp13 + 28;
 #line 229
   *((unsigned int *)__cil_tmp14) = 0U;
 #line 230
   __cil_tmp15 = (unsigned long )db;
 #line 230
   __cil_tmp16 = __cil_tmp15 + 36;
 #line 230
   *((unsigned int *)__cil_tmp16) = 0U;
 #line 231
   __cil_tmp17 = (unsigned long )db;
 #line 231
   __cil_tmp18 = __cil_tmp17 + 40;
 #line 231
   *((unsigned int *)__cil_tmp18) = 10000U;
 #line 232
   return;
 }
 }
 #line 248 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
 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 ;
   int __cil_tmp9 ;
   unsigned int __cil_tmp10 ;
   unsigned long __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   unsigned int __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   unsigned long __cil_tmp15 ;
   unsigned long __cil_tmp16 ;
   unsigned long __cil_tmp17 ;
   unsigned int __cil_tmp18 ;
   unsigned int __cil_tmp19 ;
   unsigned long __cil_tmp20 ;
   unsigned long __cil_tmp21 ;
   unsigned int __cil_tmp22 ;
   unsigned long __cil_tmp23 ;
   unsigned long __cil_tmp24 ;
   unsigned long __cil_tmp25 ;
   unsigned long __cil_tmp26 ;
   unsigned int __cil_tmp27 ;
   unsigned int __cil_tmp28 ;
   unsigned long __cil_tmp29 ;
   unsigned long __cil_tmp30 ;
   unsigned int __cil_tmp31 ;
   int __cil_tmp32 ;
   unsigned int __cil_tmp33 ;
   unsigned long __cil_tmp34 ;
   unsigned long __cil_tmp35 ;
   unsigned int __cil_tmp36 ;
   unsigned long __cil_tmp37 ;
   unsigned long __cil_tmp38 ;
   unsigned long __cil_tmp39 ;
   unsigned long __cil_tmp40 ;
   unsigned int __cil_tmp41 ;
   unsigned int __cil_tmp42 ;
   unsigned long __cil_tmp43 ;
   unsigned long __cil_tmp44 ;
   unsigned int __cil_tmp45 ;
   unsigned long __cil_tmp46 ;
   unsigned long __cil_tmp47 ;
   unsigned long __cil_tmp48 ;
   unsigned long __cil_tmp49 ;
   unsigned int __cil_tmp50 ;
   unsigned int __cil_tmp51 ;
   unsigned long __cil_tmp52 ;
   unsigned long __cil_tmp53 ;
   unsigned int __cil_tmp54 ;
   unsigned long __cil_tmp55 ;
   unsigned long __cil_tmp56 ;
   unsigned long __cil_tmp57 ;
   unsigned long __cil_tmp58 ;
   unsigned int __cil_tmp59 ;
   unsigned long __cil_tmp60 ;
   unsigned long __cil_tmp61 ;
   unsigned int __cil_tmp62 ;
   unsigned long __cil_tmp63 ;
   unsigned long __cil_tmp64 ;
   unsigned int __cil_tmp65 ;
   unsigned long __cil_tmp66 ;
   unsigned long __cil_tmp67 ;
   unsigned int __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 long __cil_tmp75 ;
   unsigned long __cil_tmp76 ;
   unsigned int __cil_tmp77 ;
   int __cil_tmp78 ;
   unsigned int __cil_tmp79 ;
   unsigned long __cil_tmp80 ;
   unsigned long __cil_tmp81 ;
 
   {
   {
 #line 252
   __cil_tmp3 = (unsigned long )db;
 #line 252
   __cil_tmp4 = __cil_tmp3 + 40;
 #line 252
   __cil_tmp5 = *((unsigned int *)__cil_tmp4);
 #line 252
   __cil_tmp6 = (unsigned long )db;
 #line 252
   __cil_tmp7 = __cil_tmp6 + 28;
 #line 252
   __cil_tmp8 = *((unsigned int *)__cil_tmp7);
 #line 252
   if (__cil_tmp8 >= __cil_tmp5) {
     {
 #line 255
     __cil_tmp9 = 2147483647 >> 8;
 #line 255
     __cil_tmp10 = (unsigned int )__cil_tmp9;
 #line 255
     __cil_tmp11 = (unsigned long )db;
 #line 255
     __cil_tmp12 = __cil_tmp11 + 28;
 #line 255
     __cil_tmp13 = *((unsigned int *)__cil_tmp12);
 #line 255
     if (__cil_tmp13 >= __cil_tmp10) {
 #line 257
       __cil_tmp14 = (unsigned long )db;
 #line 257
       __cil_tmp15 = __cil_tmp14 + 28;
 #line 257
       __cil_tmp16 = (unsigned long )db;
 #line 257
       __cil_tmp17 = __cil_tmp16 + 28;
 #line 257
       __cil_tmp18 = *((unsigned int *)__cil_tmp17);
 #line 257
       __cil_tmp19 = __cil_tmp18 >> 2;
 #line 257
       __cil_tmp20 = (unsigned long )db;
 #line 257
       __cil_tmp21 = __cil_tmp20 + 28;
 #line 257
       __cil_tmp22 = *((unsigned int *)__cil_tmp21);
 #line 257
       *((unsigned int *)__cil_tmp15) = __cil_tmp22 - __cil_tmp19;
 #line 258
       __cil_tmp23 = (unsigned long )db;
 #line 258
       __cil_tmp24 = __cil_tmp23 + 32;
 #line 258
       __cil_tmp25 = (unsigned long )db;
 #line 258
       __cil_tmp26 = __cil_tmp25 + 32;
 #line 258
       __cil_tmp27 = *((unsigned int *)__cil_tmp26);
 #line 258
       __cil_tmp28 = __cil_tmp27 >> 2;
 #line 258
       __cil_tmp29 = (unsigned long )db;
 #line 258
       __cil_tmp30 = __cil_tmp29 + 32;
 #line 258
       __cil_tmp31 = *((unsigned int *)__cil_tmp30);
 #line 258
       *((unsigned int *)__cil_tmp24) = __cil_tmp31 - __cil_tmp28;
     } else {
       {
 #line 255
       __cil_tmp32 = 2147483647 >> 8;
 #line 255
       __cil_tmp33 = (unsigned int )__cil_tmp32;
 #line 255
       __cil_tmp34 = (unsigned long )db;
 #line 255
       __cil_tmp35 = __cil_tmp34 + 32;
 #line 255
       __cil_tmp36 = *((unsigned int *)__cil_tmp35);
 #line 255
       if (__cil_tmp36 >= __cil_tmp33) {
 #line 257
         __cil_tmp37 = (unsigned long )db;
 #line 257
         __cil_tmp38 = __cil_tmp37 + 28;
 #line 257
         __cil_tmp39 = (unsigned long )db;
 #line 257
         __cil_tmp40 = __cil_tmp39 + 28;
 #line 257
         __cil_tmp41 = *((unsigned int *)__cil_tmp40);
 #line 257
         __cil_tmp42 = __cil_tmp41 >> 2;
 #line 257
         __cil_tmp43 = (unsigned long )db;
 #line 257
         __cil_tmp44 = __cil_tmp43 + 28;
 #line 257
         __cil_tmp45 = *((unsigned int *)__cil_tmp44);
 #line 257
         *((unsigned int *)__cil_tmp38) = __cil_tmp45 - __cil_tmp42;
 #line 258
         __cil_tmp46 = (unsigned long )db;
 #line 258
         __cil_tmp47 = __cil_tmp46 + 32;
 #line 258
         __cil_tmp48 = (unsigned long )db;
 #line 258
         __cil_tmp49 = __cil_tmp48 + 32;
 #line 258
         __cil_tmp50 = *((unsigned int *)__cil_tmp49);
 #line 258
         __cil_tmp51 = __cil_tmp50 >> 2;
 #line 258
         __cil_tmp52 = (unsigned long )db;
 #line 258
         __cil_tmp53 = __cil_tmp52 + 32;
 #line 258
         __cil_tmp54 = *((unsigned int *)__cil_tmp53);
 #line 258
         *((unsigned int *)__cil_tmp47) = __cil_tmp54 - __cil_tmp51;
       } else {
 
       }
       }
     }
     }
 #line 261
     __cil_tmp55 = (unsigned long )db;
 #line 261
     __cil_tmp56 = __cil_tmp55 + 40;
 #line 261
     __cil_tmp57 = (unsigned long )db;
 #line 261
     __cil_tmp58 = __cil_tmp57 + 28;
 #line 261
     __cil_tmp59 = *((unsigned int *)__cil_tmp58);
 #line 261
     *((unsigned int *)__cil_tmp56) = __cil_tmp59 + 10000U;
     {
 #line 263
     __cil_tmp60 = (unsigned long )db;
 #line 263
     __cil_tmp61 = __cil_tmp60 + 20;
 #line 263
     __cil_tmp62 = *((unsigned int *)__cil_tmp61);
 #line 263
     __cil_tmp63 = (unsigned long )db;
 #line 263
     __cil_tmp64 = __cil_tmp63 + 24;
 #line 263
     __cil_tmp65 = *((unsigned int *)__cil_tmp64);
 #line 263
     if (__cil_tmp65 >= __cil_tmp62) {
 #line 273
       __cil_tmp66 = (unsigned long )db;
 #line 273
       __cil_tmp67 = __cil_tmp66 + 28;
 #line 273
       __cil_tmp68 = *((unsigned int *)__cil_tmp67);
 #line 273
       new_ratio = __cil_tmp68 << 8;
       {
#line 274
      __cil_tmp69 = (unsigned long )db;
#line 274
      __cil_tmp70 = __cil_tmp69 + 32;
#line 274
      __cil_tmp71 = *((unsigned int *)__cil_tmp70);
#line 274
      if (__cil_tmp71 != 0U) {
#line 276
        __cil_tmp72 = (unsigned long )db;
#line 276
        __cil_tmp73 = __cil_tmp72 + 32;
#line 276
        __cil_tmp74 = *((unsigned int *)__cil_tmp73);
#line 276
        new_ratio = new_ratio / __cil_tmp74;
      } else {

      }
      }
      {
#line 279
      __cil_tmp75 = (unsigned long )db;
#line 279
      __cil_tmp76 = __cil_tmp75 + 36;
#line 279
      __cil_tmp77 = *((unsigned int *)__cil_tmp76);
#line 279
      if (new_ratio < __cil_tmp77) {
        {
#line 281
        bsd_clear(db);
        }
#line 282
        return (1);
      } else {
        {
#line 279
        __cil_tmp78 = 1 << 8;
#line 279
        __cil_tmp79 = (unsigned int )__cil_tmp78;
#line 279
        if (new_ratio < __cil_tmp79) {
          {
#line 281
          bsd_clear(db);
          }
#line 282
          return (1);
        } else {

        }
        }
      }
      }
#line 284
      __cil_tmp80 = (unsigned long )db;
#line 284
      __cil_tmp81 = __cil_tmp80 + 36;
#line 284
      *((unsigned int *)__cil_tmp81) = new_ratio;
    } else {

    }
    }
  } else {

  }
  }
#line 287
  return (0);
}
}
#line 294 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
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 296
  db = (struct bsd_db *)state;
#line 298
  __cil_tmp4 = (unsigned long )db;
#line 298
  __cil_tmp5 = __cil_tmp4 + 60;
#line 298
  *((__u32 *)stats) = *((unsigned int *)__cil_tmp5);
#line 299
  __cil_tmp6 = (unsigned long )stats;
#line 299
  __cil_tmp7 = __cil_tmp6 + 4;
#line 299
  __cil_tmp8 = (unsigned long )db;
#line 299
  __cil_tmp9 = __cil_tmp8 + 56;
#line 299
  *((__u32 *)__cil_tmp7) = *((unsigned int *)__cil_tmp9);
#line 300
  __cil_tmp10 = (unsigned long )stats;
#line 300
  __cil_tmp11 = __cil_tmp10 + 8;
#line 300
  __cil_tmp12 = (unsigned long )db;
#line 300
  __cil_tmp13 = __cil_tmp12 + 68;
#line 300
  *((__u32 *)__cil_tmp11) = *((unsigned int *)__cil_tmp13);
#line 301
  __cil_tmp14 = (unsigned long )stats;
#line 301
  __cil_tmp15 = __cil_tmp14 + 12;
#line 301
  __cil_tmp16 = (unsigned long )db;
#line 301
  __cil_tmp17 = __cil_tmp16 + 64;
#line 301
  *((__u32 *)__cil_tmp15) = *((unsigned int *)__cil_tmp17);
#line 302
  __cil_tmp18 = (unsigned long )stats;
#line 302
  __cil_tmp19 = __cil_tmp18 + 16;
#line 302
  __cil_tmp20 = (unsigned long )db;
#line 302
  __cil_tmp21 = __cil_tmp20 + 52;
#line 302
  *((__u32 *)__cil_tmp19) = *((unsigned int *)__cil_tmp21);
#line 303
  __cil_tmp22 = (unsigned long )stats;
#line 303
  __cil_tmp23 = __cil_tmp22 + 20;
#line 303
  __cil_tmp24 = (unsigned long )db;
#line 303
  __cil_tmp25 = __cil_tmp24 + 48;
#line 303
  *((__u32 *)__cil_tmp23) = *((unsigned int *)__cil_tmp25);
#line 304
  __cil_tmp26 = (unsigned long )stats;
#line 304
  __cil_tmp27 = __cil_tmp26 + 24;
#line 304
  __cil_tmp28 = (unsigned long )db;
#line 304
  __cil_tmp29 = __cil_tmp28 + 28;
#line 304
  *((__u32 *)__cil_tmp27) = *((unsigned int *)__cil_tmp29);
#line 305
  __cil_tmp30 = (unsigned long )stats;
#line 305
  __cil_tmp31 = __cil_tmp30 + 28;
#line 305
  __cil_tmp32 = (unsigned long )db;
#line 305
  __cil_tmp33 = __cil_tmp32 + 32;
#line 305
  *((__u32 *)__cil_tmp31) = *((unsigned int *)__cil_tmp33);
#line 306
  return;
}
}
#line 312 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
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 314
  db = (struct bsd_db *)state;
#line 316
  bsd_clear(db);
#line 318
  __cil_tmp3 = (unsigned long )db;
#line 318
  __cil_tmp4 = __cil_tmp3 + 14;
#line 318
  *((unsigned short *)__cil_tmp4) = (unsigned short)0;
#line 319
  __cil_tmp5 = (unsigned long )db;
#line 319
  __cil_tmp6 = __cil_tmp5 + 44;
#line 319
  *((unsigned int *)__cil_tmp6) = 0U;
  }
#line 320
  return;
}
}
#line 326 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static void bsd_free(void *state ) 
{ struct bsd_db *db ;
  unsigned long __cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  struct bsd_dict *__cil_tmp5 ;
  void const   *__cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  void *__cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned short *__cil_tmp12 ;
  void const   *__cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  void *__cil_tmp16 ;
  void const   *__cil_tmp17 ;

  {
#line 328
  db = (struct bsd_db *)state;
#line 330
  if (! db) {
#line 331
    return;
  } else {

  }
  {
#line 336
  __cil_tmp3 = (unsigned long )db;
#line 336
  __cil_tmp4 = __cil_tmp3 + 80;
#line 336
  __cil_tmp5 = *((struct bsd_dict **)__cil_tmp4);
#line 336
  __cil_tmp6 = (void const   *)__cil_tmp5;
#line 336
  vfree(__cil_tmp6);
#line 337
  __cil_tmp7 = (unsigned long )db;
#line 337
  __cil_tmp8 = __cil_tmp7 + 80;
#line 337
  __cil_tmp9 = (void *)0;
#line 337
  *((struct bsd_dict **)__cil_tmp8) = (struct bsd_dict *)__cil_tmp9;
#line 341
  __cil_tmp10 = (unsigned long )db;
#line 341
  __cil_tmp11 = __cil_tmp10 + 72;
#line 341
  __cil_tmp12 = *((unsigned short **)__cil_tmp11);
#line 341
  __cil_tmp13 = (void const   *)__cil_tmp12;
#line 341
  vfree(__cil_tmp13);
#line 342
  __cil_tmp14 = (unsigned long )db;
#line 342
  __cil_tmp15 = __cil_tmp14 + 72;
#line 342
  __cil_tmp16 = (void *)0;
#line 342
  *((unsigned short **)__cil_tmp15) = (unsigned short *)__cil_tmp16;
#line 346
  __cil_tmp17 = (void const   *)db;
#line 346
  kfree(__cil_tmp17);
  }
#line 347
  return;
}
}
#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
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 char __cil_tmp13 ;
  int __cil_tmp14 ;
  unsigned char *__cil_tmp15 ;
  unsigned char __cil_tmp16 ;
  int __cil_tmp17 ;
  unsigned char *__cil_tmp18 ;
  unsigned char __cil_tmp19 ;
  int __cil_tmp20 ;
  int __cil_tmp21 ;
  unsigned char *__cil_tmp22 ;
  unsigned char __cil_tmp23 ;
  int __cil_tmp24 ;
  int __cil_tmp25 ;
  int __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 ;
  struct bsd_dict *__cil_tmp33 ;
  void *__cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  void *__cil_tmp37 ;
  unsigned int __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned short *__cil_tmp45 ;
  void *__cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;

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

        }
        }
      }
      }
    }
    }
  }
#line 365
  __cil_tmp22 = options + 2;
#line 365
  __cil_tmp23 = *__cil_tmp22;
#line 365
  __cil_tmp24 = (int )__cil_tmp23;
#line 365
  bits = __cil_tmp24 & 31;
#line 369
  if (bits == 9) {
#line 369
    goto case_9;
  } else
#line 370
  if (bits == 10) {
#line 370
    goto case_9;
  } else
#line 371
  if (bits == 11) {
#line 371
    goto case_9;
  } else
#line 372
  if (bits == 12) {
#line 372
    goto case_9;
  } else
#line 376
  if (bits == 13) {
#line 376
    goto case_13;
  } else
#line 380
  if (bits == 14) {
#line 380
    goto case_14;
  } else
#line 384
  if (bits == 15) {
#line 384
    goto case_15;
  } else {
    {
#line 392
    goto switch_default;
#line 367
    if (0) {
      case_9: /* CIL Label */ 
      case_10: /* CIL Label */ 
      case_11: /* CIL Label */ 
      case_12: /* CIL Label */ 
#line 373
      hsize = 5003U;
#line 374
      hshift = 4U;
#line 375
      goto switch_break;
      case_13: /* CIL Label */ 
#line 377
      hsize = 9001U;
#line 378
      hshift = 5U;
#line 379
      goto switch_break;
      case_14: /* CIL Label */ 
#line 381
      hsize = 18013U;
#line 382
      hshift = 6U;
#line 383
      goto switch_break;
      case_15: /* CIL Label */ 
#line 385
      hsize = 35023U;
#line 386
      hshift = 7U;
#line 387
      goto switch_break;
      switch_default: /* CIL Label */ 
#line 393
      return ((void *)0);
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
  {
#line 398
  __cil_tmp25 = 1 << bits;
#line 398
  __cil_tmp26 = __cil_tmp25 - 1;
#line 398
  maxmaxcode = (unsigned int )__cil_tmp26;
#line 399
  tmp = kzalloc(88UL, 208U);
#line 399
  db = (struct bsd_db *)tmp;
  }
#line 401
  if (! db) {
#line 403
    return ((void *)0);
  } else {

  }
  {
#line 410
  __cil_tmp27 = (unsigned long )hsize;
#line 410
  __cil_tmp28 = __cil_tmp27 * 16UL;
#line 410
  tmp___0 = vmalloc(__cil_tmp28);
#line 410
  __cil_tmp29 = (unsigned long )db;
#line 410
  __cil_tmp30 = __cil_tmp29 + 80;
#line 410
  *((struct bsd_dict **)__cil_tmp30) = (struct bsd_dict *)tmp___0;
  }
  {
#line 411
  __cil_tmp31 = (unsigned long )db;
#line 411
  __cil_tmp32 = __cil_tmp31 + 80;
#line 411
  __cil_tmp33 = *((struct bsd_dict **)__cil_tmp32);
#line 411
  if (! __cil_tmp33) {
    {
#line 413
    __cil_tmp34 = (void *)db;
#line 413
    bsd_free(__cil_tmp34);
    }
#line 414
    return ((void *)0);
  } else {

  }
  }
#line 420
  if (! decomp) {
#line 422
    __cil_tmp35 = (unsigned long )db;
#line 422
    __cil_tmp36 = __cil_tmp35 + 72;
#line 422
    __cil_tmp37 = (void *)0;
#line 422
    *((unsigned short **)__cil_tmp36) = (unsigned short *)__cil_tmp37;
  } else {
    {
#line 429
    __cil_tmp38 = maxmaxcode + 1U;
#line 429
    __cil_tmp39 = (unsigned long )__cil_tmp38;
#line 429
    __cil_tmp40 = __cil_tmp39 * 2UL;
#line 429
    tmp___1 = vmalloc(__cil_tmp40);
#line 429
    __cil_tmp41 = (unsigned long )db;
#line 429
    __cil_tmp42 = __cil_tmp41 + 72;
#line 429
    *((unsigned short **)__cil_tmp42) = (unsigned short *)tmp___1;
    }
    {
#line 430
    __cil_tmp43 = (unsigned long )db;
#line 430
    __cil_tmp44 = __cil_tmp43 + 72;
#line 430
    __cil_tmp45 = *((unsigned short **)__cil_tmp44);
#line 430
    if (! __cil_tmp45) {
      {
#line 432
      __cil_tmp46 = (void *)db;
#line 432
      bsd_free(__cil_tmp46);
      }
#line 433
      return ((void *)0);
    } else {

    }
    }
  }
#line 439
  __cil_tmp47 = (unsigned long )hsize;
#line 439
  __cil_tmp48 = 16UL * __cil_tmp47;
#line 439
  __cil_tmp49 = 88UL + __cil_tmp48;
#line 439
  *((int *)db) = (int )__cil_tmp49;
#line 442
  __cil_tmp50 = (unsigned long )db;
#line 442
  __cil_tmp51 = __cil_tmp50 + 4;
#line 442
  *((unsigned int *)__cil_tmp51) = hsize;
#line 443
  __cil_tmp52 = (unsigned long )db;
#line 443
  __cil_tmp53 = __cil_tmp52 + 8;
#line 443
  *((unsigned char *)__cil_tmp53) = (unsigned char )hshift;
#line 444
  __cil_tmp54 = (unsigned long )db;
#line 444
  __cil_tmp55 = __cil_tmp54 + 20;
#line 444
  *((unsigned int *)__cil_tmp55) = maxmaxcode;
#line 445
  __cil_tmp56 = (unsigned long )db;
#line 445
  __cil_tmp57 = __cil_tmp56 + 10;
#line 445
  *((unsigned char *)__cil_tmp57) = (unsigned char )bits;
#line 447
  return ((void *)db);
}
}
#line 450 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static void *bsd_comp_alloc(unsigned char *options , int opt_len ) 
{ void *tmp ;

  {
  {
#line 452
  tmp = bsd_alloc(options, opt_len, 0);
  }
#line 452
  return (tmp);
}
}
#line 455 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static void *bsd_decomp_alloc(unsigned char *options , int opt_len ) 
{ void *tmp ;

  {
  {
#line 457
  tmp = bsd_alloc(options, opt_len, 1);
  }
#line 457
  return (tmp);
}
}
#line 464 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
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 char __cil_tmp12 ;
  int __cil_tmp13 ;
  unsigned char *__cil_tmp14 ;
  unsigned char __cil_tmp15 ;
  int __cil_tmp16 ;
  unsigned char *__cil_tmp17 ;
  unsigned char __cil_tmp18 ;
  int __cil_tmp19 ;
  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 ;
  void *__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 short *__cil_tmp37 ;
  unsigned short *__cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned int __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  struct bsd_dict *__cil_tmp44 ;
  struct bsd_dict *__cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  int __cil_tmp48 ;
  int __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  struct bsd_dict *__cil_tmp52 ;
  struct bsd_dict *__cil_tmp53 ;
  unsigned long __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 ;
  void *__cil_tmp62 ;

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

            }
            }
          } else {

          }
          }
        }
        }
      }
      }
    }
    }
  }
#line 478
  if (decomp) {
#line 480
    indx = 255;
    {
#line 481
    while (1) {
      while_continue: /* CIL Label */ ;
#line 483
      __cil_tmp35 = (unsigned long )db;
#line 483
      __cil_tmp36 = __cil_tmp35 + 72;
#line 483
      __cil_tmp37 = *((unsigned short **)__cil_tmp36);
#line 483
      __cil_tmp38 = __cil_tmp37 + indx;
#line 483
      *__cil_tmp38 = (unsigned short)1;
#line 481
      tmp = indx;
#line 481
      indx = indx - 1;
#line 481
      if (tmp > 0) {

      } else {
#line 481
        goto while_break;
      }
    }
    while_break: /* CIL Label */ ;
    }
  } else {

  }
#line 488
  __cil_tmp39 = (unsigned long )db;
#line 488
  __cil_tmp40 = __cil_tmp39 + 4;
#line 488
  __cil_tmp41 = *((unsigned int *)__cil_tmp40);
#line 488
  indx = (int )__cil_tmp41;
  {
#line 489
  while (1) {
    while_continue___0: /* CIL Label */ ;
#line 489
    tmp___0 = indx;
#line 489
    indx = indx - 1;
#line 489
    if (tmp___0 != 0) {

    } else {
#line 489
      goto while_break___0;
    }
#line 491
    __cil_tmp42 = (unsigned long )db;
#line 491
    __cil_tmp43 = __cil_tmp42 + 80;
#line 491
    __cil_tmp44 = *((struct bsd_dict **)__cil_tmp43);
#line 491
    __cil_tmp45 = __cil_tmp44 + indx;
#line 491
    __cil_tmp46 = (unsigned long )__cil_tmp45;
#line 491
    __cil_tmp47 = __cil_tmp46 + 8;
#line 491
    __cil_tmp48 = 1 << 15;
#line 491
    __cil_tmp49 = __cil_tmp48 - 1;
#line 491
    *((unsigned short *)__cil_tmp47) = (unsigned short )__cil_tmp49;
#line 492
    __cil_tmp50 = (unsigned long )db;
#line 492
    __cil_tmp51 = __cil_tmp50 + 80;
#line 492
    __cil_tmp52 = *((struct bsd_dict **)__cil_tmp51);
#line 492
    __cil_tmp53 = __cil_tmp52 + indx;
#line 492
    __cil_tmp54 = (unsigned long )__cil_tmp53;
#line 492
    __cil_tmp55 = __cil_tmp54 + 10;
#line 492
    *((unsigned short *)__cil_tmp55) = (unsigned short)0;
  }
  while_break___0: /* CIL Label */ ;
  }
#line 495
  __cil_tmp56 = (unsigned long )db;
#line 495
  __cil_tmp57 = __cil_tmp56 + 12;
#line 495
  *((unsigned char *)__cil_tmp57) = (unsigned char )unit;
#line 496
  __cil_tmp58 = (unsigned long )db;
#line 496
  __cil_tmp59 = __cil_tmp58 + 16;
#line 496
  *((unsigned int *)__cil_tmp59) = 0U;
#line 498
  if (debug) {
#line 500
    __cil_tmp60 = (unsigned long )db;
#line 500
    __cil_tmp61 = __cil_tmp60 + 11;
#line 500
    *((unsigned char *)__cil_tmp61) = (unsigned char)1;
  } else {

  }
  {
#line 502
  __cil_tmp62 = (void *)db;
#line 502
  bsd_reset(__cil_tmp62);
  }
#line 504
  return (1);
}
}
#line 507 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static int bsd_comp_init(void *state , unsigned char *options , int opt_len , int unit ,
                         int opthdr , int debug ) 
{ int tmp ;

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

  {
  {
#line 517
  tmp = bsd_init(state, options, opt_len, unit, debug, 1);
  }
#line 517
  return (tmp);
}
}
#line 564 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
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 ;
  __u8 *__cil_tmp55 ;
  __u8 *__cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  unsigned short __cil_tmp59 ;
  int __cil_tmp60 ;
  int __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  unsigned short __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  unsigned long __cil_tmp69 ;
  unsigned long __cil_tmp70 ;
  unsigned long __cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  struct bsd_dict *__cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned short __cil_tmp77 ;
  unsigned int __cil_tmp78 ;
  unsigned long __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  unsigned long __cil_tmp81 ;
  unsigned short __cil_tmp82 ;
  int __cil_tmp83 ;
  unsigned long __cil_tmp84 ;
  unsigned long __cil_tmp85 ;
  unsigned int __cil_tmp86 ;
  unsigned int __cil_tmp87 ;
  unsigned long __cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  unsigned int __cil_tmp90 ;
  unsigned int __cil_tmp91 ;
  unsigned int __cil_tmp92 ;
  unsigned long __cil_tmp93 ;
  unsigned long __cil_tmp94 ;
  struct bsd_dict *__cil_tmp95 ;
  unsigned long __cil_tmp96 ;
  unsigned long __cil_tmp97 ;
  unsigned short __cil_tmp98 ;
  unsigned int __cil_tmp99 ;
  unsigned long __cil_tmp100 ;
  unsigned long __cil_tmp101 ;
  unsigned long __cil_tmp102 ;
  unsigned short __cil_tmp103 ;
  int __cil_tmp104 ;
  int __cil_tmp105 ;
  unsigned long __cil_tmp106 ;
  unsigned long __cil_tmp107 ;
  void *__cil_tmp108 ;
  unsigned long __cil_tmp109 ;
  unsigned long __cil_tmp110 ;
  unsigned int __cil_tmp111 ;
  unsigned int __cil_tmp112 ;
  unsigned long __cil_tmp113 ;
  unsigned long __cil_tmp114 ;
  int __cil_tmp115 ;
  unsigned int __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  struct bsd_dict *__cil_tmp119 ;
  unsigned long __cil_tmp120 ;
  unsigned long __cil_tmp121 ;
  unsigned short __cil_tmp122 ;
  unsigned long __cil_tmp123 ;
  unsigned long __cil_tmp124 ;
  struct bsd_dict *__cil_tmp125 ;
  unsigned long __cil_tmp126 ;
  unsigned long __cil_tmp127 ;
  unsigned short __cil_tmp128 ;
  unsigned int __cil_tmp129 ;
  unsigned long __cil_tmp130 ;
  unsigned long __cil_tmp131 ;
  int __cil_tmp132 ;
  int __cil_tmp133 ;
  unsigned long __cil_tmp134 ;
  unsigned long __cil_tmp135 ;
  unsigned long __cil_tmp136 ;
  unsigned long __cil_tmp137 ;
  unsigned long __cil_tmp138 ;
  unsigned long __cil_tmp139 ;
  unsigned long __cil_tmp140 ;
  unsigned long __cil_tmp141 ;
  unsigned long __cil_tmp142 ;
  unsigned long __cil_tmp143 ;
  unsigned short *__cil_tmp144 ;
  unsigned long __cil_tmp145 ;
  unsigned long __cil_tmp146 ;
  unsigned short *__cil_tmp147 ;
  unsigned short __cil_tmp148 ;
  int __cil_tmp149 ;
  int __cil_tmp150 ;
  int __cil_tmp151 ;
  unsigned long __cil_tmp152 ;
  unsigned long __cil_tmp153 ;
  void *__cil_tmp154 ;
  unsigned long __cil_tmp155 ;
  unsigned long __cil_tmp156 ;
  int __cil_tmp157 ;
  int __cil_tmp158 ;
  unsigned int __cil_tmp159 ;
  unsigned long __cil_tmp160 ;
  unsigned long __cil_tmp161 ;
  unsigned int __cil_tmp162 ;
  unsigned long __cil_tmp163 ;
  unsigned long __cil_tmp164 ;
  unsigned int __cil_tmp165 ;
  unsigned long __cil_tmp166 ;
  unsigned long __cil_tmp167 ;
  unsigned int __cil_tmp168 ;
  unsigned long __cil_tmp169 ;
  unsigned long __cil_tmp170 ;
  unsigned int __cil_tmp171 ;
  unsigned long __cil_tmp172 ;
  unsigned long __cil_tmp173 ;
  unsigned int __cil_tmp174 ;
  unsigned long __cil_tmp175 ;
  unsigned long __cil_tmp176 ;
  unsigned long __cil_tmp177 ;
  unsigned long __cil_tmp178 ;
  unsigned int __cil_tmp179 ;
  unsigned long __cil_tmp180 ;
  unsigned long __cil_tmp181 ;
  unsigned long __cil_tmp182 ;
  unsigned long __cil_tmp183 ;
  unsigned short __cil_tmp184 ;
  int __cil_tmp185 ;
  int __cil_tmp186 ;
  unsigned long __cil_tmp187 ;
  unsigned long __cil_tmp188 ;
  unsigned long __cil_tmp189 ;
  unsigned long __cil_tmp190 ;
  unsigned int __cil_tmp191 ;
  int __cil_tmp192 ;
  unsigned long __cil_tmp193 ;
  unsigned long __cil_tmp194 ;
  void *__cil_tmp195 ;
  unsigned int __cil_tmp196 ;
  int __cil_tmp197 ;
  unsigned long __cil_tmp198 ;
  unsigned long __cil_tmp199 ;
  unsigned long __cil_tmp200 ;
  void *__cil_tmp201 ;
  unsigned int __cil_tmp202 ;
  unsigned long __cil_tmp203 ;
  unsigned long __cil_tmp204 ;
  unsigned int __cil_tmp205 ;
  unsigned long __cil_tmp206 ;
  unsigned long __cil_tmp207 ;
  unsigned long __cil_tmp208 ;
  unsigned long __cil_tmp209 ;
  unsigned char __cil_tmp210 ;
  int __cil_tmp211 ;
  int __cil_tmp212 ;
  void *__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 int __cil_tmp220 ;
  unsigned long __cil_tmp221 ;
  unsigned long __cil_tmp222 ;
  unsigned int __cil_tmp223 ;
  unsigned long __cil_tmp224 ;
  unsigned long __cil_tmp225 ;
  unsigned int __cil_tmp226 ;
  unsigned long __cil_tmp227 ;
  unsigned long __cil_tmp228 ;
  unsigned long __cil_tmp229 ;
  unsigned long __cil_tmp230 ;
  unsigned int __cil_tmp231 ;
  unsigned long __cil_tmp232 ;
  unsigned long __cil_tmp233 ;
  unsigned int __cil_tmp234 ;
  unsigned long __cil_tmp235 ;
  unsigned long __cil_tmp236 ;
  unsigned int __cil_tmp237 ;

  {
#line 616
  __cil_tmp39 = rptr + 3;
#line 616
  __cil_tmp40 = *__cil_tmp39;
#line 616
  __cil_tmp41 = (int )__cil_tmp40;
#line 616
  __cil_tmp42 = rptr + 2;
#line 616
  __cil_tmp43 = *__cil_tmp42;
#line 616
  __cil_tmp44 = (int )__cil_tmp43;
#line 616
  __cil_tmp45 = __cil_tmp44 << 8;
#line 616
  ent = __cil_tmp45 + __cil_tmp41;
#line 617
  if (ent < 33) {
#line 619
    return (0);
  } else
#line 617
  if (ent > 249) {
#line 619
    return (0);
  } else {

  }
#line 622
  db = (struct bsd_db *)state;
#line 623
  __cil_tmp46 = (unsigned long )db;
#line 623
  __cil_tmp47 = __cil_tmp46 + 8;
#line 623
  __cil_tmp48 = *((unsigned char *)__cil_tmp47);
#line 623
  hshift = (int )__cil_tmp48;
#line 624
  __cil_tmp49 = (unsigned long )db;
#line 624
  __cil_tmp50 = __cil_tmp49 + 24;
#line 624
  max_ent = *((unsigned int *)__cil_tmp50);
#line 625
  __cil_tmp51 = (unsigned long )db;
#line 625
  __cil_tmp52 = __cil_tmp51 + 9;
#line 625
  __cil_tmp53 = *((unsigned char *)__cil_tmp52);
#line 625
  n_bits = (unsigned int )__cil_tmp53;
#line 626
  bitno = 32U;
#line 627
  accm = 0UL;
#line 628
  __cil_tmp54 = 1 << n_bits;
#line 628
  mxcode = __cil_tmp54 - 1;
#line 631
  wptr = obuf;
#line 632
  olen = 6;
#line 634
  if (osize > isize) {
#line 636
    osize = isize;
  } else {

  }
#line 640
  if (wptr) {
#line 642
    tmp = wptr;
#line 642
    wptr = wptr + 1;
#line 642
    __cil_tmp55 = rptr + 0;
#line 642
    *tmp = *__cil_tmp55;
#line 643
    tmp___0 = wptr;
#line 643
    wptr = wptr + 1;
#line 643
    __cil_tmp56 = rptr + 1;
#line 643
    *tmp___0 = *__cil_tmp56;
#line 644
    tmp___1 = wptr;
#line 644
    wptr = wptr + 1;
#line 644
    *tmp___1 = (unsigned char)0;
#line 645
    tmp___2 = wptr;
#line 645
    wptr = wptr + 1;
#line 645
    *tmp___2 = (unsigned char)253;
#line 646
    tmp___3 = wptr;
#line 646
    wptr = wptr + 1;
#line 646
    __cil_tmp57 = (unsigned long )db;
#line 646
    __cil_tmp58 = __cil_tmp57 + 14;
#line 646
    __cil_tmp59 = *((unsigned short *)__cil_tmp58);
#line 646
    __cil_tmp60 = (int )__cil_tmp59;
#line 646
    __cil_tmp61 = __cil_tmp60 >> 8;
#line 646
    *tmp___3 = (unsigned char )__cil_tmp61;
#line 647
    tmp___4 = wptr;
#line 647
    wptr = wptr + 1;
#line 647
    __cil_tmp62 = (unsigned long )db;
#line 647
    __cil_tmp63 = __cil_tmp62 + 14;
#line 647
    __cil_tmp64 = *((unsigned short *)__cil_tmp63);
#line 647
    *tmp___4 = (unsigned char )__cil_tmp64;
  } else {

  }
#line 651
  rptr = rptr + 4;
#line 652
  isize = isize - 4;
#line 653
  isize = isize + 1;
#line 653
  ilen = isize;
  {
#line 655
  while (1) {
    while_continue: /* CIL Label */ ;
#line 655
    ilen = ilen - 1;
#line 655
    if (ilen > 0) {

    } else {
#line 655
      goto while_break;
    }
#line 657
    tmp___5 = rptr;
#line 657
    rptr = rptr + 1;
#line 657
    c = *tmp___5;
#line 658
    __cil_tmp65 = (unsigned long )ent;
#line 658
    __cil_tmp66 = (unsigned long )c;
#line 658
    __cil_tmp67 = __cil_tmp66 << 16;
#line 658
    fcode = __cil_tmp67 + __cil_tmp65;
#line 659
    __cil_tmp68 = (unsigned long )ent;
#line 659
    __cil_tmp69 = (unsigned long )c;
#line 659
    __cil_tmp70 = __cil_tmp69 << hshift;
#line 659
    __cil_tmp71 = __cil_tmp70 ^ __cil_tmp68;
#line 659
    hval = (int )__cil_tmp71;
#line 660
    __cil_tmp72 = (unsigned long )db;
#line 660
    __cil_tmp73 = __cil_tmp72 + 80;
#line 660
    __cil_tmp74 = *((struct bsd_dict **)__cil_tmp73);
#line 660
    dictp = __cil_tmp74 + hval;
    {
#line 663
    __cil_tmp75 = (unsigned long )dictp;
#line 663
    __cil_tmp76 = __cil_tmp75 + 8;
#line 663
    __cil_tmp77 = *((unsigned short *)__cil_tmp76);
#line 663
    __cil_tmp78 = (unsigned int )__cil_tmp77;
#line 663
    if (__cil_tmp78 >= max_ent) {
#line 665
      goto nomatch;
    } else {

    }
    }
    {
#line 668
    __cil_tmp79 = *((unsigned long *)dictp);
#line 668
    if (__cil_tmp79 == fcode) {
#line 670
      __cil_tmp80 = (unsigned long )dictp;
#line 670
      __cil_tmp81 = __cil_tmp80 + 8;
#line 670
      __cil_tmp82 = *((unsigned short *)__cil_tmp81);
#line 670
      __cil_tmp83 = (int )__cil_tmp82;
#line 670
      ent = __cil_tmp83 + 1;
#line 671
      goto while_continue;
    } else {

    }
    }
#line 675
    if (hval == 0) {
#line 675
      disp = 1;
    } else {
#line 675
      disp = hval;
    }
    {
#line 677
    while (1) {
      while_continue___0: /* CIL Label */ ;
#line 679
      hval = hval + disp;
      {
#line 680
      __cil_tmp84 = (unsigned long )db;
#line 680
      __cil_tmp85 = __cil_tmp84 + 4;
#line 680
      __cil_tmp86 = *((unsigned int *)__cil_tmp85);
#line 680
      __cil_tmp87 = (unsigned int )hval;
#line 680
      if (__cil_tmp87 >= __cil_tmp86) {
#line 682
        __cil_tmp88 = (unsigned long )db;
#line 682
        __cil_tmp89 = __cil_tmp88 + 4;
#line 682
        __cil_tmp90 = *((unsigned int *)__cil_tmp89);
#line 682
        __cil_tmp91 = (unsigned int )hval;
#line 682
        __cil_tmp92 = __cil_tmp91 - __cil_tmp90;
#line 682
        hval = (int )__cil_tmp92;
      } else {

      }
      }
#line 684
      __cil_tmp93 = (unsigned long )db;
#line 684
      __cil_tmp94 = __cil_tmp93 + 80;
#line 684
      __cil_tmp95 = *((struct bsd_dict **)__cil_tmp94);
#line 684
      dictp = __cil_tmp95 + hval;
      {
#line 685
      __cil_tmp96 = (unsigned long )dictp;
#line 685
      __cil_tmp97 = __cil_tmp96 + 8;
#line 685
      __cil_tmp98 = *((unsigned short *)__cil_tmp97);
#line 685
      __cil_tmp99 = (unsigned int )__cil_tmp98;
#line 685
      if (__cil_tmp99 >= max_ent) {
#line 687
        goto nomatch;
      } else {

      }
      }
      {
#line 677
      __cil_tmp100 = *((unsigned long *)dictp);
#line 677
      if (__cil_tmp100 != fcode) {

      } else {
#line 677
        goto while_break___0;
      }
      }
    }
    while_break___0: /* CIL Label */ ;
    }
#line 692
    __cil_tmp101 = (unsigned long )dictp;
#line 692
    __cil_tmp102 = __cil_tmp101 + 8;
#line 692
    __cil_tmp103 = *((unsigned short *)__cil_tmp102);
#line 692
    __cil_tmp104 = (int )__cil_tmp103;
#line 692
    ent = __cil_tmp104 + 1;
#line 693
    goto while_continue;
    nomatch: 
#line 696
    bitno = bitno - n_bits;
#line 696
    __cil_tmp105 = ent << bitno;
#line 696
    __cil_tmp106 = (unsigned long )__cil_tmp105;
#line 696
    accm = accm | __cil_tmp106;
    {
#line 696
    while (1) {
      while_continue___1: /* CIL Label */ ;
#line 696
      olen = olen + 1;
#line 696
      if (wptr) {
#line 696
        tmp___6 = wptr;
#line 696
        wptr = wptr + 1;
#line 696
        __cil_tmp107 = accm >> 24;
#line 696
        *tmp___6 = (unsigned char )__cil_tmp107;
#line 696
        if (olen >= osize) {
#line 696
          __cil_tmp108 = (void *)0;
#line 696
          wptr = (unsigned char *)__cil_tmp108;
        } else {

        }
      } else {

      }
#line 696
      accm = accm << 8;
#line 696
      bitno = bitno + 8U;
#line 696
      if (bitno <= 24U) {

      } else {
#line 696
        goto while_break___1;
      }
    }
    while_break___1: /* CIL Label */ ;
    }
    {
#line 699
    __cil_tmp109 = (unsigned long )db;
#line 699
    __cil_tmp110 = __cil_tmp109 + 20;
#line 699
    __cil_tmp111 = *((unsigned int *)__cil_tmp110);
#line 699
    if (max_ent < __cil_tmp111) {
      {
#line 706
      __cil_tmp112 = (unsigned int )mxcode;
#line 706
      if (max_ent >= __cil_tmp112) {
#line 708
        n_bits = n_bits + 1U;
#line 708
        __cil_tmp113 = (unsigned long )db;
#line 708
        __cil_tmp114 = __cil_tmp113 + 9;
#line 708
        *((unsigned char *)__cil_tmp114) = (unsigned char )n_bits;
#line 709
        __cil_tmp115 = 1 << n_bits;
#line 709
        mxcode = __cil_tmp115 - 1;
      } else {

      }
      }
#line 716
      __cil_tmp116 = max_ent + 1U;
#line 716
      __cil_tmp117 = (unsigned long )db;
#line 716
      __cil_tmp118 = __cil_tmp117 + 80;
#line 716
      __cil_tmp119 = *((struct bsd_dict **)__cil_tmp118);
#line 716
      dictp2 = __cil_tmp119 + __cil_tmp116;
#line 717
      __cil_tmp120 = (unsigned long )dictp2;
#line 717
      __cil_tmp121 = __cil_tmp120 + 10;
#line 717
      __cil_tmp122 = *((unsigned short *)__cil_tmp121);
#line 717
      indx = (int )__cil_tmp122;
#line 718
      __cil_tmp123 = (unsigned long )db;
#line 718
      __cil_tmp124 = __cil_tmp123 + 80;
#line 718
      __cil_tmp125 = *((struct bsd_dict **)__cil_tmp124);
#line 718
      dictp3 = __cil_tmp125 + indx;
      {
#line 720
      __cil_tmp126 = (unsigned long )dictp3;
#line 720
      __cil_tmp127 = __cil_tmp126 + 8;
#line 720
      __cil_tmp128 = *((unsigned short *)__cil_tmp127);
#line 720
      __cil_tmp129 = (unsigned int )__cil_tmp128;
#line 720
      if (__cil_tmp129 == max_ent) {
#line 722
        __cil_tmp130 = (unsigned long )dictp3;
#line 722
        __cil_tmp131 = __cil_tmp130 + 8;
#line 722
        __cil_tmp132 = 1 << 15;
#line 722
        __cil_tmp133 = __cil_tmp132 - 1;
#line 722
        *((unsigned short *)__cil_tmp131) = (unsigned short )__cil_tmp133;
      } else {

      }
      }
#line 725
      __cil_tmp134 = (unsigned long )dictp2;
#line 725
      __cil_tmp135 = __cil_tmp134 + 10;
#line 725
      *((unsigned short *)__cil_tmp135) = (unsigned short )hval;
#line 726
      __cil_tmp136 = (unsigned long )dictp;
#line 726
      __cil_tmp137 = __cil_tmp136 + 8;
#line 726
      *((unsigned short *)__cil_tmp137) = (unsigned short )max_ent;
#line 727
      *((unsigned long *)dictp) = fcode;
#line 728
      max_ent = max_ent + 1U;
#line 728
      __cil_tmp138 = (unsigned long )db;
#line 728
      __cil_tmp139 = __cil_tmp138 + 24;
#line 728
      *((unsigned int *)__cil_tmp139) = max_ent;
      {
#line 730
      __cil_tmp140 = (unsigned long )db;
#line 730
      __cil_tmp141 = __cil_tmp140 + 72;
#line 730
      if (*((unsigned short **)__cil_tmp141)) {
#line 732
        __cil_tmp142 = (unsigned long )db;
#line 732
        __cil_tmp143 = __cil_tmp142 + 72;
#line 732
        __cil_tmp144 = *((unsigned short **)__cil_tmp143);
#line 732
        len1 = __cil_tmp144 + max_ent;
#line 733
        __cil_tmp145 = (unsigned long )db;
#line 733
        __cil_tmp146 = __cil_tmp145 + 72;
#line 733
        __cil_tmp147 = *((unsigned short **)__cil_tmp146);
#line 733
        len2 = __cil_tmp147 + ent;
#line 734
        __cil_tmp148 = *len2;
#line 734
        __cil_tmp149 = (int )__cil_tmp148;
#line 734
        __cil_tmp150 = __cil_tmp149 + 1;
#line 734
        *len1 = (unsigned short )__cil_tmp150;
      } else {

      }
      }
    } else {

    }
    }
#line 737
    ent = (int )c;
  }
  while_break: /* CIL Label */ ;
  }
#line 740
  bitno = bitno - n_bits;
#line 740
  __cil_tmp151 = ent << bitno;
#line 740
  __cil_tmp152 = (unsigned long )__cil_tmp151;
#line 740
  accm = accm | __cil_tmp152;
  {
#line 740
  while (1) {
    while_continue___2: /* CIL Label */ ;
#line 740
    olen = olen + 1;
#line 740
    if (wptr) {
#line 740
      tmp___7 = wptr;
#line 740
      wptr = wptr + 1;
#line 740
      __cil_tmp153 = accm >> 24;
#line 740
      *tmp___7 = (unsigned char )__cil_tmp153;
#line 740
      if (olen >= osize) {
#line 740
        __cil_tmp154 = (void *)0;
#line 740
        wptr = (unsigned char *)__cil_tmp154;
      } else {

      }
    } else {

    }
#line 740
    accm = accm << 8;
#line 740
    bitno = bitno + 8U;
#line 740
    if (bitno <= 24U) {

    } else {
#line 740
      goto while_break___2;
    }
  }
  while_break___2: /* CIL Label */ ;
  }
#line 742
  __cil_tmp155 = (unsigned long )db;
#line 742
  __cil_tmp156 = __cil_tmp155 + 32;
#line 742
  __cil_tmp157 = olen - 4;
#line 742
  __cil_tmp158 = __cil_tmp157 - 2;
#line 742
  __cil_tmp159 = (unsigned int )__cil_tmp158;
#line 742
  __cil_tmp160 = (unsigned long )db;
#line 742
  __cil_tmp161 = __cil_tmp160 + 32;
#line 742
  __cil_tmp162 = *((unsigned int *)__cil_tmp161);
#line 742
  *((unsigned int *)__cil_tmp156) = __cil_tmp162 + __cil_tmp159;
#line 743
  __cil_tmp163 = (unsigned long )db;
#line 743
  __cil_tmp164 = __cil_tmp163 + 60;
#line 743
  __cil_tmp165 = (unsigned int )isize;
#line 743
  __cil_tmp166 = (unsigned long )db;
#line 743
  __cil_tmp167 = __cil_tmp166 + 60;
#line 743
  __cil_tmp168 = *((unsigned int *)__cil_tmp167);
#line 743
  *((unsigned int *)__cil_tmp164) = __cil_tmp168 + __cil_tmp165;
#line 744
  __cil_tmp169 = (unsigned long )db;
#line 744
  __cil_tmp170 = __cil_tmp169 + 28;
#line 744
  __cil_tmp171 = (unsigned int )isize;
#line 744
  __cil_tmp172 = (unsigned long )db;
#line 744
  __cil_tmp173 = __cil_tmp172 + 28;
#line 744
  __cil_tmp174 = *((unsigned int *)__cil_tmp173);
#line 744
  *((unsigned int *)__cil_tmp170) = __cil_tmp174 + __cil_tmp171;
#line 745
  __cil_tmp175 = (unsigned long )db;
#line 745
  __cil_tmp176 = __cil_tmp175 + 56;
#line 745
  __cil_tmp177 = (unsigned long )db;
#line 745
  __cil_tmp178 = __cil_tmp177 + 56;
#line 745
  __cil_tmp179 = *((unsigned int *)__cil_tmp178);
#line 745
  *((unsigned int *)__cil_tmp176) = __cil_tmp179 + 1U;
#line 746
  __cil_tmp180 = (unsigned long )db;
#line 746
  __cil_tmp181 = __cil_tmp180 + 14;
#line 746
  __cil_tmp182 = (unsigned long )db;
#line 746
  __cil_tmp183 = __cil_tmp182 + 14;
#line 746
  __cil_tmp184 = *((unsigned short *)__cil_tmp183);
#line 746
  __cil_tmp185 = (int )__cil_tmp184;
#line 746
  __cil_tmp186 = __cil_tmp185 + 1;
#line 746
  *((unsigned short *)__cil_tmp181) = (unsigned short )__cil_tmp186;
#line 748
  if (bitno < 32U) {
#line 750
    __cil_tmp187 = (unsigned long )db;
#line 750
    __cil_tmp188 = __cil_tmp187 + 32;
#line 750
    __cil_tmp189 = (unsigned long )db;
#line 750
    __cil_tmp190 = __cil_tmp189 + 32;
#line 750
    __cil_tmp191 = *((unsigned int *)__cil_tmp190);
#line 750
    *((unsigned int *)__cil_tmp188) = __cil_tmp191 + 1U;
  } else {

  }
  {
#line 757
  tmp___9 = bsd_check(db);
  }
#line 757
  if (tmp___9) {
#line 759
    bitno = bitno - n_bits;
#line 759
    __cil_tmp192 = 256 << bitno;
#line 759
    __cil_tmp193 = (unsigned long )__cil_tmp192;
#line 759
    accm = accm | __cil_tmp193;
    {
#line 759
    while (1) {
      while_continue___3: /* CIL Label */ ;
#line 759
      olen = olen + 1;
#line 759
      if (wptr) {
#line 759
        tmp___8 = wptr;
#line 759
        wptr = wptr + 1;
#line 759
        __cil_tmp194 = accm >> 24;
#line 759
        *tmp___8 = (unsigned char )__cil_tmp194;
#line 759
        if (olen >= osize) {
#line 759
          __cil_tmp195 = (void *)0;
#line 759
          wptr = (unsigned char *)__cil_tmp195;
        } else {

        }
      } else {

      }
#line 759
      accm = accm << 8;
#line 759
      bitno = bitno + 8U;
#line 759
      if (bitno <= 24U) {

      } else {
#line 759
        goto while_break___3;
      }
    }
    while_break___3: /* CIL Label */ ;
    }
  } else {

  }
#line 767
  if (bitno != 32U) {
#line 769
    olen = olen + 1;
#line 769
    if (wptr) {
#line 769
      tmp___10 = wptr;
#line 769
      wptr = wptr + 1;
#line 769
      __cil_tmp196 = bitno - 8U;
#line 769
      __cil_tmp197 = 255 << __cil_tmp196;
#line 769
      __cil_tmp198 = (unsigned long )__cil_tmp197;
#line 769
      __cil_tmp199 = accm | __cil_tmp198;
#line 769
      __cil_tmp200 = __cil_tmp199 >> 24;
#line 769
      *tmp___10 = (unsigned char )__cil_tmp200;
#line 769
      if (olen >= osize) {
#line 769
        __cil_tmp201 = (void *)0;
#line 769
        wptr = (unsigned char *)__cil_tmp201;
      } else {

      }
    } else {

    }
  } else {

  }
  {
#line 777
  __cil_tmp202 = (unsigned int )mxcode;
#line 777
  if (max_ent >= __cil_tmp202) {
    {
#line 777
    __cil_tmp203 = (unsigned long )db;
#line 777
    __cil_tmp204 = __cil_tmp203 + 20;
#line 777
    __cil_tmp205 = *((unsigned int *)__cil_tmp204);
#line 777
    if (max_ent < __cil_tmp205) {
#line 779
      __cil_tmp206 = (unsigned long )db;
#line 779
      __cil_tmp207 = __cil_tmp206 + 9;
#line 779
      __cil_tmp208 = (unsigned long )db;
#line 779
      __cil_tmp209 = __cil_tmp208 + 9;
#line 779
      __cil_tmp210 = *((unsigned char *)__cil_tmp209);
#line 779
      __cil_tmp211 = (int )__cil_tmp210;
#line 779
      __cil_tmp212 = __cil_tmp211 + 1;
#line 779
      *((unsigned char *)__cil_tmp207) = (unsigned char )__cil_tmp212;
    } else {

    }
    }
  } else {

  }
  }
  {
#line 783
  __cil_tmp213 = (void *)0;
#line 783
  __cil_tmp214 = (unsigned long )__cil_tmp213;
#line 783
  __cil_tmp215 = (unsigned long )wptr;
#line 783
  if (__cil_tmp215 == __cil_tmp214) {
#line 785
    __cil_tmp216 = (unsigned long )db;
#line 785
    __cil_tmp217 = __cil_tmp216 + 48;
#line 785
    __cil_tmp218 = (unsigned long )db;
#line 785
    __cil_tmp219 = __cil_tmp218 + 48;
#line 785
    __cil_tmp220 = *((unsigned int *)__cil_tmp219);
#line 785
    *((unsigned int *)__cil_tmp217) = __cil_tmp220 + 1U;
#line 786
    __cil_tmp221 = (unsigned long )db;
#line 786
    __cil_tmp222 = __cil_tmp221 + 52;
#line 786
    __cil_tmp223 = (unsigned int )isize;
#line 786
    __cil_tmp224 = (unsigned long )db;
#line 786
    __cil_tmp225 = __cil_tmp224 + 52;
#line 786
    __cil_tmp226 = *((unsigned int *)__cil_tmp225);
#line 786
    *((unsigned int *)__cil_tmp222) = __cil_tmp226 + __cil_tmp223;
#line 787
    olen = 0;
  } else {
#line 791
    __cil_tmp227 = (unsigned long )db;
#line 791
    __cil_tmp228 = __cil_tmp227 + 64;
#line 791
    __cil_tmp229 = (unsigned long )db;
#line 791
    __cil_tmp230 = __cil_tmp229 + 64;
#line 791
    __cil_tmp231 = *((unsigned int *)__cil_tmp230);
#line 791
    *((unsigned int *)__cil_tmp228) = __cil_tmp231 + 1U;
#line 792
    __cil_tmp232 = (unsigned long )db;
#line 792
    __cil_tmp233 = __cil_tmp232 + 68;
#line 792
    __cil_tmp234 = (unsigned int )olen;
#line 792
    __cil_tmp235 = (unsigned long )db;
#line 792
    __cil_tmp236 = __cil_tmp235 + 68;
#line 792
    __cil_tmp237 = *((unsigned int *)__cil_tmp236);
#line 792
    *((unsigned int *)__cil_tmp233) = __cil_tmp237 + __cil_tmp234;
  }
  }
#line 796
  return (olen);
}
}
#line 806 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static void bsd_incomp(void *state , unsigned char *ibuf , int icnt ) 
{ char *__cil_tmp4 ;
  unsigned char *__cil_tmp5 ;

  {
  {
#line 808
  __cil_tmp4 = (char *)0;
#line 808
  __cil_tmp5 = (unsigned char *)__cil_tmp4;
#line 808
  bsd_compress(state, ibuf, __cil_tmp5, icnt, 0);
  }
#line 809
  return;
}
}
#line 828 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
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 ;
  __u8 *__cil_tmp46 ;
  __u8 __cil_tmp47 ;
  __u8 *__cil_tmp48 ;
  __u8 __cil_tmp49 ;
  unsigned char *__cil_tmp50 ;
  unsigned char __cil_tmp51 ;
  int __cil_tmp52 ;
  unsigned char *__cil_tmp53 ;
  unsigned char __cil_tmp54 ;
  int __cil_tmp55 ;
  int __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  unsigned short __cil_tmp59 ;
  int __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  unsigned long __cil_tmp64 ;
  unsigned char __cil_tmp65 ;
  int __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  unsigned short __cil_tmp69 ;
  int __cil_tmp70 ;
  int __cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  unsigned short __cil_tmp76 ;
  int __cil_tmp77 ;
  int __cil_tmp78 ;
  unsigned long __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  unsigned int __cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  unsigned int __cil_tmp84 ;
  unsigned long __cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  int __cil_tmp87 ;
  unsigned int __cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  unsigned long __cil_tmp90 ;
  unsigned int __cil_tmp91 ;
  unsigned char __cil_tmp92 ;
  int __cil_tmp93 ;
  int __cil_tmp94 ;
  unsigned long __cil_tmp95 ;
  unsigned long __cil_tmp96 ;
  unsigned long __cil_tmp97 ;
  unsigned long __cil_tmp98 ;
  unsigned long __cil_tmp99 ;
  unsigned long __cil_tmp100 ;
  unsigned char __cil_tmp101 ;
  int __cil_tmp102 ;
  unsigned int __cil_tmp103 ;
  unsigned long __cil_tmp104 ;
  unsigned long __cil_tmp105 ;
  unsigned int __cil_tmp106 ;
  unsigned long __cil_tmp107 ;
  unsigned long __cil_tmp108 ;
  unsigned long __cil_tmp109 ;
  unsigned long __cil_tmp110 ;
  unsigned char __cil_tmp111 ;
  int __cil_tmp112 ;
  unsigned long __cil_tmp113 ;
  unsigned long __cil_tmp114 ;
  unsigned short __cil_tmp115 ;
  int __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  unsigned short *__cil_tmp119 ;
  unsigned short *__cil_tmp120 ;
  unsigned short __cil_tmp121 ;
  int __cil_tmp122 ;
  unsigned long __cil_tmp123 ;
  unsigned long __cil_tmp124 ;
  unsigned long __cil_tmp125 ;
  unsigned long __cil_tmp126 ;
  unsigned char __cil_tmp127 ;
  int __cil_tmp128 ;
  unsigned long __cil_tmp129 ;
  unsigned long __cil_tmp130 ;
  struct bsd_dict *__cil_tmp131 ;
  unsigned long __cil_tmp132 ;
  unsigned long __cil_tmp133 ;
  unsigned short __cil_tmp134 ;
  unsigned long __cil_tmp135 ;
  unsigned long __cil_tmp136 ;
  struct bsd_dict *__cil_tmp137 ;
  unsigned long __cil_tmp138 ;
  unsigned long __cil_tmp139 ;
  unsigned long __cil_tmp140 ;
  unsigned long __cil_tmp141 ;
  unsigned short __cil_tmp142 ;
  unsigned long __cil_tmp143 ;
  unsigned long __cil_tmp144 ;
  unsigned int __cil_tmp145 ;
  unsigned long __cil_tmp146 ;
  unsigned long __cil_tmp147 ;
  unsigned long __cil_tmp148 ;
  unsigned long __cil_tmp149 ;
  unsigned long __cil_tmp150 ;
  unsigned long __cil_tmp151 ;
  unsigned char __cil_tmp152 ;
  int __cil_tmp153 ;
  unsigned long __cil_tmp154 ;
  unsigned long __cil_tmp155 ;
  unsigned long __cil_tmp156 ;
  unsigned long __cil_tmp157 ;
  unsigned long __cil_tmp158 ;
  struct bsd_dict *__cil_tmp159 ;
  unsigned long __cil_tmp160 ;
  unsigned long __cil_tmp161 ;
  unsigned short __cil_tmp162 ;
  unsigned int __cil_tmp163 ;
  unsigned long __cil_tmp164 ;
  unsigned long __cil_tmp165 ;
  unsigned int __cil_tmp166 ;
  unsigned int __cil_tmp167 ;
  unsigned long __cil_tmp168 ;
  unsigned long __cil_tmp169 ;
  unsigned int __cil_tmp170 ;
  unsigned int __cil_tmp171 ;
  unsigned int __cil_tmp172 ;
  unsigned long __cil_tmp173 ;
  unsigned long __cil_tmp174 ;
  struct bsd_dict *__cil_tmp175 ;
  unsigned long __cil_tmp176 ;
  unsigned long __cil_tmp177 ;
  unsigned short __cil_tmp178 ;
  unsigned int __cil_tmp179 ;
  unsigned int __cil_tmp180 ;
  unsigned long __cil_tmp181 ;
  unsigned long __cil_tmp182 ;
  struct bsd_dict *__cil_tmp183 ;
  unsigned long __cil_tmp184 ;
  unsigned long __cil_tmp185 ;
  unsigned short __cil_tmp186 ;
  unsigned long __cil_tmp187 ;
  unsigned long __cil_tmp188 ;
  struct bsd_dict *__cil_tmp189 ;
  unsigned long __cil_tmp190 ;
  unsigned long __cil_tmp191 ;
  unsigned short __cil_tmp192 ;
  unsigned int __cil_tmp193 ;
  unsigned long __cil_tmp194 ;
  unsigned long __cil_tmp195 ;
  int __cil_tmp196 ;
  int __cil_tmp197 ;
  unsigned long __cil_tmp198 ;
  unsigned long __cil_tmp199 ;
  unsigned long __cil_tmp200 ;
  unsigned long __cil_tmp201 ;
  unsigned long __cil_tmp202 ;
  unsigned long __cil_tmp203 ;
  unsigned long __cil_tmp204 ;
  unsigned long __cil_tmp205 ;
  unsigned short *__cil_tmp206 ;
  unsigned long __cil_tmp207 ;
  unsigned long __cil_tmp208 ;
  unsigned short *__cil_tmp209 ;
  unsigned short __cil_tmp210 ;
  int __cil_tmp211 ;
  int __cil_tmp212 ;
  int __cil_tmp213 ;
  int __cil_tmp214 ;
  unsigned int __cil_tmp215 ;
  unsigned long __cil_tmp216 ;
  unsigned long __cil_tmp217 ;
  unsigned int __cil_tmp218 ;
  unsigned long __cil_tmp219 ;
  unsigned long __cil_tmp220 ;
  unsigned long __cil_tmp221 ;
  unsigned long __cil_tmp222 ;
  unsigned long __cil_tmp223 ;
  unsigned long __cil_tmp224 ;
  unsigned int __cil_tmp225 ;
  unsigned long __cil_tmp226 ;
  unsigned long __cil_tmp227 ;
  unsigned long __cil_tmp228 ;
  unsigned long __cil_tmp229 ;
  unsigned int __cil_tmp230 ;
  unsigned long __cil_tmp231 ;
  unsigned long __cil_tmp232 ;
  int __cil_tmp233 ;
  int __cil_tmp234 ;
  unsigned int __cil_tmp235 ;
  unsigned long __cil_tmp236 ;
  unsigned long __cil_tmp237 ;
  unsigned int __cil_tmp238 ;
  unsigned long __cil_tmp239 ;
  unsigned long __cil_tmp240 ;
  unsigned int __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 char __cil_tmp249 ;
  int __cil_tmp250 ;
  unsigned long __cil_tmp251 ;
  unsigned long __cil_tmp252 ;
  unsigned short __cil_tmp253 ;
  int __cil_tmp254 ;
  int __cil_tmp255 ;

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

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

  }
  }
#line 886
  __cil_tmp72 = (unsigned long )db;
#line 886
  __cil_tmp73 = __cil_tmp72 + 14;
#line 886
  __cil_tmp74 = (unsigned long )db;
#line 886
  __cil_tmp75 = __cil_tmp74 + 14;
#line 886
  __cil_tmp76 = *((unsigned short *)__cil_tmp75);
#line 886
  __cil_tmp77 = (int )__cil_tmp76;
#line 886
  __cil_tmp78 = __cil_tmp77 + 1;
#line 886
  *((unsigned short *)__cil_tmp73) = (unsigned short )__cil_tmp78;
#line 887
  __cil_tmp79 = (unsigned long )db;
#line 887
  __cil_tmp80 = __cil_tmp79 + 32;
#line 887
  __cil_tmp81 = (unsigned int )ilen;
#line 887
  __cil_tmp82 = (unsigned long )db;
#line 887
  __cil_tmp83 = __cil_tmp82 + 32;
#line 887
  __cil_tmp84 = *((unsigned int *)__cil_tmp83);
#line 887
  *((unsigned int *)__cil_tmp80) = __cil_tmp84 + __cil_tmp81;
#line 894
  wptr = obuf;
#line 895
  tmp = wptr;
#line 895
  wptr = wptr + 1;
#line 895
  *tmp = (unsigned char )adrs;
#line 896
  tmp___0 = wptr;
#line 896
  wptr = wptr + 1;
#line 896
  *tmp___0 = (unsigned char )ctrl;
#line 897
  tmp___1 = wptr;
#line 897
  wptr = wptr + 1;
#line 897
  *tmp___1 = (unsigned char)0;
#line 899
  oldcode = 256U;
#line 900
  explen = 3;
  {
#line 907
  while (1) {
    while_continue: /* CIL Label */ ;
#line 909
    tmp___2 = ilen;
#line 909
    ilen = ilen - 1;
#line 909
    if (tmp___2 <= 0) {
#line 911
      __cil_tmp85 = (unsigned long )db;
#line 911
      __cil_tmp86 = __cil_tmp85 + 28;
#line 911
      __cil_tmp87 = explen - 3;
#line 911
      __cil_tmp88 = (unsigned int )__cil_tmp87;
#line 911
      __cil_tmp89 = (unsigned long )db;
#line 911
      __cil_tmp90 = __cil_tmp89 + 28;
#line 911
      __cil_tmp91 = *((unsigned int *)__cil_tmp90);
#line 911
      *((unsigned int *)__cil_tmp86) = __cil_tmp91 + __cil_tmp88;
#line 912
      goto while_break;
    } else {

    }
#line 921
    bitno = bitno - 8U;
#line 922
    tmp___3 = ibuf;
#line 922
    ibuf = ibuf + 1;
#line 922
    __cil_tmp92 = *tmp___3;
#line 922
    __cil_tmp93 = (int )__cil_tmp92;
#line 922
    __cil_tmp94 = __cil_tmp93 << bitno;
#line 922
    __cil_tmp95 = (unsigned long )__cil_tmp94;
#line 922
    accm = accm | __cil_tmp95;
#line 923
    if (tgtbitno < bitno) {
#line 925
      goto __Cont;
    } else {

    }
#line 928
    __cil_tmp96 = accm >> tgtbitno;
#line 928
    incode = (unsigned int )__cil_tmp96;
#line 929
    accm = accm << n_bits;
#line 930
    bitno = bitno + n_bits;
#line 936
    if (incode == 256U) {
#line 938
      if (ilen > 0) {
        {
#line 940
        __cil_tmp97 = (unsigned long )db;
#line 940
        __cil_tmp98 = __cil_tmp97 + 11;
#line 940
        if (*((unsigned char *)__cil_tmp98)) {
          {
#line 942
          __cil_tmp99 = (unsigned long )db;
#line 942
          __cil_tmp100 = __cil_tmp99 + 12;
#line 942
          __cil_tmp101 = *((unsigned char *)__cil_tmp100);
#line 942
          __cil_tmp102 = (int )__cil_tmp101;
#line 942
          printk("bsd_decomp%d: bad CLEAR\n", __cil_tmp102);
          }
        } else {

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

      }
      {
#line 947
      bsd_clear(db);
      }
#line 948
      goto while_break;
    } else {

    }
    {
#line 951
    __cil_tmp103 = max_ent + 2U;
#line 951
    if (incode > __cil_tmp103) {
#line 951
      goto _L;
    } else {
      {
#line 951
      __cil_tmp104 = (unsigned long )db;
#line 951
      __cil_tmp105 = __cil_tmp104 + 20;
#line 951
      __cil_tmp106 = *((unsigned int *)__cil_tmp105);
#line 951
      if (incode > __cil_tmp106) {
#line 951
        goto _L;
      } else
#line 951
      if (incode > max_ent) {
#line 951
        if (oldcode == 256U) {
          _L: /* CIL Label */ 
          {
#line 954
          __cil_tmp107 = (unsigned long )db;
#line 954
          __cil_tmp108 = __cil_tmp107 + 11;
#line 954
          if (*((unsigned char *)__cil_tmp108)) {
            {
#line 956
            __cil_tmp109 = (unsigned long )db;
#line 956
            __cil_tmp110 = __cil_tmp109 + 12;
#line 956
            __cil_tmp111 = *((unsigned char *)__cil_tmp110);
#line 956
            __cil_tmp112 = (int )__cil_tmp111;
#line 956
            printk("bsd_decomp%d: bad code 0x%x oldcode=0x%x ", __cil_tmp112, incode,
                   oldcode);
#line 958
            __cil_tmp113 = (unsigned long )db;
#line 958
            __cil_tmp114 = __cil_tmp113 + 14;
#line 958
            __cil_tmp115 = *((unsigned short *)__cil_tmp114);
#line 958
            __cil_tmp116 = (int )__cil_tmp115;
#line 958
            printk("max_ent=0x%x explen=%d seqno=%d\n", max_ent, explen, __cil_tmp116);
            }
          } else {

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

        }
      } else {

      }
      }
    }
    }
#line 965
    if (incode > max_ent) {
#line 967
      finchar = oldcode;
#line 968
      extra = 1;
    } else {
#line 972
      finchar = incode;
#line 973
      extra = 0;
    }
#line 976
    __cil_tmp117 = (unsigned long )db;
#line 976
    __cil_tmp118 = __cil_tmp117 + 72;
#line 976
    __cil_tmp119 = *((unsigned short **)__cil_tmp118);
#line 976
    __cil_tmp120 = __cil_tmp119 + finchar;
#line 976
    __cil_tmp121 = *__cil_tmp120;
#line 976
    codelen = (int )__cil_tmp121;
#line 977
    __cil_tmp122 = codelen + extra;
#line 977
    explen = explen + __cil_tmp122;
#line 978
    if (explen > osize) {
      {
#line 980
      __cil_tmp123 = (unsigned long )db;
#line 980
      __cil_tmp124 = __cil_tmp123 + 11;
#line 980
      if (*((unsigned char *)__cil_tmp124)) {
        {
#line 982
        __cil_tmp125 = (unsigned long )db;
#line 982
        __cil_tmp126 = __cil_tmp125 + 12;
#line 982
        __cil_tmp127 = *((unsigned char *)__cil_tmp126);
#line 982
        __cil_tmp128 = (int )__cil_tmp127;
#line 982
        printk("bsd_decomp%d: ran out of mru\n", __cil_tmp128);
        }
      } else {

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

    }
#line 995
    wptr = wptr + codelen;
#line 996
    p = wptr;
    {
#line 997
    while (1) {
      while_continue___0: /* CIL Label */ ;
#line 997
      if (finchar > 255U) {

      } else {
#line 997
        goto while_break___0;
      }
#line 999
      __cil_tmp129 = (unsigned long )db;
#line 999
      __cil_tmp130 = __cil_tmp129 + 80;
#line 999
      __cil_tmp131 = *((struct bsd_dict **)__cil_tmp130);
#line 999
      dictp2 = __cil_tmp131 + finchar;
#line 1001
      __cil_tmp132 = (unsigned long )dictp2;
#line 1001
      __cil_tmp133 = __cil_tmp132 + 10;
#line 1001
      __cil_tmp134 = *((unsigned short *)__cil_tmp133);
#line 1001
      __cil_tmp135 = (unsigned long )db;
#line 1001
      __cil_tmp136 = __cil_tmp135 + 80;
#line 1001
      __cil_tmp137 = *((struct bsd_dict **)__cil_tmp136);
#line 1001
      dictp = __cil_tmp137 + __cil_tmp134;
#line 1026
      p = p - 1;
#line 1026
      __cil_tmp138 = 0 + 2;
#line 1026
      __cil_tmp139 = 0 + __cil_tmp138;
#line 1026
      __cil_tmp140 = (unsigned long )dictp;
#line 1026
      __cil_tmp141 = __cil_tmp140 + __cil_tmp139;
#line 1026
      *p = *((unsigned char *)__cil_tmp141);
#line 1027
      __cil_tmp142 = *((unsigned short *)dictp);
#line 1027
      finchar = (unsigned int )__cil_tmp142;
    }
    while_break___0: /* CIL Label */ ;
    }
#line 1029
    p = p - 1;
#line 1029
    *p = (unsigned char )finchar;
#line 1039
    if (extra) {
#line 1041
      tmp___4 = wptr;
#line 1041
      wptr = wptr + 1;
#line 1041
      *tmp___4 = (unsigned char )finchar;
    } else {

    }
#line 1052
    if (oldcode != 256U) {
      {
#line 1052
      __cil_tmp143 = (unsigned long )db;
#line 1052
      __cil_tmp144 = __cil_tmp143 + 20;
#line 1052
      __cil_tmp145 = *((unsigned int *)__cil_tmp144);
#line 1052
      if (max_ent < __cil_tmp145) {
#line 1059
        __cil_tmp146 = (unsigned long )oldcode;
#line 1059
        __cil_tmp147 = (unsigned long )finchar;
#line 1059
        __cil_tmp148 = __cil_tmp147 << 16;
#line 1059
        fcode = __cil_tmp148 + __cil_tmp146;
#line 1060
        __cil_tmp149 = (unsigned long )oldcode;
#line 1060
        __cil_tmp150 = (unsigned long )db;
#line 1060
        __cil_tmp151 = __cil_tmp150 + 8;
#line 1060
        __cil_tmp152 = *((unsigned char *)__cil_tmp151);
#line 1060
        __cil_tmp153 = (int )__cil_tmp152;
#line 1060
        __cil_tmp154 = (unsigned long )finchar;
#line 1060
        __cil_tmp155 = __cil_tmp154 << __cil_tmp153;
#line 1060
        __cil_tmp156 = __cil_tmp155 ^ __cil_tmp149;
#line 1060
        hval = (int )__cil_tmp156;
#line 1061
        __cil_tmp157 = (unsigned long )db;
#line 1061
        __cil_tmp158 = __cil_tmp157 + 80;
#line 1061
        __cil_tmp159 = *((struct bsd_dict **)__cil_tmp158);
#line 1061
        dictp = __cil_tmp159 + hval;
        {
#line 1064
        __cil_tmp160 = (unsigned long )dictp;
#line 1064
        __cil_tmp161 = __cil_tmp160 + 8;
#line 1064
        __cil_tmp162 = *((unsigned short *)__cil_tmp161);
#line 1064
        __cil_tmp163 = (unsigned int )__cil_tmp162;
#line 1064
        if (__cil_tmp163 < max_ent) {
#line 1066
          if (hval == 0) {
#line 1066
            disp = 1;
          } else {
#line 1066
            disp = hval;
          }
          {
#line 1067
          while (1) {
            while_continue___1: /* CIL Label */ ;
#line 1069
            hval = hval + disp;
            {
#line 1070
            __cil_tmp164 = (unsigned long )db;
#line 1070
            __cil_tmp165 = __cil_tmp164 + 4;
#line 1070
            __cil_tmp166 = *((unsigned int *)__cil_tmp165);
#line 1070
            __cil_tmp167 = (unsigned int )hval;
#line 1070
            if (__cil_tmp167 >= __cil_tmp166) {
#line 1072
              __cil_tmp168 = (unsigned long )db;
#line 1072
              __cil_tmp169 = __cil_tmp168 + 4;
#line 1072
              __cil_tmp170 = *((unsigned int *)__cil_tmp169);
#line 1072
              __cil_tmp171 = (unsigned int )hval;
#line 1072
              __cil_tmp172 = __cil_tmp171 - __cil_tmp170;
#line 1072
              hval = (int )__cil_tmp172;
            } else {

            }
            }
#line 1074
            __cil_tmp173 = (unsigned long )db;
#line 1074
            __cil_tmp174 = __cil_tmp173 + 80;
#line 1074
            __cil_tmp175 = *((struct bsd_dict **)__cil_tmp174);
#line 1074
            dictp = __cil_tmp175 + hval;
            {
#line 1067
            __cil_tmp176 = (unsigned long )dictp;
#line 1067
            __cil_tmp177 = __cil_tmp176 + 8;
#line 1067
            __cil_tmp178 = *((unsigned short *)__cil_tmp177);
#line 1067
            __cil_tmp179 = (unsigned int )__cil_tmp178;
#line 1067
            if (__cil_tmp179 < max_ent) {

            } else {
#line 1067
              goto while_break___1;
            }
            }
          }
          while_break___1: /* CIL Label */ ;
          }
        } else {

        }
        }
#line 1084
        __cil_tmp180 = max_ent + 1U;
#line 1084
        __cil_tmp181 = (unsigned long )db;
#line 1084
        __cil_tmp182 = __cil_tmp181 + 80;
#line 1084
        __cil_tmp183 = *((struct bsd_dict **)__cil_tmp182);
#line 1084
        dictp2___0 = __cil_tmp183 + __cil_tmp180;
#line 1085
        __cil_tmp184 = (unsigned long )dictp2___0;
#line 1085
        __cil_tmp185 = __cil_tmp184 + 10;
#line 1085
        __cil_tmp186 = *((unsigned short *)__cil_tmp185);
#line 1085
        indx = (int )__cil_tmp186;
#line 1086
        __cil_tmp187 = (unsigned long )db;
#line 1086
        __cil_tmp188 = __cil_tmp187 + 80;
#line 1086
        __cil_tmp189 = *((struct bsd_dict **)__cil_tmp188);
#line 1086
        dictp3 = __cil_tmp189 + indx;
        {
#line 1088
        __cil_tmp190 = (unsigned long )dictp3;
#line 1088
        __cil_tmp191 = __cil_tmp190 + 8;
#line 1088
        __cil_tmp192 = *((unsigned short *)__cil_tmp191);
#line 1088
        __cil_tmp193 = (unsigned int )__cil_tmp192;
#line 1088
        if (__cil_tmp193 == max_ent) {
#line 1090
          __cil_tmp194 = (unsigned long )dictp3;
#line 1090
          __cil_tmp195 = __cil_tmp194 + 8;
#line 1090
          __cil_tmp196 = 1 << 15;
#line 1090
          __cil_tmp197 = __cil_tmp196 - 1;
#line 1090
          *((unsigned short *)__cil_tmp195) = (unsigned short )__cil_tmp197;
        } else {

        }
        }
#line 1093
        __cil_tmp198 = (unsigned long )dictp2___0;
#line 1093
        __cil_tmp199 = __cil_tmp198 + 10;
#line 1093
        *((unsigned short *)__cil_tmp199) = (unsigned short )hval;
#line 1094
        __cil_tmp200 = (unsigned long )dictp;
#line 1094
        __cil_tmp201 = __cil_tmp200 + 8;
#line 1094
        *((unsigned short *)__cil_tmp201) = (unsigned short )max_ent;
#line 1095
        *((unsigned long *)dictp) = fcode;
#line 1096
        max_ent = max_ent + 1U;
#line 1096
        __cil_tmp202 = (unsigned long )db;
#line 1096
        __cil_tmp203 = __cil_tmp202 + 24;
#line 1096
        *((unsigned int *)__cil_tmp203) = max_ent;
#line 1099
        __cil_tmp204 = (unsigned long )db;
#line 1099
        __cil_tmp205 = __cil_tmp204 + 72;
#line 1099
        __cil_tmp206 = *((unsigned short **)__cil_tmp205);
#line 1099
        lens1 = __cil_tmp206 + max_ent;
#line 1100
        __cil_tmp207 = (unsigned long )db;
#line 1100
        __cil_tmp208 = __cil_tmp207 + 72;
#line 1100
        __cil_tmp209 = *((unsigned short **)__cil_tmp208);
#line 1100
        lens2 = __cil_tmp209 + oldcode;
#line 1101
        __cil_tmp210 = *lens2;
#line 1101
        __cil_tmp211 = (int )__cil_tmp210;
#line 1101
        __cil_tmp212 = __cil_tmp211 + 1;
#line 1101
        *lens1 = (unsigned short )__cil_tmp212;
        {
#line 1104
        __cil_tmp213 = 1 << n_bits;
#line 1104
        __cil_tmp214 = __cil_tmp213 - 1;
#line 1104
        __cil_tmp215 = (unsigned int )__cil_tmp214;
#line 1104
        if (max_ent >= __cil_tmp215) {
          {
#line 1104
          __cil_tmp216 = (unsigned long )db;
#line 1104
          __cil_tmp217 = __cil_tmp216 + 20;
#line 1104
          __cil_tmp218 = *((unsigned int *)__cil_tmp217);
#line 1104
          if (max_ent < __cil_tmp218) {
#line 1106
            n_bits = n_bits + 1U;
#line 1106
            __cil_tmp219 = (unsigned long )db;
#line 1106
            __cil_tmp220 = __cil_tmp219 + 9;
#line 1106
            *((unsigned char *)__cil_tmp220) = (unsigned char )n_bits;
#line 1107
            tgtbitno = 32U - n_bits;
          } else {

          }
          }
        } else {

        }
        }
      } else {

      }
      }
    } else {

    }
#line 1110
    oldcode = incode;
    __Cont: /* CIL Label */ ;
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 1113
  __cil_tmp221 = (unsigned long )db;
#line 1113
  __cil_tmp222 = __cil_tmp221 + 64;
#line 1113
  __cil_tmp223 = (unsigned long )db;
#line 1113
  __cil_tmp224 = __cil_tmp223 + 64;
#line 1113
  __cil_tmp225 = *((unsigned int *)__cil_tmp224);
#line 1113
  *((unsigned int *)__cil_tmp222) = __cil_tmp225 + 1U;
#line 1114
  __cil_tmp226 = (unsigned long )db;
#line 1114
  __cil_tmp227 = __cil_tmp226 + 56;
#line 1114
  __cil_tmp228 = (unsigned long )db;
#line 1114
  __cil_tmp229 = __cil_tmp228 + 56;
#line 1114
  __cil_tmp230 = *((unsigned int *)__cil_tmp229);
#line 1114
  *((unsigned int *)__cil_tmp227) = __cil_tmp230 + 1U;
#line 1115
  __cil_tmp231 = (unsigned long )db;
#line 1115
  __cil_tmp232 = __cil_tmp231 + 68;
#line 1115
  __cil_tmp233 = isize - 2;
#line 1115
  __cil_tmp234 = __cil_tmp233 - 4;
#line 1115
  __cil_tmp235 = (unsigned int )__cil_tmp234;
#line 1115
  __cil_tmp236 = (unsigned long )db;
#line 1115
  __cil_tmp237 = __cil_tmp236 + 68;
#line 1115
  __cil_tmp238 = *((unsigned int *)__cil_tmp237);
#line 1115
  *((unsigned int *)__cil_tmp232) = __cil_tmp238 + __cil_tmp235;
#line 1116
  __cil_tmp239 = (unsigned long )db;
#line 1116
  __cil_tmp240 = __cil_tmp239 + 60;
#line 1116
  __cil_tmp241 = (unsigned int )explen;
#line 1116
  __cil_tmp242 = (unsigned long )db;
#line 1116
  __cil_tmp243 = __cil_tmp242 + 60;
#line 1116
  __cil_tmp244 = *((unsigned int *)__cil_tmp243);
#line 1116
  *((unsigned int *)__cil_tmp240) = __cil_tmp244 + __cil_tmp241;
#line 1118
  tmp___5 = bsd_check(db);
  }
#line 1118
  if (tmp___5) {
    {
#line 1120
    __cil_tmp245 = (unsigned long )db;
#line 1120
    __cil_tmp246 = __cil_tmp245 + 11;
#line 1120
    if (*((unsigned char *)__cil_tmp246)) {
      {
#line 1122
      __cil_tmp247 = (unsigned long )db;
#line 1122
      __cil_tmp248 = __cil_tmp247 + 12;
#line 1122
      __cil_tmp249 = *((unsigned char *)__cil_tmp248);
#line 1122
      __cil_tmp250 = (int )__cil_tmp249;
#line 1122
      __cil_tmp251 = (unsigned long )db;
#line 1122
      __cil_tmp252 = __cil_tmp251 + 14;
#line 1122
      __cil_tmp253 = *((unsigned short *)__cil_tmp252);
#line 1122
      __cil_tmp254 = (int )__cil_tmp253;
#line 1122
      __cil_tmp255 = __cil_tmp254 - 1;
#line 1122
      printk("bsd_decomp%d: peer should have cleared dictionary on %d\n", __cil_tmp250,
             __cil_tmp255);
      }
    } else {

    }
    }
  } else {

  }
#line 1126
  return (explen);
}
}
#line 1133 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static struct compressor ppp_bsd_compress  = 
#line 1133
     {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 1155
static int bsdcomp_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
#line 1155 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static int bsdcomp_init(void) 
{ int answer ;
  int tmp ;

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

  }
#line 1160
  return (answer);
}
}
#line 1163
static void bsdcomp_cleanup(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
#line 1163 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static void bsdcomp_cleanup(void) 
{ 

  {
  {
#line 1165
  ppp_unregister_compressor(& ppp_bsd_compress);
  }
#line 1166
  return;
}
}
#line 1168 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
int init_module(void) 
{ int tmp ;

  {
  {
#line 1168
  tmp = bsdcomp_init();
  }
#line 1168
  return (tmp);
}
}
#line 1169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
void cleanup_module(void) 
{ 

  {
  {
#line 1169
  bsdcomp_cleanup();
  }
#line 1169
  return;
}
}
#line 1170 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static char const   __mod_license1170[21]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 1170
  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
        (char const   )'D',      (char const   )'u',      (char const   )'a',      (char const   )'l', 
        (char const   )' ',      (char const   )'B',      (char const   )'S',      (char const   )'D', 
        (char const   )'/',      (char const   )'G',      (char const   )'P',      (char const   )'L', 
        (char const   )'\000'};
#line 1171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
static char const   __mod_alias1171[22]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 1171
  {      (char const   )'a',      (char const   )'l',      (char const   )'i',      (char const   )'a', 
        (char const   )'s',      (char const   )'=',      (char const   )'p',      (char const   )'p', 
        (char const   )'p',      (char const   )'-',      (char const   )'c',      (char const   )'o', 
        (char const   )'m',      (char const   )'p',      (char const   )'r',      (char const   )'e', 
        (char const   )'s',      (char const   )'s',      (char const   )'-',      (char const   )'2', 
        (char const   )'1',      (char const   )'\000'};
#line 1189
void ldv_check_final_state(void) ;
#line 1195
extern void ldv_initialize(void) ;
#line 1198
extern int __VERIFIER_nondet_int(void) ;
#line 1201 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
int LDV_IN_INTERRUPT  ;
#line 1204 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
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 1992
  LDV_IN_INTERRUPT = 1;
#line 2001
  ldv_initialize();
#line 2077
  tmp = bsdcomp_init();
  }
#line 2077
  if (tmp) {
#line 2078
    goto ldv_final;
  } else {

  }
  {
#line 2082
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 2082
    tmp___1 = __VERIFIER_nondet_int();
    }
#line 2082
    if (tmp___1) {

    } else {
#line 2082
      goto while_break;
    }
    {
#line 2085
    tmp___0 = __VERIFIER_nondet_int();
    }
#line 2087
    if (tmp___0 == 0) {
#line 2087
      goto case_0;
    } else
#line 2175
    if (tmp___0 == 1) {
#line 2175
      goto case_1;
    } else
#line 2263
    if (tmp___0 == 2) {
#line 2263
      goto case_2;
    } else
#line 2351
    if (tmp___0 == 3) {
#line 2351
      goto case_3;
    } else
#line 2439
    if (tmp___0 == 4) {
#line 2439
      goto case_4;
    } else
#line 2501
    if (tmp___0 == 5) {
#line 2501
      goto case_5;
    } else
#line 2589
    if (tmp___0 == 6) {
#line 2589
      goto case_6;
    } else
#line 2677
    if (tmp___0 == 7) {
#line 2677
      goto case_7;
    } else
#line 2765
    if (tmp___0 == 8) {
#line 2765
      goto case_8;
    } else
#line 2845
    if (tmp___0 == 9) {
#line 2845
      goto case_9;
    } else {
      {
#line 2933
      goto switch_default;
#line 2085
      if (0) {
        case_0: /* CIL Label */ 
        {
#line 2124
        bsd_comp_alloc(var_bsd_comp_alloc_6_p0, var_bsd_comp_alloc_6_p1);
        }
#line 2174
        goto switch_break;
        case_1: /* CIL Label */ 
        {
#line 2212
        bsd_free(var_bsd_free_4_p0);
        }
#line 2262
        goto switch_break;
        case_2: /* CIL Label */ 
        {
#line 2302
        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 2350
        goto switch_break;
        case_3: /* CIL Label */ 
        {
#line 2388
        bsd_reset(var_bsd_reset_3_p0);
        }
#line 2438
        goto switch_break;
        case_4: /* CIL Label */ 
        {
#line 2485
        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 2500
        goto switch_break;
        case_5: /* CIL Label */ 
        {
#line 2538
        bsd_comp_stats(var_bsd_comp_stats_2_p0, var_group1);
        }
#line 2588
        goto switch_break;
        case_6: /* CIL Label */ 
        {
#line 2626
        bsd_decomp_alloc(var_bsd_decomp_alloc_7_p0, var_bsd_decomp_alloc_7_p1);
        }
#line 2676
        goto switch_break;
        case_7: /* CIL Label */ 
        {
#line 2716
        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 2764
        goto switch_break;
        case_8: /* CIL Label */ 
        {
#line 2837
        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 2844
        goto switch_break;
        case_9: /* CIL Label */ 
        {
#line 2917
        bsd_incomp(var_bsd_incomp_14_p0, var_bsd_incomp_14_p1, var_bsd_incomp_14_p2);
        }
#line 2932
        goto switch_break;
        switch_default: /* CIL Label */ 
#line 2933
        goto switch_break;
      } else {
        switch_break: /* CIL Label */ ;
      }
      }
    }
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 3015
  bsdcomp_cleanup();
  }
  ldv_final: 
  {
#line 3018
  ldv_check_final_state();
  }
#line 3021
  return;
}
}
#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/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--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
extern int __VERIFIER_nondet_int(void) ;
#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int ldv_mutex  =    1;
#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 29
  if (ldv_mutex == 1) {

  } else {
    {
#line 29
    ldv_blast_assert();
    }
  }
  {
#line 32
  nondetermined = __VERIFIER_nondet_int();
  }
#line 35
  if (nondetermined) {
#line 38
    ldv_mutex = 2;
#line 40
    return (0);
  } else {
#line 45
    return (-4);
  }
}
}
#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 57
  if (ldv_mutex == 1) {

  } else {
    {
#line 57
    ldv_blast_assert();
    }
  }
  {
#line 60
  nondetermined = __VERIFIER_nondet_int();
  }
#line 63
  if (nondetermined) {
#line 66
    ldv_mutex = 2;
#line 68
    return (0);
  } else {
#line 73
    return (-4);
  }
}
}
#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
{ int atomic_value_after_dec ;

  {
#line 83
  if (ldv_mutex == 1) {

  } else {
    {
#line 83
    ldv_blast_assert();
    }
  }
  {
#line 86
  atomic_value_after_dec = __VERIFIER_nondet_int();
  }
#line 89
  if (atomic_value_after_dec == 0) {
#line 92
    ldv_mutex = 2;
#line 94
    return (1);
  } else {

  }
#line 98
  return (0);
}
}
#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void mutex_lock(struct mutex *lock ) 
{ 

  {
#line 108
  if (ldv_mutex == 1) {

  } else {
    {
#line 108
    ldv_blast_assert();
    }
  }
#line 110
  ldv_mutex = 2;
#line 111
  return;
}
}
#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int mutex_trylock(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 121
  if (ldv_mutex == 1) {

  } else {
    {
#line 121
    ldv_blast_assert();
    }
  }
  {
#line 124
  nondetermined = __VERIFIER_nondet_int();
  }
#line 127
  if (nondetermined) {
#line 130
    ldv_mutex = 2;
#line 132
    return (1);
  } else {
#line 137
    return (0);
  }
}
}
#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void mutex_unlock(struct mutex *lock ) 
{ 

  {
#line 147
  if (ldv_mutex == 2) {

  } else {
    {
#line 147
    ldv_blast_assert();
    }
  }
#line 149
  ldv_mutex = 1;
#line 150
  return;
}
}
#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void ldv_check_final_state(void) 
{ 

  {
#line 156
  if (ldv_mutex == 1) {

  } else {
    {
#line 156
    ldv_blast_assert();
    }
  }
#line 157
  return;
}
}
#line 3030 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/drivers/net/ppp/bsd_comp.c.common.c"
long s__builtin_expect(long val , long res ) 
{ 

  {
#line 3031
  return (val);
}
}