Showing error 1216

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--staging--comedi--drivers--adl_pci8164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3478
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 49 "include/asm-generic/int-ll64.h"
  17typedef unsigned int u32;
  18#line 51 "include/asm-generic/int-ll64.h"
  19typedef long long s64;
  20#line 52 "include/asm-generic/int-ll64.h"
  21typedef unsigned long long u64;
  22#line 14 "include/asm-generic/posix_types.h"
  23typedef long __kernel_long_t;
  24#line 15 "include/asm-generic/posix_types.h"
  25typedef unsigned long __kernel_ulong_t;
  26#line 75 "include/asm-generic/posix_types.h"
  27typedef __kernel_ulong_t __kernel_size_t;
  28#line 76 "include/asm-generic/posix_types.h"
  29typedef __kernel_long_t __kernel_ssize_t;
  30#line 91 "include/asm-generic/posix_types.h"
  31typedef long long __kernel_loff_t;
  32#line 21 "include/linux/types.h"
  33typedef __u32 __kernel_dev_t;
  34#line 24 "include/linux/types.h"
  35typedef __kernel_dev_t dev_t;
  36#line 27 "include/linux/types.h"
  37typedef unsigned short umode_t;
  38#line 38 "include/linux/types.h"
  39typedef _Bool bool;
  40#line 54 "include/linux/types.h"
  41typedef __kernel_loff_t loff_t;
  42#line 63 "include/linux/types.h"
  43typedef __kernel_size_t size_t;
  44#line 68 "include/linux/types.h"
  45typedef __kernel_ssize_t ssize_t;
  46#line 155 "include/linux/types.h"
  47typedef u64 dma_addr_t;
  48#line 202 "include/linux/types.h"
  49typedef unsigned int gfp_t;
  50#line 206 "include/linux/types.h"
  51typedef u64 phys_addr_t;
  52#line 211 "include/linux/types.h"
  53typedef phys_addr_t resource_size_t;
  54#line 221 "include/linux/types.h"
  55struct __anonstruct_atomic_t_6 {
  56   int counter ;
  57};
  58#line 221 "include/linux/types.h"
  59typedef struct __anonstruct_atomic_t_6 atomic_t;
  60#line 226 "include/linux/types.h"
  61struct __anonstruct_atomic64_t_7 {
  62   long counter ;
  63};
  64#line 226 "include/linux/types.h"
  65typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  66#line 227 "include/linux/types.h"
  67struct list_head {
  68   struct list_head *next ;
  69   struct list_head *prev ;
  70};
  71#line 232
  72struct hlist_node;
  73#line 232 "include/linux/types.h"
  74struct hlist_head {
  75   struct hlist_node *first ;
  76};
  77#line 236 "include/linux/types.h"
  78struct hlist_node {
  79   struct hlist_node *next ;
  80   struct hlist_node **pprev ;
  81};
  82#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  83struct module;
  84#line 55
  85struct module;
  86#line 146 "include/linux/init.h"
  87typedef void (*ctor_fn_t)(void);
  88#line 46 "include/linux/dynamic_debug.h"
  89struct device;
  90#line 46
  91struct device;
  92#line 57
  93struct completion;
  94#line 57
  95struct completion;
  96#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  97struct page;
  98#line 58
  99struct page;
 100#line 26 "include/asm-generic/getorder.h"
 101struct task_struct;
 102#line 26
 103struct task_struct;
 104#line 28
 105struct mm_struct;
 106#line 28
 107struct mm_struct;
 108#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 109typedef unsigned long pgdval_t;
 110#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 111typedef unsigned long pgprotval_t;
 112#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 113struct pgprot {
 114   pgprotval_t pgprot ;
 115};
 116#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 117typedef struct pgprot pgprot_t;
 118#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 119struct __anonstruct_pgd_t_16 {
 120   pgdval_t pgd ;
 121};
 122#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 123typedef struct __anonstruct_pgd_t_16 pgd_t;
 124#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 125typedef struct page *pgtable_t;
 126#line 290
 127struct file;
 128#line 290
 129struct file;
 130#line 339
 131struct cpumask;
 132#line 339
 133struct cpumask;
 134#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 135struct arch_spinlock;
 136#line 327
 137struct arch_spinlock;
 138#line 306 "include/linux/bitmap.h"
 139struct bug_entry {
 140   int bug_addr_disp ;
 141   int file_disp ;
 142   unsigned short line ;
 143   unsigned short flags ;
 144};
 145#line 89 "include/linux/bug.h"
 146struct cpumask {
 147   unsigned long bits[64U] ;
 148};
 149#line 637 "include/linux/cpumask.h"
 150typedef struct cpumask *cpumask_var_t;
 151#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 152struct static_key;
 153#line 234
 154struct static_key;
 155#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 156struct kmem_cache;
 157#line 23 "include/asm-generic/atomic-long.h"
 158typedef atomic64_t atomic_long_t;
 159#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 160typedef u16 __ticket_t;
 161#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 162typedef u32 __ticketpair_t;
 163#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 164struct __raw_tickets {
 165   __ticket_t head ;
 166   __ticket_t tail ;
 167};
 168#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 169union __anonunion_ldv_5907_29 {
 170   __ticketpair_t head_tail ;
 171   struct __raw_tickets tickets ;
 172};
 173#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 174struct arch_spinlock {
 175   union __anonunion_ldv_5907_29 ldv_5907 ;
 176};
 177#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 178typedef struct arch_spinlock arch_spinlock_t;
 179#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 180struct lockdep_map;
 181#line 34
 182struct lockdep_map;
 183#line 55 "include/linux/debug_locks.h"
 184struct stack_trace {
 185   unsigned int nr_entries ;
 186   unsigned int max_entries ;
 187   unsigned long *entries ;
 188   int skip ;
 189};
 190#line 26 "include/linux/stacktrace.h"
 191struct lockdep_subclass_key {
 192   char __one_byte ;
 193};
 194#line 53 "include/linux/lockdep.h"
 195struct lock_class_key {
 196   struct lockdep_subclass_key subkeys[8U] ;
 197};
 198#line 59 "include/linux/lockdep.h"
 199struct lock_class {
 200   struct list_head hash_entry ;
 201   struct list_head lock_entry ;
 202   struct lockdep_subclass_key *key ;
 203   unsigned int subclass ;
 204   unsigned int dep_gen_id ;
 205   unsigned long usage_mask ;
 206   struct stack_trace usage_traces[13U] ;
 207   struct list_head locks_after ;
 208   struct list_head locks_before ;
 209   unsigned int version ;
 210   unsigned long ops ;
 211   char const   *name ;
 212   int name_version ;
 213   unsigned long contention_point[4U] ;
 214   unsigned long contending_point[4U] ;
 215};
 216#line 144 "include/linux/lockdep.h"
 217struct lockdep_map {
 218   struct lock_class_key *key ;
 219   struct lock_class *class_cache[2U] ;
 220   char const   *name ;
 221   int cpu ;
 222   unsigned long ip ;
 223};
 224#line 556 "include/linux/lockdep.h"
 225struct raw_spinlock {
 226   arch_spinlock_t raw_lock ;
 227   unsigned int magic ;
 228   unsigned int owner_cpu ;
 229   void *owner ;
 230   struct lockdep_map dep_map ;
 231};
 232#line 32 "include/linux/spinlock_types.h"
 233typedef struct raw_spinlock raw_spinlock_t;
 234#line 33 "include/linux/spinlock_types.h"
 235struct __anonstruct_ldv_6122_33 {
 236   u8 __padding[24U] ;
 237   struct lockdep_map dep_map ;
 238};
 239#line 33 "include/linux/spinlock_types.h"
 240union __anonunion_ldv_6123_32 {
 241   struct raw_spinlock rlock ;
 242   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 243};
 244#line 33 "include/linux/spinlock_types.h"
 245struct spinlock {
 246   union __anonunion_ldv_6123_32 ldv_6123 ;
 247};
 248#line 76 "include/linux/spinlock_types.h"
 249typedef struct spinlock spinlock_t;
 250#line 48 "include/linux/wait.h"
 251struct __wait_queue_head {
 252   spinlock_t lock ;
 253   struct list_head task_list ;
 254};
 255#line 53 "include/linux/wait.h"
 256typedef struct __wait_queue_head wait_queue_head_t;
 257#line 98 "include/linux/nodemask.h"
 258struct __anonstruct_nodemask_t_36 {
 259   unsigned long bits[16U] ;
 260};
 261#line 98 "include/linux/nodemask.h"
 262typedef struct __anonstruct_nodemask_t_36 nodemask_t;
 263#line 670 "include/linux/mmzone.h"
 264struct mutex {
 265   atomic_t count ;
 266   spinlock_t wait_lock ;
 267   struct list_head wait_list ;
 268   struct task_struct *owner ;
 269   char const   *name ;
 270   void *magic ;
 271   struct lockdep_map dep_map ;
 272};
 273#line 171 "include/linux/mutex.h"
 274struct rw_semaphore;
 275#line 171
 276struct rw_semaphore;
 277#line 172 "include/linux/mutex.h"
 278struct rw_semaphore {
 279   long count ;
 280   raw_spinlock_t wait_lock ;
 281   struct list_head wait_list ;
 282   struct lockdep_map dep_map ;
 283};
 284#line 128 "include/linux/rwsem.h"
 285struct completion {
 286   unsigned int done ;
 287   wait_queue_head_t wait ;
 288};
 289#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
 290struct resource {
 291   resource_size_t start ;
 292   resource_size_t end ;
 293   char const   *name ;
 294   unsigned long flags ;
 295   struct resource *parent ;
 296   struct resource *sibling ;
 297   struct resource *child ;
 298};
 299#line 181 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/x86_init.h"
 300struct pci_dev;
 301#line 181
 302struct pci_dev;
 303#line 312 "include/linux/jiffies.h"
 304union ktime {
 305   s64 tv64 ;
 306};
 307#line 59 "include/linux/ktime.h"
 308typedef union ktime ktime_t;
 309#line 341
 310struct tvec_base;
 311#line 341
 312struct tvec_base;
 313#line 342 "include/linux/ktime.h"
 314struct timer_list {
 315   struct list_head entry ;
 316   unsigned long expires ;
 317   struct tvec_base *base ;
 318   void (*function)(unsigned long  ) ;
 319   unsigned long data ;
 320   int slack ;
 321   int start_pid ;
 322   void *start_site ;
 323   char start_comm[16U] ;
 324   struct lockdep_map lockdep_map ;
 325};
 326#line 302 "include/linux/timer.h"
 327struct work_struct;
 328#line 302
 329struct work_struct;
 330#line 45 "include/linux/workqueue.h"
 331struct work_struct {
 332   atomic_long_t data ;
 333   struct list_head entry ;
 334   void (*func)(struct work_struct * ) ;
 335   struct lockdep_map lockdep_map ;
 336};
 337#line 46 "include/linux/pm.h"
 338struct pm_message {
 339   int event ;
 340};
 341#line 52 "include/linux/pm.h"
 342typedef struct pm_message pm_message_t;
 343#line 53 "include/linux/pm.h"
 344struct dev_pm_ops {
 345   int (*prepare)(struct device * ) ;
 346   void (*complete)(struct device * ) ;
 347   int (*suspend)(struct device * ) ;
 348   int (*resume)(struct device * ) ;
 349   int (*freeze)(struct device * ) ;
 350   int (*thaw)(struct device * ) ;
 351   int (*poweroff)(struct device * ) ;
 352   int (*restore)(struct device * ) ;
 353   int (*suspend_late)(struct device * ) ;
 354   int (*resume_early)(struct device * ) ;
 355   int (*freeze_late)(struct device * ) ;
 356   int (*thaw_early)(struct device * ) ;
 357   int (*poweroff_late)(struct device * ) ;
 358   int (*restore_early)(struct device * ) ;
 359   int (*suspend_noirq)(struct device * ) ;
 360   int (*resume_noirq)(struct device * ) ;
 361   int (*freeze_noirq)(struct device * ) ;
 362   int (*thaw_noirq)(struct device * ) ;
 363   int (*poweroff_noirq)(struct device * ) ;
 364   int (*restore_noirq)(struct device * ) ;
 365   int (*runtime_suspend)(struct device * ) ;
 366   int (*runtime_resume)(struct device * ) ;
 367   int (*runtime_idle)(struct device * ) ;
 368};
 369#line 289
 370enum rpm_status {
 371    RPM_ACTIVE = 0,
 372    RPM_RESUMING = 1,
 373    RPM_SUSPENDED = 2,
 374    RPM_SUSPENDING = 3
 375} ;
 376#line 296
 377enum rpm_request {
 378    RPM_REQ_NONE = 0,
 379    RPM_REQ_IDLE = 1,
 380    RPM_REQ_SUSPEND = 2,
 381    RPM_REQ_AUTOSUSPEND = 3,
 382    RPM_REQ_RESUME = 4
 383} ;
 384#line 304
 385struct wakeup_source;
 386#line 304
 387struct wakeup_source;
 388#line 494 "include/linux/pm.h"
 389struct pm_subsys_data {
 390   spinlock_t lock ;
 391   unsigned int refcount ;
 392};
 393#line 499
 394struct dev_pm_qos_request;
 395#line 499
 396struct pm_qos_constraints;
 397#line 499 "include/linux/pm.h"
 398struct dev_pm_info {
 399   pm_message_t power_state ;
 400   unsigned char can_wakeup : 1 ;
 401   unsigned char async_suspend : 1 ;
 402   bool is_prepared ;
 403   bool is_suspended ;
 404   bool ignore_children ;
 405   spinlock_t lock ;
 406   struct list_head entry ;
 407   struct completion completion ;
 408   struct wakeup_source *wakeup ;
 409   bool wakeup_path ;
 410   struct timer_list suspend_timer ;
 411   unsigned long timer_expires ;
 412   struct work_struct work ;
 413   wait_queue_head_t wait_queue ;
 414   atomic_t usage_count ;
 415   atomic_t child_count ;
 416   unsigned char disable_depth : 3 ;
 417   unsigned char idle_notification : 1 ;
 418   unsigned char request_pending : 1 ;
 419   unsigned char deferred_resume : 1 ;
 420   unsigned char run_wake : 1 ;
 421   unsigned char runtime_auto : 1 ;
 422   unsigned char no_callbacks : 1 ;
 423   unsigned char irq_safe : 1 ;
 424   unsigned char use_autosuspend : 1 ;
 425   unsigned char timer_autosuspends : 1 ;
 426   enum rpm_request request ;
 427   enum rpm_status runtime_status ;
 428   int runtime_error ;
 429   int autosuspend_delay ;
 430   unsigned long last_busy ;
 431   unsigned long active_jiffies ;
 432   unsigned long suspended_jiffies ;
 433   unsigned long accounting_timestamp ;
 434   ktime_t suspend_time ;
 435   s64 max_time_suspended_ns ;
 436   struct dev_pm_qos_request *pq_req ;
 437   struct pm_subsys_data *subsys_data ;
 438   struct pm_qos_constraints *constraints ;
 439};
 440#line 558 "include/linux/pm.h"
 441struct dev_pm_domain {
 442   struct dev_pm_ops ops ;
 443};
 444#line 173 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/topology.h"
 445struct pci_bus;
 446#line 173
 447struct pci_bus;
 448#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 449struct __anonstruct_mm_context_t_101 {
 450   void *ldt ;
 451   int size ;
 452   unsigned short ia32_compat ;
 453   struct mutex lock ;
 454   void *vdso ;
 455};
 456#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 457typedef struct __anonstruct_mm_context_t_101 mm_context_t;
 458#line 18 "include/asm-generic/pci_iomap.h"
 459struct vm_area_struct;
 460#line 18
 461struct vm_area_struct;
 462#line 835 "include/linux/sysctl.h"
 463struct rb_node {
 464   unsigned long rb_parent_color ;
 465   struct rb_node *rb_right ;
 466   struct rb_node *rb_left ;
 467};
 468#line 108 "include/linux/rbtree.h"
 469struct rb_root {
 470   struct rb_node *rb_node ;
 471};
 472#line 18 "include/linux/elf.h"
 473typedef __u64 Elf64_Addr;
 474#line 19 "include/linux/elf.h"
 475typedef __u16 Elf64_Half;
 476#line 23 "include/linux/elf.h"
 477typedef __u32 Elf64_Word;
 478#line 24 "include/linux/elf.h"
 479typedef __u64 Elf64_Xword;
 480#line 193 "include/linux/elf.h"
 481struct elf64_sym {
 482   Elf64_Word st_name ;
 483   unsigned char st_info ;
 484   unsigned char st_other ;
 485   Elf64_Half st_shndx ;
 486   Elf64_Addr st_value ;
 487   Elf64_Xword st_size ;
 488};
 489#line 201 "include/linux/elf.h"
 490typedef struct elf64_sym Elf64_Sym;
 491#line 445
 492struct sock;
 493#line 445
 494struct sock;
 495#line 446
 496struct kobject;
 497#line 446
 498struct kobject;
 499#line 447
 500enum kobj_ns_type {
 501    KOBJ_NS_TYPE_NONE = 0,
 502    KOBJ_NS_TYPE_NET = 1,
 503    KOBJ_NS_TYPES = 2
 504} ;
 505#line 453 "include/linux/elf.h"
 506struct kobj_ns_type_operations {
 507   enum kobj_ns_type type ;
 508   void *(*grab_current_ns)(void) ;
 509   void const   *(*netlink_ns)(struct sock * ) ;
 510   void const   *(*initial_ns)(void) ;
 511   void (*drop_ns)(void * ) ;
 512};
 513#line 57 "include/linux/kobject_ns.h"
 514struct attribute {
 515   char const   *name ;
 516   umode_t mode ;
 517   struct lock_class_key *key ;
 518   struct lock_class_key skey ;
 519};
 520#line 33 "include/linux/sysfs.h"
 521struct attribute_group {
 522   char const   *name ;
 523   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 524   struct attribute **attrs ;
 525};
 526#line 62 "include/linux/sysfs.h"
 527struct bin_attribute {
 528   struct attribute attr ;
 529   size_t size ;
 530   void *private ;
 531   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 532                   loff_t  , size_t  ) ;
 533   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 534                    loff_t  , size_t  ) ;
 535   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
 536};
 537#line 98 "include/linux/sysfs.h"
 538struct sysfs_ops {
 539   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 540   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 541   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 542};
 543#line 117
 544struct sysfs_dirent;
 545#line 117
 546struct sysfs_dirent;
 547#line 182 "include/linux/sysfs.h"
 548struct kref {
 549   atomic_t refcount ;
 550};
 551#line 49 "include/linux/kobject.h"
 552struct kset;
 553#line 49
 554struct kobj_type;
 555#line 49 "include/linux/kobject.h"
 556struct kobject {
 557   char const   *name ;
 558   struct list_head entry ;
 559   struct kobject *parent ;
 560   struct kset *kset ;
 561   struct kobj_type *ktype ;
 562   struct sysfs_dirent *sd ;
 563   struct kref kref ;
 564   unsigned char state_initialized : 1 ;
 565   unsigned char state_in_sysfs : 1 ;
 566   unsigned char state_add_uevent_sent : 1 ;
 567   unsigned char state_remove_uevent_sent : 1 ;
 568   unsigned char uevent_suppress : 1 ;
 569};
 570#line 107 "include/linux/kobject.h"
 571struct kobj_type {
 572   void (*release)(struct kobject * ) ;
 573   struct sysfs_ops  const  *sysfs_ops ;
 574   struct attribute **default_attrs ;
 575   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 576   void const   *(*namespace)(struct kobject * ) ;
 577};
 578#line 115 "include/linux/kobject.h"
 579struct kobj_uevent_env {
 580   char *envp[32U] ;
 581   int envp_idx ;
 582   char buf[2048U] ;
 583   int buflen ;
 584};
 585#line 122 "include/linux/kobject.h"
 586struct kset_uevent_ops {
 587   int (* const  filter)(struct kset * , struct kobject * ) ;
 588   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 589   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 590};
 591#line 139 "include/linux/kobject.h"
 592struct kset {
 593   struct list_head list ;
 594   spinlock_t list_lock ;
 595   struct kobject kobj ;
 596   struct kset_uevent_ops  const  *uevent_ops ;
 597};
 598#line 215
 599struct kernel_param;
 600#line 215
 601struct kernel_param;
 602#line 216 "include/linux/kobject.h"
 603struct kernel_param_ops {
 604   int (*set)(char const   * , struct kernel_param  const  * ) ;
 605   int (*get)(char * , struct kernel_param  const  * ) ;
 606   void (*free)(void * ) ;
 607};
 608#line 49 "include/linux/moduleparam.h"
 609struct kparam_string;
 610#line 49
 611struct kparam_array;
 612#line 49 "include/linux/moduleparam.h"
 613union __anonunion_ldv_13363_134 {
 614   void *arg ;
 615   struct kparam_string  const  *str ;
 616   struct kparam_array  const  *arr ;
 617};
 618#line 49 "include/linux/moduleparam.h"
 619struct kernel_param {
 620   char const   *name ;
 621   struct kernel_param_ops  const  *ops ;
 622   u16 perm ;
 623   s16 level ;
 624   union __anonunion_ldv_13363_134 ldv_13363 ;
 625};
 626#line 61 "include/linux/moduleparam.h"
 627struct kparam_string {
 628   unsigned int maxlen ;
 629   char *string ;
 630};
 631#line 67 "include/linux/moduleparam.h"
 632struct kparam_array {
 633   unsigned int max ;
 634   unsigned int elemsize ;
 635   unsigned int *num ;
 636   struct kernel_param_ops  const  *ops ;
 637   void *elem ;
 638};
 639#line 458 "include/linux/moduleparam.h"
 640struct static_key {
 641   atomic_t enabled ;
 642};
 643#line 225 "include/linux/jump_label.h"
 644struct tracepoint;
 645#line 225
 646struct tracepoint;
 647#line 226 "include/linux/jump_label.h"
 648struct tracepoint_func {
 649   void *func ;
 650   void *data ;
 651};
 652#line 29 "include/linux/tracepoint.h"
 653struct tracepoint {
 654   char const   *name ;
 655   struct static_key key ;
 656   void (*regfunc)(void) ;
 657   void (*unregfunc)(void) ;
 658   struct tracepoint_func *funcs ;
 659};
 660#line 86 "include/linux/tracepoint.h"
 661struct kernel_symbol {
 662   unsigned long value ;
 663   char const   *name ;
 664};
 665#line 27 "include/linux/export.h"
 666struct mod_arch_specific {
 667
 668};
 669#line 34 "include/linux/module.h"
 670struct module_param_attrs;
 671#line 34 "include/linux/module.h"
 672struct module_kobject {
 673   struct kobject kobj ;
 674   struct module *mod ;
 675   struct kobject *drivers_dir ;
 676   struct module_param_attrs *mp ;
 677};
 678#line 43 "include/linux/module.h"
 679struct module_attribute {
 680   struct attribute attr ;
 681   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 682   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 683                    size_t  ) ;
 684   void (*setup)(struct module * , char const   * ) ;
 685   int (*test)(struct module * ) ;
 686   void (*free)(struct module * ) ;
 687};
 688#line 69
 689struct exception_table_entry;
 690#line 69
 691struct exception_table_entry;
 692#line 198
 693enum module_state {
 694    MODULE_STATE_LIVE = 0,
 695    MODULE_STATE_COMING = 1,
 696    MODULE_STATE_GOING = 2
 697} ;
 698#line 204 "include/linux/module.h"
 699struct module_ref {
 700   unsigned long incs ;
 701   unsigned long decs ;
 702};
 703#line 219
 704struct module_sect_attrs;
 705#line 219
 706struct module_notes_attrs;
 707#line 219
 708struct ftrace_event_call;
 709#line 219 "include/linux/module.h"
 710struct module {
 711   enum module_state state ;
 712   struct list_head list ;
 713   char name[56U] ;
 714   struct module_kobject mkobj ;
 715   struct module_attribute *modinfo_attrs ;
 716   char const   *version ;
 717   char const   *srcversion ;
 718   struct kobject *holders_dir ;
 719   struct kernel_symbol  const  *syms ;
 720   unsigned long const   *crcs ;
 721   unsigned int num_syms ;
 722   struct kernel_param *kp ;
 723   unsigned int num_kp ;
 724   unsigned int num_gpl_syms ;
 725   struct kernel_symbol  const  *gpl_syms ;
 726   unsigned long const   *gpl_crcs ;
 727   struct kernel_symbol  const  *unused_syms ;
 728   unsigned long const   *unused_crcs ;
 729   unsigned int num_unused_syms ;
 730   unsigned int num_unused_gpl_syms ;
 731   struct kernel_symbol  const  *unused_gpl_syms ;
 732   unsigned long const   *unused_gpl_crcs ;
 733   struct kernel_symbol  const  *gpl_future_syms ;
 734   unsigned long const   *gpl_future_crcs ;
 735   unsigned int num_gpl_future_syms ;
 736   unsigned int num_exentries ;
 737   struct exception_table_entry *extable ;
 738   int (*init)(void) ;
 739   void *module_init ;
 740   void *module_core ;
 741   unsigned int init_size ;
 742   unsigned int core_size ;
 743   unsigned int init_text_size ;
 744   unsigned int core_text_size ;
 745   unsigned int init_ro_size ;
 746   unsigned int core_ro_size ;
 747   struct mod_arch_specific arch ;
 748   unsigned int taints ;
 749   unsigned int num_bugs ;
 750   struct list_head bug_list ;
 751   struct bug_entry *bug_table ;
 752   Elf64_Sym *symtab ;
 753   Elf64_Sym *core_symtab ;
 754   unsigned int num_symtab ;
 755   unsigned int core_num_syms ;
 756   char *strtab ;
 757   char *core_strtab ;
 758   struct module_sect_attrs *sect_attrs ;
 759   struct module_notes_attrs *notes_attrs ;
 760   char *args ;
 761   void *percpu ;
 762   unsigned int percpu_size ;
 763   unsigned int num_tracepoints ;
 764   struct tracepoint * const  *tracepoints_ptrs ;
 765   unsigned int num_trace_bprintk_fmt ;
 766   char const   **trace_bprintk_fmt_start ;
 767   struct ftrace_event_call **trace_events ;
 768   unsigned int num_trace_events ;
 769   struct list_head source_list ;
 770   struct list_head target_list ;
 771   struct task_struct *waiter ;
 772   void (*exit)(void) ;
 773   struct module_ref *refptr ;
 774   ctor_fn_t (**ctors)(void) ;
 775   unsigned int num_ctors ;
 776};
 777#line 88 "include/linux/kmemleak.h"
 778struct kmem_cache_cpu {
 779   void **freelist ;
 780   unsigned long tid ;
 781   struct page *page ;
 782   struct page *partial ;
 783   int node ;
 784   unsigned int stat[26U] ;
 785};
 786#line 55 "include/linux/slub_def.h"
 787struct kmem_cache_node {
 788   spinlock_t list_lock ;
 789   unsigned long nr_partial ;
 790   struct list_head partial ;
 791   atomic_long_t nr_slabs ;
 792   atomic_long_t total_objects ;
 793   struct list_head full ;
 794};
 795#line 66 "include/linux/slub_def.h"
 796struct kmem_cache_order_objects {
 797   unsigned long x ;
 798};
 799#line 76 "include/linux/slub_def.h"
 800struct kmem_cache {
 801   struct kmem_cache_cpu *cpu_slab ;
 802   unsigned long flags ;
 803   unsigned long min_partial ;
 804   int size ;
 805   int objsize ;
 806   int offset ;
 807   int cpu_partial ;
 808   struct kmem_cache_order_objects oo ;
 809   struct kmem_cache_order_objects max ;
 810   struct kmem_cache_order_objects min ;
 811   gfp_t allocflags ;
 812   int refcount ;
 813   void (*ctor)(void * ) ;
 814   int inuse ;
 815   int align ;
 816   int reserved ;
 817   char const   *name ;
 818   struct list_head list ;
 819   struct kobject kobj ;
 820   int remote_node_defrag_ratio ;
 821   struct kmem_cache_node *node[1024U] ;
 822};
 823#line 54 "include/linux/delay.h"
 824struct prio_tree_node;
 825#line 54 "include/linux/delay.h"
 826struct raw_prio_tree_node {
 827   struct prio_tree_node *left ;
 828   struct prio_tree_node *right ;
 829   struct prio_tree_node *parent ;
 830};
 831#line 19 "include/linux/prio_tree.h"
 832struct prio_tree_node {
 833   struct prio_tree_node *left ;
 834   struct prio_tree_node *right ;
 835   struct prio_tree_node *parent ;
 836   unsigned long start ;
 837   unsigned long last ;
 838};
 839#line 116
 840struct address_space;
 841#line 116
 842struct address_space;
 843#line 117 "include/linux/prio_tree.h"
 844union __anonunion_ldv_14287_136 {
 845   unsigned long index ;
 846   void *freelist ;
 847};
 848#line 117 "include/linux/prio_tree.h"
 849struct __anonstruct_ldv_14297_140 {
 850   unsigned short inuse ;
 851   unsigned short objects : 15 ;
 852   unsigned char frozen : 1 ;
 853};
 854#line 117 "include/linux/prio_tree.h"
 855union __anonunion_ldv_14298_139 {
 856   atomic_t _mapcount ;
 857   struct __anonstruct_ldv_14297_140 ldv_14297 ;
 858};
 859#line 117 "include/linux/prio_tree.h"
 860struct __anonstruct_ldv_14300_138 {
 861   union __anonunion_ldv_14298_139 ldv_14298 ;
 862   atomic_t _count ;
 863};
 864#line 117 "include/linux/prio_tree.h"
 865union __anonunion_ldv_14301_137 {
 866   unsigned long counters ;
 867   struct __anonstruct_ldv_14300_138 ldv_14300 ;
 868};
 869#line 117 "include/linux/prio_tree.h"
 870struct __anonstruct_ldv_14302_135 {
 871   union __anonunion_ldv_14287_136 ldv_14287 ;
 872   union __anonunion_ldv_14301_137 ldv_14301 ;
 873};
 874#line 117 "include/linux/prio_tree.h"
 875struct __anonstruct_ldv_14309_142 {
 876   struct page *next ;
 877   int pages ;
 878   int pobjects ;
 879};
 880#line 117 "include/linux/prio_tree.h"
 881union __anonunion_ldv_14310_141 {
 882   struct list_head lru ;
 883   struct __anonstruct_ldv_14309_142 ldv_14309 ;
 884};
 885#line 117 "include/linux/prio_tree.h"
 886union __anonunion_ldv_14315_143 {
 887   unsigned long private ;
 888   struct kmem_cache *slab ;
 889   struct page *first_page ;
 890};
 891#line 117 "include/linux/prio_tree.h"
 892struct page {
 893   unsigned long flags ;
 894   struct address_space *mapping ;
 895   struct __anonstruct_ldv_14302_135 ldv_14302 ;
 896   union __anonunion_ldv_14310_141 ldv_14310 ;
 897   union __anonunion_ldv_14315_143 ldv_14315 ;
 898   unsigned long debug_flags ;
 899};
 900#line 192 "include/linux/mm_types.h"
 901struct __anonstruct_vm_set_145 {
 902   struct list_head list ;
 903   void *parent ;
 904   struct vm_area_struct *head ;
 905};
 906#line 192 "include/linux/mm_types.h"
 907union __anonunion_shared_144 {
 908   struct __anonstruct_vm_set_145 vm_set ;
 909   struct raw_prio_tree_node prio_tree_node ;
 910};
 911#line 192
 912struct anon_vma;
 913#line 192
 914struct vm_operations_struct;
 915#line 192
 916struct mempolicy;
 917#line 192 "include/linux/mm_types.h"
 918struct vm_area_struct {
 919   struct mm_struct *vm_mm ;
 920   unsigned long vm_start ;
 921   unsigned long vm_end ;
 922   struct vm_area_struct *vm_next ;
 923   struct vm_area_struct *vm_prev ;
 924   pgprot_t vm_page_prot ;
 925   unsigned long vm_flags ;
 926   struct rb_node vm_rb ;
 927   union __anonunion_shared_144 shared ;
 928   struct list_head anon_vma_chain ;
 929   struct anon_vma *anon_vma ;
 930   struct vm_operations_struct  const  *vm_ops ;
 931   unsigned long vm_pgoff ;
 932   struct file *vm_file ;
 933   void *vm_private_data ;
 934   struct mempolicy *vm_policy ;
 935};
 936#line 255 "include/linux/mm_types.h"
 937struct core_thread {
 938   struct task_struct *task ;
 939   struct core_thread *next ;
 940};
 941#line 261 "include/linux/mm_types.h"
 942struct core_state {
 943   atomic_t nr_threads ;
 944   struct core_thread dumper ;
 945   struct completion startup ;
 946};
 947#line 274 "include/linux/mm_types.h"
 948struct mm_rss_stat {
 949   atomic_long_t count[3U] ;
 950};
 951#line 287
 952struct linux_binfmt;
 953#line 287
 954struct mmu_notifier_mm;
 955#line 287 "include/linux/mm_types.h"
 956struct mm_struct {
 957   struct vm_area_struct *mmap ;
 958   struct rb_root mm_rb ;
 959   struct vm_area_struct *mmap_cache ;
 960   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
 961                                      unsigned long  , unsigned long  ) ;
 962   void (*unmap_area)(struct mm_struct * , unsigned long  ) ;
 963   unsigned long mmap_base ;
 964   unsigned long task_size ;
 965   unsigned long cached_hole_size ;
 966   unsigned long free_area_cache ;
 967   pgd_t *pgd ;
 968   atomic_t mm_users ;
 969   atomic_t mm_count ;
 970   int map_count ;
 971   spinlock_t page_table_lock ;
 972   struct rw_semaphore mmap_sem ;
 973   struct list_head mmlist ;
 974   unsigned long hiwater_rss ;
 975   unsigned long hiwater_vm ;
 976   unsigned long total_vm ;
 977   unsigned long locked_vm ;
 978   unsigned long pinned_vm ;
 979   unsigned long shared_vm ;
 980   unsigned long exec_vm ;
 981   unsigned long stack_vm ;
 982   unsigned long reserved_vm ;
 983   unsigned long def_flags ;
 984   unsigned long nr_ptes ;
 985   unsigned long start_code ;
 986   unsigned long end_code ;
 987   unsigned long start_data ;
 988   unsigned long end_data ;
 989   unsigned long start_brk ;
 990   unsigned long brk ;
 991   unsigned long start_stack ;
 992   unsigned long arg_start ;
 993   unsigned long arg_end ;
 994   unsigned long env_start ;
 995   unsigned long env_end ;
 996   unsigned long saved_auxv[44U] ;
 997   struct mm_rss_stat rss_stat ;
 998   struct linux_binfmt *binfmt ;
 999   cpumask_var_t cpu_vm_mask_var ;
