Showing error 881

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--isdn--hardware--avm--b1pcmcia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 2432
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 23 "include/asm-generic/int-ll64.h"
   5typedef unsigned short __u16;
   6#line 26 "include/asm-generic/int-ll64.h"
   7typedef unsigned int __u32;
   8#line 30 "include/asm-generic/int-ll64.h"
   9typedef unsigned long long __u64;
  10#line 43 "include/asm-generic/int-ll64.h"
  11typedef unsigned char u8;
  12#line 45 "include/asm-generic/int-ll64.h"
  13typedef short s16;
  14#line 46 "include/asm-generic/int-ll64.h"
  15typedef unsigned short u16;
  16#line 48 "include/asm-generic/int-ll64.h"
  17typedef int s32;
  18#line 49 "include/asm-generic/int-ll64.h"
  19typedef unsigned int u32;
  20#line 51 "include/asm-generic/int-ll64.h"
  21typedef long long s64;
  22#line 52 "include/asm-generic/int-ll64.h"
  23typedef unsigned long long u64;
  24#line 14 "include/asm-generic/posix_types.h"
  25typedef long __kernel_long_t;
  26#line 15 "include/asm-generic/posix_types.h"
  27typedef unsigned long __kernel_ulong_t;
  28#line 75 "include/asm-generic/posix_types.h"
  29typedef __kernel_ulong_t __kernel_size_t;
  30#line 76 "include/asm-generic/posix_types.h"
  31typedef __kernel_long_t __kernel_ssize_t;
  32#line 27 "include/linux/types.h"
  33typedef unsigned short umode_t;
  34#line 63 "include/linux/types.h"
  35typedef __kernel_size_t size_t;
  36#line 68 "include/linux/types.h"
  37typedef __kernel_ssize_t ssize_t;
  38#line 94 "include/linux/types.h"
  39typedef unsigned int u_int;
  40#line 155 "include/linux/types.h"
  41typedef u64 dma_addr_t;
  42#line 179 "include/linux/types.h"
  43typedef __u16 __be16;
  44#line 186 "include/linux/types.h"
  45typedef __u32 __wsum;
  46#line 202 "include/linux/types.h"
  47typedef unsigned int gfp_t;
  48#line 221 "include/linux/types.h"
  49struct __anonstruct_atomic_t_6 {
  50   int counter ;
  51};
  52#line 221 "include/linux/types.h"
  53typedef struct __anonstruct_atomic_t_6 atomic_t;
  54#line 226 "include/linux/types.h"
  55struct __anonstruct_atomic64_t_7 {
  56   long counter ;
  57};
  58#line 226 "include/linux/types.h"
  59typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  60#line 227 "include/linux/types.h"
  61struct list_head {
  62   struct list_head *next ;
  63   struct list_head *prev ;
  64};
  65#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  66struct module;
  67#line 55
  68struct module;
  69#line 146 "include/linux/init.h"
  70typedef void (*ctor_fn_t)(void);
  71#line 51 "include/linux/dynamic_debug.h"
  72struct net_device;
  73#line 51
  74struct net_device;
  75#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  76struct page;
  77#line 58
  78struct page;
  79#line 26 "include/asm-generic/getorder.h"
  80struct task_struct;
  81#line 26
  82struct task_struct;
  83#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  84struct arch_spinlock;
  85#line 327
  86struct arch_spinlock;
  87#line 306 "include/linux/bitmap.h"
  88struct bug_entry {
  89   int bug_addr_disp ;
  90   int file_disp ;
  91   unsigned short line ;
  92   unsigned short flags ;
  93};
  94#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
  95struct static_key;
  96#line 234
  97struct static_key;
  98#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  99struct kmem_cache;
 100#line 23 "include/asm-generic/atomic-long.h"
 101typedef atomic64_t atomic_long_t;
 102#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 103typedef u16 __ticket_t;
 104#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 105typedef u32 __ticketpair_t;
 106#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 107struct __raw_tickets {
 108   __ticket_t head ;
 109   __ticket_t tail ;
 110};
 111#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 112union __anonunion_ldv_5907_29 {
 113   __ticketpair_t head_tail ;
 114   struct __raw_tickets tickets ;
 115};
 116#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 117struct arch_spinlock {
 118   union __anonunion_ldv_5907_29 ldv_5907 ;
 119};
 120#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 121typedef struct arch_spinlock arch_spinlock_t;
 122#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 123struct lockdep_map;
 124#line 34
 125struct lockdep_map;
 126#line 55 "include/linux/debug_locks.h"
 127struct stack_trace {
 128   unsigned int nr_entries ;
 129   unsigned int max_entries ;
 130   unsigned long *entries ;
 131   int skip ;
 132};
 133#line 26 "include/linux/stacktrace.h"
 134struct lockdep_subclass_key {
 135   char __one_byte ;
 136};
 137#line 53 "include/linux/lockdep.h"
 138struct lock_class_key {
 139   struct lockdep_subclass_key subkeys[8U] ;
 140};
 141#line 59 "include/linux/lockdep.h"
 142struct lock_class {
 143   struct list_head hash_entry ;
 144   struct list_head lock_entry ;
 145   struct lockdep_subclass_key *key ;
 146   unsigned int subclass ;
 147   unsigned int dep_gen_id ;
 148   unsigned long usage_mask ;
 149   struct stack_trace usage_traces[13U] ;
 150   struct list_head locks_after ;
 151   struct list_head locks_before ;
 152   unsigned int version ;
 153   unsigned long ops ;
 154   char const   *name ;
 155   int name_version ;
 156   unsigned long contention_point[4U] ;
 157   unsigned long contending_point[4U] ;
 158};
 159#line 144 "include/linux/lockdep.h"
 160struct lockdep_map {
 161   struct lock_class_key *key ;
 162   struct lock_class *class_cache[2U] ;
 163   char const   *name ;
 164   int cpu ;
 165   unsigned long ip ;
 166};
 167#line 556 "include/linux/lockdep.h"
 168struct raw_spinlock {
 169   arch_spinlock_t raw_lock ;
 170   unsigned int magic ;
 171   unsigned int owner_cpu ;
 172   void *owner ;
 173   struct lockdep_map dep_map ;
 174};
 175#line 33 "include/linux/spinlock_types.h"
 176struct __anonstruct_ldv_6122_33 {
 177   u8 __padding[24U] ;
 178   struct lockdep_map dep_map ;
 179};
 180#line 33 "include/linux/spinlock_types.h"
 181union __anonunion_ldv_6123_32 {
 182   struct raw_spinlock rlock ;
 183   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 184};
 185#line 33 "include/linux/spinlock_types.h"
 186struct spinlock {
 187   union __anonunion_ldv_6123_32 ldv_6123 ;
 188};
 189#line 76 "include/linux/spinlock_types.h"
 190typedef struct spinlock spinlock_t;
 191#line 48 "include/linux/wait.h"
 192struct __wait_queue_head {
 193   spinlock_t lock ;
 194   struct list_head task_list ;
 195};
 196#line 53 "include/linux/wait.h"
 197typedef struct __wait_queue_head wait_queue_head_t;
 198#line 181 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/x86_init.h"
 199struct pci_dev;
 200#line 181
 201struct pci_dev;
 202#line 312 "include/linux/jiffies.h"
 203union ktime {
 204   s64 tv64 ;
 205};
 206#line 59 "include/linux/ktime.h"
 207typedef union ktime ktime_t;
 208#line 18 "include/linux/elf.h"
 209typedef __u64 Elf64_Addr;
 210#line 19 "include/linux/elf.h"
 211typedef __u16 Elf64_Half;
 212#line 23 "include/linux/elf.h"
 213typedef __u32 Elf64_Word;
 214#line 24 "include/linux/elf.h"
 215typedef __u64 Elf64_Xword;
 216#line 193 "include/linux/elf.h"
 217struct elf64_sym {
 218   Elf64_Word st_name ;
 219   unsigned char st_info ;
 220   unsigned char st_other ;
 221   Elf64_Half st_shndx ;
 222   Elf64_Addr st_value ;
 223   Elf64_Xword st_size ;
 224};
 225#line 201 "include/linux/elf.h"
 226typedef struct elf64_sym Elf64_Sym;
 227#line 445
 228struct sock;
 229#line 445
 230struct sock;
 231#line 446
 232struct kobject;
 233#line 446
 234struct kobject;
 235#line 447
 236enum kobj_ns_type {
 237    KOBJ_NS_TYPE_NONE = 0,
 238    KOBJ_NS_TYPE_NET = 1,
 239    KOBJ_NS_TYPES = 2
 240} ;
 241#line 453 "include/linux/elf.h"
 242struct kobj_ns_type_operations {
 243   enum kobj_ns_type type ;
 244   void *(*grab_current_ns)(void) ;
 245   void const   *(*netlink_ns)(struct sock * ) ;
 246   void const   *(*initial_ns)(void) ;
 247   void (*drop_ns)(void * ) ;
 248};
 249#line 57 "include/linux/kobject_ns.h"
 250struct attribute {
 251   char const   *name ;
 252   umode_t mode ;
 253   struct lock_class_key *key ;
 254   struct lock_class_key skey ;
 255};
 256#line 98 "include/linux/sysfs.h"
 257struct sysfs_ops {
 258   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 259   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 260   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 261};
 262#line 117
 263struct sysfs_dirent;
 264#line 117
 265struct sysfs_dirent;
 266#line 182 "include/linux/sysfs.h"
 267struct kref {
 268   atomic_t refcount ;
 269};
 270#line 49 "include/linux/kobject.h"
 271struct kset;
 272#line 49
 273struct kobj_type;
 274#line 49 "include/linux/kobject.h"
 275struct kobject {
 276   char const   *name ;
 277   struct list_head entry ;
 278   struct kobject *parent ;
 279   struct kset *kset ;
 280   struct kobj_type *ktype ;
 281   struct sysfs_dirent *sd ;
 282   struct kref kref ;
 283   unsigned char state_initialized : 1 ;
 284   unsigned char state_in_sysfs : 1 ;
 285   unsigned char state_add_uevent_sent : 1 ;
 286   unsigned char state_remove_uevent_sent : 1 ;
 287   unsigned char uevent_suppress : 1 ;
 288};
 289#line 107 "include/linux/kobject.h"
 290struct kobj_type {
 291   void (*release)(struct kobject * ) ;
 292   struct sysfs_ops  const  *sysfs_ops ;
 293   struct attribute **default_attrs ;
 294   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 295   void const   *(*namespace)(struct kobject * ) ;
 296};
 297#line 115 "include/linux/kobject.h"
 298struct kobj_uevent_env {
 299   char *envp[32U] ;
 300   int envp_idx ;
 301   char buf[2048U] ;
 302   int buflen ;
 303};
 304#line 122 "include/linux/kobject.h"
 305struct kset_uevent_ops {
 306   int (* const  filter)(struct kset * , struct kobject * ) ;
 307   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 308   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 309};
 310#line 139 "include/linux/kobject.h"
 311struct kset {
 312   struct list_head list ;
 313   spinlock_t list_lock ;
 314   struct kobject kobj ;
 315   struct kset_uevent_ops  const  *uevent_ops ;
 316};
 317#line 215
 318struct kernel_param;
 319#line 215
 320struct kernel_param;
 321#line 216 "include/linux/kobject.h"
 322struct kernel_param_ops {
 323   int (*set)(char const   * , struct kernel_param  const  * ) ;
 324   int (*get)(char * , struct kernel_param  const  * ) ;
 325   void (*free)(void * ) ;
 326};
 327#line 49 "include/linux/moduleparam.h"
 328struct kparam_string;
 329#line 49
 330struct kparam_array;
 331#line 49 "include/linux/moduleparam.h"
 332union __anonunion_ldv_13363_134 {
 333   void *arg ;
 334   struct kparam_string  const  *str ;
 335   struct kparam_array  const  *arr ;
 336};
 337#line 49 "include/linux/moduleparam.h"
 338struct kernel_param {
 339   char const   *name ;
 340   struct kernel_param_ops  const  *ops ;
 341   u16 perm ;
 342   s16 level ;
 343   union __anonunion_ldv_13363_134 ldv_13363 ;
 344};
 345#line 61 "include/linux/moduleparam.h"
 346struct kparam_string {
 347   unsigned int maxlen ;
 348   char *string ;
 349};
 350#line 67 "include/linux/moduleparam.h"
 351struct kparam_array {
 352   unsigned int max ;
 353   unsigned int elemsize ;
 354   unsigned int *num ;
 355   struct kernel_param_ops  const  *ops ;
 356   void *elem ;
 357};
 358#line 458 "include/linux/moduleparam.h"
 359struct static_key {
 360   atomic_t enabled ;
 361};
 362#line 225 "include/linux/jump_label.h"
 363struct tracepoint;
 364#line 225
 365struct tracepoint;
 366#line 226 "include/linux/jump_label.h"
 367struct tracepoint_func {
 368   void *func ;
 369   void *data ;
 370};
 371#line 29 "include/linux/tracepoint.h"
 372struct tracepoint {
 373   char const   *name ;
 374   struct static_key key ;
 375   void (*regfunc)(void) ;
 376   void (*unregfunc)(void) ;
 377   struct tracepoint_func *funcs ;
 378};
 379#line 86 "include/linux/tracepoint.h"
 380struct kernel_symbol {
 381   unsigned long value ;
 382   char const   *name ;
 383};
 384#line 27 "include/linux/export.h"
 385struct mod_arch_specific {
 386
 387};
 388#line 34 "include/linux/module.h"
 389struct module_param_attrs;
 390#line 34 "include/linux/module.h"
 391struct module_kobject {
 392   struct kobject kobj ;
 393   struct module *mod ;
 394   struct kobject *drivers_dir ;
 395   struct module_param_attrs *mp ;
 396};
 397#line 43 "include/linux/module.h"
 398struct module_attribute {
 399   struct attribute attr ;
 400   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 401   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 402                    size_t  ) ;
 403   void (*setup)(struct module * , char const   * ) ;
 404   int (*test)(struct module * ) ;
 405   void (*free)(struct module * ) ;
 406};
 407#line 69
 408struct exception_table_entry;
 409#line 69
 410struct exception_table_entry;
 411#line 198
 412enum module_state {
 413    MODULE_STATE_LIVE = 0,
 414    MODULE_STATE_COMING = 1,
 415    MODULE_STATE_GOING = 2
 416} ;
 417#line 204 "include/linux/module.h"
 418struct module_ref {
 419   unsigned long incs ;
 420   unsigned long decs ;
 421};
 422#line 219
 423struct module_sect_attrs;
 424#line 219
 425struct module_notes_attrs;
 426#line 219
 427struct ftrace_event_call;
 428#line 219 "include/linux/module.h"
 429struct module {
 430   enum module_state state ;
 431   struct list_head list ;
 432   char name[56U] ;
 433   struct module_kobject mkobj ;
 434   struct module_attribute *modinfo_attrs ;
 435   char const   *version ;
 436   char const   *srcversion ;
 437   struct kobject *holders_dir ;
 438   struct kernel_symbol  const  *syms ;
 439   unsigned long const   *crcs ;
 440   unsigned int num_syms ;
 441   struct kernel_param *kp ;
 442   unsigned int num_kp ;
 443   unsigned int num_gpl_syms ;
 444   struct kernel_symbol  const  *gpl_syms ;
 445   unsigned long const   *gpl_crcs ;
 446   struct kernel_symbol  const  *unused_syms ;
 447   unsigned long const   *unused_crcs ;
 448   unsigned int num_unused_syms ;
 449   unsigned int num_unused_gpl_syms ;
 450   struct kernel_symbol  const  *unused_gpl_syms ;
 451   unsigned long const   *unused_gpl_crcs ;
 452   struct kernel_symbol  const  *gpl_future_syms ;
 453   unsigned long const   *gpl_future_crcs ;
 454   unsigned int num_gpl_future_syms ;
 455   unsigned int num_exentries ;
 456   struct exception_table_entry *extable ;
 457   int (*init)(void) ;
 458   void *module_init ;
 459   void *module_core ;
 460   unsigned int init_size ;
 461   unsigned int core_size ;
 462   unsigned int init_text_size ;
 463   unsigned int core_text_size ;
 464   unsigned int init_ro_size ;
 465   unsigned int core_ro_size ;
 466   struct mod_arch_specific arch ;
 467   unsigned int taints ;
 468   unsigned int num_bugs ;
 469   struct list_head bug_list ;
 470   struct bug_entry *bug_table ;
 471   Elf64_Sym *symtab ;
 472   Elf64_Sym *core_symtab ;
 473   unsigned int num_symtab ;
 474   unsigned int core_num_syms ;
 475   char *strtab ;
 476   char *core_strtab ;
 477   struct module_sect_attrs *sect_attrs ;
 478   struct module_notes_attrs *notes_attrs ;
 479   char *args ;
 480   void *percpu ;
 481   unsigned int percpu_size ;
 482   unsigned int num_tracepoints ;
 483   struct tracepoint * const  *tracepoints_ptrs ;
 484   unsigned int num_trace_bprintk_fmt ;
 485   char const   **trace_bprintk_fmt_start ;
 486   struct ftrace_event_call **trace_events ;
 487   unsigned int num_trace_events ;
 488   struct list_head source_list ;
 489   struct list_head target_list ;
 490   struct task_struct *waiter ;
 491   void (*exit)(void) ;
 492   struct module_ref *refptr ;
 493   ctor_fn_t (**ctors)(void) ;
 494   unsigned int num_ctors ;
 495};
 496#line 88 "include/linux/kmemleak.h"
 497struct kmem_cache_cpu {
 498   void **freelist ;
 499   unsigned long tid ;
 500   struct page *page ;
 501   struct page *partial ;
 502   int node ;
 503   unsigned int stat[26U] ;
 504};
 505#line 55 "include/linux/slub_def.h"
 506struct kmem_cache_node {
 507   spinlock_t list_lock ;
 508   unsigned long nr_partial ;
 509   struct list_head partial ;
 510   atomic_long_t nr_slabs ;
 511   atomic_long_t total_objects ;
 512   struct list_head full ;
 513};
 514#line 66 "include/linux/slub_def.h"
 515struct kmem_cache_order_objects {
 516   unsigned long x ;
 517};
 518#line 76 "include/linux/slub_def.h"
 519struct kmem_cache {
 520   struct kmem_cache_cpu *cpu_slab ;
 521   unsigned long flags ;
 522   unsigned long min_partial ;
 523   int size ;
 524   int objsize ;
 525   int offset ;
 526   int cpu_partial ;
 527   struct kmem_cache_order_objects oo ;
 528   struct kmem_cache_order_objects max ;
 529   struct kmem_cache_order_objects min ;
 530   gfp_t allocflags ;
 531   int refcount ;
 532   void (*ctor)(void * ) ;
 533   int inuse ;
 534   int align ;
 535   int reserved ;
 536   char const   *name ;
 537   struct list_head list ;
 538   struct kobject kobj ;
 539   int remote_node_defrag_ratio ;
 540   struct kmem_cache_node *node[1024U] ;
 541};
 542#line 116 "include/linux/prio_tree.h"
 543struct address_space;
 544#line 116
 545struct address_space;
 546#line 117 "include/linux/prio_tree.h"
 547union __anonunion_ldv_14216_136 {
 548   unsigned long index ;
 549   void *freelist ;
 550};
 551#line 117 "include/linux/prio_tree.h"
 552struct __anonstruct_ldv_14226_140 {
 553   unsigned short inuse ;
 554   unsigned short objects : 15 ;
 555   unsigned char frozen : 1 ;
 556};
 557#line 117 "include/linux/prio_tree.h"
 558union __anonunion_ldv_14227_139 {
 559   atomic_t _mapcount ;
 560   struct __anonstruct_ldv_14226_140 ldv_14226 ;
 561};
 562#line 117 "include/linux/prio_tree.h"
 563struct __anonstruct_ldv_14229_138 {
 564   union __anonunion_ldv_14227_139 ldv_14227 ;
 565   atomic_t _count ;
 566};
 567#line 117 "include/linux/prio_tree.h"
 568union __anonunion_ldv_14230_137 {
 569   unsigned long counters ;
 570   struct __anonstruct_ldv_14229_138 ldv_14229 ;
 571};
 572#line 117 "include/linux/prio_tree.h"
 573struct __anonstruct_ldv_14231_135 {
 574   union __anonunion_ldv_14216_136 ldv_14216 ;
 575   union __anonunion_ldv_14230_137 ldv_14230 ;
 576};
 577#line 117 "include/linux/prio_tree.h"
 578struct __anonstruct_ldv_14238_142 {
 579   struct page *next ;
 580   int pages ;
 581   int pobjects ;
 582};
 583#line 117 "include/linux/prio_tree.h"
 584union __anonunion_ldv_14239_141 {
 585   struct list_head lru ;
 586   struct __anonstruct_ldv_14238_142 ldv_14238 ;
 587};
 588#line 117 "include/linux/prio_tree.h"
 589union __anonunion_ldv_14244_143 {
 590   unsigned long private ;
 591   struct kmem_cache *slab ;
 592   struct page *first_page ;
 593};
 594#line 117 "include/linux/prio_tree.h"
 595struct page {
 596   unsigned long flags ;
 597   struct address_space *mapping ;
 598   struct __anonstruct_ldv_14231_135 ldv_14231 ;
 599   union __anonunion_ldv_14239_141 ldv_14239 ;
 600   union __anonunion_ldv_14244_143 ldv_14244 ;
 601   unsigned long debug_flags ;
 602};
 603#line 177 "include/linux/textsearch.h"
 604struct exception_table_entry {
 605   unsigned long insn ;
 606   unsigned long fixup ;
 607};
 608#line 108 "include/net/checksum.h"
 609struct sk_buff;
 610#line 108
 611struct sk_buff;
 612#line 37 "include/linux/dmaengine.h"
 613typedef s32 dma_cookie_t;
 614#line 56 "include/linux/netdev_features.h"
 615struct nf_conntrack {
 616   atomic_t use ;
 617};
 618#line 116 "include/linux/skbuff.h"
 619struct nf_bridge_info {
 620   atomic_t use ;
 621   struct net_device *physindev ;
 622   struct net_device *physoutdev ;
 623   unsigned int mask ;
 624   unsigned long data[4U] ;
 625};
 626#line 126 "include/linux/skbuff.h"
 627struct sk_buff_head {
 628   struct sk_buff *next ;
 629   struct sk_buff *prev ;
 630   __u32 qlen ;
 631   spinlock_t lock ;
 632};
 633#line 318 "include/linux/skbuff.h"
 634typedef unsigned int sk_buff_data_t;
 635#line 319
 636struct sec_path;
 637#line 319 "include/linux/skbuff.h"
 638struct __anonstruct_ldv_19912_149 {
 639   __u16 csum_start ;
 640   __u16 csum_offset ;
 641};
 642#line 319 "include/linux/skbuff.h"
 643union __anonunion_ldv_19913_148 {
 644   __wsum csum ;
 645   struct __anonstruct_ldv_19912_149 ldv_19912 ;
 646};
 647#line 319 "include/linux/skbuff.h"
 648union __anonunion_ldv_19949_150 {
 649   __u32 mark ;
 650   __u32 dropcount ;
 651   __u32 avail_size ;
 652};
 653#line 319 "include/linux/skbuff.h"
 654struct sk_buff {
 655   struct sk_buff *next ;
 656   struct sk_buff *prev ;
 657   ktime_t tstamp ;
 658   struct sock *sk ;
 659   struct net_device *dev ;
 660   char cb[48U] ;
 661   unsigned long _skb_refdst ;
 662   struct sec_path *sp ;
 663   unsigned int len ;
 664   unsigned int data_len ;
 665   __u16 mac_len ;
 666   __u16 hdr_len ;
 667   union __anonunion_ldv_19913_148 ldv_19913 ;
 668   __u32 priority ;
 669   unsigned char local_df : 1 ;
 670   unsigned char cloned : 1 ;
 671   unsigned char ip_summed : 2 ;
 672   unsigned char nohdr : 1 ;
 673   unsigned char nfctinfo : 3 ;
 674   unsigned char pkt_type : 3 ;
 675   unsigned char fclone : 2 ;
 676   unsigned char ipvs_property : 1 ;
 677   unsigned char peeked : 1 ;
 678   unsigned char nf_trace : 1 ;
 679   __be16 protocol ;
 680   void (*destructor)(struct sk_buff * ) ;
 681   struct nf_conntrack *nfct ;
 682   struct sk_buff *nfct_reasm ;
 683   struct nf_bridge_info *nf_bridge ;
 684   int skb_iif ;
 685   __u32 rxhash ;
 686   __u16 vlan_tci ;
 687   __u16 tc_index ;
 688   __u16 tc_verd ;
 689   __u16 queue_mapping ;
 690   unsigned char ndisc_nodetype : 2 ;
 691   unsigned char ooo_okay : 1 ;
 692   unsigned char l4_rxhash : 1 ;
 693   unsigned char wifi_acked_valid : 1 ;
 694   unsigned char wifi_acked : 1 ;
 695   unsigned char no_fcs : 1 ;
 696   dma_cookie_t dma_cookie ;
 697   __u32 secmark ;
 698   union __anonunion_ldv_19949_150 ldv_19949 ;
 699   sk_buff_data_t transport_header ;
 700   sk_buff_data_t network_header ;
 701   sk_buff_data_t mac_header ;
 702   sk_buff_data_t tail ;
 703   sk_buff_data_t end ;
 704   unsigned char *head ;
 705   unsigned char *data ;
 706   unsigned int truesize ;
 707   atomic_t users ;
 708};
 709#line 54 "include/linux/delay.h"
 710enum irqreturn {
 711    IRQ_NONE = 0,
 712    IRQ_HANDLED = 1,
 713    IRQ_WAKE_THREAD = 2
 714} ;
 715#line 16 "include/linux/irqreturn.h"
 716typedef enum irqreturn irqreturn_t;
 717#line 348 "include/linux/irq.h"
 718struct proc_dir_entry;
 719#line 348
 720struct proc_dir_entry;
 721#line 702 "include/linux/interrupt.h"
 722struct capi_register_params {
 723   __u32 level3cnt ;
 724   __u32 datablkcnt ;
 725   __u32 datablklen ;
 726};
 727#line 29 "include/linux/capi.h"
 728typedef struct capi_register_params capi_register_params;
 729#line 30 "include/linux/capi.h"
 730struct capi_version {
 731   __u32 majorversion ;
 732   __u32 minorversion ;
 733   __u32 majormanuversion ;
 734   __u32 minormanuversion ;
 735};
 736#line 50 "include/linux/capi.h"
 737typedef struct capi_version capi_version;
 738#line 51 "include/linux/capi.h"
 739struct capi_profile {
 740   __u16 ncontroller ;
 741   __u16 nbchannel ;
 742   __u32 goptions ;
 743   __u32 support1 ;
 744   __u32 support2 ;
 745   __u32 support3 ;
 746   __u32 reserved[6U] ;
 747   __u32 manu[5U] ;
 748};
 749#line 74 "include/linux/capi.h"
 750typedef struct capi_profile capi_profile;
 751#line 152 "include/linux/kernelcapi.h"
 752struct capiloaddatapart {
 753   int user ;
 754   int len ;
 755   unsigned char *data ;
 756};
 757#line 24 "include/linux/isdn/capilli.h"
 758typedef struct capiloaddatapart capiloaddatapart;
 759#line 25 "include/linux/isdn/capilli.h"
 760struct capiloaddata {
 761   capiloaddatapart firmware ;
 762   capiloaddatapart configuration ;
 763};
 764#line 29 "include/linux/isdn/capilli.h"
 765typedef struct capiloaddata capiloaddata;
 766#line 30 "include/linux/isdn/capilli.h"
 767struct capicardparams {
 768   unsigned int port ;
 769   unsigned int irq ;
 770   int cardtype ;
 771   int cardnr ;
 772   unsigned int membase ;
 773};
 774#line 37 "include/linux/isdn/capilli.h"
 775typedef struct capicardparams capicardparams;
 776#line 38
 777struct file_operations;
 778#line 38 "include/linux/isdn/capilli.h"
 779struct capi_ctr {
 780   struct module *owner ;
 781   void *driverdata ;
 782   char name[32U] ;
 783   char *driver_name ;
 784   int (*load_firmware)(struct capi_ctr * , capiloaddata * ) ;
 785   void (*reset_ctr)(struct capi_ctr * ) ;
 786   void (*register_appl)(struct capi_ctr * , u16  , capi_register_params * ) ;
 787   void (*release_appl)(struct capi_ctr * , u16  ) ;
 788   u16 (*send_message)(struct capi_ctr * , struct sk_buff * ) ;
 789   char *(*procinfo)(struct capi_ctr * ) ;
 790   struct file_operations  const  *proc_fops ;
 791   u8 manu[64U] ;
 792   capi_version version ;
 793   capi_profile profile ;
 794   u8 serial[8U] ;
 795   unsigned long nrecvctlpkt ;
 796   unsigned long nrecvdatapkt ;
 797   unsigned long nsentctlpkt ;
 798   unsigned long nsentdatapkt ;
 799   int cnr ;
 800   unsigned short state ;
 801   int blocked ;
 802   int traceflag ;
 803   wait_queue_head_t state_wait_queue ;
 804   struct proc_dir_entry *procent ;
 805   char procfn[128U] ;
 806};
 807#line 86 "include/linux/isdn/capilli.h"
 808struct capi_driver {
 809   char name[32U] ;
 810   char revision[32U] ;
 811   int (*add_card)(struct capi_driver * , capicardparams * ) ;
 812   struct list_head list ;
 813};
 814#line 112
 815enum avmcardtype {
 816    avm_b1isa = 0,
 817    avm_b1pci = 1,
 818    avm_b1pcmcia = 2,
 819    avm_m1 = 3,
 820    avm_m2 = 4,
 821    avm_t1isa = 5,
 822    avm_t1pci = 6,
 823    avm_c4 = 7,
 824    avm_c2 = 8
 825} ;
 826#line 124 "include/linux/isdn/capilli.h"
 827struct avmcard_dmabuf {
 828   long size ;
 829   u8 *dmabuf ;
 830   dma_addr_t dmaaddr ;
 831};
 832#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 833typedef struct avmcard_dmabuf avmcard_dmabuf;
 834#line 51 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 835struct avmcard_dmainfo {
 836   u32 recvlen ;
 837   avmcard_dmabuf recvbuf ;
 838   avmcard_dmabuf sendbuf ;
 839   struct sk_buff_head send_queue ;
 840   struct pci_dev *pcidev ;
 841};
 842#line 60 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 843typedef struct avmcard_dmainfo avmcard_dmainfo;
 844#line 61
 845struct avmcard;
 846#line 61 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 847struct avmctrl_info {
 848   char cardname[32U] ;
 849   int versionlen ;
 850   char versionbuf[1024U] ;
 851   char *version[8U] ;
 852   char infobuf[128U] ;
 853   struct avmcard *card ;
 854   struct capi_ctr capi_ctrl ;
 855   struct list_head ncci_head ;
 856};
 857#line 75 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 858typedef struct avmctrl_info avmctrl_info;
 859#line 76 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 860struct avmcard {
 861   char name[32U] ;
 862   spinlock_t lock ;
 863   unsigned int port ;
 864   unsigned int irq ;
 865   unsigned long membase ;
 866   enum avmcardtype cardtype ;
 867   unsigned char revision ;
 868   unsigned char class ;
 869   int cardnr ;
 870   char msgbuf[128U] ;
 871   char databuf[2048U] ;
 872   void *mbase ;
 873   u32 volatile   csr ;
 874   avmcard_dmainfo *dma ;
 875   struct avmctrl_info *ctrlinfo ;
 876   u_int nr_controllers ;
 877   u_int nlogcontr ;
 878   struct list_head list ;
 879};
 880#line 101 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
 881typedef struct avmcard avmcard;
 882#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
 883void ldv_spin_lock(void) ;
 884#line 3
 885void ldv_spin_unlock(void) ;
 886#line 4
 887int ldv_spin_trylock(void) ;
 888#line 101 "include/linux/printk.h"
 889extern int printk(char const   *  , ...) ;
 890#line 320 "include/linux/kernel.h"
 891extern int sprintf(char * , char const   *  , ...) ;
 892#line 47 "include/linux/list.h"
 893extern void __list_add(struct list_head * , struct list_head * , struct list_head * ) ;
 894#line 60 "include/linux/list.h"
 895__inline static void list_add(struct list_head *new , struct list_head *head ) 
 896{ struct list_head *__cil_tmp3 ;
 897
 898  {
 899  {
 900#line 62
 901  __cil_tmp3 = *((struct list_head **)head);
 902#line 62
 903  __list_add(new, head, __cil_tmp3);
 904  }
 905#line 63
 906  return;
 907}
 908}
 909#line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
 910extern char *strcpy(char * , char const   * ) ;
 911#line 30 "include/linux/string.h"
 912extern size_t strlcpy(char * , char const   * , size_t  ) ;
 913#line 57
 914extern char *strchr(char const   * , int  ) ;
 915#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
 916__inline static void outb(unsigned char value , int port ) 
 917{ 
 918
 919  {
 920#line 308
 921  __asm__  volatile   ("outb %b0, %w1": : "a" (value), "Nd" (port));
 922#line 309
 923  return;
 924}
 925}
 926#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
 927__inline static unsigned char inb(int port ) 
 928{ unsigned char value ;
 929
 930  {
 931#line 308
 932  __asm__  volatile   ("inb %w1, %b0": "=a" (value): "Nd" (port));
 933#line 308
 934  return (value);
 935}
 936}
 937#line 26 "include/linux/export.h"
 938extern struct module __this_module ;
 939#line 220 "include/linux/slub_def.h"
 940extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
 941#line 223
 942void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
 943#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
 944void ldv_check_alloc_flags(gfp_t flags ) ;
 945#line 12
 946void ldv_check_alloc_nonatomic(void) ;
 947#line 14
 948struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
 949#line 591 "include/linux/skbuff.h"
 950extern struct sk_buff *skb_clone(struct sk_buff * , gfp_t  ) ;
 951#line 595
 952struct sk_buff *ldv_skb_clone_22(struct sk_buff *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
 953#line 597
 954extern struct sk_buff *skb_copy(struct sk_buff  const  * , gfp_t  ) ;
 955#line 601
 956struct sk_buff *ldv_skb_copy_24(struct sk_buff  const  *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
 957#line 606
 958extern int pskb_expand_head(struct sk_buff * , int  , int  , gfp_t  ) ;
 959#line 611
 960int ldv_pskb_expand_head_27(struct sk_buff *ldv_func_arg1 , int ldv_func_arg2 , int ldv_func_arg3 ,
 961                            gfp_t ldv_func_arg4 ) ;
 962#line 1690
 963extern struct sk_buff *__netdev_alloc_skb(struct net_device * , unsigned int  , gfp_t  ) ;
 964#line 1694
 965struct sk_buff *ldv___netdev_alloc_skb_25(struct net_device *ldv_func_arg1 , unsigned int ldv_func_arg2 ,
 966                                          gfp_t ldv_func_arg3 ) ;
 967#line 1698
 968struct sk_buff *ldv___netdev_alloc_skb_26(struct net_device *ldv_func_arg1 , unsigned int ldv_func_arg2 ,
 969                                          gfp_t ldv_func_arg3 ) ;
 970#line 10 "include/asm-generic/delay.h"
 971extern void __const_udelay(unsigned long  ) ;
 972#line 127 "include/linux/interrupt.h"
 973extern int request_threaded_irq(unsigned int  , irqreturn_t (*)(int  , void * ) ,
 974                                irqreturn_t (*)(int  , void * ) , unsigned long  ,
 975                                char const   * , void * ) ;
 976#line 132 "include/linux/interrupt.h"
 977__inline static int request_irq(unsigned int irq , irqreturn_t (*handler)(int  , void * ) ,
 978                                unsigned long flags , char const   *name , void *dev ) 
 979{ int tmp ;
 980  irqreturn_t (*__cil_tmp7)(int  , void * ) ;
 981
 982  {
 983  {
 984#line 135
 985  __cil_tmp7 = (irqreturn_t (*)(int  , void * ))0;
 986#line 135
 987  tmp = request_threaded_irq(irq, handler, __cil_tmp7, flags, name, dev);
 988  }
 989#line 135
 990  return (tmp);
 991}
 992}
 993#line 184
 994extern void free_irq(unsigned int  , void * ) ;
 995#line 16 "include/linux/b1pcmcia.h"
 996int b1pcmcia_addcard_b1(unsigned int port , unsigned int irq ) ;
 997#line 17
 998int b1pcmcia_addcard_m1(unsigned int port , unsigned int irq ) ;
 999#line 18
1000int b1pcmcia_addcard_m2(unsigned int port , unsigned int irq ) ;
1001#line 19
1002int b1pcmcia_delcard(unsigned int port , unsigned int irq ) ;
1003#line 78 "include/linux/isdn/capilli.h"
1004extern int attach_capi_ctr(struct capi_ctr * ) ;
1005#line 79
1006extern int detach_capi_ctr(struct capi_ctr * ) ;
1007#line 100
1008extern void register_capi_driver(struct capi_driver * ) ;
1009#line 101
1010extern void unregister_capi_driver(struct capi_driver * ) ;
1011#line 219 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
1012__inline static unsigned char b1outp(unsigned int base , unsigned short offset , unsigned char value ) 
1013{ unsigned char tmp ;
1014  int __cil_tmp5 ;
1015  unsigned char __cil_tmp6 ;
1016  unsigned int __cil_tmp7 ;
1017  unsigned int __cil_tmp8 ;
1018  int __cil_tmp9 ;
1019  unsigned int __cil_tmp10 ;
1020  int __cil_tmp11 ;
1021
1022  {
1023  {
1024#line 223
1025  __cil_tmp5 = (int )value;
1026#line 223
1027  __cil_tmp6 = (unsigned char )__cil_tmp5;
1028#line 223
1029  __cil_tmp7 = (unsigned int )offset;
1030#line 223
1031  __cil_tmp8 = __cil_tmp7 + base;
1032#line 223
1033  __cil_tmp9 = (int )__cil_tmp8;
1034#line 223
1035  outb(__cil_tmp6, __cil_tmp9);
1036#line 224
1037  __cil_tmp10 = base + 4U;
1038#line 224
1039  __cil_tmp11 = (int )__cil_tmp10;
1040#line 224
1041  tmp = inb(__cil_tmp11);
1042  }
1043#line 224
1044  return (tmp);
1045}
1046}
1047#line 318 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/isdn/hardware/avm/avmcard.h"
1048__inline static void b1_reset(unsigned int base ) 
1049{ unsigned long __ms ;
1050  unsigned long tmp ;
1051  unsigned long __ms___0 ;
1052  unsigned long tmp___0 ;
1053  unsigned long __ms___1 ;
1054  unsigned long tmp___1 ;
1055
1056  {
1057  {
1058#line 320
1059  b1outp(base, (unsigned short)16, (unsigned char)0);
1060#line 321
1061  __ms = 110UL;
1062  }
1063#line 321
1064  goto ldv_22905;
1065  ldv_22904: 
1066  {
1067#line 321
1068  __const_udelay(4295000UL);
1069  }
1070  ldv_22905: 
1071#line 321
1072  tmp = __ms;
1073#line 321
1074  __ms = __ms - 1UL;
1075#line 321
1076  if (tmp != 0UL) {
1077#line 322
1078    goto ldv_22904;
1079  } else {
1080#line 324
1081    goto ldv_22906;
1082  }
1083  ldv_22906: 
1084  {
1085#line 323
1086  b1outp(base, (unsigned short)16, (unsigned char)1);
1087#line 324
1088  __ms___0 = 110UL;
1089  }
1090#line 324
1091  goto ldv_22909;
1092  ldv_22908: 
1093  {
1094#line 324
1095  __const_udelay(4295000UL);
1096  }
1097  ldv_22909: 
1098#line 324
1099  tmp___0 = __ms___0;
1100#line 324
1101  __ms___0 = __ms___0 - 1UL;
1102#line 324
1103  if (tmp___0 != 0UL) {
1104#line 325
1105    goto ldv_22908;
1106  } else {
1107#line 327
1108    goto ldv_22910;
1109  }
1110  ldv_22910: 
1111  {
1112#line 326
1113  b1outp(base, (unsigned short)16, (unsigned char)0);
1114#line 327
1115  __ms___1 = 110UL;
1116  }
1117#line 327
1118  goto ldv_22913;
1119  ldv_22912: 
1120  {
1121#line 327
1122  __const_udelay(4295000UL);
1123  }
1124  ldv_22913: 
1125#line 327
1126  tmp___1 = __ms___1;
1127#line 327
1128  __ms___1 = __ms___1 - 1UL;
1129#line 327
1130  if (tmp___1 != 0UL) {
1131#line 328
1132    goto ldv_22912;
1133  } else {
1134#line 330
1135    goto ldv_22914;
1136  }
1137  ldv_22914: ;
1138#line 334
1139  return;
1140}
1141}
1142#line 542
1143extern avmcard *b1_alloc_card(int  ) ;
1144#line 543
1145extern void b1_free_card(avmcard * ) ;
1146#line 544
1147extern int b1_detect(unsigned int  , enum avmcardtype  ) ;
1148#line 545
1149extern void b1_getrevision(avmcard * ) ;
1150#line 550
1151extern int b1_load_firmware(struct capi_ctr * , capiloaddata * ) ;
1152#line 551
1153extern void b1_reset_ctr(struct capi_ctr * ) ;
1154#line 552
1155extern void b1_register_appl(struct capi_ctr * , u16  , capi_register_params * ) ;
1156#line 554
1157extern void b1_release_appl(struct capi_ctr * , u16  ) ;
1158#line 555
1159extern u16 b1_send_message(struct capi_ctr * , struct sk_buff * ) ;
1160#line 557
1161extern irqreturn_t b1_interrupt(int  , void * ) ;
1162#line 559
1163extern struct file_operations  const  b1ctl_proc_fops ;
1164#line 45 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
1165static char *revision  =    (char *)"$Revision: 1.1.2.2 $";
1166#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
1167static void b1pcmcia_remove_ctr(struct capi_ctr *ctrl ) 
1168{ avmctrl_info *cinfo ;
1169  avmcard *card ;
1170  unsigned int port ;
1171  unsigned long __cil_tmp5 ;
1172  unsigned long __cil_tmp6 ;
1173  void *__cil_tmp7 ;
1174  unsigned long __cil_tmp8 ;
1175  unsigned long __cil_tmp9 ;
1176  unsigned long __cil_tmp10 ;
1177  unsigned long __cil_tmp11 ;
1178  unsigned long __cil_tmp12 ;
1179  unsigned long __cil_tmp13 ;
1180  unsigned int __cil_tmp14 ;
1181  void *__cil_tmp15 ;
1182
1183  {
1184  {
1185#line 57
1186  __cil_tmp5 = (unsigned long )ctrl;
1187#line 57
1188  __cil_tmp6 = __cil_tmp5 + 8;
1189#line 57
1190  __cil_tmp7 = *((void **)__cil_tmp6);
1191#line 57
1192  cinfo = (avmctrl_info *)__cil_tmp7;
1193#line 58
1194  __cil_tmp8 = (unsigned long )cinfo;
1195#line 58
1196  __cil_tmp9 = __cil_tmp8 + 1256;
1197#line 58
1198  card = *((struct avmcard **)__cil_tmp9);
1199#line 59
1200  __cil_tmp10 = (unsigned long )card;
1201#line 59
1202  __cil_tmp11 = __cil_tmp10 + 104;
1203#line 59
1204  port = *((unsigned int *)__cil_tmp11);
1205#line 61
1206  b1_reset(port);
1207#line 62
1208  b1_reset(port);
1209#line 64
1210  detach_capi_ctr(ctrl);
1211#line 65
1212  __cil_tmp12 = (unsigned long )card;
1213#line 65
1214  __cil_tmp13 = __cil_tmp12 + 108;
1215#line 65
1216  __cil_tmp14 = *((unsigned int *)__cil_tmp13);
1217#line 65
1218  __cil_tmp15 = (void *)card;
1219#line 65
1220  free_irq(__cil_tmp14, __cil_tmp15);
1221#line 66
1222  b1_free_card(card);
1223  }
1224#line 67
1225  return;
1226}
1227}
1228#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
1229static struct list_head cards  =    {& cards, & cards};
1230#line 73
1231static char *b1pcmcia_procinfo(struct capi_ctr *ctrl ) ;
1232#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
1233static int b1pcmcia_add_card(unsigned int port , unsigned int irq , enum avmcardtype cardtype ) 
1234{ avmctrl_info *cinfo ;
1235  avmcard *card ;
1236  char *cardname ;
1237  int retval ;
1238  avmcard *__cil_tmp8 ;
1239  unsigned long __cil_tmp9 ;
1240  unsigned long __cil_tmp10 ;
1241  unsigned long __cil_tmp11 ;
1242  unsigned long __cil_tmp12 ;
1243  unsigned int __cil_tmp13 ;
1244  char (*__cil_tmp14)[32U] ;
1245  char *__cil_tmp15 ;
1246  char (*__cil_tmp16)[32U] ;
1247  char *__cil_tmp17 ;
1248  char (*__cil_tmp18)[32U] ;
1249  char *__cil_tmp19 ;
1250  unsigned long __cil_tmp20 ;
1251  unsigned long __cil_tmp21 ;
1252  unsigned long __cil_tmp22 ;
1253  unsigned long __cil_tmp23 ;
1254  unsigned long __cil_tmp24 ;
1255  unsigned long __cil_tmp25 ;
1256  unsigned long __cil_tmp26 ;
1257  unsigned long __cil_tmp27 ;
1258  unsigned int __cil_tmp28 ;
1259  char (*__cil_tmp29)[32U] ;
1260  char const   *__cil_tmp30 ;
1261  void *__cil_tmp31 ;
1262  unsigned long __cil_tmp32 ;
1263  unsigned long __cil_tmp33 ;
1264  unsigned int __cil_tmp34 ;
1265  unsigned long __cil_tmp35 ;
1266  unsigned long __cil_tmp36 ;
1267  unsigned int __cil_tmp37 ;
1268  unsigned long __cil_tmp38 ;
1269  unsigned long __cil_tmp39 ;
1270  unsigned int __cil_tmp40 ;
1271  unsigned long __cil_tmp41 ;
1272  unsigned long __cil_tmp42 ;
1273  enum avmcardtype __cil_tmp43 ;
1274  unsigned long __cil_tmp44 ;
1275  unsigned long __cil_tmp45 ;
1276  unsigned int __cil_tmp46 ;
1277  unsigned long __cil_tmp47 ;
1278  unsigned long __cil_tmp48 ;
1279  unsigned int __cil_tmp49 ;
1280  unsigned long __cil_tmp50 ;
1281  unsigned long __cil_tmp51 ;
1282  unsigned long __cil_tmp52 ;
1283  unsigned long __cil_tmp53 ;
1284  unsigned long __cil_tmp54 ;
1285  unsigned long __cil_tmp55 ;
1286  unsigned long __cil_tmp56 ;
1287  unsigned long __cil_tmp57 ;
1288  unsigned long __cil_tmp58 ;
1289  unsigned long __cil_tmp59 ;
1290  unsigned long __cil_tmp60 ;
1291  unsigned long __cil_tmp61 ;
1292  unsigned long __cil_tmp62 ;
1293  unsigned long __cil_tmp63 ;
1294  unsigned long __cil_tmp64 ;
1295  unsigned long __cil_tmp65 ;
1296  unsigned long __cil_tmp66 ;
1297  unsigned long __cil_tmp67 ;
1298  unsigned long __cil_tmp68 ;
1299  unsigned long __cil_tmp69 ;
1300  unsigned long __cil_tmp70 ;
1301  unsigned long __cil_tmp71 ;
1302  unsigned long __cil_tmp72 ;
1303  unsigned long __cil_tmp73 ;
1304  unsigned long __cil_tmp74 ;
1305  unsigned long __cil_tmp75 ;
1306  unsigned long __cil_tmp76 ;
1307  unsigned long __cil_tmp77 ;
1308  unsigned long __cil_tmp78 ;
1309  unsigned long __cil_tmp79 ;
1310  unsigned long __cil_tmp80 ;
1311  unsigned long __cil_tmp81 ;
1312  char (*__cil_tmp82)[32U] ;
1313  char *__cil_tmp83 ;
1314  char (*__cil_tmp84)[32U] ;
1315  char const   *__cil_tmp85 ;
1316  unsigned long __cil_tmp86 ;
1317  unsigned long __cil_tmp87 ;
1318  struct capi_ctr *__cil_tmp88 ;
1319  unsigned int __cil_tmp89 ;
1320  unsigned long __cil_tmp90 ;
1321  unsigned long __cil_tmp91 ;
1322  unsigned int __cil_tmp92 ;
1323  unsigned long __cil_tmp93 ;
1324  unsigned long __cil_tmp94 ;
1325  unsigned int __cil_tmp95 ;
1326  unsigned long __cil_tmp96 ;
1327  unsigned long __cil_tmp97 ;
1328  unsigned char __cil_tmp98 ;
1329  int __cil_tmp99 ;
1330  unsigned long __cil_tmp100 ;
1331  unsigned long __cil_tmp101 ;
1332  struct list_head *__cil_tmp102 ;
1333  unsigned long __cil_tmp103 ;
1334  unsigned long __cil_tmp104 ;
1335  unsigned long __cil_tmp105 ;
1336  unsigned long __cil_tmp106 ;
1337  unsigned long __cil_tmp107 ;
1338  unsigned int __cil_tmp108 ;
1339  void *__cil_tmp109 ;
1340
1341  {
1342  {
1343#line 83
1344  card = b1_alloc_card(1);
1345  }
1346  {
1347#line 84
1348  __cil_tmp8 = (avmcard *)0;
1349#line 84
1350  __cil_tmp9 = (unsigned long )__cil_tmp8;
1351#line 84
1352  __cil_tmp10 = (unsigned long )card;
1353#line 84
1354  if (__cil_tmp10 == __cil_tmp9) {
1355    {
1356#line 85
1357    printk("<4>b1pcmcia: no memory.\n");
1358#line 86
1359    retval = -12;
1360    }
1361#line 87
1362    goto err;
1363  } else {
1364
1365  }
1366  }
1367#line 89
1368  __cil_tmp11 = (unsigned long )card;
1369#line 89
1370  __cil_tmp12 = __cil_tmp11 + 2336;
1371#line 89
1372  cinfo = *((struct avmctrl_info **)__cil_tmp12);
1373  {
1374#line 91
1375  __cil_tmp13 = (unsigned int )cardtype;
1376#line 92
1377  if ((int )__cil_tmp13 == 3) {
1378#line 92
1379    goto case_3;
1380  } else
1381#line 93
1382  if ((int )__cil_tmp13 == 4) {
1383#line 93
1384    goto case_4;
1385  } else {
1386    {
1387#line 94
1388    goto switch_default;
1389#line 91
1390    if (0) {
1391      case_3: /* CIL Label */ 
1392      {
1393#line 92
1394      __cil_tmp14 = (char (*)[32U])card;
1395#line 92
1396      __cil_tmp15 = (char *)__cil_tmp14;
1397#line 92
1398      sprintf(__cil_tmp15, "m1-%x", port);
1399      }
1400#line 92
1401      goto ldv_23092;
1402      case_4: /* CIL Label */ 
1403      {
1404#line 93
1405      __cil_tmp16 = (char (*)[32U])card;
1406#line 93
1407      __cil_tmp17 = (char *)__cil_tmp16;
1408#line 93
1409      sprintf(__cil_tmp17, "m2-%x", port);
1410      }
1411#line 93
1412      goto ldv_23092;
1413      switch_default: /* CIL Label */ 
1414      {
1415#line 94
1416      __cil_tmp18 = (char (*)[32U])card;
1417#line 94
1418      __cil_tmp19 = (char *)__cil_tmp18;
1419#line 94
1420      sprintf(__cil_tmp19, "b1pcmcia-%x", port);
1421      }
1422#line 94
1423      goto ldv_23092;
1424    } else {
1425      switch_break: /* CIL Label */ ;
1426    }
1427    }
1428  }
1429  }
1430  ldv_23092: 
1431  {
1432#line 96
1433  __cil_tmp20 = (unsigned long )card;
1434#line 96
1435  __cil_tmp21 = __cil_tmp20 + 104;
1436#line 96
1437  *((unsigned int *)__cil_tmp21) = port;
1438#line 97
1439  __cil_tmp22 = (unsigned long )card;
1440#line 97
1441  __cil_tmp23 = __cil_tmp22 + 108;
1442#line 97
1443  *((unsigned int *)__cil_tmp23) = irq;
1444#line 98
1445  __cil_tmp24 = (unsigned long )card;
1446#line 98
1447  __cil_tmp25 = __cil_tmp24 + 120;
1448#line 98
1449  *((enum avmcardtype *)__cil_tmp25) = cardtype;
1450#line 100
1451  __cil_tmp26 = (unsigned long )card;
1452#line 100
1453  __cil_tmp27 = __cil_tmp26 + 108;
1454#line 100
1455  __cil_tmp28 = *((unsigned int *)__cil_tmp27);
1456#line 100
1457  __cil_tmp29 = (char (*)[32U])card;
1458#line 100
1459  __cil_tmp30 = (char const   *)__cil_tmp29;
1460#line 100
1461  __cil_tmp31 = (void *)card;
1462#line 100
1463  retval = request_irq(__cil_tmp28, & b1_interrupt, 128UL, __cil_tmp30, __cil_tmp31);
1464  }
1465#line 101
1466  if (retval != 0) {
1467    {
1468#line 102
1469    __cil_tmp32 = (unsigned long )card;
1470#line 102
1471    __cil_tmp33 = __cil_tmp32 + 108;
1472#line 102
1473    __cil_tmp34 = *((unsigned int *)__cil_tmp33);
1474#line 102
1475    printk("<3>b1pcmcia: unable to get IRQ %d.\n", __cil_tmp34);
1476#line 104
1477    retval = -16;
1478    }
1479#line 105
1480    goto err_free;
1481  } else {
1482
1483  }
1484  {
1485#line 107
1486  __cil_tmp35 = (unsigned long )card;
1487#line 107
1488  __cil_tmp36 = __cil_tmp35 + 104;
1489#line 107
1490  __cil_tmp37 = *((unsigned int *)__cil_tmp36);
1491#line 107
1492  b1_reset(__cil_tmp37);
1493#line 108
1494  __cil_tmp38 = (unsigned long )card;
1495#line 108
1496  __cil_tmp39 = __cil_tmp38 + 104;
1497#line 108
1498  __cil_tmp40 = *((unsigned int *)__cil_tmp39);
1499#line 108
1500  __cil_tmp41 = (unsigned long )card;
1501#line 108
1502  __cil_tmp42 = __cil_tmp41 + 120;
1503#line 108
1504  __cil_tmp43 = *((enum avmcardtype *)__cil_tmp42);
1505#line 108
1506  retval = b1_detect(__cil_tmp40, __cil_tmp43);
1507  }
1508#line 108
1509  if (retval != 0) {
1510    {
1511#line 109
1512    __cil_tmp44 = (unsigned long )card;
1513#line 109
1514    __cil_tmp45 = __cil_tmp44 + 104;
1515#line 109
1516    __cil_tmp46 = *((unsigned int *)__cil_tmp45);
1517#line 109
1518    printk("<5>b1pcmcia: NO card at 0x%x (%d)\n", __cil_tmp46, retval);
1519#line 111
1520    retval = -19;
1521    }
1522#line 112
1523    goto err_free_irq;
1524  } else {
1525
1526  }
1527  {
1528#line 114
1529  __cil_tmp47 = (unsigned long )card;
1530#line 114
1531  __cil_tmp48 = __cil_tmp47 + 104;
1532#line 114
1533  __cil_tmp49 = *((unsigned int *)__cil_tmp48);
1534#line 114
1535  b1_reset(__cil_tmp49);
1536#line 115
1537  b1_getrevision(card);
1538#line 117
1539  __cil_tmp50 = (unsigned long )cinfo;
1540#line 117
1541  __cil_tmp51 = __cil_tmp50 + 1264;
1542#line 117
1543  *((struct module **)__cil_tmp51) = & __this_module;
1544#line 118
1545  __cil_tmp52 = 1264 + 48;
1546#line 118
1547  __cil_tmp53 = (unsigned long )cinfo;
1548#line 118
1549  __cil_tmp54 = __cil_tmp53 + __cil_tmp52;
1550#line 118
1551  *((char **)__cil_tmp54) = (char *)"b1pcmcia";
1552#line 119
1553  __cil_tmp55 = 1264 + 8;
1554#line 119
1555  __cil_tmp56 = (unsigned long )cinfo;
1556#line 119
1557  __cil_tmp57 = __cil_tmp56 + __cil_tmp55;
1558#line 119
1559  *((void **)__cil_tmp57) = (void *)cinfo;
1560#line 120
1561  __cil_tmp58 = 1264 + 72;
1562#line 120
1563  __cil_tmp59 = (unsigned long )cinfo;
1564#line 120
1565  __cil_tmp60 = __cil_tmp59 + __cil_tmp58;
1566#line 120
1567  *((void (**)(struct capi_ctr * , u16  , capi_register_params * ))__cil_tmp60) = & b1_register_appl;
1568#line 121
1569  __cil_tmp61 = 1264 + 80;
1570#line 121
1571  __cil_tmp62 = (unsigned long )cinfo;
1572#line 121
1573  __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
1574#line 121
1575  *((void (**)(struct capi_ctr * , u16  ))__cil_tmp63) = & b1_release_appl;
1576#line 122
1577  __cil_tmp64 = 1264 + 88;
1578#line 122
1579  __cil_tmp65 = (unsigned long )cinfo;
1580#line 122
1581  __cil_tmp66 = __cil_tmp65 + __cil_tmp64;
1582#line 122
1583  *((u16 (**)(struct capi_ctr * , struct sk_buff * ))__cil_tmp66) = & b1_send_message;
1584#line 123
1585  __cil_tmp67 = 1264 + 56;
1586#line 123
1587  __cil_tmp68 = (unsigned long )cinfo;
1588#line 123
1589  __cil_tmp69 = __cil_tmp68 + __cil_tmp67;
1590#line 123
1591  *((int (**)(struct capi_ctr * , capiloaddata * ))__cil_tmp69) = & b1_load_firmware;
1592#line 124
1593  __cil_tmp70 = 1264 + 64;
1594#line 124
1595  __cil_tmp71 = (unsigned long )cinfo;
1596#line 124
1597  __cil_tmp72 = __cil_tmp71 + __cil_tmp70;
1598#line 124
1599  *((void (**)(struct capi_ctr * ))__cil_tmp72) = & b1_reset_ctr;
1600#line 125
1601  __cil_tmp73 = 1264 + 96;
1602#line 125
1603  __cil_tmp74 = (unsigned long )cinfo;
1604#line 125
1605  __cil_tmp75 = __cil_tmp74 + __cil_tmp73;
1606#line 125
1607  *((char *(**)(struct capi_ctr * ))__cil_tmp75) = & b1pcmcia_procinfo;
1608#line 126
1609  __cil_tmp76 = 1264 + 104;
1610#line 126
1611  __cil_tmp77 = (unsigned long )cinfo;
1612#line 126
1613  __cil_tmp78 = __cil_tmp77 + __cil_tmp76;
1614#line 126
1615  *((struct file_operations  const  **)__cil_tmp78) = & b1ctl_proc_fops;
1616#line 127
1617  __cil_tmp79 = 1264 + 16;
1618#line 127
1619  __cil_tmp80 = (unsigned long )cinfo;
1620#line 127
1621  __cil_tmp81 = __cil_tmp80 + __cil_tmp79;
1622#line 127
1623  __cil_tmp82 = (char (*)[32U])__cil_tmp81;
1624#line 127
1625  __cil_tmp83 = (char *)__cil_tmp82;
1626#line 127
1627  __cil_tmp84 = (char (*)[32U])card;
1628#line 127
1629  __cil_tmp85 = (char const   *)__cil_tmp84;
1630#line 127
1631  strcpy(__cil_tmp83, __cil_tmp85);
1632#line 129
1633  __cil_tmp86 = (unsigned long )cinfo;
1634#line 129
1635  __cil_tmp87 = __cil_tmp86 + 1264;
1636#line 129
1637  __cil_tmp88 = (struct capi_ctr *)__cil_tmp87;
1638#line 129
1639  retval = attach_capi_ctr(__cil_tmp88);
1640  }
1641#line 130
1642  if (retval != 0) {
1643    {
1644#line 131
1645    printk("<3>b1pcmcia: attach controller failed.\n");
1646    }
1647#line 132
1648    goto err_free_irq;
1649  } else {
1650
1651  }
1652  {
1653#line 134
1654  __cil_tmp89 = (unsigned int )cardtype;
1655#line 135
1656  if ((int )__cil_tmp89 == 3) {
1657#line 135
1658    goto case_3___0;
1659  } else
1660#line 136
1661  if ((int )__cil_tmp89 == 4) {
1662#line 136
1663    goto case_4___0;
1664  } else {
1665    {
1666#line 137
1667    goto switch_default___0;
1668#line 134
1669    if (0) {
1670      case_3___0: /* CIL Label */ 
1671#line 135
1672      cardname = (char *)"M1";
1673#line 135
1674      goto ldv_23098;
1675      case_4___0: /* CIL Label */ 
1676#line 136
1677      cardname = (char *)"M2";
1678#line 136
1679      goto ldv_23098;
1680      switch_default___0: /* CIL Label */ 
1681#line 137
1682      cardname = (char *)"B1 PCMCIA";
1683#line 137
1684      goto ldv_23098;
1685    } else {
1686      switch_break___0: /* CIL Label */ ;
1687    }
1688    }
1689  }
1690  }
1691  ldv_23098: 
1692  {
1693#line 140
1694  __cil_tmp90 = (unsigned long )card;
1695#line 140
1696  __cil_tmp91 = __cil_tmp90 + 104;
1697#line 140
1698  __cil_tmp92 = *((unsigned int *)__cil_tmp91);
1699#line 140
1700  __cil_tmp93 = (unsigned long )card;
1701#line 140
1702  __cil_tmp94 = __cil_tmp93 + 108;
1703#line 140
1704  __cil_tmp95 = *((unsigned int *)__cil_tmp94);
1705#line 140
1706  __cil_tmp96 = (unsigned long )card;
1707#line 140
1708  __cil_tmp97 = __cil_tmp96 + 124;
1709#line 140
1710  __cil_tmp98 = *((unsigned char *)__cil_tmp97);
1711#line 140
1712  __cil_tmp99 = (int )__cil_tmp98;
1713#line 140
1714  printk("<6>b1pcmcia: AVM %s at i/o %#x, irq %d, revision %d\n", cardname, __cil_tmp92,
1715         __cil_tmp95, __cil_tmp99);
1716#line 143
1717  __cil_tmp100 = (unsigned long )card;
1718#line 143
1719  __cil_tmp101 = __cil_tmp100 + 2352;
1720#line 143
1721  __cil_tmp102 = (struct list_head *)__cil_tmp101;
1722#line 143
1723  list_add(__cil_tmp102, & cards);
1724  }
1725  {
1726#line 144
1727  __cil_tmp103 = 1264 + 296;
1728#line 144
1729  __cil_tmp104 = (unsigned long )cinfo;
1730#line 144
1731  __cil_tmp105 = __cil_tmp104 + __cil_tmp103;
1732#line 144
1733  return (*((int *)__cil_tmp105));
1734  }
1735  err_free_irq: 
1736  {
1737#line 147
1738  __cil_tmp106 = (unsigned long )card;
1739#line 147
1740  __cil_tmp107 = __cil_tmp106 + 108;
1741#line 147
1742  __cil_tmp108 = *((unsigned int *)__cil_tmp107);
1743#line 147
1744  __cil_tmp109 = (void *)card;
1745#line 147
1746  free_irq(__cil_tmp108, __cil_tmp109);
1747  }
1748  err_free: 
1749  {
1750#line 149
1751  b1_free_card(card);
1752  }
1753  err: ;
1754#line 151
1755  return (retval);
1756}
1757}
1758#line 156 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
1759static char *b1pcmcia_procinfo(struct capi_ctr *ctrl ) 
1760{ avmctrl_info *cinfo ;
1761  int tmp ;
1762  unsigned int tmp___0 ;
1763  unsigned int tmp___1 ;
1764  char *tmp___2 ;
1765  char *tmp___3 ;
1766  unsigned long __cil_tmp8 ;
1767  unsigned long __cil_tmp9 ;
1768  void *__cil_tmp10 ;
1769  avmctrl_info *__cil_tmp11 ;
1770  unsigned long __cil_tmp12 ;
1771  unsigned long __cil_tmp13 ;
1772  struct avmcard *__cil_tmp14 ;
1773  unsigned long __cil_tmp15 ;
1774  unsigned long __cil_tmp16 ;
1775  unsigned long __cil_tmp17 ;
1776  struct avmcard *__cil_tmp18 ;
1777  unsigned long __cil_tmp19 ;
1778  unsigned long __cil_tmp20 ;
1779  unsigned long __cil_tmp21 ;
1780  struct avmcard *__cil_tmp22 ;
1781  unsigned long __cil_tmp23 ;
1782  unsigned long __cil_tmp24 ;
1783  unsigned char __cil_tmp25 ;
1784  struct avmcard *__cil_tmp26 ;
1785  unsigned long __cil_tmp27 ;
1786  unsigned long __cil_tmp28 ;
1787  unsigned long __cil_tmp29 ;
1788  struct avmcard *__cil_tmp30 ;
1789  unsigned long __cil_tmp31 ;
1790  unsigned long __cil_tmp32 ;
1791  unsigned long __cil_tmp33 ;
1792  struct avmcard *__cil_tmp34 ;
1793  unsigned long __cil_tmp35 ;
1794  unsigned long __cil_tmp36 ;
1795  struct avmcard *__cil_tmp37 ;
1796  unsigned long __cil_tmp38 ;
1797  unsigned long __cil_tmp39 ;
1798  unsigned long __cil_tmp40 ;
1799  struct avmcard *__cil_tmp41 ;
1800  unsigned long __cil_tmp42 ;
1801  unsigned long __cil_tmp43 ;
1802  unsigned long __cil_tmp44 ;
1803  struct avmcard *__cil_tmp45 ;
1804  unsigned long __cil_tmp46 ;
1805  unsigned long __cil_tmp47 ;
1806  char *__cil_tmp48 ;
1807  unsigned long __cil_tmp49 ;
1808  unsigned long __cil_tmp50 ;
1809  unsigned long __cil_tmp51 ;
1810  unsigned long __cil_tmp52 ;
1811  unsigned long __cil_tmp53 ;
1812  char *__cil_tmp54 ;
1813  unsigned long __cil_tmp55 ;
1814  unsigned long __cil_tmp56 ;
1815  unsigned long __cil_tmp57 ;
1816  unsigned long __cil_tmp58 ;
1817  unsigned long __cil_tmp59 ;
1818  unsigned long __cil_tmp60 ;
1819  unsigned long __cil_tmp61 ;
1820  unsigned long __cil_tmp62 ;
1821  unsigned long __cil_tmp63 ;
1822  char __cil_tmp64 ;
1823  signed char __cil_tmp65 ;
1824  int __cil_tmp66 ;
1825  char (*__cil_tmp67)[32U] ;
1826  unsigned long __cil_tmp68 ;
1827  unsigned long __cil_tmp69 ;
1828  char (*__cil_tmp70)[128U] ;
1829  char *__cil_tmp71 ;
1830  unsigned long __cil_tmp72 ;
1831  unsigned long __cil_tmp73 ;
1832  char (*__cil_tmp74)[128U] ;
1833
1834  {
1835#line 158
1836  __cil_tmp8 = (unsigned long )ctrl;
1837#line 158
1838  __cil_tmp9 = __cil_tmp8 + 8;
1839#line 158
1840  __cil_tmp10 = *((void **)__cil_tmp9);
1841#line 158
1842  cinfo = (avmctrl_info *)__cil_tmp10;
1843  {
1844#line 160
1845  __cil_tmp11 = (avmctrl_info *)0;
1846#line 160
1847  __cil_tmp12 = (unsigned long )__cil_tmp11;
1848#line 160
1849  __cil_tmp13 = (unsigned long )cinfo;
1850#line 160
1851  if (__cil_tmp13 == __cil_tmp12) {
1852#line 161
1853    return ((char *)"");
1854  } else {
1855
1856  }
1857  }
1858  {
1859#line 162
1860  __cil_tmp14 = (struct avmcard *)0;
1861#line 162
1862  __cil_tmp15 = (unsigned long )__cil_tmp14;
1863#line 162
1864  __cil_tmp16 = (unsigned long )cinfo;
1865#line 162
1866  __cil_tmp17 = __cil_tmp16 + 1256;
1867#line 162
1868  __cil_tmp18 = *((struct avmcard **)__cil_tmp17);
1869#line 162
1870  __cil_tmp19 = (unsigned long )__cil_tmp18;
1871#line 162
1872  if (__cil_tmp19 != __cil_tmp15) {
1873#line 162
1874    __cil_tmp20 = (unsigned long )cinfo;
1875#line 162
1876    __cil_tmp21 = __cil_tmp20 + 1256;
1877#line 162
1878    __cil_tmp22 = *((struct avmcard **)__cil_tmp21);
1879#line 162
1880    __cil_tmp23 = (unsigned long )__cil_tmp22;
1881#line 162
1882    __cil_tmp24 = __cil_tmp23 + 124;
1883#line 162
1884    __cil_tmp25 = *((unsigned char *)__cil_tmp24);
1885#line 162
1886    tmp = (int )__cil_tmp25;
1887  } else {
1888#line 162
1889    tmp = 0;
1890  }
1891  }
1892  {
1893#line 162
1894  __cil_tmp26 = (struct avmcard *)0;
1895#line 162
1896  __cil_tmp27 = (unsigned long )__cil_tmp26;
1897#line 162
1898  __cil_tmp28 = (unsigned long )cinfo;
1899#line 162
1900  __cil_tmp29 = __cil_tmp28 + 1256;
1901#line 162
1902  __cil_tmp30 = *((struct avmcard **)__cil_tmp29);
1903#line 162
1904  __cil_tmp31 = (unsigned long )__cil_tmp30;
1905#line 162
1906  if (__cil_tmp31 != __cil_tmp27) {
1907#line 162
1908    __cil_tmp32 = (unsigned long )cinfo;
1909#line 162
1910    __cil_tmp33 = __cil_tmp32 + 1256;
1911#line 162
1912    __cil_tmp34 = *((struct avmcard **)__cil_tmp33);
1913#line 162
1914    __cil_tmp35 = (unsigned long )__cil_tmp34;
1915#line 162
1916    __cil_tmp36 = __cil_tmp35 + 108;
1917#line 162
1918    tmp___0 = *((unsigned int *)__cil_tmp36);
1919  } else {
1920#line 162
1921    tmp___0 = 0U;
1922  }
1923  }
1924  {
1925#line 162
1926  __cil_tmp37 = (struct avmcard *)0;
1927#line 162
1928  __cil_tmp38 = (unsigned long )__cil_tmp37;
1929#line 162
1930  __cil_tmp39 = (unsigned long )cinfo;
1931#line 162
1932  __cil_tmp40 = __cil_tmp39 + 1256;
1933#line 162
1934  __cil_tmp41 = *((struct avmcard **)__cil_tmp40);
1935#line 162
1936  __cil_tmp42 = (unsigned long )__cil_tmp41;
1937#line 162
1938  if (__cil_tmp42 != __cil_tmp38) {
1939#line 162
1940    __cil_tmp43 = (unsigned long )cinfo;
1941#line 162
1942    __cil_tmp44 = __cil_tmp43 + 1256;
1943#line 162
1944    __cil_tmp45 = *((struct avmcard **)__cil_tmp44);
1945#line 162
1946    __cil_tmp46 = (unsigned long )__cil_tmp45;
1947#line 162
1948    __cil_tmp47 = __cil_tmp46 + 104;
1949#line 162
1950    tmp___1 = *((unsigned int *)__cil_tmp47);
1951  } else {
1952#line 162
1953    tmp___1 = 0U;
1954  }
1955  }
1956  {
1957#line 162
1958  __cil_tmp48 = (char *)0;
1959#line 162
1960  __cil_tmp49 = (unsigned long )__cil_tmp48;
1961#line 162
1962  __cil_tmp50 = 0 * 8UL;
1963#line 162
1964  __cil_tmp51 = 1064 + __cil_tmp50;
1965#line 162
1966  __cil_tmp52 = (unsigned long )cinfo;
1967#line 162
1968  __cil_tmp53 = __cil_tmp52 + __cil_tmp51;
1969#line 162
1970  __cil_tmp54 = *((char **)__cil_tmp53);
1971#line 162
1972  __cil_tmp55 = (unsigned long )__cil_tmp54;
1973#line 162
1974  if (__cil_tmp55 != __cil_tmp49) {
1975#line 162
1976    __cil_tmp56 = 0 * 8UL;
1977#line 162
1978    __cil_tmp57 = 1064 + __cil_tmp56;
1979#line 162
1980    __cil_tmp58 = (unsigned long )cinfo;
1981#line 162
1982    __cil_tmp59 = __cil_tmp58 + __cil_tmp57;
1983#line 162
1984    tmp___2 = *((char **)__cil_tmp59);
1985  } else {
1986#line 162
1987    tmp___2 = (char *)"-";
1988  }
1989  }
1990  {
1991#line 162
1992  __cil_tmp60 = 0 * 1UL;
1993#line 162
1994  __cil_tmp61 = 0 + __cil_tmp60;
1995#line 162
1996  __cil_tmp62 = (unsigned long )cinfo;
1997#line 162
1998  __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
1999#line 162
2000  __cil_tmp64 = *((char *)__cil_tmp63);
2001#line 162
2002  __cil_tmp65 = (signed char )__cil_tmp64;
2003#line 162
2004  __cil_tmp66 = (int )__cil_tmp65;
2005#line 162
2006  if (__cil_tmp66 != 0) {
2007#line 162
2008    __cil_tmp67 = (char (*)[32U])cinfo;
2009#line 162
2010    tmp___3 = (char *)__cil_tmp67;
2011  } else {
2012#line 162
2013    tmp___3 = (char *)"-";
2014  }
2015  }
2016  {
2017#line 162
2018  __cil_tmp68 = (unsigned long )cinfo;
2019#line 162
2020  __cil_tmp69 = __cil_tmp68 + 1128;
2021#line 162
2022  __cil_tmp70 = (char (*)[128U])__cil_tmp69;
2023#line 162
2024  __cil_tmp71 = (char *)__cil_tmp70;
2025#line 162
2026  sprintf(__cil_tmp71, "%s %s 0x%x %d r%d", tmp___3, tmp___2, tmp___1, tmp___0, tmp);
2027  }
2028  {
2029#line 169
2030  __cil_tmp72 = (unsigned long )cinfo;
2031#line 169
2032  __cil_tmp73 = __cil_tmp72 + 1128;
2033#line 169
2034  __cil_tmp74 = (char (*)[128U])__cil_tmp73;
2035#line 169
2036  return ((char *)__cil_tmp74);
2037  }
2038}
2039}
2040#line 174 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2041int b1pcmcia_addcard_b1(unsigned int port , unsigned int irq ) 
2042{ int tmp ;
2043  enum avmcardtype __cil_tmp4 ;
2044
2045  {
2046  {
2047#line 176
2048  __cil_tmp4 = (enum avmcardtype )2;
2049#line 176
2050  tmp = b1pcmcia_add_card(port, irq, __cil_tmp4);
2051  }
2052#line 176
2053  return (tmp);
2054}
2055}
2056#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2057int b1pcmcia_addcard_m1(unsigned int port , unsigned int irq ) 
2058{ int tmp ;
2059  enum avmcardtype __cil_tmp4 ;
2060
2061  {
2062  {
2063#line 181
2064  __cil_tmp4 = (enum avmcardtype )3;
2065#line 181
2066  tmp = b1pcmcia_add_card(port, irq, __cil_tmp4);
2067  }
2068#line 181
2069  return (tmp);
2070}
2071}
2072#line 184 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2073int b1pcmcia_addcard_m2(unsigned int port , unsigned int irq ) 
2074{ int tmp ;
2075  enum avmcardtype __cil_tmp4 ;
2076
2077  {
2078  {
2079#line 186
2080  __cil_tmp4 = (enum avmcardtype )4;
2081#line 186
2082  tmp = b1pcmcia_add_card(port, irq, __cil_tmp4);
2083  }
2084#line 186
2085  return (tmp);
2086}
2087}
2088#line 189 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2089int b1pcmcia_delcard(unsigned int port , unsigned int irq ) 
2090{ struct list_head *l ;
2091  avmcard *card ;
2092  struct list_head  const  *__mptr ;
2093  struct list_head *__cil_tmp6 ;
2094  avmcard *__cil_tmp7 ;
2095  unsigned long __cil_tmp8 ;
2096  unsigned long __cil_tmp9 ;
2097  unsigned int __cil_tmp10 ;
2098  unsigned long __cil_tmp11 ;
2099  unsigned long __cil_tmp12 ;
2100  unsigned int __cil_tmp13 ;
2101  unsigned long __cil_tmp14 ;
2102  unsigned long __cil_tmp15 ;
2103  struct avmctrl_info *__cil_tmp16 ;
2104  unsigned long __cil_tmp17 ;
2105  unsigned long __cil_tmp18 ;
2106  struct capi_ctr *__cil_tmp19 ;
2107  unsigned long __cil_tmp20 ;
2108  unsigned long __cil_tmp21 ;
2109
2110  {
2111#line 194
2112  __cil_tmp6 = & cards;
2113#line 194
2114  l = *((struct list_head **)__cil_tmp6);
2115#line 194
2116  goto ldv_23126;
2117  ldv_23125: 
2118#line 195
2119  __mptr = (struct list_head  const  *)l;
2120#line 195
2121  __cil_tmp7 = (avmcard *)__mptr;
2122#line 195
2123  card = __cil_tmp7 + 0xfffffffffffff6d0UL;
2124  {
2125#line 196
2126  __cil_tmp8 = (unsigned long )card;
2127#line 196
2128  __cil_tmp9 = __cil_tmp8 + 104;
2129#line 196
2130  __cil_tmp10 = *((unsigned int *)__cil_tmp9);
2131#line 196
2132  if (__cil_tmp10 == port) {
2133    {
2134#line 196
2135    __cil_tmp11 = (unsigned long )card;
2136#line 196
2137    __cil_tmp12 = __cil_tmp11 + 108;
2138#line 196
2139    __cil_tmp13 = *((unsigned int *)__cil_tmp12);
2140#line 196
2141    if (__cil_tmp13 == irq) {
2142      {
2143#line 197
2144      __cil_tmp14 = (unsigned long )card;
2145#line 197
2146      __cil_tmp15 = __cil_tmp14 + 2336;
2147#line 197
2148      __cil_tmp16 = *((struct avmctrl_info **)__cil_tmp15);
2149#line 197
2150      __cil_tmp17 = (unsigned long )__cil_tmp16;
2151#line 197
2152      __cil_tmp18 = __cil_tmp17 + 1264;
2153#line 197
2154      __cil_tmp19 = (struct capi_ctr *)__cil_tmp18;
2155#line 197
2156      b1pcmcia_remove_ctr(__cil_tmp19);
2157      }
2158#line 198
2159      return (0);
2160    } else {
2161
2162    }
2163    }
2164  } else {
2165
2166  }
2167  }
2168#line 194
2169  l = *((struct list_head **)l);
2170  ldv_23126: ;
2171  {
2172#line 194
2173  __cil_tmp20 = (unsigned long )(& cards);
2174#line 194
2175  __cil_tmp21 = (unsigned long )l;
2176#line 194
2177  if (__cil_tmp21 != __cil_tmp20) {
2178#line 195
2179    goto ldv_23125;
2180  } else {
2181#line 197
2182    goto ldv_23127;
2183  }
2184  }
2185  ldv_23127: ;
2186#line 201
2187  return (-3);
2188}
2189}
2190#line 209 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2191static struct capi_driver capi_driver_b1pcmcia  =    {{(char )'b', (char )'1', (char )'p', (char )'c', (char )'m', (char )'c', (char )'i',
2192     (char )'a', (char )'\000'}, {(char )'1', (char )'.', (char )'0', (char )'\000'},
2193    (int (*)(struct capi_driver * , capicardparams * ))0, {(struct list_head *)0,
2194                                                           (struct list_head *)0}};
2195#line 214 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2196static int b1pcmcia_init(void) 
2197{ char *p ;
2198  char rev[32U] ;
2199  char const   *__cil_tmp3 ;
2200  char *__cil_tmp4 ;
2201  unsigned long __cil_tmp5 ;
2202  unsigned long __cil_tmp6 ;
2203  char *__cil_tmp7 ;
2204  char __cil_tmp8 ;
2205  signed char __cil_tmp9 ;
2206  int __cil_tmp10 ;
2207  char *__cil_tmp11 ;
2208  char const   *__cil_tmp12 ;
2209  char const   *__cil_tmp13 ;
2210  char const   *__cil_tmp14 ;
2211  char *__cil_tmp15 ;
2212  unsigned long __cil_tmp16 ;
2213  unsigned long __cil_tmp17 ;
2214  unsigned long __cil_tmp18 ;
2215  char *__cil_tmp19 ;
2216  unsigned long __cil_tmp20 ;
2217  char *__cil_tmp21 ;
2218  char *__cil_tmp22 ;
2219  char *__cil_tmp23 ;
2220  unsigned long __cil_tmp24 ;
2221  char (*__cil_tmp25)[32U] ;
2222  char *__cil_tmp26 ;
2223  char const   *__cil_tmp27 ;
2224  char *__cil_tmp28 ;
2225
2226  {
2227  {
2228#line 219
2229  __cil_tmp3 = (char const   *)revision;
2230#line 219
2231  p = strchr(__cil_tmp3, 58);
2232  }
2233  {
2234#line 219
2235  __cil_tmp4 = (char *)0;
2236#line 219
2237  __cil_tmp5 = (unsigned long )__cil_tmp4;
2238#line 219
2239  __cil_tmp6 = (unsigned long )p;
2240#line 219
2241  if (__cil_tmp6 != __cil_tmp5) {
2242    {
2243#line 219
2244    __cil_tmp7 = p + 1UL;
2245#line 219
2246    __cil_tmp8 = *__cil_tmp7;
2247#line 219
2248    __cil_tmp9 = (signed char )__cil_tmp8;
2249#line 219
2250    __cil_tmp10 = (int )__cil_tmp9;
2251#line 219
2252    if (__cil_tmp10 != 0) {
2253      {
2254#line 220
2255      __cil_tmp11 = (char *)(& rev);
2256#line 220
2257      __cil_tmp12 = (char const   *)p;
2258#line 220
2259      __cil_tmp13 = __cil_tmp12 + 2U;
2260#line 220
2261      strlcpy(__cil_tmp11, __cil_tmp13, 32UL);
2262#line 221
2263      __cil_tmp14 = (char const   *)(& rev);
2264#line 221
2265      p = strchr(__cil_tmp14, 36);
2266      }
2267      {
2268#line 221
2269      __cil_tmp15 = (char *)0;
2270#line 221
2271      __cil_tmp16 = (unsigned long )__cil_tmp15;
2272#line 221
2273      __cil_tmp17 = (unsigned long )p;
2274#line 221
2275      if (__cil_tmp17 != __cil_tmp16) {
2276        {
2277#line 221
2278        __cil_tmp18 = (unsigned long )p;
2279#line 221
2280        __cil_tmp19 = (char *)(& rev);
2281#line 221
2282        __cil_tmp20 = (unsigned long )__cil_tmp19;
2283#line 221
2284        if (__cil_tmp20 < __cil_tmp18) {
2285#line 222
2286          __cil_tmp21 = p + 0xffffffffffffffffUL;
2287#line 222
2288          *__cil_tmp21 = (char)0;
2289        } else {
2290
2291        }
2292        }
2293      } else {
2294
2295      }
2296      }
2297    } else {
2298      {
2299#line 224
2300      __cil_tmp22 = (char *)(& rev);
2301#line 224
2302      strcpy(__cil_tmp22, "1.0");
2303      }
2304    }
2305    }
2306  } else {
2307    {
2308#line 224
2309    __cil_tmp23 = (char *)(& rev);
2310#line 224
2311    strcpy(__cil_tmp23, "1.0");
2312    }
2313  }
2314  }
2315  {
2316#line 226
2317  __cil_tmp24 = (unsigned long )(& capi_driver_b1pcmcia) + 32;
2318#line 226
2319  __cil_tmp25 = (char (*)[32U])__cil_tmp24;
2320#line 226
2321  __cil_tmp26 = (char *)__cil_tmp25;
2322#line 226
2323  __cil_tmp27 = (char const   *)(& rev);
2324#line 226
2325  strlcpy(__cil_tmp26, __cil_tmp27, 32UL);
2326#line 227
2327  register_capi_driver(& capi_driver_b1pcmcia);
2328#line 228
2329  __cil_tmp28 = (char *)(& rev);
2330#line 228
2331  printk("<6>b1pci: revision %s\n", __cil_tmp28);
2332  }
2333#line 230
2334  return (0);
2335}
2336}
2337#line 233 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2338static void b1pcmcia_exit(void) 
2339{ 
2340
2341  {
2342  {
2343#line 235
2344  unregister_capi_driver(& capi_driver_b1pcmcia);
2345  }
2346#line 236
2347  return;
2348}
2349}
2350#line 257
2351extern void ldv_check_final_state(void) ;
2352#line 263
2353extern void ldv_initialize(void) ;
2354#line 266
2355extern int __VERIFIER_nondet_int(void) ;
2356#line 269 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2357int LDV_IN_INTERRUPT  ;
2358#line 272 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2359void main(void) 
2360{ int tmp ;
2361  int tmp___0 ;
2362  int tmp___1 ;
2363
2364  {
2365  {
2366#line 284
2367  LDV_IN_INTERRUPT = 1;
2368#line 293
2369  ldv_initialize();
2370#line 299
2371  tmp = b1pcmcia_init();
2372  }
2373#line 299
2374  if (tmp != 0) {
2375#line 300
2376    goto ldv_final;
2377  } else {
2378
2379  }
2380#line 302
2381  goto ldv_23191;
2382  ldv_23190: 
2383  {
2384#line 305
2385  tmp___0 = __VERIFIER_nondet_int();
2386  }
2387  {
2388#line 307
2389  goto switch_default;
2390#line 305
2391  if (0) {
2392    switch_default: /* CIL Label */ ;
2393#line 307
2394    goto ldv_23189;
2395  } else {
2396    switch_break: /* CIL Label */ ;
2397  }
2398  }
2399  ldv_23189: ;
2400  ldv_23191: 
2401  {
2402#line 302
2403  tmp___1 = __VERIFIER_nondet_int();
2404  }
2405#line 302
2406  if (tmp___1 != 0) {
2407#line 303
2408    goto ldv_23190;
2409  } else {
2410#line 305
2411    goto ldv_23192;
2412  }
2413  ldv_23192: ;
2414  {
2415#line 319
2416  b1pcmcia_exit();
2417  }
2418  ldv_final: 
2419  {
2420#line 322
2421  ldv_check_final_state();
2422  }
2423#line 325
2424  return;
2425}
2426}
2427#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2428void ldv_blast_assert(void) 
2429{ 
2430
2431  {
2432  ERROR: ;
2433#line 6
2434  goto ERROR;
2435}
2436}
2437#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2438extern int __VERIFIER_nondet_int(void) ;
2439#line 346 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2440int ldv_spin  =    0;
2441#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2442void ldv_check_alloc_flags(gfp_t flags ) 
2443{ 
2444
2445  {
2446#line 353
2447  if (ldv_spin != 0) {
2448#line 353
2449    if (flags != 32U) {
2450      {
2451#line 353
2452      ldv_blast_assert();
2453      }
2454    } else {
2455
2456    }
2457  } else {
2458
2459  }
2460#line 356
2461  return;
2462}
2463}
2464#line 356
2465extern struct page *ldv_some_page(void) ;
2466#line 359 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2467struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
2468{ struct page *tmp ;
2469
2470  {
2471#line 362
2472  if (ldv_spin != 0) {
2473#line 362
2474    if (flags != 32U) {
2475      {
2476#line 362
2477      ldv_blast_assert();
2478      }
2479    } else {
2480
2481    }
2482  } else {
2483
2484  }
2485  {
2486#line 364
2487  tmp = ldv_some_page();
2488  }
2489#line 364
2490  return (tmp);
2491}
2492}
2493#line 368 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2494void ldv_check_alloc_nonatomic(void) 
2495{ 
2496
2497  {
2498#line 371
2499  if (ldv_spin != 0) {
2500    {
2501#line 371
2502    ldv_blast_assert();
2503    }
2504  } else {
2505
2506  }
2507#line 374
2508  return;
2509}
2510}
2511#line 375 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2512void ldv_spin_lock(void) 
2513{ 
2514
2515  {
2516#line 378
2517  ldv_spin = 1;
2518#line 379
2519  return;
2520}
2521}
2522#line 382 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2523void ldv_spin_unlock(void) 
2524{ 
2525
2526  {
2527#line 385
2528  ldv_spin = 0;
2529#line 386
2530  return;
2531}
2532}
2533#line 389 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2534int ldv_spin_trylock(void) 
2535{ int is_lock ;
2536
2537  {
2538  {
2539#line 394
2540  is_lock = __VERIFIER_nondet_int();
2541  }
2542#line 396
2543  if (is_lock != 0) {
2544#line 399
2545    return (0);
2546  } else {
2547#line 404
2548    ldv_spin = 1;
2549#line 406
2550    return (1);
2551  }
2552}
2553}
2554#line 573 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2555void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
2556{ 
2557
2558  {
2559  {
2560#line 579
2561  ldv_check_alloc_flags(ldv_func_arg2);
2562#line 581
2563  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2564  }
2565#line 582
2566  return ((void *)0);
2567}
2568}
2569#line 638 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2570struct sk_buff *ldv_skb_clone_22(struct sk_buff *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
2571{ struct sk_buff *tmp ;
2572
2573  {
2574  {
2575#line 644
2576  ldv_check_alloc_flags(ldv_func_arg2);
2577#line 646
2578  tmp = skb_clone(ldv_func_arg1, ldv_func_arg2);
2579  }
2580#line 646
2581  return (tmp);
2582}
2583}
2584#line 660 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2585struct sk_buff *ldv_skb_copy_24(struct sk_buff  const  *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
2586{ struct sk_buff *tmp ;
2587
2588  {
2589  {
2590#line 666
2591  ldv_check_alloc_flags(ldv_func_arg2);
2592#line 668
2593  tmp = skb_copy(ldv_func_arg1, ldv_func_arg2);
2594  }
2595#line 668
2596  return (tmp);
2597}
2598}
2599#line 671 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2600struct sk_buff *ldv___netdev_alloc_skb_25(struct net_device *ldv_func_arg1 , unsigned int ldv_func_arg2 ,
2601                                          gfp_t ldv_func_arg3 ) 
2602{ struct sk_buff *tmp ;
2603
2604  {
2605  {
2606#line 678
2607  ldv_check_alloc_flags(ldv_func_arg3);
2608#line 680
2609  tmp = __netdev_alloc_skb(ldv_func_arg1, ldv_func_arg2, ldv_func_arg3);
2610  }
2611#line 680
2612  return (tmp);
2613}
2614}
2615#line 683 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2616struct sk_buff *ldv___netdev_alloc_skb_26(struct net_device *ldv_func_arg1 , unsigned int ldv_func_arg2 ,
2617                                          gfp_t ldv_func_arg3 ) 
2618{ struct sk_buff *tmp ;
2619
2620  {
2621  {
2622#line 690
2623  ldv_check_alloc_flags(ldv_func_arg3);
2624#line 692
2625  tmp = __netdev_alloc_skb(ldv_func_arg1, ldv_func_arg2, ldv_func_arg3);
2626  }
2627#line 692
2628  return (tmp);
2629}
2630}
2631#line 695 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2632int ldv_pskb_expand_head_27(struct sk_buff *ldv_func_arg1 , int ldv_func_arg2 , int ldv_func_arg3 ,
2633                            gfp_t ldv_func_arg4 ) 
2634{ int tmp ;
2635
2636  {
2637  {
2638#line 703
2639  ldv_check_alloc_flags(ldv_func_arg4);
2640#line 705
2641  tmp = pskb_expand_head(ldv_func_arg1, ldv_func_arg2, ldv_func_arg3, ldv_func_arg4);
2642  }
2643#line 705
2644  return (tmp);
2645}
2646}