Showing error 637

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--8255.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 4207
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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