ClabureDB: Classified Bug-Reports Database

   /* Generated by CIL v. 1.3.7 */
   /* print_CIL_Input is true */
   
   #line 20 "include/asm-generic/int-ll64.h"
   typedef unsigned char __u8;
   #line 23 "include/asm-generic/int-ll64.h"
   typedef unsigned short __u16;
   #line 26 "include/asm-generic/int-ll64.h"
   typedef unsigned int __u32;
  #line 30 "include/asm-generic/int-ll64.h"
  typedef unsigned long long __u64;
  #line 43 "include/asm-generic/int-ll64.h"
  typedef unsigned char u8;
  #line 45 "include/asm-generic/int-ll64.h"
  typedef short s16;
  #line 46 "include/asm-generic/int-ll64.h"
  typedef unsigned short u16;
  #line 48 "include/asm-generic/int-ll64.h"
  typedef int s32;
  #line 49 "include/asm-generic/int-ll64.h"
  typedef unsigned int u32;
  #line 51 "include/asm-generic/int-ll64.h"
  typedef long long s64;
  #line 52 "include/asm-generic/int-ll64.h"
  typedef unsigned long long u64;
  #line 14 "include/asm-generic/posix_types.h"
  typedef long __kernel_long_t;
  #line 15 "include/asm-generic/posix_types.h"
  typedef unsigned long __kernel_ulong_t;
  #line 75 "include/asm-generic/posix_types.h"
  typedef __kernel_ulong_t __kernel_size_t;
  #line 76 "include/asm-generic/posix_types.h"
  typedef __kernel_long_t __kernel_ssize_t;
  #line 27 "include/linux/types.h"
  typedef unsigned short umode_t;
  #line 63 "include/linux/types.h"
  typedef __kernel_size_t size_t;
  #line 68 "include/linux/types.h"
  typedef __kernel_ssize_t ssize_t;
  #line 94 "include/linux/types.h"
  typedef unsigned int u_int;
  #line 155 "include/linux/types.h"
  typedef u64 dma_addr_t;
  #line 179 "include/linux/types.h"
  typedef __u16 __be16;
  #line 186 "include/linux/types.h"
  typedef __u32 __wsum;
  #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 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 53 "include/linux/dynamic_debug.h"
  struct net_device;
  #line 53
  struct net_device;
  #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 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  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 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 49 "include/linux/wait.h"
 struct __wait_queue_head {
    spinlock_t lock ;
    struct list_head task_list ;
 };
 #line 53 "include/linux/wait.h"
 typedef struct __wait_queue_head wait_queue_head_t;
 #line 55
 struct task_struct;
 #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 182 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/x86_init.h"
 struct pci_dev;
 #line 182
 struct pci_dev;
 #line 46 "include/linux/ktime.h"
 union ktime {
    s64 tv64 ;
 };
 #line 59 "include/linux/ktime.h"
 typedef union ktime ktime_t;
 #line 71 "include/asm-generic/iomap.h"
 struct pci_dev;
 #line 14 "include/asm-generic/pci_iomap.h"
 struct pci_dev;
 #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 159 "include/linux/net.h"
 struct module;
 #line 10 "include/linux/textsearch.h"
 struct module;
 #line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess.h"
 struct exception_table_entry {
    unsigned long insn ;
    unsigned long fixup ;
 };
 #line 109 "include/net/checksum.h"
 struct sk_buff;
 #line 109
 struct sk_buff;
 #line 32 "include/linux/device.h"
 struct module;
 #line 8 "include/linux/debug_locks.h"
 struct task_struct;
 #line 48
 struct task_struct;
 #line 37 "include/linux/dmaengine.h"
 typedef s32 dma_cookie_t;
 #line 108 "include/linux/skbuff.h"
 struct net_device;
 #line 113 "include/linux/skbuff.h"
 struct nf_conntrack {
    atomic_t use ;
 };
 #line 119 "include/linux/skbuff.h"
 struct nf_bridge_info {
    atomic_t use ;
    struct net_device *physindev ;
    struct net_device *physoutdev ;
    unsigned int mask ;
    unsigned long data[32UL / sizeof(unsigned long )] ;
 };
 #line 128 "include/linux/skbuff.h"
 struct sk_buff_head {
    struct sk_buff *next ;
    struct sk_buff *prev ;
    __u32 qlen ;
    spinlock_t lock ;
 };
 #line 137
 struct sk_buff;
 #line 318 "include/linux/skbuff.h"
 typedef unsigned int sk_buff_data_t;
 #line 391
 struct sec_path;
 #line 391 "include/linux/skbuff.h"
 struct __anonstruct____missing_field_name_222 {
    __u16 csum_start ;
    __u16 csum_offset ;
 };
 #line 391 "include/linux/skbuff.h"
 union __anonunion____missing_field_name_221 {
    __wsum csum ;
    struct __anonstruct____missing_field_name_222 __annonCompField42 ;
 };
 #line 391 "include/linux/skbuff.h"
 union __anonunion____missing_field_name_223 {
    __u32 mark ;
    __u32 dropcount ;
    __u32 avail_size ;
 };
 #line 391 "include/linux/skbuff.h"
 struct sk_buff {
    struct sk_buff *next ;
    struct sk_buff *prev ;
    ktime_t tstamp ;
    struct sock *sk ;
    struct net_device *dev ;
    char cb[48]  __attribute__((__aligned__(8))) ;
    unsigned long _skb_refdst ;
    struct sec_path *sp ;
    unsigned int len ;
    unsigned int data_len ;
    __u16 mac_len ;
    __u16 hdr_len ;
    union __anonunion____missing_field_name_221 __annonCompField43 ;
    __u32 priority ;
    __u8 local_df : 1 ;
    __u8 cloned : 1 ;
    __u8 ip_summed : 2 ;
    __u8 nohdr : 1 ;
    __u8 nfctinfo : 3 ;
    __u8 pkt_type : 3 ;
    __u8 fclone : 2 ;
    __u8 ipvs_property : 1 ;
    __u8 peeked : 1 ;
    __u8 nf_trace : 1 ;
    __be16 protocol ;
    void (*destructor)(struct sk_buff *skb ) ;
    struct nf_conntrack *nfct ;
    struct sk_buff *nfct_reasm ;
    struct nf_bridge_info *nf_bridge ;
    int skb_iif ;
    __u32 rxhash ;
    __u16 vlan_tci ;
    __u16 tc_index ;
    __u16 tc_verd ;
    __u16 queue_mapping ;
    __u8 ndisc_nodetype : 2 ;
    __u8 ooo_okay : 1 ;
    __u8 l4_rxhash : 1 ;
    __u8 wifi_acked_valid : 1 ;
    __u8 wifi_acked : 1 ;
    __u8 no_fcs : 1 ;
    dma_cookie_t dma_cookie ;
    __u32 secmark ;
    union __anonunion____missing_field_name_223 __annonCompField44 ;
    sk_buff_data_t transport_header ;
    sk_buff_data_t network_header ;
    sk_buff_data_t mac_header ;
    sk_buff_data_t tail ;
    sk_buff_data_t end ;
    unsigned char *head ;
    unsigned char *data ;
    unsigned int truesize ;
    atomic_t users ;
 };
 #line 10 "include/linux/irqreturn.h"
 enum irqreturn {
     IRQ_NONE = 0,
     IRQ_HANDLED = 1,
     IRQ_WAKE_THREAD = 2
 } ;
 #line 16 "include/linux/irqreturn.h"
 typedef enum irqreturn irqreturn_t;
 #line 32 "include/linux/irq.h"
 struct module;
 #line 12 "include/linux/irqdesc.h"
 struct proc_dir_entry;
 #line 12
 struct proc_dir_entry;
 #line 14
 struct module;
 #line 16 "include/linux/profile.h"
 struct proc_dir_entry;
 #line 65
 struct task_struct;
 #line 132 "include/linux/hardirq.h"
 struct task_struct;
 #line 25 "include/linux/capi.h"
 struct capi_register_params {
    __u32 level3cnt ;
    __u32 datablkcnt ;
    __u32 datablklen ;
 };
 #line 25 "include/linux/capi.h"
 typedef struct capi_register_params capi_register_params;
 #line 45 "include/linux/capi.h"
 struct capi_version {
    __u32 majorversion ;
    __u32 minorversion ;
    __u32 majormanuversion ;
    __u32 minormanuversion ;
 };
 #line 45 "include/linux/capi.h"
 typedef struct capi_version capi_version;
 #line 65 "include/linux/capi.h"
 struct capi_profile {
    __u16 ncontroller ;
    __u16 nbchannel ;
    __u32 goptions ;
    __u32 support1 ;
    __u32 support2 ;
    __u32 support3 ;
    __u32 reserved[6] ;
    __u32 manu[5] ;
 };
 #line 65 "include/linux/capi.h"
 typedef struct capi_profile capi_profile;
 #line 20 "include/linux/isdn/capilli.h"
 struct capiloaddatapart {
    int user ;
    int len ;
    unsigned char *data ;
 };
 #line 20 "include/linux/isdn/capilli.h"
 typedef struct capiloaddatapart capiloaddatapart;
 #line 26 "include/linux/isdn/capilli.h"
 struct capiloaddata {
    capiloaddatapart firmware ;
    capiloaddatapart configuration ;
 };
 #line 26 "include/linux/isdn/capilli.h"
 typedef struct capiloaddata capiloaddata;
 #line 31 "include/linux/isdn/capilli.h"
 struct capicardparams {
    unsigned int port ;
    unsigned int irq ;
    int cardtype ;
    int cardnr ;
    unsigned int membase ;
 };
 #line 31 "include/linux/isdn/capilli.h"
 typedef struct capicardparams capicardparams;
 #line 39
 struct file_operations;
 #line 39 "include/linux/isdn/capilli.h"
 struct capi_ctr {
    struct module *owner ;
    void *driverdata ;
    char name[32] ;
    char *driver_name ;
    int (*load_firmware)(struct capi_ctr * , capiloaddata * ) ;
    void (*reset_ctr)(struct capi_ctr * ) ;
    void (*register_appl)(struct capi_ctr * , u16 appl , capi_register_params * ) ;
    void (*release_appl)(struct capi_ctr * , u16 appl ) ;
    u16 (*send_message)(struct capi_ctr * , struct sk_buff *skb ) ;
    char *(*procinfo)(struct capi_ctr * ) ;
    struct file_operations  const  *proc_fops ;
    u8 manu[64] ;
    capi_version version ;
    capi_profile profile ;
    u8 serial[8] ;
    unsigned long nrecvctlpkt ;
    unsigned long nrecvdatapkt ;
    unsigned long nsentctlpkt ;
    unsigned long nsentdatapkt ;
    int cnr ;
    unsigned short state ;
    int blocked ;
    int traceflag ;
    wait_queue_head_t state_wait_queue ;
    struct proc_dir_entry *procent ;
    char procfn[128] ;
 };
 #line 90 "include/linux/isdn/capilli.h"
 struct capi_driver {
    char name[32] ;
    char revision[32] ;
    int (*add_card)(struct capi_driver *driver , capicardparams *data ) ;
    struct list_head list ;
 };
 #line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 enum avmcardtype {
     avm_b1isa = 0,
     avm_b1pci = 1,
     avm_b1pcmcia = 2,
     avm_m1 = 3,
     avm_m2 = 4,
     avm_t1isa = 5,
     avm_t1pci = 6,
     avm_c4 = 7,
     avm_c2 = 8
 } ;
 #line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 struct avmcard_dmabuf {
    long size ;
    u8 *dmabuf ;
    dma_addr_t dmaaddr ;
 };
 #line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 typedef struct avmcard_dmabuf avmcard_dmabuf;
 #line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 struct avmcard_dmainfo {
    u32 recvlen ;
    avmcard_dmabuf recvbuf ;
    avmcard_dmabuf sendbuf ;
    struct sk_buff_head send_queue ;
    struct pci_dev *pcidev ;
 };
 #line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 typedef struct avmcard_dmainfo avmcard_dmainfo;
 #line 62
 struct avmcard;
 #line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 struct avmctrl_info {
    char cardname[32] ;
    int versionlen ;
    char versionbuf[1024] ;
    char *version[8] ;
    char infobuf[128] ;
    struct avmcard *card ;
    struct capi_ctr capi_ctrl ;
    struct list_head ncci_head ;
 };
 #line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 typedef struct avmctrl_info avmctrl_info;
 #line 77 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 struct avmcard {
    char name[32] ;
    spinlock_t lock ;
    unsigned int port ;
    unsigned int irq ;
    unsigned long membase ;
    enum avmcardtype cardtype ;
    unsigned char revision ;
    unsigned char class ;
    int cardnr ;
    char msgbuf[128] ;
    char databuf[2048] ;
    void *mbase ;
    u32 volatile   csr ;
    avmcard_dmainfo *dma ;
    struct avmctrl_info *ctrlinfo ;
    u_int nr_controllers ;
    u_int nlogcontr ;
    struct list_head list ;
 };
 #line 77 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 typedef struct avmcard avmcard;
 #line 1 "<compiler builtins>"
 long __builtin_expect(long val , long res ) ;
 #line 47 "include/linux/list.h"
 extern void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next ) ;
 #line 60
 __inline static void list_add(struct list_head *new , struct list_head *head )  __attribute__((__no_instrument_function__)) ;
 #line 60 "include/linux/list.h"
 __inline static void list_add(struct list_head *new , struct list_head *head ) 
 { struct list_head *__cil_tmp3 ;
 
   {
   {
 #line 62
   __cil_tmp3 = *((struct list_head **)head);
 #line 62
   __list_add(new, head, __cil_tmp3);
   }
 #line 63
   return;
 }
 }
 #line 100 "include/linux/printk.h"
 extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
 #line 320 "include/linux/kernel.h"
 extern int ( /* format attribute */  sprintf)(char *buf , char const   *fmt  , ...) ;
 #line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
 extern char *strcpy(char *dest , char const   *src ) ;
 #line 30 "include/linux/string.h"
 extern size_t strlcpy(char * , char const   * , size_t  ) ;
 #line 57
 extern char *strchr(char const   * , int  ) ;
 #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 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
 __inline static void outb(unsigned char value , int port )  __attribute__((__no_instrument_function__)) ;
 #line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
 __inline static void outb(unsigned char value , int port ) 
 { 
 
   {
 #line 308
   __asm__  volatile   ("out"
                        "b"
                        " %"
                        "b"
                        "0, %w1": : "a" (value), "Nd" (port));
 #line 308
   return;
 }
 }
 #line 308
 __inline static unsigned char inb(int port )  __attribute__((__no_instrument_function__)) ;
 #line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
 __inline static unsigned char inb(int port ) 
 { unsigned char value ;
 
   {
 #line 308
   __asm__  volatile   ("in"
                        "b"
                        " %w1, %"
                        "b"
                        "0": "=a" (value): "Nd" (port));
 #line 308
   return (value);
 }
 }
 #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 10 "include/asm-generic/delay.h"
 extern void __const_udelay(unsigned long xloops ) ;
 #line 126 "include/linux/interrupt.h"
 extern int __attribute__((__warn_unused_result__))  request_threaded_irq(unsigned int irq ,
                                                                          irqreturn_t (*handler)(int  ,
                                                                                                 void * ) ,
                                                                          irqreturn_t (*thread_fn)(int  ,
                                                                                                   void * ) ,
                                                                          unsigned long flags ,
                                                                          char const   *name ,
                                                                          void *dev ) ;
 #line 131
 __inline static int __attribute__((__warn_unused_result__))  request_irq(unsigned int irq ,
                                                                          irqreturn_t (*handler)(int  ,
                                                                                                 void * ) ,
                                                                          unsigned long flags ,
                                                                          char const   *name ,
                                                                          void *dev )  __attribute__((__no_instrument_function__)) ;
 #line 131 "include/linux/interrupt.h"
 __inline static int __attribute__((__warn_unused_result__))  request_irq(unsigned int irq ,
                                                                          irqreturn_t (*handler)(int  ,
                                                                                                 void * ) ,
                                                                          unsigned long flags ,
                                                                          char const   *name ,
                                                                          void *dev ) 
 { int tmp ;
   void *__cil_tmp7 ;
   irqreturn_t (*__cil_tmp8)(int  , void * ) ;
 
   {
   {
 #line 135
   __cil_tmp7 = (void *)0;
 #line 135
   __cil_tmp8 = (irqreturn_t (*)(int  , void * ))__cil_tmp7;
 #line 135
   tmp = (int )request_threaded_irq(irq, handler, __cil_tmp8, flags, name, dev);
   }
 #line 135
   return (tmp);
 }
 }
 #line 184
 extern void free_irq(unsigned int  , void * ) ;
 #line 16 "include/linux/b1pcmcia.h"
 int b1pcmcia_addcard_b1(unsigned int port , unsigned int irq ) ;
 #line 17
 int b1pcmcia_addcard_m1(unsigned int port , unsigned int irq ) ;
 #line 18
 int b1pcmcia_addcard_m2(unsigned int port , unsigned int irq ) ;
 #line 19
 int b1pcmcia_delcard(unsigned int port , unsigned int irq ) ;
 #line 78 "include/linux/isdn/capilli.h"
 extern int attach_capi_ctr(struct capi_ctr * ) ;
 #line 79
 extern int detach_capi_ctr(struct capi_ctr * ) ;
 #line 100
 extern void register_capi_driver(struct capi_driver *driver ) ;
 #line 101
 extern void unregister_capi_driver(struct capi_driver *driver ) ;
 #line 219 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 __inline static unsigned char b1outp(unsigned int base , unsigned short offset , unsigned char value )  __attribute__((__no_instrument_function__)) ;
 #line 219 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 __inline static unsigned char b1outp(unsigned int base , unsigned short offset , unsigned char value ) 
 { unsigned char tmp ;
   unsigned int __cil_tmp5 ;
   unsigned int __cil_tmp6 ;
   int __cil_tmp7 ;
   unsigned int __cil_tmp8 ;
   int __cil_tmp9 ;
 
   {
   {
 #line 223
   __cil_tmp5 = (unsigned int )offset;
 #line 223
   __cil_tmp6 = base + __cil_tmp5;
 #line 223
   __cil_tmp7 = (int )__cil_tmp6;
 #line 223
   outb(value, __cil_tmp7);
 #line 224
   __cil_tmp8 = base + 4U;
 #line 224
   __cil_tmp9 = (int )__cil_tmp8;
 #line 224
   tmp = inb(__cil_tmp9);
   }
 #line 224
   return (tmp);
 }
 }
 #line 318
 __inline static void b1_reset(unsigned int base )  __attribute__((__no_instrument_function__)) ;
 #line 318 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 __inline static void b1_reset(unsigned int base ) 
 { unsigned long __ms ;
   unsigned long tmp ;
   unsigned long __ms___0 ;
   unsigned long tmp___0 ;
   unsigned long __ms___1 ;
   unsigned long tmp___1 ;
 
   {
   {
 #line 320
   b1outp(base, (unsigned short)16, (unsigned char)0);
 #line 321
   __ms = 110UL;
   }
   {
 #line 321
   while (1) {
     while_continue: /* CIL Label */ ;
 #line 321
     tmp = __ms;
 #line 321
     __ms = __ms - 1UL;
 #line 321
     if (tmp) {
 
     } else {
 #line 321
       goto while_break;
     }
     {
 #line 321
     __const_udelay(4295000UL);
     }
   }
   while_break: /* CIL Label */ ;
   }
   {
 #line 323
   b1outp(base, (unsigned short)16, (unsigned char)1);
 #line 324
   __ms___0 = 110UL;
   }
   {
 #line 324
   while (1) {
     while_continue___0: /* CIL Label */ ;
 #line 324
    tmp___0 = __ms___0;
#line 324
    __ms___0 = __ms___0 - 1UL;
#line 324
    if (tmp___0) {

    } else {
#line 324
      goto while_break___0;
    }
    {
#line 324
    __const_udelay(4295000UL);
    }
  }
  while_break___0: /* CIL Label */ ;
  }
  {
#line 326
  b1outp(base, (unsigned short)16, (unsigned char)0);
#line 327
  __ms___1 = 110UL;
  }
  {
#line 327
  while (1) {
    while_continue___1: /* CIL Label */ ;
#line 327
    tmp___1 = __ms___1;
#line 327
    __ms___1 = __ms___1 - 1UL;
#line 327
    if (tmp___1) {

    } else {
#line 327
      goto while_break___1;
    }
    {
#line 327
    __const_udelay(4295000UL);
    }
  }
  while_break___1: /* CIL Label */ ;
  }
#line 328
  return;
}
}
#line 542
extern avmcard *b1_alloc_card(int nr_controllers ) ;
#line 543
extern void b1_free_card(avmcard *card ) ;
#line 544
extern int b1_detect(unsigned int base , enum avmcardtype cardtype ) ;
#line 545
extern void b1_getrevision(avmcard *card ) ;
#line 550
extern int b1_load_firmware(struct capi_ctr *ctrl , capiloaddata *data ) ;
#line 551
extern void b1_reset_ctr(struct capi_ctr *ctrl ) ;
#line 552
extern void b1_register_appl(struct capi_ctr *ctrl , u16 appl , capi_register_params *rp ) ;
#line 554
extern void b1_release_appl(struct capi_ctr *ctrl , u16 appl ) ;
#line 555
extern u16 b1_send_message(struct capi_ctr *ctrl , struct sk_buff *skb ) ;
#line 557
extern irqreturn_t b1_interrupt(int interrupt , void *devptr ) ;
#line 559
extern struct file_operations  const  b1ctl_proc_fops ;
#line 31 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char *revision  =    (char *)"$Revision: 1.1.2.2 $";
#line 35 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char const   __mod_description35[52]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 35
  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
        (char const   )'C',      (char const   )'A',      (char const   )'P',      (char const   )'I', 
        (char const   )'4',      (char const   )'L',      (char const   )'i',      (char const   )'n', 
        (char const   )'u',      (char const   )'x',      (char const   )':',      (char const   )' ', 
        (char const   )'D',      (char const   )'r',      (char const   )'i',      (char const   )'v', 
        (char const   )'e',      (char const   )'r',      (char const   )' ',      (char const   )'f', 
        (char const   )'o',      (char const   )'r',      (char const   )' ',      (char const   )'A', 
        (char const   )'V',      (char const   )'M',      (char const   )' ',      (char const   )'P', 
        (char const   )'C',      (char const   )'M',      (char const   )'C',      (char const   )'I', 
        (char const   )'A',      (char const   )' ',      (char const   )'c',      (char const   )'a', 
        (char const   )'r',      (char const   )'d',      (char const   )'s',      (char const   )'\000'};
