Showing error 632

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