Showing error 1229

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


Source:

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