#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char const   __mod_author36[21]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 36
  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'C', 
        (char const   )'a',      (char const   )'r',      (char const   )'s',      (char const   )'t', 
        (char const   )'e',      (char const   )'n',      (char const   )' ',      (char const   )'P', 
        (char const   )'a',      (char const   )'e',      (char const   )'t',      (char const   )'h', 
        (char const   )'\000'};
#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char const   __mod_license37[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 37
  {      (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   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static void b1pcmcia_remove_ctr(struct capi_ctr *ctrl ) 
{ avmctrl_info *cinfo ;
  avmcard *card ;
  unsigned int port ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  void *__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 int __cil_tmp14 ;
  void *__cil_tmp15 ;

  {
  {
#line 43
  __cil_tmp5 = (unsigned long )ctrl;
#line 43
  __cil_tmp6 = __cil_tmp5 + 8;
#line 43
  __cil_tmp7 = *((void **)__cil_tmp6);
#line 43
  cinfo = (avmctrl_info *)__cil_tmp7;
#line 44
  __cil_tmp8 = (unsigned long )cinfo;
#line 44
  __cil_tmp9 = __cil_tmp8 + 1256;
#line 44
  card = *((struct avmcard **)__cil_tmp9);
#line 45
  __cil_tmp10 = (unsigned long )card;
#line 45
  __cil_tmp11 = __cil_tmp10 + 56;
#line 45
  port = *((unsigned int *)__cil_tmp11);
#line 47
  b1_reset(port);
#line 48
  b1_reset(port);
#line 50
  detach_capi_ctr(ctrl);
#line 51
  __cil_tmp12 = (unsigned long )card;
#line 51
  __cil_tmp13 = __cil_tmp12 + 60;
#line 51
  __cil_tmp14 = *((unsigned int *)__cil_tmp13);
#line 51
  __cil_tmp15 = (void *)card;
#line 51
  free_irq(__cil_tmp14, __cil_tmp15);
#line 52
  b1_free_card(card);
  }
#line 53
  return;
}
}
#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static struct list_head cards  =    {& cards, & cards};
#line 59
static char *b1pcmcia_procinfo(struct capi_ctr *ctrl ) ;
#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static int b1pcmcia_add_card(unsigned int port , unsigned int irq , enum avmcardtype cardtype ) 
{ avmctrl_info *cinfo ;
  avmcard *card ;
  char *cardname ;
  int retval ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  char *__cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  char *__cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  char *__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 int __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  char *__cil_tmp38 ;
  char const   *__cil_tmp39 ;
  void *__cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned int __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  unsigned int __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  unsigned int __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  enum avmcardtype __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  unsigned int __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned int __cil_tmp58 ;
  unsigned long __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  unsigned long __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  unsigned long __cil_tmp69 ;
  unsigned long __cil_tmp70 ;
  unsigned long __cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  unsigned long __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  unsigned long __cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  unsigned long __cil_tmp84 ;
  unsigned long __cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  unsigned long __cil_tmp87 ;
  unsigned long __cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  unsigned long __cil_tmp90 ;
  unsigned long __cil_tmp91 ;
  unsigned long __cil_tmp92 ;
  char *__cil_tmp93 ;
  unsigned long __cil_tmp94 ;
  unsigned long __cil_tmp95 ;
  unsigned long __cil_tmp96 ;
  unsigned long __cil_tmp97 ;
  char *__cil_tmp98 ;
  char const   *__cil_tmp99 ;
  unsigned long __cil_tmp100 ;
  unsigned long __cil_tmp101 ;
  struct capi_ctr *__cil_tmp102 ;
  unsigned long __cil_tmp103 ;
  unsigned long __cil_tmp104 ;
  unsigned int __cil_tmp105 ;
  unsigned long __cil_tmp106 ;
  unsigned long __cil_tmp107 ;
  unsigned int __cil_tmp108 ;
  unsigned long __cil_tmp109 ;
  unsigned long __cil_tmp110 ;
  unsigned char __cil_tmp111 ;
  int __cil_tmp112 ;
  unsigned long __cil_tmp113 ;
  unsigned long __cil_tmp114 ;
  struct list_head *__cil_tmp115 ;
  unsigned long __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  unsigned long __cil_tmp119 ;
  unsigned long __cil_tmp120 ;
  unsigned int __cil_tmp121 ;
  void *__cil_tmp122 ;

  {
  {
#line 69
  card = b1_alloc_card(1);
  }
#line 70
  if (! card) {
    {
#line 71
    printk("<4>b1pcmcia: no memory.\n");
#line 72
    retval = -12;
    }
#line 73
    goto err;
  } else {

  }
#line 75
  __cil_tmp8 = (unsigned long )card;
#line 75
  __cil_tmp9 = __cil_tmp8 + 2288;
#line 75
  cinfo = *((struct avmctrl_info **)__cil_tmp9);
#line 78
  if ((int )cardtype == 3) {
#line 78
    goto case_3;
  } else
#line 79
  if ((int )cardtype == 4) {
#line 79
    goto case_4;
  } else {
    {
#line 80
    goto switch_default;
#line 77
    if (0) {
      case_3: /* CIL Label */ 
      {
#line 78
      __cil_tmp10 = 0 * 1UL;
#line 78
      __cil_tmp11 = 0 + __cil_tmp10;
#line 78
      __cil_tmp12 = (unsigned long )card;
#line 78
      __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
#line 78
      __cil_tmp14 = (char *)__cil_tmp13;
#line 78
      sprintf(__cil_tmp14, "m1-%x", port);
      }
#line 78
      goto switch_break;
      case_4: /* CIL Label */ 
      {
#line 79
      __cil_tmp15 = 0 * 1UL;
#line 79
      __cil_tmp16 = 0 + __cil_tmp15;
#line 79
      __cil_tmp17 = (unsigned long )card;
#line 79
      __cil_tmp18 = __cil_tmp17 + __cil_tmp16;
#line 79
      __cil_tmp19 = (char *)__cil_tmp18;
#line 79
      sprintf(__cil_tmp19, "m2-%x", port);
      }
#line 79
      goto switch_break;
      switch_default: /* CIL Label */ 
      {
#line 80
      __cil_tmp20 = 0 * 1UL;
#line 80
      __cil_tmp21 = 0 + __cil_tmp20;
#line 80
      __cil_tmp22 = (unsigned long )card;
#line 80
      __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
#line 80
      __cil_tmp24 = (char *)__cil_tmp23;
#line 80
      sprintf(__cil_tmp24, "b1pcmcia-%x", port);
      }
#line 80
      goto switch_break;
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
  {
#line 82
  __cil_tmp25 = (unsigned long )card;
#line 82
  __cil_tmp26 = __cil_tmp25 + 56;
#line 82
  *((unsigned int *)__cil_tmp26) = port;
#line 83
  __cil_tmp27 = (unsigned long )card;
#line 83
  __cil_tmp28 = __cil_tmp27 + 60;
#line 83
  *((unsigned int *)__cil_tmp28) = irq;
#line 84
  __cil_tmp29 = (unsigned long )card;
#line 84
  __cil_tmp30 = __cil_tmp29 + 72;
#line 84
  *((enum avmcardtype *)__cil_tmp30) = cardtype;
#line 86
  __cil_tmp31 = (unsigned long )card;
#line 86
  __cil_tmp32 = __cil_tmp31 + 60;
#line 86
  __cil_tmp33 = *((unsigned int *)__cil_tmp32);
#line 86
  __cil_tmp34 = 0 * 1UL;
#line 86
  __cil_tmp35 = 0 + __cil_tmp34;
#line 86
  __cil_tmp36 = (unsigned long )card;
#line 86
  __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
#line 86
  __cil_tmp38 = (char *)__cil_tmp37;
#line 86
  __cil_tmp39 = (char const   *)__cil_tmp38;
#line 86
  __cil_tmp40 = (void *)card;
#line 86
  retval = (int )request_irq(__cil_tmp33, & b1_interrupt, 128UL, __cil_tmp39, __cil_tmp40);
  }
#line 87
  if (retval) {
    {
#line 88
    __cil_tmp41 = (unsigned long )card;
#line 88
    __cil_tmp42 = __cil_tmp41 + 60;
#line 88
    __cil_tmp43 = *((unsigned int *)__cil_tmp42);
#line 88
    printk("<3>b1pcmcia: unable to get IRQ %d.\n", __cil_tmp43);
#line 90
    retval = -16;
    }
#line 91
    goto err_free;
  } else {

  }
  {
#line 93
  __cil_tmp44 = (unsigned long )card;
#line 93
  __cil_tmp45 = __cil_tmp44 + 56;
#line 93
  __cil_tmp46 = *((unsigned int *)__cil_tmp45);
#line 93
  b1_reset(__cil_tmp46);
#line 94
  __cil_tmp47 = (unsigned long )card;
#line 94
  __cil_tmp48 = __cil_tmp47 + 56;
#line 94
  __cil_tmp49 = *((unsigned int *)__cil_tmp48);
#line 94
  __cil_tmp50 = (unsigned long )card;
#line 94
  __cil_tmp51 = __cil_tmp50 + 72;
#line 94
  __cil_tmp52 = *((enum avmcardtype *)__cil_tmp51);
#line 94
  retval = b1_detect(__cil_tmp49, __cil_tmp52);
  }
#line 94
  if (retval != 0) {
    {
#line 95
    __cil_tmp53 = (unsigned long )card;
#line 95
    __cil_tmp54 = __cil_tmp53 + 56;
#line 95
    __cil_tmp55 = *((unsigned int *)__cil_tmp54);
#line 95
    printk("<5>b1pcmcia: NO card at 0x%x (%d)\n", __cil_tmp55, retval);
#line 97
    retval = -19;
    }
#line 98
    goto err_free_irq;
  } else {

  }
  {
#line 100
  __cil_tmp56 = (unsigned long )card;
#line 100
  __cil_tmp57 = __cil_tmp56 + 56;
#line 100
  __cil_tmp58 = *((unsigned int *)__cil_tmp57);
#line 100
  b1_reset(__cil_tmp58);
#line 101
  b1_getrevision(card);
#line 103
  __cil_tmp59 = (unsigned long )cinfo;
#line 103
  __cil_tmp60 = __cil_tmp59 + 1264;
#line 103
  *((struct module **)__cil_tmp60) = & __this_module;
#line 104
  __cil_tmp61 = 1264 + 48;
#line 104
  __cil_tmp62 = (unsigned long )cinfo;
#line 104
  __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
#line 104
  *((char **)__cil_tmp63) = (char *)"b1pcmcia";
#line 105
  __cil_tmp64 = 1264 + 8;
#line 105
  __cil_tmp65 = (unsigned long )cinfo;
#line 105
  __cil_tmp66 = __cil_tmp65 + __cil_tmp64;
#line 105
  *((void **)__cil_tmp66) = (void *)cinfo;
#line 106
  __cil_tmp67 = 1264 + 72;
#line 106
  __cil_tmp68 = (unsigned long )cinfo;
#line 106
  __cil_tmp69 = __cil_tmp68 + __cil_tmp67;
#line 106
  *((void (**)(struct capi_ctr * , u16 appl , capi_register_params * ))__cil_tmp69) = & b1_register_appl;
#line 107
  __cil_tmp70 = 1264 + 80;
#line 107
  __cil_tmp71 = (unsigned long )cinfo;
#line 107
  __cil_tmp72 = __cil_tmp71 + __cil_tmp70;
#line 107
  *((void (**)(struct capi_ctr * , u16 appl ))__cil_tmp72) = & b1_release_appl;
#line 108
  __cil_tmp73 = 1264 + 88;
#line 108
  __cil_tmp74 = (unsigned long )cinfo;
#line 108
  __cil_tmp75 = __cil_tmp74 + __cil_tmp73;
#line 108
  *((u16 (**)(struct capi_ctr * , struct sk_buff *skb ))__cil_tmp75) = & b1_send_message;
#line 109
  __cil_tmp76 = 1264 + 56;
#line 109
  __cil_tmp77 = (unsigned long )cinfo;
#line 109
  __cil_tmp78 = __cil_tmp77 + __cil_tmp76;
#line 109
  *((int (**)(struct capi_ctr * , capiloaddata * ))__cil_tmp78) = & b1_load_firmware;
#line 110
  __cil_tmp79 = 1264 + 64;
#line 110
  __cil_tmp80 = (unsigned long )cinfo;
#line 110
  __cil_tmp81 = __cil_tmp80 + __cil_tmp79;
#line 110
  *((void (**)(struct capi_ctr * ))__cil_tmp81) = & b1_reset_ctr;
#line 111
  __cil_tmp82 = 1264 + 96;
#line 111
  __cil_tmp83 = (unsigned long )cinfo;
#line 111
  __cil_tmp84 = __cil_tmp83 + __cil_tmp82;
#line 111
  *((char *(**)(struct capi_ctr * ))__cil_tmp84) = & b1pcmcia_procinfo;
#line 112
  __cil_tmp85 = 1264 + 104;
#line 112
  __cil_tmp86 = (unsigned long )cinfo;
#line 112
  __cil_tmp87 = __cil_tmp86 + __cil_tmp85;
#line 112
  *((struct file_operations  const  **)__cil_tmp87) = & b1ctl_proc_fops;
#line 113
  __cil_tmp88 = 0 * 1UL;
#line 113
  __cil_tmp89 = 16 + __cil_tmp88;
#line 113
  __cil_tmp90 = 1264 + __cil_tmp89;
#line 113
  __cil_tmp91 = (unsigned long )cinfo;
#line 113
  __cil_tmp92 = __cil_tmp91 + __cil_tmp90;
#line 113
  __cil_tmp93 = (char *)__cil_tmp92;
#line 113
  __cil_tmp94 = 0 * 1UL;
#line 113
  __cil_tmp95 = 0 + __cil_tmp94;
#line 113
  __cil_tmp96 = (unsigned long )card;
#line 113
  __cil_tmp97 = __cil_tmp96 + __cil_tmp95;
#line 113
  __cil_tmp98 = (char *)__cil_tmp97;
#line 113
  __cil_tmp99 = (char const   *)__cil_tmp98;
#line 113
  strcpy(__cil_tmp93, __cil_tmp99);
#line 115
  __cil_tmp100 = (unsigned long )cinfo;
#line 115
  __cil_tmp101 = __cil_tmp100 + 1264;
#line 115
  __cil_tmp102 = (struct capi_ctr *)__cil_tmp101;
#line 115
  retval = attach_capi_ctr(__cil_tmp102);
  }
#line 116
  if (retval) {
    {
#line 117
    printk("<3>b1pcmcia: attach controller failed.\n");
    }
#line 118
    goto err_free_irq;
  } else {

  }
#line 121
  if ((int )cardtype == 3) {
#line 121
    goto case_3___0;
  } else
#line 122
  if ((int )cardtype == 4) {
#line 122
    goto case_4___0;
  } else {
    {
#line 123
    goto switch_default___0;
#line 120
    if (0) {
      case_3___0: /* CIL Label */ 
#line 121
      cardname = (char *)"M1";
#line 121
      goto switch_break___0;
      case_4___0: /* CIL Label */ 
#line 122
      cardname = (char *)"M2";
#line 122
      goto switch_break___0;
      switch_default___0: /* CIL Label */ 
#line 123
      cardname = (char *)"B1 PCMCIA";
#line 123
      goto switch_break___0;
    } else {
      switch_break___0: /* CIL Label */ ;
    }
    }
  }
  {
#line 126
  __cil_tmp103 = (unsigned long )card;
#line 126
  __cil_tmp104 = __cil_tmp103 + 56;
#line 126
  __cil_tmp105 = *((unsigned int *)__cil_tmp104);
#line 126
  __cil_tmp106 = (unsigned long )card;
#line 126
  __cil_tmp107 = __cil_tmp106 + 60;
#line 126
  __cil_tmp108 = *((unsigned int *)__cil_tmp107);
#line 126
  __cil_tmp109 = (unsigned long )card;
#line 126
  __cil_tmp110 = __cil_tmp109 + 76;
#line 126
  __cil_tmp111 = *((unsigned char *)__cil_tmp110);
#line 126
  __cil_tmp112 = (int )__cil_tmp111;
#line 126
  printk("<6>b1pcmcia: AVM %s at i/o %#x, irq %d, revision %d\n", cardname, __cil_tmp105,
         __cil_tmp108, __cil_tmp112);
#line 129
  __cil_tmp113 = (unsigned long )card;
#line 129
  __cil_tmp114 = __cil_tmp113 + 2304;
#line 129
  __cil_tmp115 = (struct list_head *)__cil_tmp114;
#line 129
  list_add(__cil_tmp115, & cards);
  }
  {
#line 130
  __cil_tmp116 = 1264 + 296;
#line 130
  __cil_tmp117 = (unsigned long )cinfo;
#line 130
  __cil_tmp118 = __cil_tmp117 + __cil_tmp116;
#line 130
  return (*((int *)__cil_tmp118));
  }
  err_free_irq: 
  {
#line 133
  __cil_tmp119 = (unsigned long )card;
#line 133
  __cil_tmp120 = __cil_tmp119 + 60;
#line 133
  __cil_tmp121 = *((unsigned int *)__cil_tmp120);
#line 133
  __cil_tmp122 = (void *)card;
#line 133
  free_irq(__cil_tmp121, __cil_tmp122);
  }
  err_free: 
  {
#line 135
  b1_free_card(card);
  }
  err: 
#line 137
  return (retval);
}
}
#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char *b1pcmcia_procinfo(struct capi_ctr *ctrl ) 
{ avmctrl_info *cinfo ;
  int tmp ;
  unsigned int tmp___0 ;
  unsigned int tmp___1 ;
  char const   *tmp___2 ;
  char const   *tmp___3 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  void *__cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  struct avmcard *__cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned char __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  struct avmcard *__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 ;
  struct avmcard *__cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  char *__cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  char *__cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  char *__cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  unsigned long __cil_tmp59 ;

  {
#line 144
  __cil_tmp8 = (unsigned long )ctrl;
#line 144
  __cil_tmp9 = __cil_tmp8 + 8;
#line 144
  __cil_tmp10 = *((void **)__cil_tmp9);
#line 144
  cinfo = (avmctrl_info *)__cil_tmp10;
#line 146
  if (! cinfo) {
#line 147
    return ((char *)"");
  } else {

  }
  {
#line 148
  __cil_tmp11 = (unsigned long )cinfo;
#line 148
  __cil_tmp12 = __cil_tmp11 + 1256;
#line 148
  if (*((struct avmcard **)__cil_tmp12)) {
#line 148
    __cil_tmp13 = (unsigned long )cinfo;
#line 148
    __cil_tmp14 = __cil_tmp13 + 1256;
#line 148
    __cil_tmp15 = *((struct avmcard **)__cil_tmp14);
#line 148
    __cil_tmp16 = (unsigned long )__cil_tmp15;
#line 148
    __cil_tmp17 = __cil_tmp16 + 76;
#line 148
    __cil_tmp18 = *((unsigned char *)__cil_tmp17);
#line 148
    tmp = (int )__cil_tmp18;
  } else {
#line 148
    tmp = 0;
  }
  }
  {
#line 148
  __cil_tmp19 = (unsigned long )cinfo;
#line 148
  __cil_tmp20 = __cil_tmp19 + 1256;
#line 148
  if (*((struct avmcard **)__cil_tmp20)) {
#line 148
    __cil_tmp21 = (unsigned long )cinfo;
#line 148
    __cil_tmp22 = __cil_tmp21 + 1256;
#line 148
    __cil_tmp23 = *((struct avmcard **)__cil_tmp22);
#line 148
    __cil_tmp24 = (unsigned long )__cil_tmp23;
#line 148
    __cil_tmp25 = __cil_tmp24 + 60;
#line 148
    tmp___0 = *((unsigned int *)__cil_tmp25);
  } else {
#line 148
    tmp___0 = 0U;
  }
  }
  {
#line 148
  __cil_tmp26 = (unsigned long )cinfo;
#line 148
  __cil_tmp27 = __cil_tmp26 + 1256;
#line 148
  if (*((struct avmcard **)__cil_tmp27)) {
#line 148
    __cil_tmp28 = (unsigned long )cinfo;
#line 148
    __cil_tmp29 = __cil_tmp28 + 1256;
#line 148
    __cil_tmp30 = *((struct avmcard **)__cil_tmp29);
#line 148
    __cil_tmp31 = (unsigned long )__cil_tmp30;
#line 148
    __cil_tmp32 = __cil_tmp31 + 56;
#line 148
    tmp___1 = *((unsigned int *)__cil_tmp32);
  } else {
#line 148
    tmp___1 = 0U;
  }
  }
  {
#line 148
  __cil_tmp33 = 0 * 8UL;
#line 148
  __cil_tmp34 = 1064 + __cil_tmp33;
#line 148
  __cil_tmp35 = (unsigned long )cinfo;
#line 148
  __cil_tmp36 = __cil_tmp35 + __cil_tmp34;
#line 148
  if (*((char **)__cil_tmp36)) {
#line 148
    __cil_tmp37 = 0 * 8UL;
#line 148
    __cil_tmp38 = 1064 + __cil_tmp37;
#line 148
    __cil_tmp39 = (unsigned long )cinfo;
#line 148
    __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
#line 148
    __cil_tmp41 = *((char **)__cil_tmp40);
#line 148
    tmp___2 = (char const   *)__cil_tmp41;
  } else {
#line 148
    tmp___2 = "-";
  }
  }
  {
#line 148
  __cil_tmp42 = 0 * 1UL;
#line 148
  __cil_tmp43 = 0 + __cil_tmp42;
#line 148
  __cil_tmp44 = (unsigned long )cinfo;
#line 148
  __cil_tmp45 = __cil_tmp44 + __cil_tmp43;
#line 148
  if (*((char *)__cil_tmp45)) {
#line 148
    __cil_tmp46 = 0 * 1UL;
#line 148
    __cil_tmp47 = 0 + __cil_tmp46;
#line 148
    __cil_tmp48 = (unsigned long )cinfo;
#line 148
    __cil_tmp49 = __cil_tmp48 + __cil_tmp47;
#line 148
    __cil_tmp50 = (char *)__cil_tmp49;
#line 148
    tmp___3 = (char const   *)__cil_tmp50;
  } else {
#line 148
    tmp___3 = "-";
  }
  }
  {
#line 148
  __cil_tmp51 = 0 * 1UL;
#line 148
  __cil_tmp52 = 1128 + __cil_tmp51;
#line 148
  __cil_tmp53 = (unsigned long )cinfo;
#line 148
  __cil_tmp54 = __cil_tmp53 + __cil_tmp52;
#line 148
  __cil_tmp55 = (char *)__cil_tmp54;
#line 148
  sprintf(__cil_tmp55, "%s %s 0x%x %d r%d", tmp___3, tmp___2, tmp___1, tmp___0, tmp);
  }
  {
#line 155
  __cil_tmp56 = 0 * 1UL;
#line 155
  __cil_tmp57 = 1128 + __cil_tmp56;
#line 155
  __cil_tmp58 = (unsigned long )cinfo;
#line 155
  __cil_tmp59 = __cil_tmp58 + __cil_tmp57;
#line 155
  return ((char *)__cil_tmp59);
  }
}
}
#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
int b1pcmcia_addcard_b1(unsigned int port , unsigned int irq ) 
{ int tmp ;
  enum avmcardtype __cil_tmp4 ;

  {
  {
#line 162
  __cil_tmp4 = (enum avmcardtype )2;
#line 162
  tmp = b1pcmcia_add_card(port, irq, __cil_tmp4);
  }
#line 162
  return (tmp);
}
}
#line 165 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
int b1pcmcia_addcard_m1(unsigned int port , unsigned int irq ) 
{ int tmp ;
  enum avmcardtype __cil_tmp4 ;

  {
  {
#line 167
  __cil_tmp4 = (enum avmcardtype )3;
#line 167
  tmp = b1pcmcia_add_card(port, irq, __cil_tmp4);
  }
#line 167
  return (tmp);
}
}
#line 170 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
int b1pcmcia_addcard_m2(unsigned int port , unsigned int irq ) 
{ int tmp ;
  enum avmcardtype __cil_tmp4 ;

  {
  {
#line 172
  __cil_tmp4 = (enum avmcardtype )4;
#line 172
  tmp = b1pcmcia_add_card(port, irq, __cil_tmp4);
  }
#line 172
  return (tmp);
}
}
#line 175 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
int b1pcmcia_delcard(unsigned int port , unsigned int irq ) 
{ struct list_head *l ;
  avmcard *card ;
  struct list_head  const  *__mptr ;
  struct list_head *__cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  avmcard *__cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  struct list_head *__cil_tmp12 ;
  unsigned int __cil_tmp13 ;
  char *__cil_tmp14 ;
  char *__cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned int __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned int __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  struct avmctrl_info *__cil_tmp24 ;
  struct avmctrl_info *__cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  struct capi_ctr *__cil_tmp28 ;

  {
#line 180
  __cil_tmp6 = & cards;
#line 180
  l = *((struct list_head **)__cil_tmp6);
  {
#line 180
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 180
    __cil_tmp7 = (unsigned long )(& cards);
#line 180
    __cil_tmp8 = (unsigned long )l;
#line 180
    if (__cil_tmp8 != __cil_tmp7) {

    } else {
#line 180
      goto while_break;
    }
    }
#line 181
    __mptr = (struct list_head  const  *)l;
#line 181
    __cil_tmp9 = (avmcard *)0;
#line 181
    __cil_tmp10 = (unsigned long )__cil_tmp9;
#line 181
    __cil_tmp11 = __cil_tmp10 + 2304;
#line 181
    __cil_tmp12 = (struct list_head *)__cil_tmp11;
#line 181
    __cil_tmp13 = (unsigned int )__cil_tmp12;
#line 181
    __cil_tmp14 = (char *)__mptr;
#line 181
    __cil_tmp15 = __cil_tmp14 - __cil_tmp13;
#line 181
    card = (avmcard *)__cil_tmp15;
    {
#line 182
    __cil_tmp16 = (unsigned long )card;
#line 182
    __cil_tmp17 = __cil_tmp16 + 56;
#line 182
    __cil_tmp18 = *((unsigned int *)__cil_tmp17);
#line 182
    if (__cil_tmp18 == port) {
      {
#line 182
      __cil_tmp19 = (unsigned long )card;
#line 182
      __cil_tmp20 = __cil_tmp19 + 60;
#line 182
      __cil_tmp21 = *((unsigned int *)__cil_tmp20);
#line 182
      if (__cil_tmp21 == irq) {
        {
#line 183
        __cil_tmp22 = (unsigned long )card;
#line 183
        __cil_tmp23 = __cil_tmp22 + 2288;
#line 183
        __cil_tmp24 = *((struct avmctrl_info **)__cil_tmp23);
#line 183
        __cil_tmp25 = __cil_tmp24 + 0;
#line 183
        __cil_tmp26 = (unsigned long )__cil_tmp25;
#line 183
        __cil_tmp27 = __cil_tmp26 + 1264;
#line 183
        __cil_tmp28 = (struct capi_ctr *)__cil_tmp27;
#line 183
        b1pcmcia_remove_ctr(__cil_tmp28);
        }
#line 184
        return (0);
      } else {

      }
      }
    } else {

    }
    }
#line 180
    l = *((struct list_head **)l);
  }
  while_break: /* CIL Label */ ;
  }
#line 187
  return (-3);
}
}
#line 190
extern void *__crc_b1pcmcia_addcard_b1  __attribute__((__weak__)) ;
#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static unsigned long const   __kcrctab_b1pcmcia_addcard_b1  __attribute__((__used__,
__unused__, __section__("___kcrctab+b1pcmcia_addcard_b1")))  =    (unsigned long const   )((unsigned long )(& __crc_b1pcmcia_addcard_b1));
#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char const   __kstrtab_b1pcmcia_addcard_b1[20]  __attribute__((__section__("__ksymtab_strings"),
__aligned__(1)))  = 
#line 190
  {      (char const   )'b',      (char const   )'1',      (char const   )'p',      (char const   )'c', 
        (char const   )'m',      (char const   )'c',      (char const   )'i',      (char const   )'a', 
        (char const   )'_',      (char const   )'a',      (char const   )'d',      (char const   )'d', 
        (char const   )'c',      (char const   )'a',      (char const   )'r',      (char const   )'d', 
        (char const   )'_',      (char const   )'b',      (char const   )'1',      (char const   )'\000'};