1000   mm_context_t context ;
1001   unsigned int faultstamp ;
1002   unsigned int token_priority ;
1003   unsigned int last_interval ;
1004   unsigned long flags ;
1005   struct core_state *core_state ;
1006   spinlock_t ioctx_lock ;
1007   struct hlist_head ioctx_list ;
1008   struct task_struct *owner ;
1009   struct file *exe_file ;
1010   unsigned long num_exe_file_vmas ;
1011   struct mmu_notifier_mm *mmu_notifier_mm ;
1012   pgtable_t pmd_huge_pte ;
1013   struct cpumask cpumask_allocation ;
1014};
1015#line 178 "include/linux/mm.h"
1016struct vm_fault {
1017   unsigned int flags ;
1018   unsigned long pgoff ;
1019   void *virtual_address ;
1020   struct page *page ;
1021};
1022#line 195 "include/linux/mm.h"
1023struct vm_operations_struct {
1024   void (*open)(struct vm_area_struct * ) ;
1025   void (*close)(struct vm_area_struct * ) ;
1026   int (*fault)(struct vm_area_struct * , struct vm_fault * ) ;
1027   int (*page_mkwrite)(struct vm_area_struct * , struct vm_fault * ) ;
1028   int (*access)(struct vm_area_struct * , unsigned long  , void * , int  , int  ) ;
1029   int (*set_policy)(struct vm_area_struct * , struct mempolicy * ) ;
1030   struct mempolicy *(*get_policy)(struct vm_area_struct * , unsigned long  ) ;
1031   int (*migrate)(struct vm_area_struct * , nodemask_t const   * , nodemask_t const   * ,
1032                  unsigned long  ) ;
1033};
1034#line 1631
1035struct klist_node;
1036#line 1631
1037struct klist_node;
1038#line 37 "include/linux/klist.h"
1039struct klist_node {
1040   void *n_klist ;
1041   struct list_head n_node ;
1042   struct kref n_ref ;
1043};
1044#line 67
1045struct dma_map_ops;
1046#line 67 "include/linux/klist.h"
1047struct dev_archdata {
1048   void *acpi_handle ;
1049   struct dma_map_ops *dma_ops ;
1050   void *iommu ;
1051};
1052#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1053struct device_private;
1054#line 17
1055struct device_private;
1056#line 18
1057struct device_driver;
1058#line 18
1059struct device_driver;
1060#line 19
1061struct driver_private;
1062#line 19
1063struct driver_private;
1064#line 20
1065struct class;
1066#line 20
1067struct class;
1068#line 21
1069struct subsys_private;
1070#line 21
1071struct subsys_private;
1072#line 22
1073struct bus_type;
1074#line 22
1075struct bus_type;
1076#line 23
1077struct device_node;
1078#line 23
1079struct device_node;
1080#line 24
1081struct iommu_ops;
1082#line 24
1083struct iommu_ops;
1084#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1085struct bus_attribute {
1086   struct attribute attr ;
1087   ssize_t (*show)(struct bus_type * , char * ) ;
1088   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
1089};
1090#line 51 "include/linux/device.h"
1091struct device_attribute;
1092#line 51
1093struct driver_attribute;
1094#line 51 "include/linux/device.h"
1095struct bus_type {
1096   char const   *name ;
1097   char const   *dev_name ;
1098   struct device *dev_root ;
1099   struct bus_attribute *bus_attrs ;
1100   struct device_attribute *dev_attrs ;
1101   struct driver_attribute *drv_attrs ;
1102   int (*match)(struct device * , struct device_driver * ) ;
1103   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1104   int (*probe)(struct device * ) ;
1105   int (*remove)(struct device * ) ;
1106   void (*shutdown)(struct device * ) ;
1107   int (*suspend)(struct device * , pm_message_t  ) ;
1108   int (*resume)(struct device * ) ;
1109   struct dev_pm_ops  const  *pm ;
1110   struct iommu_ops *iommu_ops ;
1111   struct subsys_private *p ;
1112};
1113#line 125
1114struct device_type;
1115#line 182
1116struct of_device_id;
1117#line 182 "include/linux/device.h"
1118struct device_driver {
1119   char const   *name ;
1120   struct bus_type *bus ;
1121   struct module *owner ;
1122   char const   *mod_name ;
1123   bool suppress_bind_attrs ;
1124   struct of_device_id  const  *of_match_table ;
1125   int (*probe)(struct device * ) ;
1126   int (*remove)(struct device * ) ;
1127   void (*shutdown)(struct device * ) ;
1128   int (*suspend)(struct device * , pm_message_t  ) ;
1129   int (*resume)(struct device * ) ;
1130   struct attribute_group  const  **groups ;
1131   struct dev_pm_ops  const  *pm ;
1132   struct driver_private *p ;
1133};
1134#line 245 "include/linux/device.h"
1135struct driver_attribute {
1136   struct attribute attr ;
1137   ssize_t (*show)(struct device_driver * , char * ) ;
1138   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
1139};
1140#line 299
1141struct class_attribute;
1142#line 299 "include/linux/device.h"
1143struct class {
1144   char const   *name ;
1145   struct module *owner ;
1146   struct class_attribute *class_attrs ;
1147   struct device_attribute *dev_attrs ;
1148   struct bin_attribute *dev_bin_attrs ;
1149   struct kobject *dev_kobj ;
1150   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
1151   char *(*devnode)(struct device * , umode_t * ) ;
1152   void (*class_release)(struct class * ) ;
1153   void (*dev_release)(struct device * ) ;
1154   int (*suspend)(struct device * , pm_message_t  ) ;
1155   int (*resume)(struct device * ) ;
1156   struct kobj_ns_type_operations  const  *ns_type ;
1157   void const   *(*namespace)(struct device * ) ;
1158   struct dev_pm_ops  const  *pm ;
1159   struct subsys_private *p ;
1160};
1161#line 394 "include/linux/device.h"
1162struct class_attribute {
1163   struct attribute attr ;
1164   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
1165   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
1166   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
1167};
1168#line 447 "include/linux/device.h"
1169struct device_type {
1170   char const   *name ;
1171   struct attribute_group  const  **groups ;
1172   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1173   char *(*devnode)(struct device * , umode_t * ) ;
1174   void (*release)(struct device * ) ;
1175   struct dev_pm_ops  const  *pm ;
1176};
1177#line 474 "include/linux/device.h"
1178struct device_attribute {
1179   struct attribute attr ;
1180   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
1181   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
1182                    size_t  ) ;
1183};
1184#line 557 "include/linux/device.h"
1185struct device_dma_parameters {
1186   unsigned int max_segment_size ;
1187   unsigned long segment_boundary_mask ;
1188};
1189#line 567
1190struct dma_coherent_mem;
1191#line 567 "include/linux/device.h"
1192struct device {
1193   struct device *parent ;
1194   struct device_private *p ;
1195   struct kobject kobj ;
1196   char const   *init_name ;
1197   struct device_type  const  *type ;
1198   struct mutex mutex ;
1199   struct bus_type *bus ;
1200   struct device_driver *driver ;
1201   void *platform_data ;
1202   struct dev_pm_info power ;
1203   struct dev_pm_domain *pm_domain ;
1204   int numa_node ;
1205   u64 *dma_mask ;
1206   u64 coherent_dma_mask ;
1207   struct device_dma_parameters *dma_parms ;
1208   struct list_head dma_pools ;
1209   struct dma_coherent_mem *dma_mem ;
1210   struct dev_archdata archdata ;
1211   struct device_node *of_node ;
1212   dev_t devt ;
1213   u32 id ;
1214   spinlock_t devres_lock ;
1215   struct list_head devres_head ;
1216   struct klist_node knode_class ;
1217   struct class *class ;
1218   struct attribute_group  const  **groups ;
1219   void (*release)(struct device * ) ;
1220};
1221#line 681 "include/linux/device.h"
1222struct wakeup_source {
1223   char const   *name ;
1224   struct list_head entry ;
1225   spinlock_t lock ;
1226   struct timer_list timer ;
1227   unsigned long timer_expires ;
1228   ktime_t total_time ;
1229   ktime_t max_time ;
1230   ktime_t last_time ;
1231   unsigned long event_count ;
1232   unsigned long active_count ;
1233   unsigned long relax_count ;
1234   unsigned long hit_count ;
1235   unsigned char active : 1 ;
1236};
1237#line 999 "include/linux/device.h"
1238struct dma_attrs {
1239   unsigned long flags[1U] ;
1240};
1241#line 67 "include/linux/dma-attrs.h"
1242enum dma_data_direction {
1243    DMA_BIDIRECTIONAL = 0,
1244    DMA_TO_DEVICE = 1,
1245    DMA_FROM_DEVICE = 2,
1246    DMA_NONE = 3
1247} ;
1248#line 74 "include/linux/dma-attrs.h"
1249struct scatterlist {
1250   unsigned long sg_magic ;
1251   unsigned long page_link ;
1252   unsigned int offset ;
1253   unsigned int length ;
1254   dma_addr_t dma_address ;
1255   unsigned int dma_length ;
1256};
1257#line 268 "include/linux/scatterlist.h"
1258struct dma_map_ops {
1259   void *(*alloc)(struct device * , size_t  , dma_addr_t * , gfp_t  , struct dma_attrs * ) ;
1260   void (*free)(struct device * , size_t  , void * , dma_addr_t  , struct dma_attrs * ) ;
1261   int (*mmap)(struct device * , struct vm_area_struct * , void * , dma_addr_t  ,
1262               size_t  , struct dma_attrs * ) ;
1263   dma_addr_t (*map_page)(struct device * , struct page * , unsigned long  , size_t  ,
1264                          enum dma_data_direction  , struct dma_attrs * ) ;
1265   void (*unmap_page)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ,
1266                      struct dma_attrs * ) ;
1267   int (*map_sg)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ,
1268                 struct dma_attrs * ) ;
1269   void (*unmap_sg)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ,
1270                    struct dma_attrs * ) ;
1271   void (*sync_single_for_cpu)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ) ;
1272   void (*sync_single_for_device)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ) ;
1273   void (*sync_sg_for_cpu)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ) ;
1274   void (*sync_sg_for_device)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ) ;
1275   int (*mapping_error)(struct device * , dma_addr_t  ) ;
1276   int (*dma_supported)(struct device * , u64  ) ;
1277   int (*set_dma_mask)(struct device * , u64  ) ;
1278   int is_phys ;
1279};
1280#line 202 "include/linux/dma-mapping.h"
1281struct exception_table_entry {
1282   unsigned long insn ;
1283   unsigned long fixup ;
1284};
1285#line 334 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedi.h"
1286struct comedi_insn {
1287   unsigned int insn ;
1288   unsigned int n ;
1289   unsigned int *data ;
1290   unsigned int subdev ;
1291   unsigned int chanspec ;
1292   unsigned int unused[3U] ;
1293};
1294#line 348 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedi.h"
1295struct comedi_cmd {
1296   unsigned int subdev ;
1297   unsigned int flags ;
1298   unsigned int start_src ;
1299   unsigned int start_arg ;
1300   unsigned int scan_begin_src ;
1301   unsigned int scan_begin_arg ;
1302   unsigned int convert_src ;
1303   unsigned int convert_arg ;
1304   unsigned int scan_end_src ;
1305   unsigned int scan_end_arg ;
1306   unsigned int stop_src ;
1307   unsigned int stop_arg ;
1308   unsigned int *chanlist ;
1309   unsigned int chanlist_len ;
1310   short *data ;
1311   unsigned int data_len ;
1312};
1313#line 387 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedi.h"
1314struct comedi_krange {
1315   int min ;
1316   int max ;
1317   unsigned int flags ;
1318};
1319#line 418 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedi.h"
1320struct comedi_devconfig {
1321   char board_name[20U] ;
1322   int options[32U] ;
1323};
1324#line 892
1325struct comedi_device;
1326#line 892
1327struct comedi_async;
1328#line 892
1329struct comedi_lrange;
1330#line 892 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedi.h"
1331struct comedi_subdevice {
1332   struct comedi_device *device ;
1333   int type ;
1334   int n_chan ;
1335   int subdev_flags ;
1336   int len_chanlist ;
1337   void *private ;
1338   struct comedi_async *async ;
1339   void *lock ;
1340   void *busy ;
1341   unsigned int runflags ;
1342   spinlock_t spin_lock ;
1343   int io_bits ;
1344   unsigned int maxdata ;
1345   unsigned int const   *maxdata_list ;
1346   unsigned int flags ;
1347   unsigned int const   *flaglist ;
1348   unsigned int settling_time_0 ;
1349   struct comedi_lrange  const  *range_table ;
1350   struct comedi_lrange  const  * const  *range_table_list ;
1351   unsigned int *chanlist ;
1352   int (*insn_read)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
1353                    unsigned int * ) ;
1354   int (*insn_write)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
1355                     unsigned int * ) ;
1356   int (*insn_bits)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
1357                    unsigned int * ) ;
1358   int (*insn_config)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
1359                      unsigned int * ) ;
1360   int (*do_cmd)(struct comedi_device * , struct comedi_subdevice * ) ;
1361   int (*do_cmdtest)(struct comedi_device * , struct comedi_subdevice * , struct comedi_cmd * ) ;
1362   int (*poll)(struct comedi_device * , struct comedi_subdevice * ) ;
1363   int (*cancel)(struct comedi_device * , struct comedi_subdevice * ) ;
1364   int (*buf_change)(struct comedi_device * , struct comedi_subdevice * , unsigned long  ) ;
1365   void (*munge)(struct comedi_device * , struct comedi_subdevice * , void * , unsigned int  ,
1366                 unsigned int  ) ;
1367   enum dma_data_direction async_dma_dir ;
1368   unsigned int state ;
1369   struct device *class_dev ;
1370   int minor ;
1371};
1372#line 127 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1373struct comedi_buf_page {
1374   void *virt_addr ;
1375   dma_addr_t dma_addr ;
1376};
1377#line 132 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1378struct comedi_async {
1379   struct comedi_subdevice *subdevice ;
1380   void *prealloc_buf ;
1381   unsigned int prealloc_bufsz ;
1382   struct comedi_buf_page *buf_page_list ;
1383   unsigned int n_buf_pages ;
1384   unsigned int max_bufsize ;
1385   unsigned int mmap_count ;
1386   unsigned int buf_write_count ;
1387   unsigned int buf_write_alloc_count ;
1388   unsigned int buf_read_count ;
1389   unsigned int buf_read_alloc_count ;
1390   unsigned int buf_write_ptr ;
1391   unsigned int buf_read_ptr ;
1392   unsigned int cur_chan ;
1393   unsigned int scan_progress ;
1394   unsigned int munge_chan ;
1395   unsigned int munge_count ;
1396   unsigned int munge_ptr ;
1397   unsigned int events ;
1398   struct comedi_cmd cmd ;
1399   wait_queue_head_t wait_head ;
1400   unsigned int cb_mask ;
1401   int (*cb_func)(unsigned int  , void * ) ;
1402   void *cb_arg ;
1403   int (*inttrig)(struct comedi_device * , struct comedi_subdevice * , unsigned int  ) ;
1404};
1405#line 181 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1406struct comedi_driver {
1407   struct comedi_driver *next ;
1408   char const   *driver_name ;
1409   struct module *module ;
1410   int (*attach)(struct comedi_device * , struct comedi_devconfig * ) ;
1411   int (*detach)(struct comedi_device * ) ;
1412   unsigned int num_names ;
1413   char const   * const  *board_name ;
1414   int offset ;
1415};
1416#line 197
1417struct fasync_struct;
1418#line 197 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1419struct comedi_device {
1420   int use_count ;
1421   struct comedi_driver *driver ;
1422   void *private ;
1423   struct device *class_dev ;
1424   int minor ;
1425   struct device *hw_dev ;
1426   char const   *board_name ;
1427   void const   *board_ptr ;
1428   int attached ;
1429   spinlock_t spinlock ;
1430   struct mutex mutex ;
1431   int in_request_module ;
1432   int n_subdevices ;
1433   struct comedi_subdevice *subdevices ;
1434   unsigned long iobase ;
1435   unsigned int irq ;
1436   struct comedi_subdevice *read_subdev ;
1437   struct comedi_subdevice *write_subdev ;
1438   struct fasync_struct *async_queue ;
1439   int (*open)(struct comedi_device * ) ;
1440   void (*close)(struct comedi_device * ) ;
1441};
1442#line 338 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1443struct comedi_lrange {
1444   int length ;
1445   struct comedi_krange range[0U] ;
1446};
1447#line 12 "include/linux/mod_devicetable.h"
1448typedef unsigned long kernel_ulong_t;
1449#line 13 "include/linux/mod_devicetable.h"
1450struct pci_device_id {
1451   __u32 vendor ;
1452   __u32 device ;
1453   __u32 subvendor ;
1454   __u32 subdevice ;
1455   __u32 class ;
1456   __u32 class_mask ;
1457   kernel_ulong_t driver_data ;
1458};
1459#line 215 "include/linux/mod_devicetable.h"
1460struct of_device_id {
1461   char name[32U] ;
1462   char type[32U] ;
1463   char compatible[128U] ;
1464   void *data ;
1465};
1466#line 17 "include/linux/irqreturn.h"
1467struct hotplug_slot;
1468#line 17 "include/linux/irqreturn.h"
1469struct pci_slot {
1470   struct pci_bus *bus ;
1471   struct list_head list ;
1472   struct hotplug_slot *hotplug ;
1473   unsigned char number ;
1474   struct kobject kobj ;
1475};
1476#line 117 "include/linux/pci.h"
1477typedef int pci_power_t;
1478#line 143 "include/linux/pci.h"
1479typedef unsigned int pci_channel_state_t;
1480#line 144
1481enum pci_channel_state {
1482    pci_channel_io_normal = 1,
1483    pci_channel_io_frozen = 2,
1484    pci_channel_io_perm_failure = 3
1485} ;
1486#line 169 "include/linux/pci.h"
1487typedef unsigned short pci_dev_flags_t;
1488#line 186 "include/linux/pci.h"
1489typedef unsigned short pci_bus_flags_t;
1490#line 229
1491struct pcie_link_state;
1492#line 229
1493struct pcie_link_state;
1494#line 230
1495struct pci_vpd;
1496#line 230
1497struct pci_vpd;
1498#line 231
1499struct pci_sriov;
1500#line 231
1501struct pci_sriov;
1502#line 232
1503struct pci_ats;
1504#line 232
1505struct pci_ats;
1506#line 233
1507struct proc_dir_entry;
1508#line 233
1509struct pci_driver;
1510#line 233 "include/linux/pci.h"
1511union __anonunion_ldv_19654_147 {
1512   struct pci_sriov *sriov ;
1513   struct pci_dev *physfn ;
1514};
1515#line 233 "include/linux/pci.h"
1516struct pci_dev {
1517   struct list_head bus_list ;
1518   struct pci_bus *bus ;
1519   struct pci_bus *subordinate ;
1520   void *sysdata ;
1521   struct proc_dir_entry *procent ;
1522   struct pci_slot *slot ;
1523   unsigned int devfn ;
1524   unsigned short vendor ;
1525   unsigned short device ;
1526   unsigned short subsystem_vendor ;
1527   unsigned short subsystem_device ;
1528   unsigned int class ;
1529   u8 revision ;
1530   u8 hdr_type ;
1531   u8 pcie_cap ;
1532   unsigned char pcie_type : 4 ;
1533   unsigned char pcie_mpss : 3 ;
1534   u8 rom_base_reg ;
1535   u8 pin ;
1536   struct pci_driver *driver ;
1537   u64 dma_mask ;
1538   struct device_dma_parameters dma_parms ;
1539   pci_power_t current_state ;
1540   int pm_cap ;
1541   unsigned char pme_support : 5 ;
1542   unsigned char pme_interrupt : 1 ;
1543   unsigned char pme_poll : 1 ;
1544   unsigned char d1_support : 1 ;
1545   unsigned char d2_support : 1 ;
1546   unsigned char no_d1d2 : 1 ;
1547   unsigned char mmio_always_on : 1 ;
1548   unsigned char wakeup_prepared : 1 ;
1549   unsigned int d3_delay ;
1550   struct pcie_link_state *link_state ;
1551   pci_channel_state_t error_state ;
1552   struct device dev ;
1553   int cfg_size ;
1554   unsigned int irq ;
1555   struct resource resource[17U] ;
1556   unsigned char transparent : 1 ;
1557   unsigned char multifunction : 1 ;
1558   unsigned char is_added : 1 ;
1559   unsigned char is_busmaster : 1 ;
1560   unsigned char no_msi : 1 ;
1561   unsigned char block_cfg_access : 1 ;
1562   unsigned char broken_parity_status : 1 ;
1563   unsigned char irq_reroute_variant : 2 ;
1564   unsigned char msi_enabled : 1 ;
1565   unsigned char msix_enabled : 1 ;
1566   unsigned char ari_enabled : 1 ;
1567   unsigned char is_managed : 1 ;
1568   unsigned char is_pcie : 1 ;
1569   unsigned char needs_freset : 1 ;
1570   unsigned char state_saved : 1 ;
1571   unsigned char is_physfn : 1 ;
1572   unsigned char is_virtfn : 1 ;
1573   unsigned char reset_fn : 1 ;
1574   unsigned char is_hotplug_bridge : 1 ;
1575   unsigned char __aer_firmware_first_valid : 1 ;
1576   unsigned char __aer_firmware_first : 1 ;
1577   pci_dev_flags_t dev_flags ;
1578   atomic_t enable_cnt ;
1579   u32 saved_config_space[16U] ;
1580   struct hlist_head saved_cap_space ;
1581   struct bin_attribute *rom_attr ;
1582   int rom_attr_enabled ;
1583   struct bin_attribute *res_attr[17U] ;
1584   struct bin_attribute *res_attr_wc[17U] ;
1585   struct list_head msi_list ;
1586   struct kset *msi_kset ;
1587   struct pci_vpd *vpd ;
1588   union __anonunion_ldv_19654_147 ldv_19654 ;
1589   struct pci_ats *ats ;
1590};
1591#line 403
1592struct pci_ops;
1593#line 403 "include/linux/pci.h"
1594struct pci_bus {
1595   struct list_head node ;
1596   struct pci_bus *parent ;
1597   struct list_head children ;
1598   struct list_head devices ;
1599   struct pci_dev *self ;
1600   struct list_head slots ;
1601   struct resource *resource[4U] ;
1602   struct list_head resources ;
1603   struct pci_ops *ops ;
1604   void *sysdata ;
1605   struct proc_dir_entry *procdir ;
1606   unsigned char number ;
1607   unsigned char primary ;
1608   unsigned char secondary ;
1609   unsigned char subordinate ;
1610   unsigned char max_bus_speed ;
1611   unsigned char cur_bus_speed ;
1612   char name[48U] ;
1613   unsigned short bridge_ctl ;
1614   pci_bus_flags_t bus_flags ;
1615   struct device *bridge ;
1616   struct device dev ;
1617   struct bin_attribute *legacy_io ;
1618   struct bin_attribute *legacy_mem ;
1619   unsigned char is_added : 1 ;
1620};
1621#line 455 "include/linux/pci.h"
1622struct pci_ops {
1623   int (*read)(struct pci_bus * , unsigned int  , int  , int  , u32 * ) ;
1624   int (*write)(struct pci_bus * , unsigned int  , int  , int  , u32  ) ;
1625};
1626#line 490 "include/linux/pci.h"
1627struct pci_dynids {
1628   spinlock_t lock ;
1629   struct list_head list ;
1630};
1631#line 503 "include/linux/pci.h"
1632typedef unsigned int pci_ers_result_t;
1633#line 512 "include/linux/pci.h"
1634struct pci_error_handlers {
1635   pci_ers_result_t (*error_detected)(struct pci_dev * , enum pci_channel_state  ) ;
1636   pci_ers_result_t (*mmio_enabled)(struct pci_dev * ) ;
1637   pci_ers_result_t (*link_reset)(struct pci_dev * ) ;
1638   pci_ers_result_t (*slot_reset)(struct pci_dev * ) ;
1639   void (*resume)(struct pci_dev * ) ;
1640};
1641#line 540 "include/linux/pci.h"
1642struct pci_driver {
1643   struct list_head node ;
1644   char const   *name ;
1645   struct pci_device_id  const  *id_table ;
1646   int (*probe)(struct pci_dev * , struct pci_device_id  const  * ) ;
1647   void (*remove)(struct pci_dev * ) ;
1648   int (*suspend)(struct pci_dev * , pm_message_t  ) ;
1649   int (*suspend_late)(struct pci_dev * , pm_message_t  ) ;
1650   int (*resume_early)(struct pci_dev * ) ;
1651   int (*resume)(struct pci_dev * ) ;
1652   void (*shutdown)(struct pci_dev * ) ;
1653   struct pci_error_handlers *err_handler ;
1654   struct device_driver driver ;
1655   struct pci_dynids dynids ;
1656};
1657#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
1658struct adl_pci8164_private {
1659   int data ;
1660   struct pci_dev *pci_dev ;
1661};
1662#line 2
1663void ldv_spin_lock(void) ;
1664#line 3
1665void ldv_spin_unlock(void) ;
1666#line 4
1667int ldv_spin_trylock(void) ;
1668#line 101 "include/linux/printk.h"
1669extern int printk(char const   *  , ...) ;
1670#line 93 "include/linux/spinlock.h"
1671extern void __raw_spin_lock_init(raw_spinlock_t * , char const   * , struct lock_class_key * ) ;
1672#line 272 "include/linux/spinlock.h"
1673__inline static raw_spinlock_t *spinlock_check(spinlock_t *lock ) 
1674{ 
1675
1676  {
1677#line 274
1678  return ((struct raw_spinlock *)lock);
1679}
1680}
1681#line 309 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1682__inline static void outw(unsigned short value , int port ) 
1683{ 
1684
1685  {
1686#line 309
1687  __asm__  volatile   ("outw %w0, %w1": : "a" (value), "Nd" (port));
1688#line 310
1689  return;
1690}
1691}
1692#line 309 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1693__inline static unsigned short inw(int port ) 
1694{ unsigned short value ;
1695
1696  {
1697#line 309
1698  __asm__  volatile   ("inw %w1, %w0": "=a" (value): "Nd" (port));
1699#line 309
1700  return (value);
1701}
1702}
1703#line 26 "include/linux/export.h"
1704extern struct module __this_module ;
1705#line 220 "include/linux/slub_def.h"
1706extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1707#line 223
1708void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1709#line 225
1710extern void *__kmalloc(size_t  , gfp_t  ) ;
1711#line 243 "include/linux/slab.h"
1712__inline static void *kmalloc_array(size_t n , size_t size , gfp_t flags ) 
1713{ void *tmp ;
1714  unsigned long __cil_tmp5 ;
1715  size_t __cil_tmp6 ;
1716
1717  {
1718#line 245
1719  if (size != 0UL) {
1720    {
1721#line 245
1722    __cil_tmp5 = 0xffffffffffffffffUL / size;
1723#line 245
1724    if (__cil_tmp5 < n) {
1725#line 246
1726      return ((void *)0);
1727    } else {
1728
1729    }
1730    }
1731  } else {
1732
1733  }
1734  {
1735#line 247
1736  __cil_tmp6 = n * size;
1737#line 247
1738  tmp = __kmalloc(__cil_tmp6, flags);
1739  }
1740#line 247
1741  return (tmp);
1742}
1743}
1744#line 256 "include/linux/slab.h"
1745__inline static void *ldv_kcalloc_14(size_t n , size_t size , gfp_t flags ) 
1746{ void *tmp ;
1747  unsigned int __cil_tmp5 ;
1748
1749  {
1750  {
1751#line 258
1752  __cil_tmp5 = flags | 32768U;
1753#line 258
1754  tmp = kmalloc_array(n, size, __cil_tmp5);
1755  }
1756#line 258
1757  return (tmp);
1758}
1759}
1760#line 256
1761__inline static void *kcalloc(size_t n , size_t size , gfp_t flags ) ;
1762#line 353
1763__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1764#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
1765extern void *__VERIFIER_nondet_pointer(void) ;
1766#line 11
1767void ldv_check_alloc_flags(gfp_t flags ) ;
1768#line 12
1769void ldv_check_alloc_nonatomic(void) ;
1770#line 14
1771struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1772#line 287 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1773extern int comedi_driver_register(struct comedi_driver * ) ;
1774#line 288
1775extern int comedi_driver_unregister(struct comedi_driver * ) ;
1776#line 354 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1777__inline static int alloc_subdevices(struct comedi_device *dev , unsigned int num_subdevices ) 
1778{ unsigned int i ;
1779  void *tmp ;
1780  struct lock_class_key __key ;
1781  unsigned long __cil_tmp6 ;
1782  unsigned long __cil_tmp7 ;
1783  size_t __cil_tmp8 ;
1784  unsigned long __cil_tmp9 ;
1785  unsigned long __cil_tmp10 ;
1786  struct comedi_subdevice *__cil_tmp11 ;
1787  unsigned long __cil_tmp12 ;
1788  unsigned long __cil_tmp13 ;
1789  unsigned long __cil_tmp14 ;
1790  struct comedi_subdevice *__cil_tmp15 ;
1791  unsigned long __cil_tmp16 ;
1792  unsigned long __cil_tmp17 ;
1793  unsigned long __cil_tmp18 ;
1794  unsigned long __cil_tmp19 ;
1795  struct comedi_subdevice *__cil_tmp20 ;
1796  struct comedi_subdevice *__cil_tmp21 ;
1797  unsigned long __cil_tmp22 ;
1798  unsigned long __cil_tmp23 ;
1799  unsigned long __cil_tmp24 ;
1800  struct comedi_subdevice *__cil_tmp25 ;
1801  struct comedi_subdevice *__cil_tmp26 ;
1802  unsigned long __cil_tmp27 ;
1803  unsigned long __cil_tmp28 ;
1804  unsigned long __cil_tmp29 ;
1805  unsigned long __cil_tmp30 ;
1806  unsigned long __cil_tmp31 ;
1807  struct comedi_subdevice *__cil_tmp32 ;
1808  struct comedi_subdevice *__cil_tmp33 ;
1809  unsigned long __cil_tmp34 ;
1810  unsigned long __cil_tmp35 ;
1811  spinlock_t *__cil_tmp36 ;
1812  unsigned long __cil_tmp37 ;
1813  unsigned long __cil_tmp38 ;
1814  unsigned long __cil_tmp39 ;
1815  struct comedi_subdevice *__cil_tmp40 ;
1816  struct comedi_subdevice *__cil_tmp41 ;
1817  unsigned long __cil_tmp42 ;
1818  unsigned long __cil_tmp43 ;
1819  struct raw_spinlock *__cil_tmp44 ;
1820  unsigned long __cil_tmp45 ;
1821  unsigned long __cil_tmp46 ;
1822  unsigned long __cil_tmp47 ;
1823  struct comedi_subdevice *__cil_tmp48 ;
1824  struct comedi_subdevice *__cil_tmp49 ;
1825  unsigned long __cil_tmp50 ;
1826  unsigned long __cil_tmp51 ;
1827
1828  {
1829  {
1830#line 359
1831  __cil_tmp6 = (unsigned long )dev;
1832#line 359
1833  __cil_tmp7 = __cil_tmp6 + 316;
1834#line 359
1835  *((int *)__cil_tmp7) = (int )num_subdevices;
1836#line 360
1837  __cil_tmp8 = (size_t )num_subdevices;
1838#line 360
1839  tmp = kcalloc(__cil_tmp8, 304UL, 208U);
1840#line 360
1841  __cil_tmp9 = (unsigned long )dev;
1842#line 360
1843  __cil_tmp10 = __cil_tmp9 + 320;
1844#line 360
1845  *((struct comedi_subdevice **)__cil_tmp10) = (struct comedi_subdevice *)tmp;
1846  }
1847  {
1848#line 363
1849  __cil_tmp11 = (struct comedi_subdevice *)0;
1850#line 363
1851  __cil_tmp12 = (unsigned long )__cil_tmp11;
1852#line 363
1853  __cil_tmp13 = (unsigned long )dev;
1854#line 363
1855  __cil_tmp14 = __cil_tmp13 + 320;
1856#line 363
1857  __cil_tmp15 = *((struct comedi_subdevice **)__cil_tmp14);
1858#line 363
1859  __cil_tmp16 = (unsigned long )__cil_tmp15;
1860#line 363
1861  if (__cil_tmp16 == __cil_tmp12) {
1862#line 364
1863    return (-12);
1864  } else {
1865
1866  }
1867  }
1868#line 365
1869  i = 0U;
1870#line 365
1871  goto ldv_19184;
1872  ldv_19183: 
1873  {
1874#line 366
1875  __cil_tmp17 = (unsigned long )i;
1876#line 366
1877  __cil_tmp18 = (unsigned long )dev;
1878#line 366
1879  __cil_tmp19 = __cil_tmp18 + 320;
1880#line 366
1881  __cil_tmp20 = *((struct comedi_subdevice **)__cil_tmp19);
1882#line 366
1883  __cil_tmp21 = __cil_tmp20 + __cil_tmp17;
1884#line 366
1885  *((struct comedi_device **)__cil_tmp21) = dev;
1886#line 367
1887  __cil_tmp22 = (unsigned long )i;
1888#line 367
1889  __cil_tmp23 = (unsigned long )dev;
1890#line 367
1891  __cil_tmp24 = __cil_tmp23 + 320;
1892#line 367
1893  __cil_tmp25 = *((struct comedi_subdevice **)__cil_tmp24);
1894#line 367
1895  __cil_tmp26 = __cil_tmp25 + __cil_tmp22;
1896#line 367
1897  __cil_tmp27 = (unsigned long )__cil_tmp26;
1898#line 367
1899  __cil_tmp28 = __cil_tmp27 + 280;
1900#line 367
1901  *((enum dma_data_direction *)__cil_tmp28) = (enum dma_data_direction )3;
1902#line 368
1903  __cil_tmp29 = (unsigned long )i;
1904#line 368
1905  __cil_tmp30 = (unsigned long )dev;
1906#line 368
1907  __cil_tmp31 = __cil_tmp30 + 320;
1908#line 368
1909  __cil_tmp32 = *((struct comedi_subdevice **)__cil_tmp31);
1910#line 368
1911  __cil_tmp33 = __cil_tmp32 + __cil_tmp29;
1912#line 368
1913  __cil_tmp34 = (unsigned long )__cil_tmp33;
1914#line 368
1915  __cil_tmp35 = __cil_tmp34 + 64;
1916#line 368
1917  __cil_tmp36 = (spinlock_t *)__cil_tmp35;
1918#line 368
1919  spinlock_check(__cil_tmp36);
1920#line 368
1921  __cil_tmp37 = (unsigned long )i;
1922#line 368
1923  __cil_tmp38 = (unsigned long )dev;
1924#line 368
1925  __cil_tmp39 = __cil_tmp38 + 320;
1926#line 368
1927  __cil_tmp40 = *((struct comedi_subdevice **)__cil_tmp39);
1928#line 368
1929  __cil_tmp41 = __cil_tmp40 + __cil_tmp37;
1930#line 368
1931  __cil_tmp42 = (unsigned long )__cil_tmp41;
1932#line 368
1933  __cil_tmp43 = __cil_tmp42 + 64;
1934#line 368
1935  __cil_tmp44 = (struct raw_spinlock *)__cil_tmp43;
1936#line 368
1937  __raw_spin_lock_init(__cil_tmp44, "&(&dev->subdevices[i].spin_lock)->rlock", & __key);
1938#line 369
1939  __cil_tmp45 = (unsigned long )i;
1940#line 369
1941  __cil_tmp46 = (unsigned long )dev;
1942#line 369
1943  __cil_tmp47 = __cil_tmp46 + 320;
1944#line 369
1945  __cil_tmp48 = *((struct comedi_subdevice **)__cil_tmp47);
1946#line 369
1947  __cil_tmp49 = __cil_tmp48 + __cil_tmp45;
1948#line 369
1949  __cil_tmp50 = (unsigned long )__cil_tmp49;
1950#line 369
1951  __cil_tmp51 = __cil_tmp50 + 296;
1952#line 369
1953  *((int *)__cil_tmp51) = -1;
1954#line 365
1955  i = i + 1U;
1956  }
1957  ldv_19184: ;
1958#line 365
1959  if (i < num_subdevices) {
1960#line 366
1961    goto ldv_19183;
1962  } else {
1963#line 368
1964    goto ldv_19185;
1965  }
1966  ldv_19185: ;
1967#line 371
1968  return (0);
1969}
1970}
1971#line 374 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1972__inline static int alloc_private(struct comedi_device *dev , int size ) 
1973{ unsigned long __cil_tmp3 ;
1974  unsigned long __cil_tmp4 ;
1975  size_t __cil_tmp5 ;
1976  void *__cil_tmp6 ;
1977  unsigned long __cil_tmp7 ;
1978  unsigned long __cil_tmp8 ;
1979  unsigned long __cil_tmp9 ;
1980  void *__cil_tmp10 ;
1981  unsigned long __cil_tmp11 ;
1982
1983  {
1984  {
1985#line 376
1986  __cil_tmp3 = (unsigned long )dev;
1987#line 376
1988  __cil_tmp4 = __cil_tmp3 + 16;
1989#line 376
1990  __cil_tmp5 = (size_t )size;
1991#line 376
1992  *((void **)__cil_tmp4) = kzalloc(__cil_tmp5, 208U);
1993  }
1994  {
1995#line 377
1996  __cil_tmp6 = (void *)0;
1997#line 377
1998  __cil_tmp7 = (unsigned long )__cil_tmp6;
1999#line 377
2000  __cil_tmp8 = (unsigned long )dev;
2001#line 377
2002  __cil_tmp9 = __cil_tmp8 + 16;
2003#line 377
2004  __cil_tmp10 = *((void **)__cil_tmp9);
2005#line 377
2006  __cil_tmp11 = (unsigned long )__cil_tmp10;
2007#line 377
2008  if (__cil_tmp11 == __cil_tmp7) {
2009#line 378
2010    return (-12);
2011  } else {
2012
2013  }
2014  }
2015#line 379
2016  return (0);
2017}
2018}
2019#line 459
2020extern int comedi_pci_auto_config(struct pci_dev * , char const   * ) ;
2021#line 460
2022extern void comedi_pci_auto_unconfig(struct pci_dev * ) ;
2023#line 687 "include/linux/pci.h"
2024extern void pci_dev_put(struct pci_dev * ) ;
2025#line 716
2026extern struct pci_dev *pci_get_device(unsigned int  , unsigned int  , struct pci_dev * ) ;
2027#line 773
2028extern int pci_enable_device(struct pci_dev * ) ;
2029#line 790
2030extern void pci_disable_device(struct pci_dev * ) ;
2031#line 904
2032extern int pci_request_regions(struct pci_dev * , char const   * ) ;
2033#line 906
2034extern void pci_release_regions(struct pci_dev * ) ;
2035#line 940
2036extern int __pci_register_driver(struct pci_driver * , struct module * , char const   * ) ;
2037#line 949
2038extern void pci_unregister_driver(struct pci_driver * ) ;
2039#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/comedi_pci.h"
2040__inline static int comedi_pci_enable(struct pci_dev *pdev , char const   *res_name ) 
2041{ int rc ;
2042
2043  {
2044  {
2045#line 38
2046  rc = pci_enable_device(pdev);
2047  }
2048#line 39
2049  if (rc < 0) {
2050#line 40
2051    return (rc);
2052  } else {
2053
2054  }
2055  {
2056#line 42
2057  rc = pci_request_regions(pdev, res_name);
2058  }
2059#line 43
2060  if (rc < 0) {
2061    {
2062#line 44
2063    pci_disable_device(pdev);
2064    }
2065  } else {
2066
2067  }
2068#line 46
2069  return (rc);
2070}
2071}
2072#line 54 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/comedi_pci.h"
2073__inline static void comedi_pci_disable(struct pci_dev *pdev ) 
2074{ 
2075
2076  {
2077  {
2078#line 56
2079  pci_release_regions(pdev);
2080#line 57
2081  pci_disable_device(pdev);
2082  }
2083#line 58
2084  return;
2085}
2086}
2087#line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
2088static struct pci_device_id  const  adl_pci8164_pci_table[2U]  = {      {5194U, 33124U, 4294967295U, 4294967295U, 0U, 0U, 0UL}, 
2089        {0U, 0U, 0U, 0U, 0U, 0U, 0UL}};
2090#line 79 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
2091struct pci_device_id  const  __mod_pci_device_table  ;
2092#line 88
2093static int adl_pci8164_attach(struct comedi_device *dev , struct comedi_devconfig *it ) ;
2094#line 90
2095static int adl_pci8164_detach(struct comedi_device *dev ) ;
2096#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
2097static struct comedi_driver driver_adl_pci8164  = 
2098#line 91
2099     {(struct comedi_driver *)0, "adl_pci8164", & __this_module, & adl_pci8164_attach,
2100    & adl_pci8164_detach, 0U, (char const   * const  *)0, 0};
2101#line 98
2102static int adl_pci8164_insn_read_msts(struct comedi_device *dev , struct comedi_subdevice *s ,
2103                                      struct comedi_insn *insn , unsigned int *data ) ;
2104#line 103
2105static int adl_pci8164_insn_read_ssts(struct comedi_device *dev , struct comedi_subdevice *s ,
2106                                      struct comedi_insn *insn , unsigned int *data ) ;
2107#line 108
2108static int adl_pci8164_insn_read_buf0(struct comedi_device *dev , struct comedi_subdevice *s ,
2109                                      struct comedi_insn *insn , unsigned int *data ) ;
2110#line 113
2111static int adl_pci8164_insn_read_buf1(struct comedi_device *dev , struct comedi_subdevice *s ,
2112                                      struct comedi_insn *insn , unsigned int *data ) ;
2113#line 118
2114static int adl_pci8164_insn_write_cmd(struct comedi_device *dev , struct comedi_subdevice *s ,
2115                                      struct comedi_insn *insn , unsigned int *data ) ;
2116#line 123
2117static int adl_pci8164_insn_write_otp(struct comedi_device *dev , struct comedi_subdevice *s ,
2118                                      struct comedi_insn *insn , unsigned int *data ) ;
2119#line 128
2120static int adl_pci8164_insn_write_buf0(struct comedi_device *dev , struct comedi_subdevice *s ,
2121                                       struct comedi_insn *insn , unsigned int *data ) ;
2122#line 133
2123static int adl_pci8164_insn_write_buf1(struct comedi_device *dev , struct comedi_subdevice *s ,
2124                                       struct comedi_insn *insn , unsigned int *data ) ;
2125#line 138 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
2126static int adl_pci8164_attach(struct comedi_device *dev , struct comedi_devconfig *it ) 
2127{ struct pci_dev *pcidev ;
2128  struct comedi_subdevice *s ;
2129  int bus ;
2130  int slot ;
2131  int tmp ;
2132  int tmp___0 ;
2133  int tmp___1 ;
2134  unsigned long __cil_tmp10 ;
2135  unsigned long __cil_tmp11 ;
2136  int __cil_tmp12 ;
2137  unsigned long __cil_tmp13 ;
2138  unsigned long __cil_tmp14 ;
2139  unsigned long __cil_tmp15 ;
2140  unsigned long __cil_tmp16 ;
2141  unsigned long __cil_tmp17 ;
2142  unsigned long __cil_tmp18 ;
2143  unsigned long __cil_tmp19 ;
2144  unsigned long __cil_tmp20 ;
2145  unsigned long __cil_tmp21 ;
2146  unsigned long __cil_tmp22 ;
2147  unsigned long __cil_tmp23 ;
2148  unsigned long __cil_tmp24 ;
2149  unsigned short __cil_tmp25 ;
2150  unsigned int __cil_tmp26 ;
2151  unsigned long __cil_tmp27 ;
2152  unsigned long __cil_tmp28 ;
2153  unsigned short __cil_tmp29 ;
2154  unsigned int __cil_tmp30 ;
2155  unsigned long __cil_tmp31 ;
2156  unsigned long __cil_tmp32 ;
2157  struct pci_bus *__cil_tmp33 ;
2158  unsigned long __cil_tmp34 ;
2159  unsigned long __cil_tmp35 ;
2160  unsigned char __cil_tmp36 ;
2161  int __cil_tmp37 ;
2162  unsigned int __cil_tmp38 ;
2163  unsigned long __cil_tmp39 ;
2164  unsigned long __cil_tmp40 ;
2165  unsigned int __cil_tmp41 ;
2166  unsigned int __cil_tmp42 ;
2167  unsigned int __cil_tmp43 ;
2168  unsigned long __cil_tmp44 ;
2169  unsigned long __cil_tmp45 ;
2170  void *__cil_tmp46 ;
2171  struct adl_pci8164_private *__cil_tmp47 ;
2172  unsigned long __cil_tmp48 ;
2173  unsigned long __cil_tmp49 ;
2174  unsigned long __cil_tmp50 ;
2175  unsigned long __cil_tmp51 ;
2176  int __cil_tmp52 ;
2177  unsigned long __cil_tmp53 ;
2178  unsigned long __cil_tmp54 ;
2179  unsigned long __cil_tmp55 ;
2180  unsigned long __cil_tmp56 ;
2181  unsigned long __cil_tmp57 ;
2182  unsigned long __cil_tmp58 ;
2183  resource_size_t __cil_tmp59 ;
2184  unsigned long __cil_tmp60 ;
2185  unsigned long __cil_tmp61 ;
2186  unsigned long __cil_tmp62 ;
2187  unsigned long __cil_tmp63 ;
2188  unsigned long __cil_tmp64 ;
2189  unsigned long __cil_tmp65 ;
2190  unsigned long __cil_tmp66 ;
2191  unsigned long __cil_tmp67 ;
2192  unsigned long __cil_tmp68 ;
2193  unsigned long __cil_tmp69 ;
2194  unsigned long __cil_tmp70 ;
2195  unsigned long __cil_tmp71 ;
2196  unsigned long __cil_tmp72 ;
2197  unsigned long __cil_tmp73 ;
2198  unsigned long __cil_tmp74 ;
2199  unsigned long __cil_tmp75 ;
2200  unsigned long __cil_tmp76 ;
2201  unsigned long __cil_tmp77 ;
2202  unsigned long __cil_tmp78 ;
2203  unsigned long __cil_tmp79 ;
2204  unsigned long __cil_tmp80 ;
2205  struct comedi_subdevice *__cil_tmp81 ;
2206  unsigned long __cil_tmp82 ;
2207  unsigned long __cil_tmp83 ;
2208  unsigned long __cil_tmp84 ;
2209  unsigned long __cil_tmp85 ;
2210  unsigned long __cil_tmp86 ;
2211  unsigned long __cil_tmp87 ;
2212  unsigned long __cil_tmp88 ;
2213  unsigned long __cil_tmp89 ;
2214  unsigned long __cil_tmp90 ;
2215  unsigned long __cil_tmp91 ;
2216  unsigned long __cil_tmp92 ;
2217  unsigned long __cil_tmp93 ;
2218  unsigned long __cil_tmp94 ;
2219  unsigned long __cil_tmp95 ;
2220  unsigned long __cil_tmp96 ;
2221  unsigned long __cil_tmp97 ;
2222  struct comedi_subdevice *__cil_tmp98 ;
2223  unsigned long __cil_tmp99 ;
2224  unsigned long __cil_tmp100 ;
2225  unsigned long __cil_tmp101 ;
2226  unsigned long __cil_tmp102 ;
2227  unsigned long __cil_tmp103 ;
2228  unsigned long __cil_tmp104 ;
2229  unsigned long __cil_tmp105 ;
2230  unsigned long __cil_tmp106 ;
2231  unsigned long __cil_tmp107 ;
2232  unsigned long __cil_tmp108 ;
2233  unsigned long __cil_tmp109 ;
2234  unsigned long __cil_tmp110 ;
2235  unsigned long __cil_tmp111 ;
2236  unsigned long __cil_tmp112 ;
2237  unsigned long __cil_tmp113 ;
2238  unsigned long __cil_tmp114 ;
2239  struct comedi_subdevice *__cil_tmp115 ;
2240  unsigned long __cil_tmp116 ;
2241  unsigned long __cil_tmp117 ;
2242  unsigned long __cil_tmp118 ;
2243  unsigned long __cil_tmp119 ;
2244  unsigned long __cil_tmp120 ;
2245  unsigned long __cil_tmp121 ;
2246  unsigned long __cil_tmp122 ;
2247  unsigned long __cil_tmp123 ;
2248  unsigned long __cil_tmp124 ;
2249  unsigned long __cil_tmp125 ;
2250  unsigned long __cil_tmp126 ;
2251  unsigned long __cil_tmp127 ;
2252  unsigned long __cil_tmp128 ;
2253  unsigned long __cil_tmp129 ;
2254  struct pci_dev *__cil_tmp130 ;
2255  unsigned long __cil_tmp131 ;
2256  unsigned long __cil_tmp132 ;
2257  unsigned long __cil_tmp133 ;
2258  unsigned long __cil_tmp134 ;
2259  int __cil_tmp135 ;
2260
2261  {
2262  {
2263#line 141
2264  pcidev = (struct pci_dev *)0;
2265#line 145
2266  printk("<6>comedi: attempt to attach...\n");
2267#line 146
2268  __cil_tmp10 = (unsigned long )dev;
2269#line 146
2270  __cil_tmp11 = __cil_tmp10 + 32;
2271#line 146
2272  __cil_tmp12 = *((int *)__cil_tmp11);
2273#line 146
2274  printk("<6>comedi%d: adl_pci8164\n", __cil_tmp12);
2275#line 148
2276  __cil_tmp13 = (unsigned long )dev;
2277#line 148
2278  __cil_tmp14 = __cil_tmp13 + 48;
2279#line 148
2280  *((char const   **)__cil_tmp14) = "pci8164";
2281#line 149
2282  __cil_tmp15 = 0 * 4UL;
2283#line 149
2284  __cil_tmp16 = 20 + __cil_tmp15;
2285#line 149
2286  __cil_tmp17 = (unsigned long )it;
2287#line 149
2288  __cil_tmp18 = __cil_tmp17 + __cil_tmp16;
2289#line 149
2290  bus = *((int *)__cil_tmp18);
2291#line 150
2292  __cil_tmp19 = 1 * 4UL;
2293#line 150
2294  __cil_tmp20 = 20 + __cil_tmp19;
2295#line 150
2296  __cil_tmp21 = (unsigned long )it;
2297#line 150
2298  __cil_tmp22 = __cil_tmp21 + __cil_tmp20;
2299#line 150
2300  slot = *((int *)__cil_tmp22);
2301#line 152
2302  tmp = alloc_private(dev, 16);
2303  }
2304#line 152
2305  if (tmp < 0) {
2306#line 153
2307    return (-12);
2308  } else {
2309
2310  }
2311  {
2312#line 155
2313  tmp___0 = alloc_subdevices(dev, 4U);
2314  }
2315#line 155
2316  if (tmp___0 < 0) {
2317#line 156
2318    return (-12);
2319  } else {
2320
2321  }
2322#line 158
2323  goto ldv_21011;
2324  ldv_21012: ;
2325  {
2326#line 159
2327  __cil_tmp23 = (unsigned long )pcidev;
2328#line 159
2329  __cil_tmp24 = __cil_tmp23 + 60;
2330#line 159
2331  __cil_tmp25 = *((unsigned short *)__cil_tmp24);
2332#line 159
2333  __cil_tmp26 = (unsigned int )__cil_tmp25;
2334#line 159
2335  if (__cil_tmp26 == 5194U) {
2336    {
2337#line 159
2338    __cil_tmp27 = (unsigned long )pcidev;
2339#line 159
2340    __cil_tmp28 = __cil_tmp27 + 62;
2341#line 159
2342    __cil_tmp29 = *((unsigned short *)__cil_tmp28);
2343#line 159
2344    __cil_tmp30 = (unsigned int )__cil_tmp29;
2345#line 159
2346    if (__cil_tmp30 == 33124U) {
2347#line 161
2348      if (bus != 0) {
2349#line 161
2350        goto _L;
2351      } else
2352#line 161
2353      if (slot != 0) {
2354        _L: /* CIL Label */ 
2355        {
2356#line 163
2357        __cil_tmp31 = (unsigned long )pcidev;
2358#line 163
2359        __cil_tmp32 = __cil_tmp31 + 16;
2360#line 163
2361        __cil_tmp33 = *((struct pci_bus **)__cil_tmp32);
2362#line 163
2363        __cil_tmp34 = (unsigned long )__cil_tmp33;
2364#line 163
2365        __cil_tmp35 = __cil_tmp34 + 152;
2366#line 163
2367        __cil_tmp36 = *((unsigned char *)__cil_tmp35);
2368#line 163
2369        __cil_tmp37 = (int )__cil_tmp36;
2370#line 163
2371        if (__cil_tmp37 != bus) {
2372#line 165
2373          goto ldv_21011;
2374        } else {
2375          {
2376#line 163
2377          __cil_tmp38 = (unsigned int )slot;
2378#line 163
2379          __cil_tmp39 = (unsigned long )pcidev;
2380#line 163
2381          __cil_tmp40 = __cil_tmp39 + 56;
2382#line 163
2383          __cil_tmp41 = *((unsigned int *)__cil_tmp40);
2384#line 163
2385          __cil_tmp42 = __cil_tmp41 >> 3;
2386#line 163
2387          __cil_tmp43 = __cil_tmp42 & 31U;
2388#line 163
2389          if (__cil_tmp43 != __cil_tmp38) {
2390#line 165
2391            goto ldv_21011;
2392          } else {
2393
2394          }
2395          }
2396        }
2397        }
2398      } else {
2399
2400      }
2401      {
2402#line 167
2403      __cil_tmp44 = (unsigned long )dev;
2404#line 167
2405      __cil_tmp45 = __cil_tmp44 + 16;
2406#line 167
2407      __cil_tmp46 = *((void **)__cil_tmp45);
2408#line 167
2409      __cil_tmp47 = (struct adl_pci8164_private *)__cil_tmp46;
2410#line 167
2411      __cil_tmp48 = (unsigned long )__cil_tmp47;
2412#line 167
2413      __cil_tmp49 = __cil_tmp48 + 8;
2414#line 167
2415      *((struct pci_dev **)__cil_tmp49) = pcidev;
2416#line 168
2417      tmp___1 = comedi_pci_enable(pcidev, "adl_pci8164");
2418      }
2419#line 168
2420      if (tmp___1 < 0) {
2421        {
2422#line 169
2423        __cil_tmp50 = (unsigned long )dev;
2424#line 169
2425        __cil_tmp51 = __cil_tmp50 + 32;
2426#line 169
2427        __cil_tmp52 = *((int *)__cil_tmp51);
2428#line 169
2429        printk("<3>comedi%d: Failed to enable PCI device and request regions\n", __cil_tmp52);
2430        }
2431#line 171
2432        return (-5);
2433      } else {
2434
2435      }
2436      {
2437#line 173
2438      __cil_tmp53 = (unsigned long )dev;
2439#line 173
2440      __cil_tmp54 = __cil_tmp53 + 328;
2441#line 173
2442      __cil_tmp55 = 2 * 56UL;
2443#line 173
2444      __cil_tmp56 = 1304 + __cil_tmp55;
2445#line 173
2446      __cil_tmp57 = (unsigned long )pcidev;
2447#line 173
2448      __cil_tmp58 = __cil_tmp57 + __cil_tmp56;
2449#line 173
2450      __cil_tmp59 = *((resource_size_t *)__cil_tmp58);
2451#line 173
2452      *((unsigned long *)__cil_tmp54) = (unsigned long )__cil_tmp59;
2453#line 174
2454      __cil_tmp60 = (unsigned long )dev;
2455#line 174
2456      __cil_tmp61 = __cil_tmp60 + 328;
2457#line 174
2458      __cil_tmp62 = *((unsigned long *)__cil_tmp61);
2459#line 174
2460      printk("<7>comedi: base addr %4lx\n", __cil_tmp62);
2461#line 177
2462      __cil_tmp63 = (unsigned long )dev;
2463#line 177
2464      __cil_tmp64 = __cil_tmp63 + 320;
2465#line 177
2466      s = *((struct comedi_subdevice **)__cil_tmp64);
2467#line 178
2468      __cil_tmp65 = (unsigned long )s;
2469#line 178
2470      __cil_tmp66 = __cil_tmp65 + 8;
2471#line 178
2472      *((int *)__cil_tmp66) = 10;
2473#line 179
2474      __cil_tmp67 = (unsigned long )s;
2475#line 179
2476      __cil_tmp68 = __cil_tmp67 + 16;
2477#line 179
2478      *((int *)__cil_tmp68) = 196608;
2479#line 180
2480      __cil_tmp69 = (unsigned long )s;
2481#line 180
2482      __cil_tmp70 = __cil_tmp69 + 12;
2483#line 180
2484      *((int *)__cil_tmp70) = 4;
2485#line 181
2486      __cil_tmp71 = (unsigned long )s;
2487#line 181
2488      __cil_tmp72 = __cil_tmp71 + 140;
2489#line 181
2490      *((unsigned int *)__cil_tmp72) = 65535U;
2491#line 182
2492      __cil_tmp73 = (unsigned long )s;
2493#line 182
2494      __cil_tmp74 = __cil_tmp73 + 20;
2495#line 182
2496      *((int *)__cil_tmp74) = 4;
2497#line 184
2498      __cil_tmp75 = (unsigned long )s;
2499#line 184
2500      __cil_tmp76 = __cil_tmp75 + 200;
2501#line 184
2502      *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
2503                  unsigned int * ))__cil_tmp76) = & adl_pci8164_insn_read_msts;
2504#line 185
2505      __cil_tmp77 = (unsigned long )s;
2506#line 185
2507      __cil_tmp78 = __cil_tmp77 + 208;
2508#line 185
2509      *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
2510                  unsigned int * ))__cil_tmp78) = & adl_pci8164_insn_write_cmd;
2511#line 187
2512      __cil_tmp79 = (unsigned long )dev;
2513#line 187
2514      __cil_tmp80 = __cil_tmp79 + 320;
2515#line 187
2516      __cil_tmp81 = *((struct comedi_subdevice **)__cil_tmp80);
2517#line 187
2518      s = __cil_tmp81 + 1UL;
2519#line 188
2520      __cil_tmp82 = (unsigned long )s;
2521#line 188
2522      __cil_tmp83 = __cil_tmp82 + 8;
2523#line 188
2524      *((int *)__cil_tmp83) = 10;
2525#line 189
2526      __cil_tmp84 = (unsigned long )s;
2527#line 189
2528      __cil_tmp85 = __cil_tmp84 + 16;
2529#line 189
2530      *((int *)__cil_tmp85) = 196608;
2531#line 190
2532      __cil_tmp86 = (unsigned long )s;
2533#line 190
2534      __cil_tmp87 = __cil_tmp86 + 12;
2535#line 190
2536      *((int *)__cil_tmp87) = 4;
2537#line 191
2538      __cil_tmp88 = (unsigned long )s;
2539#line 191
2540      __cil_tmp89 = __cil_tmp88 + 140;
2541#line 191
2542      *((unsigned int *)__cil_tmp89) = 65535U;
2543#line 192
2544      __cil_tmp90 = (unsigned long )s;
2545#line 192
2546      __cil_tmp91 = __cil_tmp90 + 20;
2547#line 192
2548      *((int *)__cil_tmp91) = 4;
2549#line 194
2550      __cil_tmp92 = (unsigned long )s;
2551#line 194
2552      __cil_tmp93 = __cil_tmp92 + 200;
2553#line 194
2554      *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
2555                  unsigned int * ))__cil_tmp93) = & adl_pci8164_insn_read_ssts;
2556#line 195
2557      __cil_tmp94 = (unsigned long )s;
2558#line 195
2559      __cil_tmp95 = __cil_tmp94 + 208;
2560#line 195
2561      *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
2562                  unsigned int * ))__cil_tmp95) = & adl_pci8164_insn_write_otp;
2563#line 197
2564      __cil_tmp96 = (unsigned long )dev;
2565#line 197
2566      __cil_tmp97 = __cil_tmp96 + 320;
2567#line 197
2568      __cil_tmp98 = *((struct comedi_subdevice **)__cil_tmp97);
2569#line 197
2570      s = __cil_tmp98 + 2UL;
2571#line 198
2572      __cil_tmp99 = (unsigned long )s;
2573#line 198
2574      __cil_tmp100 = __cil_tmp99 + 8;
2575#line 198
2576      *((int *)__cil_tmp100) = 10;
2577#line 199
2578      __cil_tmp101 = (unsigned long )s;
2579#line 199
2580      __cil_tmp102 = __cil_tmp101 + 16;
2581#line 199
2582      *((int *)__cil_tmp102) = 196608;
2583#line 200
2584      __cil_tmp103 = (unsigned long )s;
2585#line 200
2586      __cil_tmp104 = __cil_tmp103 + 12;
2587#line 200
2588      *((int *)__cil_tmp104) = 4;
2589#line 201
2590      __cil_tmp105 = (unsigned long )s;
2591#line 201
2592      __cil_tmp106 = __cil_tmp105 + 140;
2593#line 201
2594      *((unsigned int *)__cil_tmp106) = 65535U;
2595#line 202
2596      __cil_tmp107 = (unsigned long )s;
2597#line 202
2598      __cil_tmp108 = __cil_tmp107 + 20;
2599#line 202
2600      *((int *)__cil_tmp108) = 4;
2601#line 204
2602      __cil_tmp109 = (unsigned long )s;
2603#line 204
2604      __cil_tmp110 = __cil_tmp109 + 200;
2605#line 204
2606      *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
2607                  unsigned int * ))__cil_tmp110) = & adl_pci8164_insn_read_buf0;
2608#line 205
2609      __cil_tmp111 = (unsigned long )s;
2610#line 205
2611      __cil_tmp112 = __cil_tmp111 + 208;
2612#line 205
2613      *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
2614                  unsigned int * ))__cil_tmp112) = & adl_pci8164_insn_write_buf0;
2615#line 207
2616      __cil_tmp113 = (unsigned long )dev;
2617#line 207
2618      __cil_tmp114 = __cil_tmp113 + 320;
2619#line 207
2620      __cil_tmp115 = *((struct comedi_subdevice **)__cil_tmp114);
2621#line 207
2622      s = __cil_tmp115 + 3UL;
2623#line 208
2624      __cil_tmp116 = (unsigned long )s;
2625#line 208
2626      __cil_tmp117 = __cil_tmp116 + 8;
2627#line 208
2628      *((int *)__cil_tmp117) = 10;
2629#line 209
2630      __cil_tmp118 = (unsigned long )s;
2631#line 209
2632      __cil_tmp119 = __cil_tmp118 + 16;
2633#line 209
2634      *((int *)__cil_tmp119) = 196608;
2635#line 210
2636      __cil_tmp120 = (unsigned long )s;
2637#line 210
2638      __cil_tmp121 = __cil_tmp120 + 12;
2639#line 210
2640      *((int *)__cil_tmp121) = 4;
2641#line 211
2642      __cil_tmp122 = (unsigned long )s;
2643#line 211
2644      __cil_tmp123 = __cil_tmp122 + 140;
2645#line 211
2646      *((unsigned int *)__cil_tmp123) = 65535U;
2647#line 212
2648      __cil_tmp124 = (unsigned long )s;
2649#line 212
2650      __cil_tmp125 = __cil_tmp124 + 20;
2651#line 212
2652      *((int *)__cil_tmp125) = 4;
2653#line 214
2654      __cil_tmp126 = (unsigned long )s;
2655#line 214
2656      __cil_tmp127 = __cil_tmp126 + 200;
2657#line 214
2658      *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
2659                  unsigned int * ))__cil_tmp127) = & adl_pci8164_insn_read_buf1;
2660#line 215
2661      __cil_tmp128 = (unsigned long )s;
2662#line 215
2663      __cil_tmp129 = __cil_tmp128 + 208;
2664#line 215
2665      *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
2666                  unsigned int * ))__cil_tmp129) = & adl_pci8164_insn_write_buf1;
2667#line 217
2668      printk("<6>comedi: attached\n");
2669      }
2670#line 219
2671      return (1);
2672    } else {
2673
2674    }
2675    }
2676  } else {
2677
2678  }
2679  }
2680  ldv_21011: 
2681  {
2682#line 158
2683  pcidev = pci_get_device(4294967295U, 4294967295U, pcidev);
2684  }
2685  {
2686#line 158
2687  __cil_tmp130 = (struct pci_dev *)0;
2688#line 158
2689  __cil_tmp131 = (unsigned long )__cil_tmp130;
2690#line 158
2691  __cil_tmp132 = (unsigned long )pcidev;
2692#line 158
2693  if (__cil_tmp132 != __cil_tmp131) {
2694#line 159
2695    goto ldv_21012;
2696  } else {
2697#line 161
2698    goto ldv_21013;
2699  }
2700  }
2701  ldv_21013: 
2702  {
2703#line 223
2704  __cil_tmp133 = (unsigned long )dev;
2705#line 223
2706  __cil_tmp134 = __cil_tmp133 + 32;
2707#line 223
2708  __cil_tmp135 = *((int *)__cil_tmp134);
2709#line 223
2710  printk("<3>comedi%d: no supported board found!(req. bus/slot : %d/%d)\n", __cil_tmp135,
2711         bus, slot);
2712  }
2713#line 225
2714  return (-5);
2715}
2716}
2717#line 228 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
2718static int adl_pci8164_detach(struct comedi_device *dev ) 
2719{ unsigned long __cil_tmp2 ;
2720  unsigned long __cil_tmp3 ;
2721  int __cil_tmp4 ;
2722  void *__cil_tmp5 ;
2723  unsigned long __cil_tmp6 ;
2724  unsigned long __cil_tmp7 ;
2725  unsigned long __cil_tmp8 ;
2726  void *__cil_tmp9 ;
2727  unsigned long __cil_tmp10 ;
2728  struct pci_dev *__cil_tmp11 ;
2729  unsigned long __cil_tmp12 ;
2730  unsigned long __cil_tmp13 ;
2731  unsigned long __cil_tmp14 ;
2732  void *__cil_tmp15 ;
2733  struct adl_pci8164_private *__cil_tmp16 ;
2734  unsigned long __cil_tmp17 ;
2735  unsigned long __cil_tmp18 ;
2736  struct pci_dev *__cil_tmp19 ;
2737  unsigned long __cil_tmp20 ;
2738  unsigned long __cil_tmp21 ;
2739  unsigned long __cil_tmp22 ;
2740  unsigned long __cil_tmp23 ;
2741  unsigned long __cil_tmp24 ;
2742  unsigned long __cil_tmp25 ;
2743  void *__cil_tmp26 ;
2744  struct adl_pci8164_private *__cil_tmp27 ;
2745  unsigned long __cil_tmp28 ;
2746  unsigned long __cil_tmp29 ;
2747  struct pci_dev *__cil_tmp30 ;
2748  unsigned long __cil_tmp31 ;
2749  unsigned long __cil_tmp32 ;
2750  void *__cil_tmp33 ;
2751  struct adl_pci8164_private *__cil_tmp34 ;
2752  unsigned long __cil_tmp35 ;
2753  unsigned long __cil_tmp36 ;
2754  struct pci_dev *__cil_tmp37 ;
2755
2756  {
2757  {
2758#line 230
2759  __cil_tmp2 = (unsigned long )dev;
2760#line 230
2761  __cil_tmp3 = __cil_tmp2 + 32;
2762#line 230
2763  __cil_tmp4 = *((int *)__cil_tmp3);
2764#line 230
2765  printk("<6>comedi%d: pci8164: remove\n", __cil_tmp4);
2766  }
2767  {
2768#line 232
2769  __cil_tmp5 = (void *)0;
2770#line 232
2771  __cil_tmp6 = (unsigned long )__cil_tmp5;
2772#line 232
2773  __cil_tmp7 = (unsigned long )dev;
2774#line 232
2775  __cil_tmp8 = __cil_tmp7 + 16;
2776#line 232
2777  __cil_tmp9 = *((void **)__cil_tmp8);
2778#line 232
2779  __cil_tmp10 = (unsigned long )__cil_tmp9;
2780#line 232
2781  if (__cil_tmp10 != __cil_tmp6) {
2782    {
2783#line 232
2784    __cil_tmp11 = (struct pci_dev *)0;
2785#line 232
2786    __cil_tmp12 = (unsigned long )__cil_tmp11;
2787#line 232
2788    __cil_tmp13 = (unsigned long )dev;
2789#line 232
2790    __cil_tmp14 = __cil_tmp13 + 16;
2791#line 232
2792    __cil_tmp15 = *((void **)__cil_tmp14);
2793#line 232
2794    __cil_tmp16 = (struct adl_pci8164_private *)__cil_tmp15;
2795#line 232
2796    __cil_tmp17 = (unsigned long )__cil_tmp16;
2797#line 232
2798    __cil_tmp18 = __cil_tmp17 + 8;
2799#line 232
2800    __cil_tmp19 = *((struct pci_dev **)__cil_tmp18);
2801#line 232
2802    __cil_tmp20 = (unsigned long )__cil_tmp19;
2803#line 232
2804    if (__cil_tmp20 != __cil_tmp12) {
2805      {
2806#line 233
2807      __cil_tmp21 = (unsigned long )dev;
2808#line 233
2809      __cil_tmp22 = __cil_tmp21 + 328;
2810#line 233
2811      __cil_tmp23 = *((unsigned long *)__cil_tmp22);
2812#line 233
2813      if (__cil_tmp23 != 0UL) {
2814        {
2815#line 234
2816        __cil_tmp24 = (unsigned long )dev;
2817#line 234
2818        __cil_tmp25 = __cil_tmp24 + 16;
2819#line 234
2820        __cil_tmp26 = *((void **)__cil_tmp25);
2821#line 234
2822        __cil_tmp27 = (struct adl_pci8164_private *)__cil_tmp26;
2823#line 234
2824        __cil_tmp28 = (unsigned long )__cil_tmp27;
2825#line 234
2826        __cil_tmp29 = __cil_tmp28 + 8;
2827#line 234
2828        __cil_tmp30 = *((struct pci_dev **)__cil_tmp29);
2829#line 234
2830        comedi_pci_disable(__cil_tmp30);
2831        }
2832      } else {
2833
2834      }
2835      }
2836      {
2837#line 235
2838      __cil_tmp31 = (unsigned long )dev;
2839#line 235
2840      __cil_tmp32 = __cil_tmp31 + 16;
2841#line 235
2842      __cil_tmp33 = *((void **)__cil_tmp32);
2843#line 235
2844      __cil_tmp34 = (struct adl_pci8164_private *)__cil_tmp33;
2845#line 235
2846      __cil_tmp35 = (unsigned long )__cil_tmp34;
2847#line 235
2848      __cil_tmp36 = __cil_tmp35 + 8;
2849#line 235
2850      __cil_tmp37 = *((struct pci_dev **)__cil_tmp36);
2851#line 235
2852      pci_dev_put(__cil_tmp37);
2853      }
2854    } else {
2855
2856    }
2857    }
2858  } else {
2859
2860  }
2861  }
2862#line 238
2863  return (0);
2864}
2865}
2866#line 245 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
2867static void adl_pci8164_insn_read(struct comedi_device *dev , struct comedi_subdevice *s ,
2868                                  struct comedi_insn *insn , unsigned int *data ,
2869                                  char *action , unsigned short offset ) 
2870{ int axis ;
2871  int axis_reg ;
2872  char *axisname ;
2873  unsigned short tmp ;
2874  unsigned long __cil_tmp11 ;
2875  unsigned long __cil_tmp12 ;
2876  unsigned int __cil_tmp13 ;
2877  int __cil_tmp14 ;
2878  unsigned int __cil_tmp15 ;
2879  unsigned int __cil_tmp16 ;
2880  unsigned long __cil_tmp17 ;
2881  unsigned long __cil_tmp18 ;
2882  unsigned long __cil_tmp19 ;
2883  unsigned int __cil_tmp20 ;
2884  unsigned int __cil_tmp21 ;
2885  unsigned int __cil_tmp22 ;
2886  int __cil_tmp23 ;
2887  unsigned int __cil_tmp24 ;
2888  unsigned int *__cil_tmp25 ;
2889  unsigned int __cil_tmp26 ;
2890
2891  {
2892#line 254
2893  __cil_tmp11 = (unsigned long )insn;
2894#line 254
2895  __cil_tmp12 = __cil_tmp11 + 20;
2896#line 254
2897  __cil_tmp13 = *((unsigned int *)__cil_tmp12);
2898#line 254
2899  __cil_tmp14 = (int )__cil_tmp13;
2900#line 254
2901  axis = __cil_tmp14 & 65535;
2902#line 257
2903  if (axis == 0) {
2904#line 257
2905    goto case_0;
2906  } else
2907#line 261
2908  if (axis == 1) {
2909#line 261
2910    goto case_1;
2911  } else
2912#line 265
2913  if (axis == 2) {
2914#line 265
2915    goto case_2;
2916  } else
2917#line 269
2918  if (axis == 3) {
2919#line 269
2920    goto case_3;
2921  } else {
2922    {
2923#line 273
2924    goto switch_default;
2925#line 256
2926    if (0) {
2927      case_0: /* CIL Label */ 
2928#line 258
2929      axis_reg = 0;
2930#line 259
2931      axisname = (char *)"X";
2932#line 260
2933      goto ldv_21029;
2934      case_1: /* CIL Label */ 
2935#line 262
2936      axis_reg = 8;
2937#line 263
2938      axisname = (char *)"Y";
2939#line 264
2940      goto ldv_21029;
2941      case_2: /* CIL Label */ 
2942#line 266
2943      axis_reg = 16;
2944#line 267
2945      axisname = (char *)"Z";
2946#line 268
2947      goto ldv_21029;
2948      case_3: /* CIL Label */ 
2949#line 270
2950      axis_reg = 24;
2951#line 271
2952      axisname = (char *)"U";
2953#line 272
2954      goto ldv_21029;
2955      switch_default: /* CIL Label */ 
2956#line 274
2957      axis_reg = 0;
2958#line 275
2959      axisname = (char *)"X";
2960    } else {
2961      switch_break: /* CIL Label */ ;
2962    }
2963    }
2964  }
2965  ldv_21029: 
2966  {
2967#line 278
2968  __cil_tmp15 = (unsigned int )offset;
2969#line 278
2970  __cil_tmp16 = (unsigned int )axis_reg;
2971#line 278
2972  __cil_tmp17 = (unsigned long )dev;
2973#line 278
2974  __cil_tmp18 = __cil_tmp17 + 328;
2975#line 278
2976  __cil_tmp19 = *((unsigned long *)__cil_tmp18);
2977#line 278
2978  __cil_tmp20 = (unsigned int )__cil_tmp19;
2979#line 278
2980  __cil_tmp21 = __cil_tmp20 + __cil_tmp16;
2981#line 278
2982  __cil_tmp22 = __cil_tmp21 + __cil_tmp15;
2983#line 278
2984  __cil_tmp23 = (int )__cil_tmp22;
2985#line 278
2986  tmp = inw(__cil_tmp23);
2987#line 278
2988  *data = (unsigned int )tmp;
2989#line 279
2990  __cil_tmp24 = *data;
2991#line 279
2992  __cil_tmp25 = data + 1UL;
2993#line 279
2994  __cil_tmp26 = *__cil_tmp25;
2995#line 279
2996  printk("<7>comedi: pci8164 %s read -> %04X:%04X on axis %s\n", action, __cil_tmp24,
2997         __cil_tmp26, axisname);
2998  }
2999#line 282
3000  return;
3001}
3002}
3003#line 284 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3004static int adl_pci8164_insn_read_msts(struct comedi_device *dev , struct comedi_subdevice *s ,
3005                                      struct comedi_insn *insn , unsigned int *data ) 
3006{ char *__cil_tmp5 ;
3007
3008  {
3009  {
3010#line 289
3011  __cil_tmp5 = (char *)"MSTS";
3012#line 289
3013  adl_pci8164_insn_read(dev, s, insn, data, __cil_tmp5, (unsigned short)0);
3014  }
3015#line 290
3016  return (2);
3017}
3018}
3019#line 293 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3020static int adl_pci8164_insn_read_ssts(struct comedi_device *dev , struct comedi_subdevice *s ,
3021                                      struct comedi_insn *insn , unsigned int *data ) 
3022{ char *__cil_tmp5 ;
3023
3024  {
3025  {
3026#line 298
3027  __cil_tmp5 = (char *)"SSTS";
3028#line 298
3029  adl_pci8164_insn_read(dev, s, insn, data, __cil_tmp5, (unsigned short)2);
3030  }
3031#line 299
3032  return (2);
3033}
3034}
3035#line 302 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3036static int adl_pci8164_insn_read_buf0(struct comedi_device *dev , struct comedi_subdevice *s ,
3037                                      struct comedi_insn *insn , unsigned int *data ) 
3038{ char *__cil_tmp5 ;
3039
3040  {
3041  {
3042#line 307
3043  __cil_tmp5 = (char *)"BUF0";
3044#line 307
3045  adl_pci8164_insn_read(dev, s, insn, data, __cil_tmp5, (unsigned short)4);
3046  }
3047#line 308
3048  return (2);
3049}
3050}
3051#line 311 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3052static int adl_pci8164_insn_read_buf1(struct comedi_device *dev , struct comedi_subdevice *s ,
3053                                      struct comedi_insn *insn , unsigned int *data ) 
3054{ char *__cil_tmp5 ;
3055
3056  {
3057  {
3058#line 316
3059  __cil_tmp5 = (char *)"BUF1";
3060#line 316
3061  adl_pci8164_insn_read(dev, s, insn, data, __cil_tmp5, (unsigned short)6);
3062  }
3063#line 317
3064  return (2);
3065}
3066}
3067#line 324 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3068static void adl_pci8164_insn_out(struct comedi_device *dev , struct comedi_subdevice *s ,
3069                                 struct comedi_insn *insn , unsigned int *data , char *action ,
3070                                 unsigned short offset ) 
3071{ unsigned int axis ;
3072  unsigned int axis_reg ;
3073  char *axisname ;
3074  unsigned long __cil_tmp10 ;
3075  unsigned long __cil_tmp11 ;
3076  unsigned int __cil_tmp12 ;
3077  unsigned int __cil_tmp13 ;
3078  unsigned short __cil_tmp14 ;
3079  int __cil_tmp15 ;
3080  unsigned short __cil_tmp16 ;
3081  unsigned int __cil_tmp17 ;
3082  unsigned long __cil_tmp18 ;
3083  unsigned long __cil_tmp19 ;
3084  unsigned long __cil_tmp20 ;
3085  unsigned int __cil_tmp21 ;
3086  unsigned int __cil_tmp22 ;
3087  unsigned int __cil_tmp23 ;
3088  int __cil_tmp24 ;
3089  unsigned int __cil_tmp25 ;
3090  unsigned int *__cil_tmp26 ;
3091  unsigned int __cil_tmp27 ;
3092
3093  {
3094#line 334
3095  __cil_tmp10 = (unsigned long )insn;
3096#line 334
3097  __cil_tmp11 = __cil_tmp10 + 20;
3098#line 334
3099  __cil_tmp12 = *((unsigned int *)__cil_tmp11);
3100#line 334
3101  axis = __cil_tmp12 & 65535U;
3102#line 337
3103  if ((int )axis == 0) {
3104#line 337
3105    goto case_0;
3106  } else
3107#line 341
3108  if ((int )axis == 1) {
3109#line 341
3110    goto case_1;
3111  } else
3112#line 345
3113  if ((int )axis == 2) {
3114#line 345
3115    goto case_2;
3116  } else
3117#line 349
3118  if ((int )axis == 3) {
3119#line 349
3120    goto case_3;
3121  } else {
3122    {
3123#line 353
3124    goto switch_default;
3125#line 336
3126    if (0) {
3127      case_0: /* CIL Label */ 
3128#line 338
3129      axis_reg = 0U;
3130#line 339
3131      axisname = (char *)"X";
3132#line 340
3133      goto ldv_21070;
3134      case_1: /* CIL Label */ 
3135#line 342
3136      axis_reg = 8U;
3137#line 343
3138      axisname = (char *)"Y";
3139#line 344
3140      goto ldv_21070;
3141      case_2: /* CIL Label */ 
3142#line 346
3143      axis_reg = 16U;
3144#line 347
3145      axisname = (char *)"Z";
3146#line 348
3147      goto ldv_21070;
3148      case_3: /* CIL Label */ 
3149#line 350
3150      axis_reg = 24U;
3151#line 351
3152      axisname = (char *)"U";
3153#line 352
3154      goto ldv_21070;
3155      switch_default: /* CIL Label */ 
3156#line 354
3157      axis_reg = 0U;
3158#line 355
3159      axisname = (char *)"X";
3160    } else {
3161      switch_break: /* CIL Label */ ;
3162    }
3163    }
3164  }
3165  ldv_21070: 
3166  {
3167#line 358
3168  __cil_tmp13 = *data;
3169#line 358
3170  __cil_tmp14 = (unsigned short )__cil_tmp13;
3171#line 358
3172  __cil_tmp15 = (int )__cil_tmp14;
3173#line 358
3174  __cil_tmp16 = (unsigned short )__cil_tmp15;
3175#line 358
3176  __cil_tmp17 = (unsigned int )offset;
3177#line 358
3178  __cil_tmp18 = (unsigned long )dev;
3179#line 358
3180  __cil_tmp19 = __cil_tmp18 + 328;
3181#line 358
3182  __cil_tmp20 = *((unsigned long *)__cil_tmp19);
3183#line 358
3184  __cil_tmp21 = (unsigned int )__cil_tmp20;
3185#line 358
3186  __cil_tmp22 = __cil_tmp21 + axis_reg;
3187#line 358
3188  __cil_tmp23 = __cil_tmp22 + __cil_tmp17;
3189#line 358
3190  __cil_tmp24 = (int )__cil_tmp23;
3191#line 358
3192  outw(__cil_tmp16, __cil_tmp24);
3193#line 360
3194  __cil_tmp25 = *data;
3195#line 360
3196  __cil_tmp26 = data + 1UL;
3197#line 360
3198  __cil_tmp27 = *__cil_tmp26;
3199#line 360
3200  printk("<7>comedi: pci8164 %s write -> %04X:%04X on axis %s\n", action, __cil_tmp25,
3201         __cil_tmp27, axisname);
3202  }
3203#line 363
3204  return;
3205}
3206}
3207#line 366 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3208static int adl_pci8164_insn_write_cmd(struct comedi_device *dev , struct comedi_subdevice *s ,
3209                                      struct comedi_insn *insn , unsigned int *data ) 
3210{ char *__cil_tmp5 ;
3211
3212  {
3213  {
3214#line 371
3215  __cil_tmp5 = (char *)"CMD";
3216#line 371
3217  adl_pci8164_insn_out(dev, s, insn, data, __cil_tmp5, (unsigned short)0);
3218  }
3219#line 372
3220  return (2);
3221}
3222}
3223#line 375 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3224static int adl_pci8164_insn_write_otp(struct comedi_device *dev , struct comedi_subdevice *s ,
3225                                      struct comedi_insn *insn , unsigned int *data ) 
3226{ char *__cil_tmp5 ;
3227
3228  {
3229  {
3230#line 380
3231  __cil_tmp5 = (char *)"OTP";
3232#line 380
3233  adl_pci8164_insn_out(dev, s, insn, data, __cil_tmp5, (unsigned short)2);
3234  }
3235#line 381
3236  return (2);
3237}
3238}
3239#line 384 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3240static int adl_pci8164_insn_write_buf0(struct comedi_device *dev , struct comedi_subdevice *s ,
3241                                       struct comedi_insn *insn , unsigned int *data ) 
3242{ char *__cil_tmp5 ;
3243
3244  {
3245  {
3246#line 389
3247  __cil_tmp5 = (char *)"BUF0";
3248#line 389
3249  adl_pci8164_insn_out(dev, s, insn, data, __cil_tmp5, (unsigned short)4);
3250  }
3251#line 390
3252  return (2);
3253}
3254}
3255#line 393 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3256static int adl_pci8164_insn_write_buf1(struct comedi_device *dev , struct comedi_subdevice *s ,
3257                                       struct comedi_insn *insn , unsigned int *data ) 
3258{ char *__cil_tmp5 ;
3259
3260  {
3261  {
3262#line 398
3263  __cil_tmp5 = (char *)"BUF1";
3264#line 398
3265  adl_pci8164_insn_out(dev, s, insn, data, __cil_tmp5, (unsigned short)6);
3266  }
3267#line 399
3268  return (2);
3269}
3270}
3271#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3272static int driver_adl_pci8164_pci_probe(struct pci_dev *dev , struct pci_device_id  const  *ent ) 
3273{ int tmp ;
3274  unsigned long __cil_tmp4 ;
3275  char const   *__cil_tmp5 ;
3276
3277  {
3278  {
3279#line 406
3280  __cil_tmp4 = (unsigned long )(& driver_adl_pci8164) + 8;
3281#line 406
3282  __cil_tmp5 = *((char const   **)__cil_tmp4);
3283#line 406
3284  tmp = comedi_pci_auto_config(dev, __cil_tmp5);
3285  }
3286#line 406
3287  return (tmp);
3288}
3289}
3290#line 409 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3291static void driver_adl_pci8164_pci_remove(struct pci_dev *dev ) 
3292{ 
3293
3294  {
3295  {
3296#line 411
3297  comedi_pci_auto_unconfig(dev);
3298  }
3299#line 412
3300  return;
3301}
3302}
3303#line 414 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3304static struct pci_driver driver_adl_pci8164_pci_driver  = 
3305#line 414
3306     {{(struct list_head *)0, (struct list_head *)0}, (char const   *)0, (struct pci_device_id  const  *)(& adl_pci8164_pci_table),
3307    & driver_adl_pci8164_pci_probe, & driver_adl_pci8164_pci_remove, (int (*)(struct pci_dev * ,
3308                                                                              pm_message_t  ))0,
3309    (int (*)(struct pci_dev * , pm_message_t  ))0, (int (*)(struct pci_dev * ))0,
3310    (int (*)(struct pci_dev * ))0, (void (*)(struct pci_dev * ))0, (struct pci_error_handlers *)0,
3311    {(char const   *)0, (struct bus_type *)0, (struct module *)0, (char const   *)0,
3312     (_Bool)0, (struct of_device_id  const  *)0, (int (*)(struct device * ))0, (int (*)(struct device * ))0,
3313     (void (*)(struct device * ))0, (int (*)(struct device * , pm_message_t  ))0,
3314     (int (*)(struct device * ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
3315     (struct driver_private *)0}, {{{{{{0U}}, 0U, 0U, (void *)0, {(struct lock_class_key *)0,
3316                                                                  {(struct lock_class *)0,
3317                                                                   (struct lock_class *)0},
3318                                                                  (char const   *)0,
3319                                                                  0, 0UL}}}}, {(struct list_head *)0,
3320                                                                               (struct list_head *)0}}};
3321#line 420 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3322static int driver_adl_pci8164_init_module(void) 
3323{ int retval ;
3324  int tmp ;
3325  unsigned long __cil_tmp3 ;
3326  unsigned long __cil_tmp4 ;
3327
3328  {
3329  {
3330#line 424
3331  retval = comedi_driver_register(& driver_adl_pci8164);
3332  }
3333#line 425
3334  if (retval < 0) {
3335#line 426
3336    return (retval);
3337  } else {
3338
3339  }
3340  {
3341#line 428
3342  __cil_tmp3 = (unsigned long )(& driver_adl_pci8164_pci_driver) + 16;
3343#line 428
3344  __cil_tmp4 = (unsigned long )(& driver_adl_pci8164) + 8;
3345#line 428
3346  *((char const   **)__cil_tmp3) = *((char const   **)__cil_tmp4);
3347#line 430
3348  tmp = __pci_register_driver(& driver_adl_pci8164_pci_driver, & __this_module, "adl_pci8164");
3349  }
3350#line 430
3351  return (tmp);
3352}
3353}
3354#line 433 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3355static void driver_adl_pci8164_cleanup_module(void) 
3356{ 
3357
3358  {
3359  {
3360#line 435
3361  pci_unregister_driver(& driver_adl_pci8164_pci_driver);
3362#line 436
3363  comedi_driver_unregister(& driver_adl_pci8164);
3364  }
3365#line 437
3366  return;
3367}
3368}
3369#line 462
3370extern void ldv_check_final_state(void) ;
3371#line 468
3372extern void ldv_initialize(void) ;
3373#line 471
3374extern int __VERIFIER_nondet_int(void) ;
3375#line 474 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3376int LDV_IN_INTERRUPT  ;
3377#line 477 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3378void main(void) 
3379{ struct comedi_device *var_group1 ;
3380  struct comedi_devconfig *var_group2 ;
3381  int tmp ;
3382  int tmp___0 ;
3383  int tmp___1 ;
3384
3385  {
3386  {
3387#line 525
3388  LDV_IN_INTERRUPT = 1;
3389#line 534
3390  ldv_initialize();
3391#line 553
3392  tmp = driver_adl_pci8164_init_module();
3393  }
3394#line 553
3395  if (tmp != 0) {
3396#line 554
3397    goto ldv_final;
3398  } else {
3399
3400  }
3401#line 558
3402  goto ldv_21147;
3403  ldv_21146: 
3404  {
3405#line 561
3406  tmp___0 = __VERIFIER_nondet_int();
3407  }
3408#line 563
3409  if (tmp___0 == 0) {
3410#line 563
3411    goto case_0;
3412  } else
3413#line 592
3414  if (tmp___0 == 1) {
3415#line 592
3416    goto case_1;
3417  } else {
3418    {
3419#line 621
3420    goto switch_default;
3421#line 561
3422    if (0) {
3423      case_0: /* CIL Label */ 
3424      {
3425#line 584
3426      adl_pci8164_attach(var_group1, var_group2);
3427      }
3428#line 591
3429      goto ldv_21143;
3430      case_1: /* CIL Label */ 
3431      {
3432#line 613
3433      adl_pci8164_detach(var_group1);
3434      }
3435#line 620
3436      goto ldv_21143;
3437      switch_default: /* CIL Label */ ;
3438#line 621
3439      goto ldv_21143;
3440    } else {
3441      switch_break: /* CIL Label */ ;
3442    }
3443    }
3444  }
3445  ldv_21143: ;
3446  ldv_21147: 
3447  {
3448#line 558
3449  tmp___1 = __VERIFIER_nondet_int();
3450  }
3451#line 558
3452  if (tmp___1 != 0) {
3453#line 559
3454    goto ldv_21146;
3455  } else {
3456#line 561
3457    goto ldv_21148;
3458  }
3459  ldv_21148: ;
3460  {
3461#line 646
3462  driver_adl_pci8164_cleanup_module();
3463  }
3464  ldv_final: 
3465  {
3466#line 649
3467  ldv_check_final_state();
3468  }
3469#line 652
3470  return;
3471}
3472}
3473#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3474void ldv_blast_assert(void) 
3475{ 
3476
3477  {
3478  ERROR: ;
3479#line 6
3480  goto ERROR;
3481}
3482}
3483#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3484extern int __VERIFIER_nondet_int(void) ;
3485#line 673 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3486int ldv_spin  =    0;
3487#line 677 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3488void ldv_check_alloc_flags(gfp_t flags ) 
3489{ 
3490
3491  {
3492#line 680
3493  if (ldv_spin != 0) {
3494#line 680
3495    if (flags != 32U) {
3496      {
3497#line 680
3498      ldv_blast_assert();
3499      }
3500    } else {
3501
3502    }
3503  } else {
3504
3505  }
3506#line 683
3507  return;
3508}
3509}
3510#line 683
3511extern struct page *ldv_some_page(void) ;
3512#line 686 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3513struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
3514{ struct page *tmp ;
3515
3516  {
3517#line 689
3518  if (ldv_spin != 0) {
3519#line 689
3520    if (flags != 32U) {
3521      {
3522#line 689
3523      ldv_blast_assert();
3524      }
3525    } else {
3526
3527    }
3528  } else {
3529
3530  }
3531  {
3532#line 691
3533  tmp = ldv_some_page();
3534  }
3535#line 691
3536  return (tmp);
3537}
3538}
3539#line 695 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3540void ldv_check_alloc_nonatomic(void) 
3541{ 
3542
3543  {
3544#line 698
3545  if (ldv_spin != 0) {
3546    {
3547#line 698
3548    ldv_blast_assert();
3549    }
3550  } else {
3551
3552  }
3553#line 701
3554  return;
3555}
3556}
3557#line 702 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3558void ldv_spin_lock(void) 
3559{ 
3560
3561  {
3562#line 705
3563  ldv_spin = 1;
3564#line 706
3565  return;
3566}
3567}
3568#line 709 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3569void ldv_spin_unlock(void) 
3570{ 
3571
3572  {
3573#line 712
3574  ldv_spin = 0;
3575#line 713
3576  return;
3577}
3578}
3579#line 716 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3580int ldv_spin_trylock(void) 
3581{ int is_lock ;
3582
3583  {
3584  {
3585#line 721
3586  is_lock = __VERIFIER_nondet_int();
3587  }
3588#line 723
3589  if (is_lock != 0) {
3590#line 726
3591    return (0);
3592  } else {
3593#line 731
3594    ldv_spin = 1;
3595#line 733
3596    return (1);
3597  }
3598}
3599}
3600#line 878 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3601__inline static void *kcalloc(size_t n , size_t size , gfp_t flags ) 
3602{ 
3603
3604  {
3605  {
3606#line 885
3607  ldv_check_alloc_flags(flags);
3608#line 887
3609  ldv_kcalloc_14(n, size, flags);
3610  }
3611#line 888
3612  return ((void *)0);
3613}
3614}
3615#line 900 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3616void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
3617{ 
3618
3619  {
3620  {
3621#line 906
3622  ldv_check_alloc_flags(ldv_func_arg2);
3623#line 908
3624  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
3625  }
3626#line 909
3627  return ((void *)0);
3628}
3629}
3630#line 911 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5900/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci8164.c.p"
3631__inline static void *kzalloc(size_t size , gfp_t flags ) 
3632{ void *tmp ;
3633
3634  {
3635  {
3636#line 917
3637  ldv_check_alloc_flags(flags);
3638#line 918
3639  tmp = __VERIFIER_nondet_pointer();
3640  }
3641#line 918
3642  return (tmp);
3643}
3644}