Showing error 636

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