#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static struct kernel_symbol  const  __ksymtab_b1pcmcia_addcard_b1  __attribute__((__used__,
__unused__, __section__("___ksymtab+b1pcmcia_addcard_b1")))  =    {(unsigned long )(& b1pcmcia_addcard_b1), __kstrtab_b1pcmcia_addcard_b1};
#line 191
extern void *__crc_b1pcmcia_addcard_m1  __attribute__((__weak__)) ;
#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static unsigned long const   __kcrctab_b1pcmcia_addcard_m1  __attribute__((__used__,
__unused__, __section__("___kcrctab+b1pcmcia_addcard_m1")))  =    (unsigned long const   )((unsigned long )(& __crc_b1pcmcia_addcard_m1));
#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char const   __kstrtab_b1pcmcia_addcard_m1[20]  __attribute__((__section__("__ksymtab_strings"),
__aligned__(1)))  = 
#line 191
  {      (char const   )'b',      (char const   )'1',      (char const   )'p',      (char const   )'c', 
        (char const   )'m',      (char const   )'c',      (char const   )'i',      (char const   )'a', 
        (char const   )'_',      (char const   )'a',      (char const   )'d',      (char const   )'d', 
        (char const   )'c',      (char const   )'a',      (char const   )'r',      (char const   )'d', 
        (char const   )'_',      (char const   )'m',      (char const   )'1',      (char const   )'\000'};
#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static struct kernel_symbol  const  __ksymtab_b1pcmcia_addcard_m1  __attribute__((__used__,
__unused__, __section__("___ksymtab+b1pcmcia_addcard_m1")))  =    {(unsigned long )(& b1pcmcia_addcard_m1), __kstrtab_b1pcmcia_addcard_m1};
#line 192
extern void *__crc_b1pcmcia_addcard_m2  __attribute__((__weak__)) ;
#line 192 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static unsigned long const   __kcrctab_b1pcmcia_addcard_m2  __attribute__((__used__,
__unused__, __section__("___kcrctab+b1pcmcia_addcard_m2")))  =    (unsigned long const   )((unsigned long )(& __crc_b1pcmcia_addcard_m2));
#line 192 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char const   __kstrtab_b1pcmcia_addcard_m2[20]  __attribute__((__section__("__ksymtab_strings"),
__aligned__(1)))  = 
#line 192
  {      (char const   )'b',      (char const   )'1',      (char const   )'p',      (char const   )'c', 
        (char const   )'m',      (char const   )'c',      (char const   )'i',      (char const   )'a', 
        (char const   )'_',      (char const   )'a',      (char const   )'d',      (char const   )'d', 
        (char const   )'c',      (char const   )'a',      (char const   )'r',      (char const   )'d', 
        (char const   )'_',      (char const   )'m',      (char const   )'2',      (char const   )'\000'};
#line 192 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static struct kernel_symbol  const  __ksymtab_b1pcmcia_addcard_m2  __attribute__((__used__,
__unused__, __section__("___ksymtab+b1pcmcia_addcard_m2")))  =    {(unsigned long )(& b1pcmcia_addcard_m2), __kstrtab_b1pcmcia_addcard_m2};
#line 193
extern void *__crc_b1pcmcia_delcard  __attribute__((__weak__)) ;
#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static unsigned long const   __kcrctab_b1pcmcia_delcard  __attribute__((__used__,
__unused__, __section__("___kcrctab+b1pcmcia_delcard")))  =    (unsigned long const   )((unsigned long )(& __crc_b1pcmcia_delcard));
#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static char const   __kstrtab_b1pcmcia_delcard[17]  __attribute__((__section__("__ksymtab_strings"),
__aligned__(1)))  = 
#line 193
  {      (char const   )'b',      (char const   )'1',      (char const   )'p',      (char const   )'c', 
        (char const   )'m',      (char const   )'c',      (char const   )'i',      (char const   )'a', 
        (char const   )'_',      (char const   )'d',      (char const   )'e',      (char const   )'l', 
        (char const   )'c',      (char const   )'a',      (char const   )'r',      (char const   )'d', 
        (char const   )'\000'};
#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static struct kernel_symbol  const  __ksymtab_b1pcmcia_delcard  __attribute__((__used__,
__unused__, __section__("___ksymtab+b1pcmcia_delcard")))  =    {(unsigned long )(& b1pcmcia_delcard), __kstrtab_b1pcmcia_delcard};
#line 195 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static struct capi_driver capi_driver_b1pcmcia  =    {{(char )'b', (char )'1', (char )'p', (char )'c', (char )'m', (char )'c', (char )'i',
     (char )'a', (char )'\000'}, {(char )'1', (char )'.', (char )'0', (char )'\000'},
    (int (*)(struct capi_driver *driver , capicardparams *data ))0, {(struct list_head *)0,
                                                                     (struct list_head *)0}};
#line 200
static int b1pcmcia_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
#line 200 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static int b1pcmcia_init(void) 
{ char *p ;
  char rev[32] ;
  char const   *__cil_tmp3 ;
  void *__cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  char *__cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  char *__cil_tmp10 ;
  char *__cil_tmp11 ;
  char const   *__cil_tmp12 ;
  size_t __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  char *__cil_tmp16 ;
  char const   *__cil_tmp17 ;
  void *__cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  char *__cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  char *__cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  char *__cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  char *__cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  char *__cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  char *__cil_tmp39 ;
  char const   *__cil_tmp40 ;
  size_t __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  char *__cil_tmp44 ;

  {
  {
#line 205
  __cil_tmp3 = (char const   *)revision;
#line 205
  p = strchr(__cil_tmp3, ':');
  }
  {
#line 205
  __cil_tmp4 = (void *)0;
#line 205
  __cil_tmp5 = (unsigned long )__cil_tmp4;
#line 205
  __cil_tmp6 = (unsigned long )p;
#line 205
  if (__cil_tmp6 != __cil_tmp5) {
    {
#line 205
    __cil_tmp7 = p + 1;
#line 205
    if (*__cil_tmp7) {
      {
#line 206
      __cil_tmp8 = 0 * 1UL;
#line 206
      __cil_tmp9 = (unsigned long )(rev) + __cil_tmp8;
#line 206
      __cil_tmp10 = (char *)__cil_tmp9;
#line 206
      __cil_tmp11 = p + 2;
#line 206
      __cil_tmp12 = (char const   *)__cil_tmp11;
#line 206
      __cil_tmp13 = (size_t )32;
#line 206
      strlcpy(__cil_tmp10, __cil_tmp12, __cil_tmp13);
#line 207
      __cil_tmp14 = 0 * 1UL;
#line 207
      __cil_tmp15 = (unsigned long )(rev) + __cil_tmp14;
#line 207
      __cil_tmp16 = (char *)__cil_tmp15;
#line 207
      __cil_tmp17 = (char const   *)__cil_tmp16;
#line 207
      p = strchr(__cil_tmp17, '$');
      }
      {
#line 207
      __cil_tmp18 = (void *)0;
#line 207
      __cil_tmp19 = (unsigned long )__cil_tmp18;
#line 207
      __cil_tmp20 = (unsigned long )p;
#line 207
      if (__cil_tmp20 != __cil_tmp19) {
        {
#line 207
        __cil_tmp21 = 0 * 1UL;
#line 207
        __cil_tmp22 = (unsigned long )(rev) + __cil_tmp21;
#line 207
        __cil_tmp23 = (char *)__cil_tmp22;
#line 207
        __cil_tmp24 = (unsigned long )__cil_tmp23;
#line 207
        __cil_tmp25 = (unsigned long )p;
#line 207
        if (__cil_tmp25 > __cil_tmp24) {
#line 208
          __cil_tmp26 = p - 1;
#line 208
          *__cil_tmp26 = (char)0;
        } else {

        }
        }
      } else {

      }
      }
    } else {
      {
#line 210
      __cil_tmp27 = 0 * 1UL;
#line 210
      __cil_tmp28 = (unsigned long )(rev) + __cil_tmp27;
#line 210
      __cil_tmp29 = (char *)__cil_tmp28;
#line 210
      strcpy(__cil_tmp29, "1.0");
      }
    }
    }
  } else {
    {
#line 210
    __cil_tmp30 = 0 * 1UL;
#line 210
    __cil_tmp31 = (unsigned long )(rev) + __cil_tmp30;
#line 210
    __cil_tmp32 = (char *)__cil_tmp31;
#line 210
    strcpy(__cil_tmp32, "1.0");
    }
  }
  }
  {
#line 212
  __cil_tmp33 = 0 * 1UL;
#line 212
  __cil_tmp34 = 32 + __cil_tmp33;
#line 212
  __cil_tmp35 = (unsigned long )(& capi_driver_b1pcmcia) + __cil_tmp34;
#line 212
  __cil_tmp36 = (char *)__cil_tmp35;
#line 212
  __cil_tmp37 = 0 * 1UL;
#line 212
  __cil_tmp38 = (unsigned long )(rev) + __cil_tmp37;
#line 212
  __cil_tmp39 = (char *)__cil_tmp38;
#line 212
  __cil_tmp40 = (char const   *)__cil_tmp39;
#line 212
  __cil_tmp41 = (size_t )32;
#line 212
  strlcpy(__cil_tmp36, __cil_tmp40, __cil_tmp41);
#line 213
  register_capi_driver(& capi_driver_b1pcmcia);
#line 214
  __cil_tmp42 = 0 * 1UL;
#line 214
  __cil_tmp43 = (unsigned long )(rev) + __cil_tmp42;
#line 214
  __cil_tmp44 = (char *)__cil_tmp43;
#line 214
  printk("<6>b1pci: revision %s\n", __cil_tmp44);
  }
#line 216
  return (0);
}
}
#line 219
static void b1pcmcia_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
#line 219 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
static void b1pcmcia_exit(void) 
{ 

  {
  {
#line 221
  unregister_capi_driver(& capi_driver_b1pcmcia);
  }
#line 222
  return;
}
}
#line 224 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
int init_module(void) 
{ int tmp ;

  {
  {
#line 224
  tmp = b1pcmcia_init();
  }
#line 224
  return (tmp);
}
}
#line 225 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
void cleanup_module(void) 
{ 

  {
  {
#line 225
  b1pcmcia_exit();
  }
#line 225
  return;
}
}
#line 243
void ldv_check_final_state(void) ;
#line 249
extern void ldv_initialize(void) ;
#line 252
extern int __VERIFIER_nondet_int(void) ;
#line 255 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
int LDV_IN_INTERRUPT  ;
#line 258 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
void main(void) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
  {
#line 270
  LDV_IN_INTERRUPT = 1;
#line 279
  ldv_initialize();
#line 285
  tmp = b1pcmcia_init();
  }
#line 285
  if (tmp) {
#line 286
    goto ldv_final;
  } else {

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

    } else {
#line 288
      goto while_break;
    }
    {
#line 291
    tmp___0 = __VERIFIER_nondet_int();
    }
    {
#line 293
    goto switch_default;
#line 291
    if (0) {
      switch_default: /* CIL Label */ 
#line 293
      goto switch_break;
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 305
  b1pcmcia_exit();
  }
  ldv_final: 
  {
#line 308
  ldv_check_final_state();
  }
#line 311
  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/3477/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/3477/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/3477/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/3477/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/3477/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/3477/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/3477/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/3477/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/3477/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/3477/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 320 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3477/dscv_tempdir/dscv/ri/32_1/drivers/isdn/hardware/avm/b1pcmcia.c.common.c"
long s__builtin_expect(long val , long res ) 
{ 

  {
#line 321
  return (val);
}
}