Showing error 1227

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--comedi_parport.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 4122
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 464
1440enum irqreturn {
1441    IRQ_NONE = 0,
1442    IRQ_HANDLED = 1,
1443    IRQ_WAKE_THREAD = 2
1444} ;
1445#line 16 "include/linux/irqreturn.h"
1446typedef enum irqreturn irqreturn_t;
1447#line 131 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
1448struct parport_private {
1449   unsigned int a_data ;
1450   unsigned int c_data ;
1451   int enable_irq ;
1452};
1453#line 2
1454void ldv_spin_lock(void) ;
1455#line 3
1456void ldv_spin_unlock(void) ;
1457#line 4
1458int ldv_spin_trylock(void) ;
1459#line 101 "include/linux/printk.h"
1460extern int printk(char const   *  , ...) ;
1461#line 93 "include/linux/spinlock.h"
1462extern void __raw_spin_lock_init(raw_spinlock_t * , char const   * , struct lock_class_key * ) ;
1463#line 272 "include/linux/spinlock.h"
1464__inline static raw_spinlock_t *spinlock_check(spinlock_t *lock ) 
1465{ 
1466
1467  {
1468#line 274
1469  return ((struct raw_spinlock *)lock);
1470}
1471}
1472#line 137 "include/linux/ioport.h"
1473extern struct resource ioport_resource ;
1474#line 181
1475extern struct resource *__request_region(struct resource * , resource_size_t  , resource_size_t  ,
1476                                         char const   * , int  ) ;
1477#line 192
1478extern void __release_region(struct resource * , resource_size_t  , resource_size_t  ) ;
1479#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1480__inline static void outb(unsigned char value , int port ) 
1481{ 
1482
1483  {
1484#line 308
1485  __asm__  volatile   ("outb %b0, %w1": : "a" (value), "Nd" (port));
1486#line 309
1487  return;
1488}
1489}
1490#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1491__inline static unsigned char inb(int port ) 
1492{ unsigned char value ;
1493
1494  {
1495#line 308
1496  __asm__  volatile   ("inb %w1, %b0": "=a" (value): "Nd" (port));
1497#line 308
1498  return (value);
1499}
1500}
1501#line 26 "include/linux/export.h"
1502extern struct module __this_module ;
1503#line 220 "include/linux/slub_def.h"
1504extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1505#line 223
1506void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1507#line 225
1508extern void *__kmalloc(size_t  , gfp_t  ) ;
1509#line 243 "include/linux/slab.h"
1510__inline static void *kmalloc_array(size_t n , size_t size , gfp_t flags ) 
1511{ void *tmp ;
1512  unsigned long __cil_tmp5 ;
1513  size_t __cil_tmp6 ;
1514
1515  {
1516#line 245
1517  if (size != 0UL) {
1518    {
1519#line 245
1520    __cil_tmp5 = 0xffffffffffffffffUL / size;
1521#line 245
1522    if (__cil_tmp5 < n) {
1523#line 246
1524      return ((void *)0);
1525    } else {
1526
1527    }
1528    }
1529  } else {
1530
1531  }
1532  {
1533#line 247
1534  __cil_tmp6 = n * size;
1535#line 247
1536  tmp = __kmalloc(__cil_tmp6, flags);
1537  }
1538#line 247
1539  return (tmp);
1540}
1541}
1542#line 256 "include/linux/slab.h"
1543__inline static void *ldv_kcalloc_14(size_t n , size_t size , gfp_t flags ) 
1544{ void *tmp ;
1545  unsigned int __cil_tmp5 ;
1546
1547  {
1548  {
1549#line 258
1550  __cil_tmp5 = flags | 32768U;
1551#line 258
1552  tmp = kmalloc_array(n, size, __cil_tmp5);
1553  }
1554#line 258
1555  return (tmp);
1556}
1557}
1558#line 256
1559__inline static void *kcalloc(size_t n , size_t size , gfp_t flags ) ;
1560#line 353
1561__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1562#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
1563extern void *__VERIFIER_nondet_pointer(void) ;
1564#line 11
1565void ldv_check_alloc_flags(gfp_t flags ) ;
1566#line 12
1567void ldv_check_alloc_nonatomic(void) ;
1568#line 14
1569struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1570#line 249 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1571extern void comedi_event(struct comedi_device * , struct comedi_subdevice * ) ;
1572#line 287
1573extern int comedi_driver_register(struct comedi_driver * ) ;
1574#line 288
1575extern int comedi_driver_unregister(struct comedi_driver * ) ;
1576#line 336
1577extern struct comedi_lrange  const  range_unipolar5 ;
1578#line 354 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1579__inline static int alloc_subdevices(struct comedi_device *dev , unsigned int num_subdevices ) 
1580{ unsigned int i ;
1581  void *tmp ;
1582  struct lock_class_key __key ;
1583  unsigned long __cil_tmp6 ;
1584  unsigned long __cil_tmp7 ;
1585  size_t __cil_tmp8 ;
1586  unsigned long __cil_tmp9 ;
1587  unsigned long __cil_tmp10 ;
1588  struct comedi_subdevice *__cil_tmp11 ;
1589  unsigned long __cil_tmp12 ;
1590  unsigned long __cil_tmp13 ;
1591  unsigned long __cil_tmp14 ;
1592  struct comedi_subdevice *__cil_tmp15 ;
1593  unsigned long __cil_tmp16 ;
1594  unsigned long __cil_tmp17 ;
1595  unsigned long __cil_tmp18 ;
1596  unsigned long __cil_tmp19 ;
1597  struct comedi_subdevice *__cil_tmp20 ;
1598  struct comedi_subdevice *__cil_tmp21 ;
1599  unsigned long __cil_tmp22 ;
1600  unsigned long __cil_tmp23 ;
1601  unsigned long __cil_tmp24 ;
1602  struct comedi_subdevice *__cil_tmp25 ;
1603  struct comedi_subdevice *__cil_tmp26 ;
1604  unsigned long __cil_tmp27 ;
1605  unsigned long __cil_tmp28 ;
1606  unsigned long __cil_tmp29 ;
1607  unsigned long __cil_tmp30 ;
1608  unsigned long __cil_tmp31 ;
1609  struct comedi_subdevice *__cil_tmp32 ;
1610  struct comedi_subdevice *__cil_tmp33 ;
1611  unsigned long __cil_tmp34 ;
1612  unsigned long __cil_tmp35 ;
1613  spinlock_t *__cil_tmp36 ;
1614  unsigned long __cil_tmp37 ;
1615  unsigned long __cil_tmp38 ;
1616  unsigned long __cil_tmp39 ;
1617  struct comedi_subdevice *__cil_tmp40 ;
1618  struct comedi_subdevice *__cil_tmp41 ;
1619  unsigned long __cil_tmp42 ;
1620  unsigned long __cil_tmp43 ;
1621  struct raw_spinlock *__cil_tmp44 ;
1622  unsigned long __cil_tmp45 ;
1623  unsigned long __cil_tmp46 ;
1624  unsigned long __cil_tmp47 ;
1625  struct comedi_subdevice *__cil_tmp48 ;
1626  struct comedi_subdevice *__cil_tmp49 ;
1627  unsigned long __cil_tmp50 ;
1628  unsigned long __cil_tmp51 ;
1629
1630  {
1631  {
1632#line 359
1633  __cil_tmp6 = (unsigned long )dev;
1634#line 359
1635  __cil_tmp7 = __cil_tmp6 + 316;
1636#line 359
1637  *((int *)__cil_tmp7) = (int )num_subdevices;
1638#line 360
1639  __cil_tmp8 = (size_t )num_subdevices;
1640#line 360
1641  tmp = kcalloc(__cil_tmp8, 304UL, 208U);
1642#line 360
1643  __cil_tmp9 = (unsigned long )dev;
1644#line 360
1645  __cil_tmp10 = __cil_tmp9 + 320;
1646#line 360
1647  *((struct comedi_subdevice **)__cil_tmp10) = (struct comedi_subdevice *)tmp;
1648  }
1649  {
1650#line 363
1651  __cil_tmp11 = (struct comedi_subdevice *)0;
1652#line 363
1653  __cil_tmp12 = (unsigned long )__cil_tmp11;
1654#line 363
1655  __cil_tmp13 = (unsigned long )dev;
1656#line 363
1657  __cil_tmp14 = __cil_tmp13 + 320;
1658#line 363
1659  __cil_tmp15 = *((struct comedi_subdevice **)__cil_tmp14);
1660#line 363
1661  __cil_tmp16 = (unsigned long )__cil_tmp15;
1662#line 363
1663  if (__cil_tmp16 == __cil_tmp12) {
1664#line 364
1665    return (-12);
1666  } else {
1667
1668  }
1669  }
1670#line 365
1671  i = 0U;
1672#line 365
1673  goto ldv_19184;
1674  ldv_19183: 
1675  {
1676#line 366
1677  __cil_tmp17 = (unsigned long )i;
1678#line 366
1679  __cil_tmp18 = (unsigned long )dev;
1680#line 366
1681  __cil_tmp19 = __cil_tmp18 + 320;
1682#line 366
1683  __cil_tmp20 = *((struct comedi_subdevice **)__cil_tmp19);
1684#line 366
1685  __cil_tmp21 = __cil_tmp20 + __cil_tmp17;
1686#line 366
1687  *((struct comedi_device **)__cil_tmp21) = dev;
1688#line 367
1689  __cil_tmp22 = (unsigned long )i;
1690#line 367
1691  __cil_tmp23 = (unsigned long )dev;
1692#line 367
1693  __cil_tmp24 = __cil_tmp23 + 320;
1694#line 367
1695  __cil_tmp25 = *((struct comedi_subdevice **)__cil_tmp24);
1696#line 367
1697  __cil_tmp26 = __cil_tmp25 + __cil_tmp22;
1698#line 367
1699  __cil_tmp27 = (unsigned long )__cil_tmp26;
1700#line 367
1701  __cil_tmp28 = __cil_tmp27 + 280;
1702#line 367
1703  *((enum dma_data_direction *)__cil_tmp28) = (enum dma_data_direction )3;
1704#line 368
1705  __cil_tmp29 = (unsigned long )i;
1706#line 368
1707  __cil_tmp30 = (unsigned long )dev;
1708#line 368
1709  __cil_tmp31 = __cil_tmp30 + 320;
1710#line 368
1711  __cil_tmp32 = *((struct comedi_subdevice **)__cil_tmp31);
1712#line 368
1713  __cil_tmp33 = __cil_tmp32 + __cil_tmp29;
1714#line 368
1715  __cil_tmp34 = (unsigned long )__cil_tmp33;
1716#line 368
1717  __cil_tmp35 = __cil_tmp34 + 64;
1718#line 368
1719  __cil_tmp36 = (spinlock_t *)__cil_tmp35;
1720#line 368
1721  spinlock_check(__cil_tmp36);
1722#line 368
1723  __cil_tmp37 = (unsigned long )i;
1724#line 368
1725  __cil_tmp38 = (unsigned long )dev;
1726#line 368
1727  __cil_tmp39 = __cil_tmp38 + 320;
1728#line 368
1729  __cil_tmp40 = *((struct comedi_subdevice **)__cil_tmp39);
1730#line 368
1731  __cil_tmp41 = __cil_tmp40 + __cil_tmp37;
1732#line 368
1733  __cil_tmp42 = (unsigned long )__cil_tmp41;
1734#line 368
1735  __cil_tmp43 = __cil_tmp42 + 64;
1736#line 368
1737  __cil_tmp44 = (struct raw_spinlock *)__cil_tmp43;
1738#line 368
1739  __raw_spin_lock_init(__cil_tmp44, "&(&dev->subdevices[i].spin_lock)->rlock", & __key);
1740#line 369
1741  __cil_tmp45 = (unsigned long )i;
1742#line 369
1743  __cil_tmp46 = (unsigned long )dev;
1744#line 369
1745  __cil_tmp47 = __cil_tmp46 + 320;
1746#line 369
1747  __cil_tmp48 = *((struct comedi_subdevice **)__cil_tmp47);
1748#line 369
1749  __cil_tmp49 = __cil_tmp48 + __cil_tmp45;
1750#line 369
1751  __cil_tmp50 = (unsigned long )__cil_tmp49;
1752#line 369
1753  __cil_tmp51 = __cil_tmp50 + 296;
1754#line 369
1755  *((int *)__cil_tmp51) = -1;
1756#line 365
1757  i = i + 1U;
1758  }
1759  ldv_19184: ;
1760#line 365
1761  if (i < num_subdevices) {
1762#line 366
1763    goto ldv_19183;
1764  } else {
1765#line 368
1766    goto ldv_19185;
1767  }
1768  ldv_19185: ;
1769#line 371
1770  return (0);
1771}
1772}
1773#line 374 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/comedi/drivers/../comedidev.h"
1774__inline static int alloc_private(struct comedi_device *dev , int size ) 
1775{ unsigned long __cil_tmp3 ;
1776  unsigned long __cil_tmp4 ;
1777  size_t __cil_tmp5 ;
1778  void *__cil_tmp6 ;
1779  unsigned long __cil_tmp7 ;
1780  unsigned long __cil_tmp8 ;
1781  unsigned long __cil_tmp9 ;
1782  void *__cil_tmp10 ;
1783  unsigned long __cil_tmp11 ;
1784
1785  {
1786  {
1787#line 376
1788  __cil_tmp3 = (unsigned long )dev;
1789#line 376
1790  __cil_tmp4 = __cil_tmp3 + 16;
1791#line 376
1792  __cil_tmp5 = (size_t )size;
1793#line 376
1794  *((void **)__cil_tmp4) = kzalloc(__cil_tmp5, 208U);
1795  }
1796  {
1797#line 377
1798  __cil_tmp6 = (void *)0;
1799#line 377
1800  __cil_tmp7 = (unsigned long )__cil_tmp6;
1801#line 377
1802  __cil_tmp8 = (unsigned long )dev;
1803#line 377
1804  __cil_tmp9 = __cil_tmp8 + 16;
1805#line 377
1806  __cil_tmp10 = *((void **)__cil_tmp9);
1807#line 377
1808  __cil_tmp11 = (unsigned long )__cil_tmp10;
1809#line 377
1810  if (__cil_tmp11 == __cil_tmp7) {
1811#line 378
1812    return (-12);
1813  } else {
1814
1815  }
1816  }
1817#line 379
1818  return (0);
1819}
1820}
1821#line 405
1822extern int comedi_buf_put(struct comedi_async * , short  ) ;
1823#line 127 "include/linux/interrupt.h"
1824extern int request_threaded_irq(unsigned int  , irqreturn_t (*)(int  , void * ) ,
1825                                irqreturn_t (*)(int  , void * ) , unsigned long  ,
1826                                char const   * , void * ) ;
1827#line 132 "include/linux/interrupt.h"
1828__inline static int request_irq(unsigned int irq , irqreturn_t (*handler)(int  , void * ) ,
1829                                unsigned long flags , char const   *name , void *dev ) 
1830{ int tmp ;
1831  irqreturn_t (*__cil_tmp7)(int  , void * ) ;
1832
1833  {
1834  {
1835#line 135
1836  __cil_tmp7 = (irqreturn_t (*)(int  , void * ))0;
1837#line 135
1838  tmp = request_threaded_irq(irq, handler, __cil_tmp7, flags, name, dev);
1839  }
1840#line 135
1841  return (tmp);
1842}
1843}
1844#line 184
1845extern void free_irq(unsigned int  , void * ) ;
1846#line 109 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
1847static int parport_attach(struct comedi_device *dev , struct comedi_devconfig *it ) ;
1848#line 111
1849static int parport_detach(struct comedi_device *dev ) ;
1850#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
1851static struct comedi_driver driver_parport  = 
1852#line 112
1853     {(struct comedi_driver *)0, "comedi_parport", & __this_module, & parport_attach,
1854    & parport_detach, 0U, (char const   * const  *)0, 0};
1855#line 119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
1856static int driver_parport_init_module(void) 
1857{ int tmp ;
1858
1859  {
1860  {
1861#line 121
1862  tmp = comedi_driver_register(& driver_parport);
1863  }
1864#line 121
1865  return (tmp);
1866}
1867}
1868#line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
1869static void driver_parport_cleanup_module(void) 
1870{ 
1871
1872  {
1873  {
1874#line 126
1875  comedi_driver_unregister(& driver_parport);
1876  }
1877#line 127
1878  return;
1879}
1880}
1881#line 139 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
1882static int parport_insn_a(struct comedi_device *dev , struct comedi_subdevice *s ,
1883                          struct comedi_insn *insn , unsigned int *data ) 
1884{ unsigned char tmp ;
1885  unsigned int __cil_tmp6 ;
1886  unsigned long __cil_tmp7 ;
1887  unsigned long __cil_tmp8 ;
1888  void *__cil_tmp9 ;
1889  struct parport_private *__cil_tmp10 ;
1890  unsigned int __cil_tmp11 ;
1891  unsigned int __cil_tmp12 ;
1892  unsigned long __cil_tmp13 ;
1893  unsigned long __cil_tmp14 ;
1894  void *__cil_tmp15 ;
1895  struct parport_private *__cil_tmp16 ;
1896  unsigned int __cil_tmp17 ;
1897  unsigned long __cil_tmp18 ;
1898  unsigned long __cil_tmp19 ;
1899  void *__cil_tmp20 ;
1900  struct parport_private *__cil_tmp21 ;
1901  unsigned int *__cil_tmp22 ;
1902  unsigned int __cil_tmp23 ;
1903  unsigned int __cil_tmp24 ;
1904  unsigned int __cil_tmp25 ;
1905  unsigned long __cil_tmp26 ;
1906  unsigned long __cil_tmp27 ;
1907  void *__cil_tmp28 ;
1908  struct parport_private *__cil_tmp29 ;
1909  unsigned int __cil_tmp30 ;
1910  unsigned long __cil_tmp31 ;
1911  unsigned long __cil_tmp32 ;
1912  void *__cil_tmp33 ;
1913  struct parport_private *__cil_tmp34 ;
1914  unsigned int __cil_tmp35 ;
1915  unsigned char __cil_tmp36 ;
1916  int __cil_tmp37 ;
1917  unsigned char __cil_tmp38 ;
1918  unsigned long __cil_tmp39 ;
1919  unsigned long __cil_tmp40 ;
1920  unsigned long __cil_tmp41 ;
1921  int __cil_tmp42 ;
1922  unsigned long __cil_tmp43 ;
1923  unsigned long __cil_tmp44 ;
1924  unsigned long __cil_tmp45 ;
1925  int __cil_tmp46 ;
1926  unsigned int *__cil_tmp47 ;
1927
1928  {
1929  {
1930#line 142
1931  __cil_tmp6 = *data;
1932#line 142
1933  if (__cil_tmp6 != 0U) {
1934    {
1935#line 143
1936    __cil_tmp7 = (unsigned long )dev;
1937#line 143
1938    __cil_tmp8 = __cil_tmp7 + 16;
1939#line 143
1940    __cil_tmp9 = *((void **)__cil_tmp8);
1941#line 143
1942    __cil_tmp10 = (struct parport_private *)__cil_tmp9;
1943#line 143
1944    __cil_tmp11 = *data;
1945#line 143
1946    __cil_tmp12 = ~ __cil_tmp11;
1947#line 143
1948    __cil_tmp13 = (unsigned long )dev;
1949#line 143
1950    __cil_tmp14 = __cil_tmp13 + 16;
1951#line 143
1952    __cil_tmp15 = *((void **)__cil_tmp14);
1953#line 143
1954    __cil_tmp16 = (struct parport_private *)__cil_tmp15;
1955#line 143
1956    __cil_tmp17 = *((unsigned int *)__cil_tmp16);
1957#line 143
1958    *((unsigned int *)__cil_tmp10) = __cil_tmp17 & __cil_tmp12;
1959#line 144
1960    __cil_tmp18 = (unsigned long )dev;
1961#line 144
1962    __cil_tmp19 = __cil_tmp18 + 16;
1963#line 144
1964    __cil_tmp20 = *((void **)__cil_tmp19);
1965#line 144
1966    __cil_tmp21 = (struct parport_private *)__cil_tmp20;
1967#line 144
1968    __cil_tmp22 = data + 1UL;
1969#line 144
1970    __cil_tmp23 = *__cil_tmp22;
1971#line 144
1972    __cil_tmp24 = *data;
1973#line 144
1974    __cil_tmp25 = __cil_tmp24 & __cil_tmp23;
1975#line 144
1976    __cil_tmp26 = (unsigned long )dev;
1977#line 144
1978    __cil_tmp27 = __cil_tmp26 + 16;
1979#line 144
1980    __cil_tmp28 = *((void **)__cil_tmp27);
1981#line 144
1982    __cil_tmp29 = (struct parport_private *)__cil_tmp28;
1983#line 144
1984    __cil_tmp30 = *((unsigned int *)__cil_tmp29);
1985#line 144
1986    *((unsigned int *)__cil_tmp21) = __cil_tmp30 | __cil_tmp25;
1987#line 146
1988    __cil_tmp31 = (unsigned long )dev;
1989#line 146
1990    __cil_tmp32 = __cil_tmp31 + 16;
1991#line 146
1992    __cil_tmp33 = *((void **)__cil_tmp32);
1993#line 146
1994    __cil_tmp34 = (struct parport_private *)__cil_tmp33;
1995#line 146
1996    __cil_tmp35 = *((unsigned int *)__cil_tmp34);
1997#line 146
1998    __cil_tmp36 = (unsigned char )__cil_tmp35;
1999#line 146
2000    __cil_tmp37 = (int )__cil_tmp36;
2001#line 146
2002    __cil_tmp38 = (unsigned char )__cil_tmp37;
2003#line 146
2004    __cil_tmp39 = (unsigned long )dev;
2005#line 146
2006    __cil_tmp40 = __cil_tmp39 + 328;
2007#line 146
2008    __cil_tmp41 = *((unsigned long *)__cil_tmp40);
2009#line 146
2010    __cil_tmp42 = (int )__cil_tmp41;
2011#line 146
2012    outb(__cil_tmp38, __cil_tmp42);
2013    }
2014  } else {
2015
2016  }
2017  }
2018  {
2019#line 149
2020  __cil_tmp43 = (unsigned long )dev;
2021#line 149
2022  __cil_tmp44 = __cil_tmp43 + 328;
2023#line 149
2024  __cil_tmp45 = *((unsigned long *)__cil_tmp44);
2025#line 149
2026  __cil_tmp46 = (int )__cil_tmp45;
2027#line 149
2028  tmp = inb(__cil_tmp46);
2029#line 149
2030  __cil_tmp47 = data + 1UL;
2031#line 149
2032  *__cil_tmp47 = (unsigned int )tmp;
2033  }
2034#line 151
2035  return (2);
2036}
2037}
2038#line 154 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
2039static int parport_insn_config_a(struct comedi_device *dev , struct comedi_subdevice *s ,
2040                                 struct comedi_insn *insn , unsigned int *data ) 
2041{ unsigned int __cil_tmp5 ;
2042  unsigned long __cil_tmp6 ;
2043  unsigned long __cil_tmp7 ;
2044  unsigned long __cil_tmp8 ;
2045  unsigned long __cil_tmp9 ;
2046  void *__cil_tmp10 ;
2047  struct parport_private *__cil_tmp11 ;
2048  unsigned long __cil_tmp12 ;
2049  unsigned long __cil_tmp13 ;
2050  unsigned long __cil_tmp14 ;
2051  unsigned long __cil_tmp15 ;
2052  void *__cil_tmp16 ;
2053  struct parport_private *__cil_tmp17 ;
2054  unsigned long __cil_tmp18 ;
2055  unsigned long __cil_tmp19 ;
2056  unsigned int __cil_tmp20 ;
2057  unsigned long __cil_tmp21 ;
2058  unsigned long __cil_tmp22 ;
2059  unsigned long __cil_tmp23 ;
2060  unsigned long __cil_tmp24 ;
2061  void *__cil_tmp25 ;
2062  struct parport_private *__cil_tmp26 ;
2063  unsigned long __cil_tmp27 ;
2064  unsigned long __cil_tmp28 ;
2065  unsigned long __cil_tmp29 ;
2066  unsigned long __cil_tmp30 ;
2067  void *__cil_tmp31 ;
2068  struct parport_private *__cil_tmp32 ;
2069  unsigned long __cil_tmp33 ;
2070  unsigned long __cil_tmp34 ;
2071  unsigned int __cil_tmp35 ;
2072  unsigned long __cil_tmp36 ;
2073  unsigned long __cil_tmp37 ;
2074  void *__cil_tmp38 ;
2075  struct parport_private *__cil_tmp39 ;
2076  unsigned long __cil_tmp40 ;
2077  unsigned long __cil_tmp41 ;
2078  unsigned int __cil_tmp42 ;
2079  unsigned char __cil_tmp43 ;
2080  int __cil_tmp44 ;
2081  unsigned char __cil_tmp45 ;
2082  unsigned long __cil_tmp46 ;
2083  unsigned long __cil_tmp47 ;
2084  unsigned long __cil_tmp48 ;
2085  unsigned int __cil_tmp49 ;
2086  unsigned int __cil_tmp50 ;
2087  int __cil_tmp51 ;
2088
2089  {
2090  {
2091#line 158
2092  __cil_tmp5 = *data;
2093#line 158
2094  if (__cil_tmp5 != 0U) {
2095#line 159
2096    __cil_tmp6 = (unsigned long )s;
2097#line 159
2098    __cil_tmp7 = __cil_tmp6 + 136;
2099#line 159
2100    *((int *)__cil_tmp7) = 255;
2101#line 160
2102    __cil_tmp8 = (unsigned long )dev;
2103#line 160
2104    __cil_tmp9 = __cil_tmp8 + 16;
2105#line 160
2106    __cil_tmp10 = *((void **)__cil_tmp9);
2107#line 160
2108    __cil_tmp11 = (struct parport_private *)__cil_tmp10;
2109#line 160
2110    __cil_tmp12 = (unsigned long )__cil_tmp11;
2111#line 160
2112    __cil_tmp13 = __cil_tmp12 + 4;
2113#line 160
2114    __cil_tmp14 = (unsigned long )dev;
2115#line 160
2116    __cil_tmp15 = __cil_tmp14 + 16;
2117#line 160
2118    __cil_tmp16 = *((void **)__cil_tmp15);
2119#line 160
2120    __cil_tmp17 = (struct parport_private *)__cil_tmp16;
2121#line 160
2122    __cil_tmp18 = (unsigned long )__cil_tmp17;
2123#line 160
2124    __cil_tmp19 = __cil_tmp18 + 4;
2125#line 160
2126    __cil_tmp20 = *((unsigned int *)__cil_tmp19);
2127#line 160
2128    *((unsigned int *)__cil_tmp13) = __cil_tmp20 & 4294967263U;
2129  } else {
2130#line 162
2131    __cil_tmp21 = (unsigned long )s;
2132#line 162
2133    __cil_tmp22 = __cil_tmp21 + 136;
2134#line 162
2135    *((int *)__cil_tmp22) = 0;
2136#line 163
2137    __cil_tmp23 = (unsigned long )dev;
2138#line 163
2139    __cil_tmp24 = __cil_tmp23 + 16;
2140#line 163
2141    __cil_tmp25 = *((void **)__cil_tmp24);
2142#line 163
2143    __cil_tmp26 = (struct parport_private *)__cil_tmp25;
2144#line 163
2145    __cil_tmp27 = (unsigned long )__cil_tmp26;
2146#line 163
2147    __cil_tmp28 = __cil_tmp27 + 4;
2148#line 163
2149    __cil_tmp29 = (unsigned long )dev;
2150#line 163
2151    __cil_tmp30 = __cil_tmp29 + 16;
2152#line 163
2153    __cil_tmp31 = *((void **)__cil_tmp30);
2154#line 163
2155    __cil_tmp32 = (struct parport_private *)__cil_tmp31;
2156#line 163
2157    __cil_tmp33 = (unsigned long )__cil_tmp32;
2158#line 163
2159    __cil_tmp34 = __cil_tmp33 + 4;
2160#line 163
2161    __cil_tmp35 = *((unsigned int *)__cil_tmp34);
2162#line 163
2163    *((unsigned int *)__cil_tmp28) = __cil_tmp35 | 32U;
2164  }
2165  }
2166  {
2167#line 165
2168  __cil_tmp36 = (unsigned long )dev;
2169#line 165
2170  __cil_tmp37 = __cil_tmp36 + 16;
2171#line 165
2172  __cil_tmp38 = *((void **)__cil_tmp37);
2173#line 165
2174  __cil_tmp39 = (struct parport_private *)__cil_tmp38;
2175#line 165
2176  __cil_tmp40 = (unsigned long )__cil_tmp39;
2177#line 165
2178  __cil_tmp41 = __cil_tmp40 + 4;
2179#line 165
2180  __cil_tmp42 = *((unsigned int *)__cil_tmp41);
2181#line 165
2182  __cil_tmp43 = (unsigned char )__cil_tmp42;
2183#line 165
2184  __cil_tmp44 = (int )__cil_tmp43;
2185#line 165
2186  __cil_tmp45 = (unsigned char )__cil_tmp44;
2187#line 165
2188  __cil_tmp46 = (unsigned long )dev;
2189#line 165
2190  __cil_tmp47 = __cil_tmp46 + 328;
2191#line 165
2192  __cil_tmp48 = *((unsigned long *)__cil_tmp47);
2193#line 165
2194  __cil_tmp49 = (unsigned int )__cil_tmp48;
2195#line 165
2196  __cil_tmp50 = __cil_tmp49 + 2U;
2197#line 165
2198  __cil_tmp51 = (int )__cil_tmp50;
2199#line 165
2200  outb(__cil_tmp45, __cil_tmp51);
2201  }
2202#line 167
2203  return (1);
2204}
2205}
2206#line 170 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
2207static int parport_insn_b(struct comedi_device *dev , struct comedi_subdevice *s ,
2208                          struct comedi_insn *insn , unsigned int *data ) 
2209{ unsigned char tmp ;
2210  unsigned long __cil_tmp6 ;
2211  unsigned long __cil_tmp7 ;
2212  unsigned long __cil_tmp8 ;
2213  unsigned int __cil_tmp9 ;
2214  unsigned int __cil_tmp10 ;
2215  int __cil_tmp11 ;
2216  unsigned int *__cil_tmp12 ;
2217  int __cil_tmp13 ;
2218  int __cil_tmp14 ;
2219
2220  {
2221  {
2222#line 178
2223  __cil_tmp6 = (unsigned long )dev;
2224#line 178
2225  __cil_tmp7 = __cil_tmp6 + 328;
2226#line 178
2227  __cil_tmp8 = *((unsigned long *)__cil_tmp7);
2228#line 178
2229  __cil_tmp9 = (unsigned int )__cil_tmp8;
2230#line 178
2231  __cil_tmp10 = __cil_tmp9 + 1U;
2232#line 178
2233  __cil_tmp11 = (int )__cil_tmp10;
2234#line 178
2235  tmp = inb(__cil_tmp11);
2236#line 178
2237  __cil_tmp12 = data + 1UL;
2238#line 178
2239  __cil_tmp13 = (int )tmp;
2240#line 178
2241  __cil_tmp14 = __cil_tmp13 >> 3;
2242#line 178
2243  *__cil_tmp12 = (unsigned int )__cil_tmp14;
2244  }
2245#line 180
2246  return (2);
2247}
2248}
2249#line 183 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
2250static int parport_insn_c(struct comedi_device *dev , struct comedi_subdevice *s ,
2251                          struct comedi_insn *insn , unsigned int *data ) 
2252{ unsigned int __cil_tmp5 ;
2253  unsigned int __cil_tmp6 ;
2254  unsigned long __cil_tmp7 ;
2255  unsigned long __cil_tmp8 ;
2256  void *__cil_tmp9 ;
2257  struct parport_private *__cil_tmp10 ;
2258  unsigned long __cil_tmp11 ;
2259  unsigned long __cil_tmp12 ;
2260  unsigned int __cil_tmp13 ;
2261  unsigned int __cil_tmp14 ;
2262  unsigned long __cil_tmp15 ;
2263  unsigned long __cil_tmp16 ;
2264  void *__cil_tmp17 ;
2265  struct parport_private *__cil_tmp18 ;
2266  unsigned long __cil_tmp19 ;
2267  unsigned long __cil_tmp20 ;
2268  unsigned int __cil_tmp21 ;
2269  unsigned long __cil_tmp22 ;
2270  unsigned long __cil_tmp23 ;
2271  void *__cil_tmp24 ;
2272  struct parport_private *__cil_tmp25 ;
2273  unsigned long __cil_tmp26 ;
2274  unsigned long __cil_tmp27 ;
2275  unsigned int *__cil_tmp28 ;
2276  unsigned int __cil_tmp29 ;
2277  unsigned int __cil_tmp30 ;
2278  unsigned int __cil_tmp31 ;
2279  unsigned long __cil_tmp32 ;
2280  unsigned long __cil_tmp33 ;
2281  void *__cil_tmp34 ;
2282  struct parport_private *__cil_tmp35 ;
2283  unsigned long __cil_tmp36 ;
2284  unsigned long __cil_tmp37 ;
2285  unsigned int __cil_tmp38 ;
2286  unsigned long __cil_tmp39 ;
2287  unsigned long __cil_tmp40 ;
2288  void *__cil_tmp41 ;
2289  struct parport_private *__cil_tmp42 ;
2290  unsigned long __cil_tmp43 ;
2291  unsigned long __cil_tmp44 ;
2292  unsigned int __cil_tmp45 ;
2293  unsigned char __cil_tmp46 ;
2294  int __cil_tmp47 ;
2295  unsigned char __cil_tmp48 ;
2296  unsigned long __cil_tmp49 ;
2297  unsigned long __cil_tmp50 ;
2298  unsigned long __cil_tmp51 ;
2299  unsigned int __cil_tmp52 ;
2300  unsigned int __cil_tmp53 ;
2301  int __cil_tmp54 ;
2302  unsigned int *__cil_tmp55 ;
2303  unsigned long __cil_tmp56 ;
2304  unsigned long __cil_tmp57 ;
2305  void *__cil_tmp58 ;
2306  struct parport_private *__cil_tmp59 ;
2307  unsigned long __cil_tmp60 ;
2308  unsigned long __cil_tmp61 ;
2309  unsigned int __cil_tmp62 ;
2310
2311  {
2312#line 186
2313  __cil_tmp5 = *data;
2314#line 186
2315  *data = __cil_tmp5 & 15U;
2316  {
2317#line 187
2318  __cil_tmp6 = *data;
2319#line 187
2320  if (__cil_tmp6 != 0U) {
2321    {
2322#line 188
2323    __cil_tmp7 = (unsigned long )dev;
2324#line 188
2325    __cil_tmp8 = __cil_tmp7 + 16;
2326#line 188
2327    __cil_tmp9 = *((void **)__cil_tmp8);
2328#line 188
2329    __cil_tmp10 = (struct parport_private *)__cil_tmp9;
2330#line 188
2331    __cil_tmp11 = (unsigned long )__cil_tmp10;
2332#line 188
2333    __cil_tmp12 = __cil_tmp11 + 4;
2334#line 188
2335    __cil_tmp13 = *data;
2336#line 188
2337    __cil_tmp14 = ~ __cil_tmp13;
2338#line 188
2339    __cil_tmp15 = (unsigned long )dev;
2340#line 188
2341    __cil_tmp16 = __cil_tmp15 + 16;
2342#line 188
2343    __cil_tmp17 = *((void **)__cil_tmp16);
2344#line 188
2345    __cil_tmp18 = (struct parport_private *)__cil_tmp17;
2346#line 188
2347    __cil_tmp19 = (unsigned long )__cil_tmp18;
2348#line 188
2349    __cil_tmp20 = __cil_tmp19 + 4;
2350#line 188
2351    __cil_tmp21 = *((unsigned int *)__cil_tmp20);
2352#line 188
2353    *((unsigned int *)__cil_tmp12) = __cil_tmp21 & __cil_tmp14;
2354#line 189
2355    __cil_tmp22 = (unsigned long )dev;
2356#line 189
2357    __cil_tmp23 = __cil_tmp22 + 16;
2358#line 189
2359    __cil_tmp24 = *((void **)__cil_tmp23);
2360#line 189
2361    __cil_tmp25 = (struct parport_private *)__cil_tmp24;
2362#line 189
2363    __cil_tmp26 = (unsigned long )__cil_tmp25;
2364#line 189
2365    __cil_tmp27 = __cil_tmp26 + 4;
2366#line 189
2367    __cil_tmp28 = data + 1UL;
2368#line 189
2369    __cil_tmp29 = *__cil_tmp28;
2370#line 189
2371    __cil_tmp30 = *data;
2372#line 189
2373    __cil_tmp31 = __cil_tmp30 & __cil_tmp29;
2374#line 189
2375    __cil_tmp32 = (unsigned long )dev;
2376#line 189
2377    __cil_tmp33 = __cil_tmp32 + 16;
2378#line 189
2379    __cil_tmp34 = *((void **)__cil_tmp33);
2380#line 189
2381    __cil_tmp35 = (struct parport_private *)__cil_tmp34;
2382#line 189
2383    __cil_tmp36 = (unsigned long )__cil_tmp35;
2384#line 189
2385    __cil_tmp37 = __cil_tmp36 + 4;
2386#line 189
2387    __cil_tmp38 = *((unsigned int *)__cil_tmp37);
2388#line 189
2389    *((unsigned int *)__cil_tmp27) = __cil_tmp38 | __cil_tmp31;
2390#line 191
2391    __cil_tmp39 = (unsigned long )dev;
2392#line 191
2393    __cil_tmp40 = __cil_tmp39 + 16;
2394#line 191
2395    __cil_tmp41 = *((void **)__cil_tmp40);
2396#line 191
2397    __cil_tmp42 = (struct parport_private *)__cil_tmp41;
2398#line 191
2399    __cil_tmp43 = (unsigned long )__cil_tmp42;
2400#line 191
2401    __cil_tmp44 = __cil_tmp43 + 4;
2402#line 191
2403    __cil_tmp45 = *((unsigned int *)__cil_tmp44);
2404#line 191
2405    __cil_tmp46 = (unsigned char )__cil_tmp45;
2406#line 191
2407    __cil_tmp47 = (int )__cil_tmp46;
2408#line 191
2409    __cil_tmp48 = (unsigned char )__cil_tmp47;
2410#line 191
2411    __cil_tmp49 = (unsigned long )dev;
2412#line 191
2413    __cil_tmp50 = __cil_tmp49 + 328;
2414#line 191
2415    __cil_tmp51 = *((unsigned long *)__cil_tmp50);
2416#line 191
2417    __cil_tmp52 = (unsigned int )__cil_tmp51;
2418#line 191
2419    __cil_tmp53 = __cil_tmp52 + 2U;
2420#line 191
2421    __cil_tmp54 = (int )__cil_tmp53;
2422#line 191
2423    outb(__cil_tmp48, __cil_tmp54);
2424    }
2425  } else {
2426
2427  }
2428  }
2429#line 194
2430  __cil_tmp55 = data + 1UL;
2431#line 194
2432  __cil_tmp56 = (unsigned long )dev;
2433#line 194
2434  __cil_tmp57 = __cil_tmp56 + 16;
2435#line 194
2436  __cil_tmp58 = *((void **)__cil_tmp57);
2437#line 194
2438  __cil_tmp59 = (struct parport_private *)__cil_tmp58;
2439#line 194
2440  __cil_tmp60 = (unsigned long )__cil_tmp59;
2441#line 194
2442  __cil_tmp61 = __cil_tmp60 + 4;
2443#line 194
2444  __cil_tmp62 = *((unsigned int *)__cil_tmp61);
2445#line 194
2446  *__cil_tmp55 = __cil_tmp62 & 15U;
2447#line 196
2448  return (2);
2449}
2450}
2451#line 199 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
2452static int parport_intr_insn(struct comedi_device *dev , struct comedi_subdevice *s ,
2453                             struct comedi_insn *insn , unsigned int *data ) 
2454{ unsigned long __cil_tmp5 ;
2455  unsigned long __cil_tmp6 ;
2456  unsigned int __cil_tmp7 ;
2457  unsigned int *__cil_tmp8 ;
2458
2459  {
2460  {
2461#line 203
2462  __cil_tmp5 = (unsigned long )insn;
2463#line 203
2464  __cil_tmp6 = __cil_tmp5 + 4;
2465#line 203
2466  __cil_tmp7 = *((unsigned int *)__cil_tmp6);
2467#line 203
2468  if (__cil_tmp7 == 0U) {
2469#line 204
2470    return (-22);
2471  } else {
2472
2473  }
2474  }
2475#line 206
2476  __cil_tmp8 = data + 1UL;
2477#line 206
2478  *__cil_tmp8 = 0U;
2479#line 207
2480  return (2);
2481}
2482}
2483#line 210 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
2484static int parport_intr_cmdtest(struct comedi_device *dev , struct comedi_subdevice *s ,
2485                                struct comedi_cmd *cmd ) 
2486{ int err ;
2487  int tmp ;
2488  unsigned long __cil_tmp6 ;
2489  unsigned long __cil_tmp7 ;
2490  unsigned int __cil_tmp8 ;
2491  unsigned long __cil_tmp9 ;
2492  unsigned long __cil_tmp10 ;
2493  unsigned long __cil_tmp11 ;
2494  unsigned long __cil_tmp12 ;
2495  unsigned int __cil_tmp13 ;
2496  unsigned long __cil_tmp14 ;
2497  unsigned long __cil_tmp15 ;
2498  unsigned int __cil_tmp16 ;
2499  unsigned long __cil_tmp17 ;
2500  unsigned long __cil_tmp18 ;
2501  unsigned int __cil_tmp19 ;
2502  unsigned int __cil_tmp20 ;
2503  unsigned long __cil_tmp21 ;
2504  unsigned long __cil_tmp22 ;
2505  unsigned int __cil_tmp23 ;
2506  unsigned long __cil_tmp24 ;
2507  unsigned long __cil_tmp25 ;
2508  unsigned long __cil_tmp26 ;
2509  unsigned long __cil_tmp27 ;
2510  unsigned int __cil_tmp28 ;
2511  unsigned long __cil_tmp29 ;
2512  unsigned long __cil_tmp30 ;
2513  unsigned int __cil_tmp31 ;
2514  unsigned long __cil_tmp32 ;
2515  unsigned long __cil_tmp33 ;
2516  unsigned int __cil_tmp34 ;
2517  unsigned int __cil_tmp35 ;
2518  unsigned long __cil_tmp36 ;
2519  unsigned long __cil_tmp37 ;
2520  unsigned int __cil_tmp38 ;
2521  unsigned long __cil_tmp39 ;
2522  unsigned long __cil_tmp40 ;
2523  unsigned long __cil_tmp41 ;
2524  unsigned long __cil_tmp42 ;
2525  unsigned int __cil_tmp43 ;
2526  unsigned long __cil_tmp44 ;
2527  unsigned long __cil_tmp45 ;
2528  unsigned int __cil_tmp46 ;
2529  unsigned long __cil_tmp47 ;
2530  unsigned long __cil_tmp48 ;
2531  unsigned int __cil_tmp49 ;
2532  unsigned int __cil_tmp50 ;
2533  unsigned long __cil_tmp51 ;
2534  unsigned long __cil_tmp52 ;
2535  unsigned int __cil_tmp53 ;
2536  unsigned long __cil_tmp54 ;
2537  unsigned long __cil_tmp55 ;
2538  unsigned long __cil_tmp56 ;
2539  unsigned long __cil_tmp57 ;
2540  unsigned int __cil_tmp58 ;
2541  unsigned long __cil_tmp59 ;
2542  unsigned long __cil_tmp60 ;
2543  unsigned int __cil_tmp61 ;
2544  unsigned long __cil_tmp62 ;
2545  unsigned long __cil_tmp63 ;
2546  unsigned int __cil_tmp64 ;
2547  unsigned int __cil_tmp65 ;
2548  unsigned long __cil_tmp66 ;
2549  unsigned long __cil_tmp67 ;
2550  unsigned int __cil_tmp68 ;
2551  unsigned long __cil_tmp69 ;
2552  unsigned long __cil_tmp70 ;
2553  unsigned long __cil_tmp71 ;
2554  unsigned long __cil_tmp72 ;
2555  unsigned int __cil_tmp73 ;
2556  unsigned long __cil_tmp74 ;
2557  unsigned long __cil_tmp75 ;
2558  unsigned int __cil_tmp76 ;
2559  unsigned long __cil_tmp77 ;
2560  unsigned long __cil_tmp78 ;
2561  unsigned int __cil_tmp79 ;
2562  unsigned int __cil_tmp80 ;
2563  unsigned long __cil_tmp81 ;
2564  unsigned long __cil_tmp82 ;
2565  unsigned int __cil_tmp83 ;
2566  unsigned long __cil_tmp84 ;
2567  unsigned long __cil_tmp85 ;
2568  unsigned long __cil_tmp86 ;
2569  unsigned long __cil_tmp87 ;
2570  unsigned int __cil_tmp88 ;
2571  unsigned long __cil_tmp89 ;
2572  unsigned long __cil_tmp90 ;
2573  unsigned long __cil_tmp91 ;
2574  unsigned long __cil_tmp92 ;
2575  unsigned int __cil_tmp93 ;
2576  unsigned long __cil_tmp94 ;
2577  unsigned long __cil_tmp95 ;
2578  unsigned long __cil_tmp96 ;
2579  unsigned long __cil_tmp97 ;
2580  unsigned int __cil_tmp98 ;
2581  unsigned long __cil_tmp99 ;
2582  unsigned long __cil_tmp100 ;
2583  unsigned long __cil_tmp101 ;
2584  unsigned long __cil_tmp102 ;
2585  unsigned int __cil_tmp103 ;
2586  unsigned long __cil_tmp104 ;
2587  unsigned long __cil_tmp105 ;
2588
2589  {
2590#line 214
2591  err = 0;
2592#line 219
2593  __cil_tmp6 = (unsigned long )cmd;
2594#line 219
2595  __cil_tmp7 = __cil_tmp6 + 8;
2596#line 219
2597  __cil_tmp8 = *((unsigned int *)__cil_tmp7);
2598#line 219
2599  tmp = (int )__cil_tmp8;
2600#line 220
2601  __cil_tmp9 = (unsigned long )cmd;
2602#line 220
2603  __cil_tmp10 = __cil_tmp9 + 8;
2604#line 220
2605  __cil_tmp11 = (unsigned long )cmd;
2606#line 220
2607  __cil_tmp12 = __cil_tmp11 + 8;
2608#line 220
2609  __cil_tmp13 = *((unsigned int *)__cil_tmp12);
2610#line 220
2611  *((unsigned int *)__cil_tmp10) = __cil_tmp13 & 2U;
2612  {
2613#line 221
2614  __cil_tmp14 = (unsigned long )cmd;
2615#line 221
2616  __cil_tmp15 = __cil_tmp14 + 8;
2617#line 221
2618  __cil_tmp16 = *((unsigned int *)__cil_tmp15);
2619#line 221
2620  if (__cil_tmp16 == 0U) {
2621#line 222
2622    err = err + 1;
2623  } else {
2624    {
2625#line 221
2626    __cil_tmp17 = (unsigned long )cmd;
2627#line 221
2628    __cil_tmp18 = __cil_tmp17 + 8;
2629#line 221
2630    __cil_tmp19 = *((unsigned int *)__cil_tmp18);
2631#line 221
2632    __cil_tmp20 = (unsigned int )tmp;
2633#line 221
2634    if (__cil_tmp20 != __cil_tmp19) {
2635#line 222
2636      err = err + 1;
2637    } else {
2638
2639    }
2640    }
2641  }
2642  }
2643#line 224
2644  __cil_tmp21 = (unsigned long )cmd;
2645#line 224
2646  __cil_tmp22 = __cil_tmp21 + 16;
2647#line 224
2648  __cil_tmp23 = *((unsigned int *)__cil_tmp22);
2649#line 224
2650  tmp = (int )__cil_tmp23;
2651#line 225
2652  __cil_tmp24 = (unsigned long )cmd;
2653#line 225
2654  __cil_tmp25 = __cil_tmp24 + 16;
2655#line 225
2656  __cil_tmp26 = (unsigned long )cmd;
2657#line 225
2658  __cil_tmp27 = __cil_tmp26 + 16;
2659#line 225
2660  __cil_tmp28 = *((unsigned int *)__cil_tmp27);
2661#line 225
2662  *((unsigned int *)__cil_tmp25) = __cil_tmp28 & 64U;
2663  {
2664#line 226
2665  __cil_tmp29 = (unsigned long )cmd;
2666#line 226
2667  __cil_tmp30 = __cil_tmp29 + 16;
2668#line 226
2669  __cil_tmp31 = *((unsigned int *)__cil_tmp30);
2670#line 226
2671  if (__cil_tmp31 == 0U) {
2672#line 227
2673    err = err + 1;
2674  } else {
2675    {
2676#line 226
2677    __cil_tmp32 = (unsigned long )cmd;
2678#line 226
2679    __cil_tmp33 = __cil_tmp32 + 16;
2680#line 226
2681    __cil_tmp34 = *((unsigned int *)__cil_tmp33);
2682#line 226
2683    __cil_tmp35 = (unsigned int )tmp;
2684#line 226
2685    if (__cil_tmp35 != __cil_tmp34) {
2686#line 227
2687      err = err + 1;
2688    } else {
2689
2690    }
2691    }
2692  }
2693  }
2694#line 229
2695  __cil_tmp36 = (unsigned long )cmd;
2696#line 229
2697  __cil_tmp37 = __cil_tmp36 + 24;
2698#line 229
2699  __cil_tmp38 = *((unsigned int *)__cil_tmp37);
2700#line 229
2701  tmp = (int )__cil_tmp38;
2702#line 230
2703  __cil_tmp39 = (unsigned long )cmd;
2704#line 230
2705  __cil_tmp40 = __cil_tmp39 + 24;
2706#line 230
2707  __cil_tmp41 = (unsigned long )cmd;
2708#line 230
2709  __cil_tmp42 = __cil_tmp41 + 24;
2710#line 230
2711  __cil_tmp43 = *((unsigned int *)__cil_tmp42);
2712#line 230
2713  *((unsigned int *)__cil_tmp40) = __cil_tmp43 & 4U;
2714  {
2715#line 231
2716  __cil_tmp44 = (unsigned long )cmd;
2717#line 231
2718  __cil_tmp45 = __cil_tmp44 + 24;
2719#line 231
2720  __cil_tmp46 = *((unsigned int *)__cil_tmp45);
2721#line 231
2722  if (__cil_tmp46 == 0U) {
2723#line 232
2724    err = err + 1;
2725  } else {
2726    {
2727#line 231
2728    __cil_tmp47 = (unsigned long )cmd;
2729#line 231
2730    __cil_tmp48 = __cil_tmp47 + 24;
2731#line 231
2732    __cil_tmp49 = *((unsigned int *)__cil_tmp48);
2733#line 231
2734    __cil_tmp50 = (unsigned int )tmp;
2735#line 231
2736    if (__cil_tmp50 != __cil_tmp49) {
2737#line 232
2738      err = err + 1;
2739    } else {
2740
2741    }
2742    }
2743  }
2744  }
2745#line 234
2746  __cil_tmp51 = (unsigned long )cmd;
2747#line 234
2748  __cil_tmp52 = __cil_tmp51 + 32;
2749#line 234
2750  __cil_tmp53 = *((unsigned int *)__cil_tmp52);
2751#line 234
2752  tmp = (int )__cil_tmp53;
2753#line 235
2754  __cil_tmp54 = (unsigned long )cmd;
2755#line 235
2756  __cil_tmp55 = __cil_tmp54 + 32;
2757#line 235
2758  __cil_tmp56 = (unsigned long )cmd;
2759#line 235
2760  __cil_tmp57 = __cil_tmp56 + 32;
2761#line 235
2762  __cil_tmp58 = *((unsigned int *)__cil_tmp57);
2763#line 235
2764  *((unsigned int *)__cil_tmp55) = __cil_tmp58 & 32U;
2765  {
2766#line 236
2767  __cil_tmp59 = (unsigned long )cmd;
2768#line 236
2769  __cil_tmp60 = __cil_tmp59 + 32;
2770#line 236
2771  __cil_tmp61 = *((unsigned int *)__cil_tmp60);
2772#line 236
2773  if (__cil_tmp61 == 0U) {
2774#line 237
2775    err = err + 1;
2776  } else {
2777    {
2778#line 236
2779    __cil_tmp62 = (unsigned long )cmd;
2780#line 236
2781    __cil_tmp63 = __cil_tmp62 + 32;
2782#line 236
2783    __cil_tmp64 = *((unsigned int *)__cil_tmp63);
2784#line 236
2785    __cil_tmp65 = (unsigned int )tmp;
2786#line 236
2787    if (__cil_tmp65 != __cil_tmp64) {
2788#line 237
2789      err = err + 1;
2790    } else {
2791
2792    }
2793    }
2794  }
2795  }
2796#line 239
2797  __cil_tmp66 = (unsigned long )cmd;
2798#line 239
2799  __cil_tmp67 = __cil_tmp66 + 40;
2800#line 239
2801  __cil_tmp68 = *((unsigned int *)__cil_tmp67);
2802#line 239
2803  tmp = (int )__cil_tmp68;
2804#line 240
2805  __cil_tmp69 = (unsigned long )cmd;
2806#line 240
2807  __cil_tmp70 = __cil_tmp69 + 40;
2808#line 240
2809  __cil_tmp71 = (unsigned long )cmd;
2810#line 240
2811  __cil_tmp72 = __cil_tmp71 + 40;
2812#line 240
2813  __cil_tmp73 = *((unsigned int *)__cil_tmp72);
2814#line 240
2815  *((unsigned int *)__cil_tmp70) = __cil_tmp73 & 1U;
2816  {
2817#line 241
2818  __cil_tmp74 = (unsigned long )cmd;
2819#line 241
2820  __cil_tmp75 = __cil_tmp74 + 40;
2821#line 241
2822  __cil_tmp76 = *((unsigned int *)__cil_tmp75);
2823#line 241
2824  if (__cil_tmp76 == 0U) {
2825#line 242
2826    err = err + 1;
2827  } else {
2828    {
2829#line 241
2830    __cil_tmp77 = (unsigned long )cmd;
2831#line 241
2832    __cil_tmp78 = __cil_tmp77 + 40;
2833#line 241
2834    __cil_tmp79 = *((unsigned int *)__cil_tmp78);
2835#line 241
2836    __cil_tmp80 = (unsigned int )tmp;
2837#line 241
2838    if (__cil_tmp80 != __cil_tmp79) {
2839#line 242
2840      err = err + 1;
2841    } else {
2842
2843    }
2844    }
2845  }
2846  }
2847#line 244
2848  if (err != 0) {
2849#line 245
2850    return (1);
2851  } else {
2852
2853  }
2854#line 249
2855  if (err != 0) {
2856#line 250
2857    return (2);
2858  } else {
2859
2860  }
2861  {
2862#line 254
2863  __cil_tmp81 = (unsigned long )cmd;
2864#line 254
2865  __cil_tmp82 = __cil_tmp81 + 12;
2866#line 254
2867  __cil_tmp83 = *((unsigned int *)__cil_tmp82);
2868#line 254
2869  if (__cil_tmp83 != 0U) {
2870#line 255
2871    __cil_tmp84 = (unsigned long )cmd;
2872#line 255
2873    __cil_tmp85 = __cil_tmp84 + 12;
2874#line 255
2875    *((unsigned int *)__cil_tmp85) = 0U;
2876#line 256
2877    err = err + 1;
2878  } else {
2879
2880  }
2881  }
2882  {
2883#line 258
2884  __cil_tmp86 = (unsigned long )cmd;
2885#line 258
2886  __cil_tmp87 = __cil_tmp86 + 20;
2887#line 258
2888  __cil_tmp88 = *((unsigned int *)__cil_tmp87);
2889#line 258
2890  if (__cil_tmp88 != 0U) {
2891#line 259
2892    __cil_tmp89 = (unsigned long )cmd;
2893#line 259
2894    __cil_tmp90 = __cil_tmp89 + 20;
2895#line 259
2896    *((unsigned int *)__cil_tmp90) = 0U;
2897#line 260
2898    err = err + 1;
2899  } else {
2900
2901  }
2902  }
2903  {
2904#line 262
2905  __cil_tmp91 = (unsigned long )cmd;
2906#line 262
2907  __cil_tmp92 = __cil_tmp91 + 28;
2908#line 262
2909  __cil_tmp93 = *((unsigned int *)__cil_tmp92);
2910#line 262
2911  if (__cil_tmp93 != 0U) {
2912#line 263
2913    __cil_tmp94 = (unsigned long )cmd;
2914#line 263
2915    __cil_tmp95 = __cil_tmp94 + 28;
2916#line 263
2917    *((unsigned int *)__cil_tmp95) = 0U;
2918#line 264
2919    err = err + 1;
2920  } else {
2921
2922  }
2923  }
2924  {
2925#line 266
2926  __cil_tmp96 = (unsigned long )cmd;
2927#line 266
2928  __cil_tmp97 = __cil_tmp96 + 36;
2929#line 266
2930  __cil_tmp98 = *((unsigned int *)__cil_tmp97);
2931#line 266
2932  if (__cil_tmp98 != 1U) {
2933#line 267
2934    __cil_tmp99 = (unsigned long )cmd;
2935#line 267
2936    __cil_tmp100 = __cil_tmp99 + 36;
2937#line 267
2938    *((unsigned int *)__cil_tmp100) = 1U;
2939#line 268
2940    err = err + 1;
2941  } else {
2942
2943  }
2944  }
2945  {
2946#line 270
2947  __cil_tmp101 = (unsigned long )cmd;
2948#line 270
2949  __cil_tmp102 = __cil_tmp101 + 44;
2950#line 270
2951  __cil_tmp103 = *((unsigned int *)__cil_tmp102);
2952#line 270
2953  if (__cil_tmp103 != 0U) {
2954#line 271
2955    __cil_tmp104 = (unsigned long )cmd;
2956#line 271
2957    __cil_tmp105 = __cil_tmp104 + 44;
2958#line 271
2959    *((unsigned int *)__cil_tmp105) = 0U;
2960#line 272
2961    err = err + 1;
2962  } else {
2963
2964  }
2965  }
2966#line 275
2967  if (err != 0) {
2968#line 276
2969    return (3);
2970  } else {
2971
2972  }
2973#line 280
2974  if (err != 0) {
2975#line 281
2976    return (4);
2977  } else {
2978
2979  }
2980#line 283
2981  return (0);
2982}
2983}
2984#line 286 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
2985static int parport_intr_cmd(struct comedi_device *dev , struct comedi_subdevice *s ) 
2986{ unsigned long __cil_tmp3 ;
2987  unsigned long __cil_tmp4 ;
2988  void *__cil_tmp5 ;
2989  struct parport_private *__cil_tmp6 ;
2990  unsigned long __cil_tmp7 ;
2991  unsigned long __cil_tmp8 ;
2992  unsigned long __cil_tmp9 ;
2993  unsigned long __cil_tmp10 ;
2994  void *__cil_tmp11 ;
2995  struct parport_private *__cil_tmp12 ;
2996  unsigned long __cil_tmp13 ;
2997  unsigned long __cil_tmp14 ;
2998  unsigned int __cil_tmp15 ;
2999  unsigned long __cil_tmp16 ;
3000  unsigned long __cil_tmp17 ;
3001  void *__cil_tmp18 ;
3002  struct parport_private *__cil_tmp19 ;
3003  unsigned long __cil_tmp20 ;
3004  unsigned long __cil_tmp21 ;
3005  unsigned int __cil_tmp22 ;
3006  unsigned char __cil_tmp23 ;
3007  int __cil_tmp24 ;
3008  unsigned char __cil_tmp25 ;
3009  unsigned long __cil_tmp26 ;
3010  unsigned long __cil_tmp27 ;
3011  unsigned long __cil_tmp28 ;
3012  unsigned int __cil_tmp29 ;
3013  unsigned int __cil_tmp30 ;
3014  int __cil_tmp31 ;
3015  unsigned long __cil_tmp32 ;
3016  unsigned long __cil_tmp33 ;
3017  void *__cil_tmp34 ;
3018  struct parport_private *__cil_tmp35 ;
3019  unsigned long __cil_tmp36 ;
3020  unsigned long __cil_tmp37 ;
3021
3022  {
3023  {
3024#line 289
3025  __cil_tmp3 = (unsigned long )dev;
3026#line 289
3027  __cil_tmp4 = __cil_tmp3 + 16;
3028#line 289
3029  __cil_tmp5 = *((void **)__cil_tmp4);
3030#line 289
3031  __cil_tmp6 = (struct parport_private *)__cil_tmp5;
3032#line 289
3033  __cil_tmp7 = (unsigned long )__cil_tmp6;
3034#line 289
3035  __cil_tmp8 = __cil_tmp7 + 4;
3036#line 289
3037  __cil_tmp9 = (unsigned long )dev;
3038#line 289
3039  __cil_tmp10 = __cil_tmp9 + 16;
3040#line 289
3041  __cil_tmp11 = *((void **)__cil_tmp10);
3042#line 289
3043  __cil_tmp12 = (struct parport_private *)__cil_tmp11;
3044#line 289
3045  __cil_tmp13 = (unsigned long )__cil_tmp12;
3046#line 289
3047  __cil_tmp14 = __cil_tmp13 + 4;
3048#line 289
3049  __cil_tmp15 = *((unsigned int *)__cil_tmp14);
3050#line 289
3051  *((unsigned int *)__cil_tmp8) = __cil_tmp15 | 16U;
3052#line 290
3053  __cil_tmp16 = (unsigned long )dev;
3054#line 290
3055  __cil_tmp17 = __cil_tmp16 + 16;
3056#line 290
3057  __cil_tmp18 = *((void **)__cil_tmp17);
3058#line 290
3059  __cil_tmp19 = (struct parport_private *)__cil_tmp18;
3060#line 290
3061  __cil_tmp20 = (unsigned long )__cil_tmp19;
3062#line 290
3063  __cil_tmp21 = __cil_tmp20 + 4;
3064#line 290
3065  __cil_tmp22 = *((unsigned int *)__cil_tmp21);
3066#line 290
3067  __cil_tmp23 = (unsigned char )__cil_tmp22;
3068#line 290
3069  __cil_tmp24 = (int )__cil_tmp23;
3070#line 290
3071  __cil_tmp25 = (unsigned char )__cil_tmp24;
3072#line 290
3073  __cil_tmp26 = (unsigned long )dev;
3074#line 290
3075  __cil_tmp27 = __cil_tmp26 + 328;
3076#line 290
3077  __cil_tmp28 = *((unsigned long *)__cil_tmp27);
3078#line 290
3079  __cil_tmp29 = (unsigned int )__cil_tmp28;
3080#line 290
3081  __cil_tmp30 = __cil_tmp29 + 2U;
3082#line 290
3083  __cil_tmp31 = (int )__cil_tmp30;
3084#line 290
3085  outb(__cil_tmp25, __cil_tmp31);
3086#line 292
3087  __cil_tmp32 = (unsigned long )dev;
3088#line 292
3089  __cil_tmp33 = __cil_tmp32 + 16;
3090#line 292
3091  __cil_tmp34 = *((void **)__cil_tmp33);
3092#line 292
3093  __cil_tmp35 = (struct parport_private *)__cil_tmp34;
3094#line 292
3095  __cil_tmp36 = (unsigned long )__cil_tmp35;
3096#line 292
3097  __cil_tmp37 = __cil_tmp36 + 8;
3098#line 292
3099  *((int *)__cil_tmp37) = 1;
3100  }
3101#line 294
3102  return (0);
3103}
3104}
3105#line 297 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
3106static int parport_intr_cancel(struct comedi_device *dev , struct comedi_subdevice *s ) 
3107{ unsigned long __cil_tmp3 ;
3108  unsigned long __cil_tmp4 ;
3109  void *__cil_tmp5 ;
3110  struct parport_private *__cil_tmp6 ;
3111  unsigned long __cil_tmp7 ;
3112  unsigned long __cil_tmp8 ;
3113  unsigned long __cil_tmp9 ;
3114  unsigned long __cil_tmp10 ;
3115  void *__cil_tmp11 ;
3116  struct parport_private *__cil_tmp12 ;
3117  unsigned long __cil_tmp13 ;
3118  unsigned long __cil_tmp14 ;
3119  unsigned int __cil_tmp15 ;
3120  unsigned long __cil_tmp16 ;
3121  unsigned long __cil_tmp17 ;
3122  void *__cil_tmp18 ;
3123  struct parport_private *__cil_tmp19 ;
3124  unsigned long __cil_tmp20 ;
3125  unsigned long __cil_tmp21 ;
3126  unsigned int __cil_tmp22 ;
3127  unsigned char __cil_tmp23 ;
3128  int __cil_tmp24 ;
3129  unsigned char __cil_tmp25 ;
3130  unsigned long __cil_tmp26 ;
3131  unsigned long __cil_tmp27 ;
3132  unsigned long __cil_tmp28 ;
3133  unsigned int __cil_tmp29 ;
3134  unsigned int __cil_tmp30 ;
3135  int __cil_tmp31 ;
3136  unsigned long __cil_tmp32 ;
3137  unsigned long __cil_tmp33 ;
3138  void *__cil_tmp34 ;
3139  struct parport_private *__cil_tmp35 ;
3140  unsigned long __cil_tmp36 ;
3141  unsigned long __cil_tmp37 ;
3142
3143  {
3144  {
3145#line 300
3146  printk("<7>parport_intr_cancel()\n");
3147#line 302
3148  __cil_tmp3 = (unsigned long )dev;
3149#line 302
3150  __cil_tmp4 = __cil_tmp3 + 16;
3151#line 302
3152  __cil_tmp5 = *((void **)__cil_tmp4);
3153#line 302
3154  __cil_tmp6 = (struct parport_private *)__cil_tmp5;
3155#line 302
3156  __cil_tmp7 = (unsigned long )__cil_tmp6;
3157#line 302
3158  __cil_tmp8 = __cil_tmp7 + 4;
3159#line 302
3160  __cil_tmp9 = (unsigned long )dev;
3161#line 302
3162  __cil_tmp10 = __cil_tmp9 + 16;
3163#line 302
3164  __cil_tmp11 = *((void **)__cil_tmp10);
3165#line 302
3166  __cil_tmp12 = (struct parport_private *)__cil_tmp11;
3167#line 302
3168  __cil_tmp13 = (unsigned long )__cil_tmp12;
3169#line 302
3170  __cil_tmp14 = __cil_tmp13 + 4;
3171#line 302
3172  __cil_tmp15 = *((unsigned int *)__cil_tmp14);
3173#line 302
3174  *((unsigned int *)__cil_tmp8) = __cil_tmp15 & 4294967279U;
3175#line 303
3176  __cil_tmp16 = (unsigned long )dev;
3177#line 303
3178  __cil_tmp17 = __cil_tmp16 + 16;
3179#line 303
3180  __cil_tmp18 = *((void **)__cil_tmp17);
3181#line 303
3182  __cil_tmp19 = (struct parport_private *)__cil_tmp18;
3183#line 303
3184  __cil_tmp20 = (unsigned long )__cil_tmp19;
3185#line 303
3186  __cil_tmp21 = __cil_tmp20 + 4;
3187#line 303
3188  __cil_tmp22 = *((unsigned int *)__cil_tmp21);
3189#line 303
3190  __cil_tmp23 = (unsigned char )__cil_tmp22;
3191#line 303
3192  __cil_tmp24 = (int )__cil_tmp23;
3193#line 303
3194  __cil_tmp25 = (unsigned char )__cil_tmp24;
3195#line 303
3196  __cil_tmp26 = (unsigned long )dev;
3197#line 303
3198  __cil_tmp27 = __cil_tmp26 + 328;
3199#line 303
3200  __cil_tmp28 = *((unsigned long *)__cil_tmp27);
3201#line 303
3202  __cil_tmp29 = (unsigned int )__cil_tmp28;
3203#line 303
3204  __cil_tmp30 = __cil_tmp29 + 2U;
3205#line 303
3206  __cil_tmp31 = (int )__cil_tmp30;
3207#line 303
3208  outb(__cil_tmp25, __cil_tmp31);
3209#line 305
3210  __cil_tmp32 = (unsigned long )dev;
3211#line 305
3212  __cil_tmp33 = __cil_tmp32 + 16;
3213#line 305
3214  __cil_tmp34 = *((void **)__cil_tmp33);
3215#line 305
3216  __cil_tmp35 = (struct parport_private *)__cil_tmp34;
3217#line 305
3218  __cil_tmp36 = (unsigned long )__cil_tmp35;
3219#line 305
3220  __cil_tmp37 = __cil_tmp36 + 8;
3221#line 305
3222  *((int *)__cil_tmp37) = 0;
3223  }
3224#line 307
3225  return (0);
3226}
3227}
3228#line 310 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
3229static irqreturn_t parport_interrupt(int irq , void *d ) 
3230{ struct comedi_device *dev ;
3231  struct comedi_subdevice *s ;
3232  unsigned long __cil_tmp5 ;
3233  unsigned long __cil_tmp6 ;
3234  struct comedi_subdevice *__cil_tmp7 ;
3235  unsigned long __cil_tmp8 ;
3236  unsigned long __cil_tmp9 ;
3237  void *__cil_tmp10 ;
3238  struct parport_private *__cil_tmp11 ;
3239  unsigned long __cil_tmp12 ;
3240  unsigned long __cil_tmp13 ;
3241  int __cil_tmp14 ;
3242  unsigned long __cil_tmp15 ;
3243  unsigned long __cil_tmp16 ;
3244  struct comedi_async *__cil_tmp17 ;
3245  unsigned long __cil_tmp18 ;
3246  unsigned long __cil_tmp19 ;
3247  struct comedi_async *__cil_tmp20 ;
3248  unsigned long __cil_tmp21 ;
3249  unsigned long __cil_tmp22 ;
3250  unsigned long __cil_tmp23 ;
3251  unsigned long __cil_tmp24 ;
3252  struct comedi_async *__cil_tmp25 ;
3253  unsigned long __cil_tmp26 ;
3254  unsigned long __cil_tmp27 ;
3255  unsigned int __cil_tmp28 ;
3256
3257  {
3258#line 312
3259  dev = (struct comedi_device *)d;
3260#line 313
3261  __cil_tmp5 = (unsigned long )dev;
3262#line 313
3263  __cil_tmp6 = __cil_tmp5 + 320;
3264#line 313
3265  __cil_tmp7 = *((struct comedi_subdevice **)__cil_tmp6);
3266#line 313
3267  s = __cil_tmp7 + 3UL;
3268  {
3269#line 315
3270  __cil_tmp8 = (unsigned long )dev;
3271#line 315
3272  __cil_tmp9 = __cil_tmp8 + 16;
3273#line 315
3274  __cil_tmp10 = *((void **)__cil_tmp9);
3275#line 315
3276  __cil_tmp11 = (struct parport_private *)__cil_tmp10;
3277#line 315
3278  __cil_tmp12 = (unsigned long )__cil_tmp11;
3279#line 315
3280  __cil_tmp13 = __cil_tmp12 + 8;
3281#line 315
3282  __cil_tmp14 = *((int *)__cil_tmp13);
3283#line 315
3284  if (__cil_tmp14 == 0) {
3285    {
3286#line 316
3287    printk("<3>comedi_parport: bogus irq, ignored\n");
3288    }
3289#line 317
3290    return ((irqreturn_t )0);
3291  } else {
3292
3293  }
3294  }
3295  {
3296#line 320
3297  __cil_tmp15 = (unsigned long )s;
3298#line 320
3299  __cil_tmp16 = __cil_tmp15 + 32;
3300#line 320
3301  __cil_tmp17 = *((struct comedi_async **)__cil_tmp16);
3302#line 320
3303  comedi_buf_put(__cil_tmp17, (short)0);
3304#line 321
3305  __cil_tmp18 = (unsigned long )s;
3306#line 321
3307  __cil_tmp19 = __cil_tmp18 + 32;
3308#line 321
3309  __cil_tmp20 = *((struct comedi_async **)__cil_tmp19);
3310#line 321
3311  __cil_tmp21 = (unsigned long )__cil_tmp20;
3312#line 321
3313  __cil_tmp22 = __cil_tmp21 + 88;
3314#line 321
3315  __cil_tmp23 = (unsigned long )s;
3316#line 321
3317  __cil_tmp24 = __cil_tmp23 + 32;
3318#line 321
3319  __cil_tmp25 = *((struct comedi_async **)__cil_tmp24);
3320#line 321
3321  __cil_tmp26 = (unsigned long )__cil_tmp25;
3322#line 321
3323  __cil_tmp27 = __cil_tmp26 + 88;
3324#line 321
3325  __cil_tmp28 = *((unsigned int *)__cil_tmp27);
3326#line 321
3327  *((unsigned int *)__cil_tmp22) = __cil_tmp28 | 5U;
3328#line 323
3329  comedi_event(dev, s);
3330  }
3331#line 324
3332  return ((irqreturn_t )1);
3333}
3334}
3335#line 327 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
3336static int parport_attach(struct comedi_device *dev , struct comedi_devconfig *it ) 
3337{ int ret ;
3338  unsigned int irq ;
3339  unsigned long iobase ;
3340  struct comedi_subdevice *s ;
3341  struct resource *tmp ;
3342  unsigned long __cil_tmp8 ;
3343  unsigned long __cil_tmp9 ;
3344  unsigned long __cil_tmp10 ;
3345  unsigned long __cil_tmp11 ;
3346  int __cil_tmp12 ;
3347  unsigned long __cil_tmp13 ;
3348  unsigned long __cil_tmp14 ;
3349  int __cil_tmp15 ;
3350  resource_size_t __cil_tmp16 ;
3351  struct resource *__cil_tmp17 ;
3352  unsigned long __cil_tmp18 ;
3353  unsigned long __cil_tmp19 ;
3354  unsigned long __cil_tmp20 ;
3355  unsigned long __cil_tmp21 ;
3356  unsigned long __cil_tmp22 ;
3357  unsigned long __cil_tmp23 ;
3358  unsigned long __cil_tmp24 ;
3359  unsigned long __cil_tmp25 ;
3360  int __cil_tmp26 ;
3361  void *__cil_tmp27 ;
3362  unsigned long __cil_tmp28 ;
3363  unsigned long __cil_tmp29 ;
3364  unsigned long __cil_tmp30 ;
3365  unsigned long __cil_tmp31 ;
3366  unsigned long __cil_tmp32 ;
3367  unsigned long __cil_tmp33 ;
3368  unsigned long __cil_tmp34 ;
3369  unsigned long __cil_tmp35 ;
3370  unsigned long __cil_tmp36 ;
3371  unsigned long __cil_tmp37 ;
3372  unsigned long __cil_tmp38 ;
3373  unsigned long __cil_tmp39 ;
3374  unsigned long __cil_tmp40 ;
3375  unsigned long __cil_tmp41 ;
3376  unsigned long __cil_tmp42 ;
3377  unsigned long __cil_tmp43 ;
3378  unsigned long __cil_tmp44 ;
3379  unsigned long __cil_tmp45 ;
3380  unsigned long __cil_tmp46 ;
3381  unsigned long __cil_tmp47 ;
3382  unsigned long __cil_tmp48 ;
3383  unsigned long __cil_tmp49 ;
3384  struct comedi_subdevice *__cil_tmp50 ;
3385  unsigned long __cil_tmp51 ;
3386  unsigned long __cil_tmp52 ;
3387  unsigned long __cil_tmp53 ;
3388  unsigned long __cil_tmp54 ;
3389  unsigned long __cil_tmp55 ;
3390  unsigned long __cil_tmp56 ;
3391  unsigned long __cil_tmp57 ;
3392  unsigned long __cil_tmp58 ;
3393  unsigned long __cil_tmp59 ;
3394  unsigned long __cil_tmp60 ;
3395  unsigned long __cil_tmp61 ;
3396  unsigned long __cil_tmp62 ;
3397  unsigned long __cil_tmp63 ;
3398  unsigned long __cil_tmp64 ;
3399  struct comedi_subdevice *__cil_tmp65 ;
3400  unsigned long __cil_tmp66 ;
3401  unsigned long __cil_tmp67 ;
3402  unsigned long __cil_tmp68 ;
3403  unsigned long __cil_tmp69 ;
3404  unsigned long __cil_tmp70 ;
3405  unsigned long __cil_tmp71 ;
3406  unsigned long __cil_tmp72 ;
3407  unsigned long __cil_tmp73 ;
3408  unsigned long __cil_tmp74 ;
3409  unsigned long __cil_tmp75 ;
3410  unsigned long __cil_tmp76 ;
3411  unsigned long __cil_tmp77 ;
3412  unsigned long __cil_tmp78 ;
3413  unsigned long __cil_tmp79 ;
3414  struct comedi_subdevice *__cil_tmp80 ;
3415  unsigned long __cil_tmp81 ;
3416  unsigned long __cil_tmp82 ;
3417  unsigned long __cil_tmp83 ;
3418  unsigned long __cil_tmp84 ;
3419  unsigned long __cil_tmp85 ;
3420  unsigned long __cil_tmp86 ;
3421  unsigned long __cil_tmp87 ;
3422  unsigned long __cil_tmp88 ;
3423  unsigned long __cil_tmp89 ;
3424  unsigned long __cil_tmp90 ;
3425  unsigned long __cil_tmp91 ;
3426  unsigned long __cil_tmp92 ;
3427  unsigned long __cil_tmp93 ;
3428  unsigned long __cil_tmp94 ;
3429  unsigned long __cil_tmp95 ;
3430  unsigned long __cil_tmp96 ;
3431  unsigned long __cil_tmp97 ;
3432  unsigned long __cil_tmp98 ;
3433  unsigned long __cil_tmp99 ;
3434  unsigned long __cil_tmp100 ;
3435  unsigned long __cil_tmp101 ;
3436  unsigned long __cil_tmp102 ;
3437  unsigned long __cil_tmp103 ;
3438  unsigned long __cil_tmp104 ;
3439  void *__cil_tmp105 ;
3440  struct parport_private *__cil_tmp106 ;
3441  unsigned long __cil_tmp107 ;
3442  unsigned long __cil_tmp108 ;
3443  void *__cil_tmp109 ;
3444  struct parport_private *__cil_tmp110 ;
3445  unsigned int __cil_tmp111 ;
3446  unsigned char __cil_tmp112 ;
3447  int __cil_tmp113 ;
3448  unsigned char __cil_tmp114 ;
3449  unsigned long __cil_tmp115 ;
3450  unsigned long __cil_tmp116 ;
3451  unsigned long __cil_tmp117 ;
3452  int __cil_tmp118 ;
3453  unsigned long __cil_tmp119 ;
3454  unsigned long __cil_tmp120 ;
3455  void *__cil_tmp121 ;
3456  struct parport_private *__cil_tmp122 ;
3457  unsigned long __cil_tmp123 ;
3458  unsigned long __cil_tmp124 ;
3459  unsigned long __cil_tmp125 ;
3460  unsigned long __cil_tmp126 ;
3461  void *__cil_tmp127 ;
3462  struct parport_private *__cil_tmp128 ;
3463  unsigned long __cil_tmp129 ;
3464  unsigned long __cil_tmp130 ;
3465  unsigned int __cil_tmp131 ;
3466  unsigned char __cil_tmp132 ;
3467  int __cil_tmp133 ;
3468  unsigned char __cil_tmp134 ;
3469  unsigned long __cil_tmp135 ;
3470  unsigned long __cil_tmp136 ;
3471  unsigned long __cil_tmp137 ;
3472  unsigned int __cil_tmp138 ;
3473  unsigned int __cil_tmp139 ;
3474  int __cil_tmp140 ;
3475
3476  {
3477  {
3478#line 335
3479  __cil_tmp8 = 0 * 4UL;
3480#line 335
3481  __cil_tmp9 = 20 + __cil_tmp8;
3482#line 335
3483  __cil_tmp10 = (unsigned long )it;
3484#line 335
3485  __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
3486#line 335
3487  __cil_tmp12 = *((int *)__cil_tmp11);
3488#line 335
3489  iobase = (unsigned long )__cil_tmp12;
3490#line 336
3491  __cil_tmp13 = (unsigned long )dev;
3492#line 336
3493  __cil_tmp14 = __cil_tmp13 + 32;
3494#line 336
3495  __cil_tmp15 = *((int *)__cil_tmp14);
3496#line 336
3497  printk("<6>comedi%d: parport: 0x%04lx ", __cil_tmp15, iobase);
3498#line 337
3499  __cil_tmp16 = (resource_size_t )iobase;
3500#line 337
3501  tmp = __request_region(& ioport_resource, __cil_tmp16, 3ULL, "parport (comedi)",
3502                         0);
3503  }
3504  {
3505#line 337
3506  __cil_tmp17 = (struct resource *)0;
3507#line 337
3508  __cil_tmp18 = (unsigned long )__cil_tmp17;
3509#line 337
3510  __cil_tmp19 = (unsigned long )tmp;
3511#line 337
3512  if (__cil_tmp19 == __cil_tmp18) {
3513    {
3514#line 338
3515    printk("<3>I/O port conflict\n");
3516    }
3517#line 339
3518    return (-5);
3519  } else {
3520
3521  }
3522  }
3523#line 341
3524  __cil_tmp20 = (unsigned long )dev;
3525#line 341
3526  __cil_tmp21 = __cil_tmp20 + 328;
3527#line 341
3528  *((unsigned long *)__cil_tmp21) = iobase;
3529#line 343
3530  __cil_tmp22 = 1 * 4UL;
3531#line 343
3532  __cil_tmp23 = 20 + __cil_tmp22;
3533#line 343
3534  __cil_tmp24 = (unsigned long )it;
3535#line 343
3536  __cil_tmp25 = __cil_tmp24 + __cil_tmp23;
3537#line 343
3538  __cil_tmp26 = *((int *)__cil_tmp25);
3539#line 343
3540  irq = (unsigned int )__cil_tmp26;
3541#line 344
3542  if (irq != 0U) {
3543    {
3544#line 345
3545    printk("<6> irq=%u", irq);
3546#line 346
3547    __cil_tmp27 = (void *)dev;
3548#line 346
3549    ret = request_irq(irq, & parport_interrupt, 0UL, "comedi_parport", __cil_tmp27);
3550    }
3551#line 348
3552    if (ret < 0) {
3553      {
3554#line 349
3555      printk("<3> irq not available\n");
3556      }
3557#line 350
3558      return (-22);
3559    } else {
3560
3561    }
3562#line 352
3563    __cil_tmp28 = (unsigned long )dev;
3564#line 352
3565    __cil_tmp29 = __cil_tmp28 + 336;
3566#line 352
3567    *((unsigned int *)__cil_tmp29) = irq;
3568  } else {
3569
3570  }
3571  {
3572#line 354
3573  __cil_tmp30 = (unsigned long )dev;
3574#line 354
3575  __cil_tmp31 = __cil_tmp30 + 48;
3576#line 354
3577  *((char const   **)__cil_tmp31) = "parport";
3578#line 356
3579  ret = alloc_subdevices(dev, 4U);
3580  }
3581#line 357
3582  if (ret < 0) {
3583#line 358
3584    return (ret);
3585  } else {
3586
3587  }
3588  {
3589#line 359
3590  ret = alloc_private(dev, 12);
3591  }
3592#line 360
3593  if (ret < 0) {
3594#line 361
3595    return (ret);
3596  } else {
3597
3598  }
3599#line 363
3600  __cil_tmp32 = (unsigned long )dev;
3601#line 363
3602  __cil_tmp33 = __cil_tmp32 + 320;
3603#line 363
3604  s = *((struct comedi_subdevice **)__cil_tmp33);
3605#line 364
3606  __cil_tmp34 = (unsigned long )s;
3607#line 364
3608  __cil_tmp35 = __cil_tmp34 + 8;
3609#line 364
3610  *((int *)__cil_tmp35) = 5;
3611#line 365
3612  __cil_tmp36 = (unsigned long )s;
3613#line 365
3614  __cil_tmp37 = __cil_tmp36 + 16;
3615#line 365
3616  *((int *)__cil_tmp37) = 196608;
3617#line 366
3618  __cil_tmp38 = (unsigned long )s;
3619#line 366
3620  __cil_tmp39 = __cil_tmp38 + 12;
3621#line 366
3622  *((int *)__cil_tmp39) = 8;
3623#line 367
3624  __cil_tmp40 = (unsigned long )s;
3625#line 367
3626  __cil_tmp41 = __cil_tmp40 + 140;
3627#line 367
3628  *((unsigned int *)__cil_tmp41) = 1U;
3629#line 368
3630  __cil_tmp42 = (unsigned long )s;
3631#line 368
3632  __cil_tmp43 = __cil_tmp42 + 176;
3633#line 368
3634  *((struct comedi_lrange  const  **)__cil_tmp43) = & range_unipolar5;
3635#line 369
3636  __cil_tmp44 = (unsigned long )s;
3637#line 369
3638  __cil_tmp45 = __cil_tmp44 + 216;
3639#line 369
3640  *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
3641              unsigned int * ))__cil_tmp45) = & parport_insn_a;
3642#line 370
3643  __cil_tmp46 = (unsigned long )s;
3644#line 370
3645  __cil_tmp47 = __cil_tmp46 + 224;
3646#line 370
3647  *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
3648              unsigned int * ))__cil_tmp47) = & parport_insn_config_a;
3649#line 372
3650  __cil_tmp48 = (unsigned long )dev;
3651#line 372
3652  __cil_tmp49 = __cil_tmp48 + 320;
3653#line 372
3654  __cil_tmp50 = *((struct comedi_subdevice **)__cil_tmp49);
3655#line 372
3656  s = __cil_tmp50 + 1UL;
3657#line 373
3658  __cil_tmp51 = (unsigned long )s;
3659#line 373
3660  __cil_tmp52 = __cil_tmp51 + 8;
3661#line 373
3662  *((int *)__cil_tmp52) = 3;
3663#line 374
3664  __cil_tmp53 = (unsigned long )s;
3665#line 374
3666  __cil_tmp54 = __cil_tmp53 + 16;
3667#line 374
3668  *((int *)__cil_tmp54) = 65536;
3669#line 375
3670  __cil_tmp55 = (unsigned long )s;
3671#line 375
3672  __cil_tmp56 = __cil_tmp55 + 12;
3673#line 375
3674  *((int *)__cil_tmp56) = 5;
3675#line 376
3676  __cil_tmp57 = (unsigned long )s;
3677#line 376
3678  __cil_tmp58 = __cil_tmp57 + 140;
3679#line 376
3680  *((unsigned int *)__cil_tmp58) = 1U;
3681#line 377
3682  __cil_tmp59 = (unsigned long )s;
3683#line 377
3684  __cil_tmp60 = __cil_tmp59 + 176;
3685#line 377
3686  *((struct comedi_lrange  const  **)__cil_tmp60) = & range_unipolar5;
3687#line 378
3688  __cil_tmp61 = (unsigned long )s;
3689#line 378
3690  __cil_tmp62 = __cil_tmp61 + 216;
3691#line 378
3692  *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
3693              unsigned int * ))__cil_tmp62) = & parport_insn_b;
3694#line 380
3695  __cil_tmp63 = (unsigned long )dev;
3696#line 380
3697  __cil_tmp64 = __cil_tmp63 + 320;
3698#line 380
3699  __cil_tmp65 = *((struct comedi_subdevice **)__cil_tmp64);
3700#line 380
3701  s = __cil_tmp65 + 2UL;
3702#line 381
3703  __cil_tmp66 = (unsigned long )s;
3704#line 381
3705  __cil_tmp67 = __cil_tmp66 + 8;
3706#line 381
3707  *((int *)__cil_tmp67) = 4;
3708#line 382
3709  __cil_tmp68 = (unsigned long )s;
3710#line 382
3711  __cil_tmp69 = __cil_tmp68 + 16;
3712#line 382
3713  *((int *)__cil_tmp69) = 131072;
3714#line 383
3715  __cil_tmp70 = (unsigned long )s;
3716#line 383
3717  __cil_tmp71 = __cil_tmp70 + 12;
3718#line 383
3719  *((int *)__cil_tmp71) = 4;
3720#line 384
3721  __cil_tmp72 = (unsigned long )s;
3722#line 384
3723  __cil_tmp73 = __cil_tmp72 + 140;
3724#line 384
3725  *((unsigned int *)__cil_tmp73) = 1U;
3726#line 385
3727  __cil_tmp74 = (unsigned long )s;
3728#line 385
3729  __cil_tmp75 = __cil_tmp74 + 176;
3730#line 385
3731  *((struct comedi_lrange  const  **)__cil_tmp75) = & range_unipolar5;
3732#line 386
3733  __cil_tmp76 = (unsigned long )s;
3734#line 386
3735  __cil_tmp77 = __cil_tmp76 + 216;
3736#line 386
3737  *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
3738              unsigned int * ))__cil_tmp77) = & parport_insn_c;
3739#line 388
3740  __cil_tmp78 = (unsigned long )dev;
3741#line 388
3742  __cil_tmp79 = __cil_tmp78 + 320;
3743#line 388
3744  __cil_tmp80 = *((struct comedi_subdevice **)__cil_tmp79);
3745#line 388
3746  s = __cil_tmp80 + 3UL;
3747#line 389
3748  if (irq != 0U) {
3749#line 390
3750    __cil_tmp81 = (unsigned long )dev;
3751#line 390
3752    __cil_tmp82 = __cil_tmp81 + 344;
3753#line 390
3754    *((struct comedi_subdevice **)__cil_tmp82) = s;
3755#line 391
3756    __cil_tmp83 = (unsigned long )s;
3757#line 391
3758    __cil_tmp84 = __cil_tmp83 + 8;
3759#line 391
3760    *((int *)__cil_tmp84) = 3;
3761#line 392
3762    __cil_tmp85 = (unsigned long )s;
3763#line 392
3764    __cil_tmp86 = __cil_tmp85 + 16;
3765#line 392
3766    *((int *)__cil_tmp86) = 98304;
3767#line 393
3768    __cil_tmp87 = (unsigned long )s;
3769#line 393
3770    __cil_tmp88 = __cil_tmp87 + 12;
3771#line 393
3772    *((int *)__cil_tmp88) = 1;
3773#line 394
3774    __cil_tmp89 = (unsigned long )s;
3775#line 394
3776    __cil_tmp90 = __cil_tmp89 + 140;
3777#line 394
3778    *((unsigned int *)__cil_tmp90) = 1U;
3779#line 395
3780    __cil_tmp91 = (unsigned long )s;
3781#line 395
3782    __cil_tmp92 = __cil_tmp91 + 176;
3783#line 395
3784    *((struct comedi_lrange  const  **)__cil_tmp92) = & range_unipolar5;
3785#line 396
3786    __cil_tmp93 = (unsigned long )s;
3787#line 396
3788    __cil_tmp94 = __cil_tmp93 + 216;
3789#line 396
3790    *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_insn * ,
3791                unsigned int * ))__cil_tmp94) = & parport_intr_insn;
3792#line 397
3793    __cil_tmp95 = (unsigned long )s;
3794#line 397
3795    __cil_tmp96 = __cil_tmp95 + 240;
3796#line 397
3797    *((int (**)(struct comedi_device * , struct comedi_subdevice * , struct comedi_cmd * ))__cil_tmp96) = & parport_intr_cmdtest;
3798#line 398
3799    __cil_tmp97 = (unsigned long )s;
3800#line 398
3801    __cil_tmp98 = __cil_tmp97 + 232;
3802#line 398
3803    *((int (**)(struct comedi_device * , struct comedi_subdevice * ))__cil_tmp98) = & parport_intr_cmd;
3804#line 399
3805    __cil_tmp99 = (unsigned long )s;
3806#line 399
3807    __cil_tmp100 = __cil_tmp99 + 256;
3808#line 399
3809    *((int (**)(struct comedi_device * , struct comedi_subdevice * ))__cil_tmp100) = & parport_intr_cancel;
3810  } else {
3811#line 401
3812    __cil_tmp101 = (unsigned long )s;
3813#line 401
3814    __cil_tmp102 = __cil_tmp101 + 8;
3815#line 401
3816    *((int *)__cil_tmp102) = 0;
3817  }
3818  {
3819#line 404
3820  __cil_tmp103 = (unsigned long )dev;
3821#line 404
3822  __cil_tmp104 = __cil_tmp103 + 16;
3823#line 404
3824  __cil_tmp105 = *((void **)__cil_tmp104);
3825#line 404
3826  __cil_tmp106 = (struct parport_private *)__cil_tmp105;
3827#line 404
3828  *((unsigned int *)__cil_tmp106) = 0U;
3829#line 405
3830  __cil_tmp107 = (unsigned long )dev;
3831#line 405
3832  __cil_tmp108 = __cil_tmp107 + 16;
3833#line 405
3834  __cil_tmp109 = *((void **)__cil_tmp108);
3835#line 405
3836  __cil_tmp110 = (struct parport_private *)__cil_tmp109;
3837#line 405
3838  __cil_tmp111 = *((unsigned int *)__cil_tmp110);
3839#line 405
3840  __cil_tmp112 = (unsigned char )__cil_tmp111;
3841#line 405
3842  __cil_tmp113 = (int )__cil_tmp112;
3843#line 405
3844  __cil_tmp114 = (unsigned char )__cil_tmp113;
3845#line 405
3846  __cil_tmp115 = (unsigned long )dev;
3847#line 405
3848  __cil_tmp116 = __cil_tmp115 + 328;
3849#line 405
3850  __cil_tmp117 = *((unsigned long *)__cil_tmp116);
3851#line 405
3852  __cil_tmp118 = (int )__cil_tmp117;
3853#line 405
3854  outb(__cil_tmp114, __cil_tmp118);
3855#line 406
3856  __cil_tmp119 = (unsigned long )dev;
3857#line 406
3858  __cil_tmp120 = __cil_tmp119 + 16;
3859#line 406
3860  __cil_tmp121 = *((void **)__cil_tmp120);
3861#line 406
3862  __cil_tmp122 = (struct parport_private *)__cil_tmp121;
3863#line 406
3864  __cil_tmp123 = (unsigned long )__cil_tmp122;
3865#line 406
3866  __cil_tmp124 = __cil_tmp123 + 4;
3867#line 406
3868  *((unsigned int *)__cil_tmp124) = 0U;
3869#line 407
3870  __cil_tmp125 = (unsigned long )dev;
3871#line 407
3872  __cil_tmp126 = __cil_tmp125 + 16;
3873#line 407
3874  __cil_tmp127 = *((void **)__cil_tmp126);
3875#line 407
3876  __cil_tmp128 = (struct parport_private *)__cil_tmp127;
3877#line 407
3878  __cil_tmp129 = (unsigned long )__cil_tmp128;
3879#line 407
3880  __cil_tmp130 = __cil_tmp129 + 4;
3881#line 407
3882  __cil_tmp131 = *((unsigned int *)__cil_tmp130);
3883#line 407
3884  __cil_tmp132 = (unsigned char )__cil_tmp131;
3885#line 407
3886  __cil_tmp133 = (int )__cil_tmp132;
3887#line 407
3888  __cil_tmp134 = (unsigned char )__cil_tmp133;
3889#line 407
3890  __cil_tmp135 = (unsigned long )dev;
3891#line 407
3892  __cil_tmp136 = __cil_tmp135 + 328;
3893#line 407
3894  __cil_tmp137 = *((unsigned long *)__cil_tmp136);
3895#line 407
3896  __cil_tmp138 = (unsigned int )__cil_tmp137;
3897#line 407
3898  __cil_tmp139 = __cil_tmp138 + 2U;
3899#line 407
3900  __cil_tmp140 = (int )__cil_tmp139;
3901#line 407
3902  outb(__cil_tmp134, __cil_tmp140);
3903#line 409
3904  printk("<6>\n");
3905  }
3906#line 410
3907  return (1);
3908}
3909}
3910#line 413 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
3911static int parport_detach(struct comedi_device *dev ) 
3912{ unsigned long __cil_tmp2 ;
3913  unsigned long __cil_tmp3 ;
3914  int __cil_tmp4 ;
3915  unsigned long __cil_tmp5 ;
3916  unsigned long __cil_tmp6 ;
3917  unsigned long __cil_tmp7 ;
3918  unsigned long __cil_tmp8 ;
3919  unsigned long __cil_tmp9 ;
3920  unsigned long __cil_tmp10 ;
3921  resource_size_t __cil_tmp11 ;
3922  unsigned long __cil_tmp12 ;
3923  unsigned long __cil_tmp13 ;
3924  unsigned int __cil_tmp14 ;
3925  unsigned long __cil_tmp15 ;
3926  unsigned long __cil_tmp16 ;
3927  unsigned int __cil_tmp17 ;
3928  void *__cil_tmp18 ;
3929
3930  {
3931  {
3932#line 415
3933  __cil_tmp2 = (unsigned long )dev;
3934#line 415
3935  __cil_tmp3 = __cil_tmp2 + 32;
3936#line 415
3937  __cil_tmp4 = *((int *)__cil_tmp3);
3938#line 415
3939  printk("<6>comedi%d: parport: remove\n", __cil_tmp4);
3940  }
3941  {
3942#line 417
3943  __cil_tmp5 = (unsigned long )dev;
3944#line 417
3945  __cil_tmp6 = __cil_tmp5 + 328;
3946#line 417
3947  __cil_tmp7 = *((unsigned long *)__cil_tmp6);
3948#line 417
3949  if (__cil_tmp7 != 0UL) {
3950    {
3951#line 418
3952    __cil_tmp8 = (unsigned long )dev;
3953#line 418
3954    __cil_tmp9 = __cil_tmp8 + 328;
3955#line 418
3956    __cil_tmp10 = *((unsigned long *)__cil_tmp9);
3957#line 418
3958    __cil_tmp11 = (resource_size_t )__cil_tmp10;
3959#line 418
3960    __release_region(& ioport_resource, __cil_tmp11, 3ULL);
3961    }
3962  } else {
3963
3964  }
3965  }
3966  {
3967#line 420
3968  __cil_tmp12 = (unsigned long )dev;
3969#line 420
3970  __cil_tmp13 = __cil_tmp12 + 336;
3971#line 420
3972  __cil_tmp14 = *((unsigned int *)__cil_tmp13);
3973#line 420
3974  if (__cil_tmp14 != 0U) {
3975    {
3976#line 421
3977    __cil_tmp15 = (unsigned long )dev;
3978#line 421
3979    __cil_tmp16 = __cil_tmp15 + 336;
3980#line 421
3981    __cil_tmp17 = *((unsigned int *)__cil_tmp16);
3982#line 421
3983    __cil_tmp18 = (void *)dev;
3984#line 421
3985    free_irq(__cil_tmp17, __cil_tmp18);
3986    }
3987  } else {
3988
3989  }
3990  }
3991#line 423
3992  return (0);
3993}
3994}
3995#line 446
3996extern void ldv_check_final_state(void) ;
3997#line 452
3998extern void ldv_initialize(void) ;
3999#line 455
4000extern int __VERIFIER_nondet_int(void) ;
4001#line 458 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4002int LDV_IN_INTERRUPT  ;
4003#line 461 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4004void main(void) 
4005{ struct comedi_device *var_group1 ;
4006  struct comedi_devconfig *var_group2 ;
4007  int var_parport_interrupt_10_p0 ;
4008  void *var_parport_interrupt_10_p1 ;
4009  int tmp ;
4010  int tmp___0 ;
4011  int tmp___1 ;
4012
4013  {
4014  {
4015#line 509
4016  LDV_IN_INTERRUPT = 1;
4017#line 518
4018  ldv_initialize();
4019#line 529
4020  tmp = driver_parport_init_module();
4021  }
4022#line 529
4023  if (tmp != 0) {
4024#line 530
4025    goto ldv_final;
4026  } else {
4027
4028  }
4029#line 539
4030  goto ldv_20819;
4031  ldv_20818: 
4032  {
4033#line 542
4034  tmp___0 = __VERIFIER_nondet_int();
4035  }
4036#line 544
4037  if (tmp___0 == 0) {
4038#line 544
4039    goto case_0;
4040  } else
4041#line 566
4042  if (tmp___0 == 1) {
4043#line 566
4044    goto case_1;
4045  } else
4046#line 588
4047  if (tmp___0 == 2) {
4048#line 588
4049    goto case_2;
4050  } else {
4051    {
4052#line 610
4053    goto switch_default;
4054#line 542
4055    if (0) {
4056      case_0: /* CIL Label */ 
4057      {
4058#line 558
4059      parport_attach(var_group1, var_group2);
4060      }
4061#line 565
4062      goto ldv_20814;
4063      case_1: /* CIL Label */ 
4064      {
4065#line 580
4066      parport_detach(var_group1);
4067      }
4068#line 587
4069      goto ldv_20814;
4070      case_2: /* CIL Label */ 
4071      {
4072#line 591
4073      LDV_IN_INTERRUPT = 2;
4074#line 602
4075      parport_interrupt(var_parport_interrupt_10_p0, var_parport_interrupt_10_p1);
4076#line 603
4077      LDV_IN_INTERRUPT = 1;
4078      }
4079#line 609
4080      goto ldv_20814;
4081      switch_default: /* CIL Label */ ;
4082#line 610
4083      goto ldv_20814;
4084    } else {
4085      switch_break: /* CIL Label */ ;
4086    }
4087    }
4088  }
4089  ldv_20814: ;
4090  ldv_20819: 
4091  {
4092#line 539
4093  tmp___1 = __VERIFIER_nondet_int();
4094  }
4095#line 539
4096  if (tmp___1 != 0) {
4097#line 540
4098    goto ldv_20818;
4099  } else {
4100#line 542
4101    goto ldv_20820;
4102  }
4103  ldv_20820: ;
4104  {
4105#line 627
4106  driver_parport_cleanup_module();
4107  }
4108  ldv_final: 
4109  {
4110#line 633
4111  ldv_check_final_state();
4112  }
4113#line 636
4114  return;
4115}
4116}
4117#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4118void ldv_blast_assert(void) 
4119{ 
4120
4121  {
4122  ERROR: ;
4123#line 6
4124  goto ERROR;
4125}
4126}
4127#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4128extern int __VERIFIER_nondet_int(void) ;
4129#line 657 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4130int ldv_spin  =    0;
4131#line 661 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4132void ldv_check_alloc_flags(gfp_t flags ) 
4133{ 
4134
4135  {
4136#line 664
4137  if (ldv_spin != 0) {
4138#line 664
4139    if (flags != 32U) {
4140      {
4141#line 664
4142      ldv_blast_assert();
4143      }
4144    } else {
4145
4146    }
4147  } else {
4148
4149  }
4150#line 667
4151  return;
4152}
4153}
4154#line 667
4155extern struct page *ldv_some_page(void) ;
4156#line 670 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4157struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
4158{ struct page *tmp ;
4159
4160  {
4161#line 673
4162  if (ldv_spin != 0) {
4163#line 673
4164    if (flags != 32U) {
4165      {
4166#line 673
4167      ldv_blast_assert();
4168      }
4169    } else {
4170
4171    }
4172  } else {
4173
4174  }
4175  {
4176#line 675
4177  tmp = ldv_some_page();
4178  }
4179#line 675
4180  return (tmp);
4181}
4182}
4183#line 679 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4184void ldv_check_alloc_nonatomic(void) 
4185{ 
4186
4187  {
4188#line 682
4189  if (ldv_spin != 0) {
4190    {
4191#line 682
4192    ldv_blast_assert();
4193    }
4194  } else {
4195
4196  }
4197#line 685
4198  return;
4199}
4200}
4201#line 686 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4202void ldv_spin_lock(void) 
4203{ 
4204
4205  {
4206#line 689
4207  ldv_spin = 1;
4208#line 690
4209  return;
4210}
4211}
4212#line 693 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4213void ldv_spin_unlock(void) 
4214{ 
4215
4216  {
4217#line 696
4218  ldv_spin = 0;
4219#line 697
4220  return;
4221}
4222}
4223#line 700 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4224int ldv_spin_trylock(void) 
4225{ int is_lock ;
4226
4227  {
4228  {
4229#line 705
4230  is_lock = __VERIFIER_nondet_int();
4231  }
4232#line 707
4233  if (is_lock != 0) {
4234#line 710
4235    return (0);
4236  } else {
4237#line 715
4238    ldv_spin = 1;
4239#line 717
4240    return (1);
4241  }
4242}
4243}
4244#line 862 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4245__inline static void *kcalloc(size_t n , size_t size , gfp_t flags ) 
4246{ 
4247
4248  {
4249  {
4250#line 869
4251  ldv_check_alloc_flags(flags);
4252#line 871
4253  ldv_kcalloc_14(n, size, flags);
4254  }
4255#line 872
4256  return ((void *)0);
4257}
4258}
4259#line 884 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4260void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
4261{ 
4262
4263  {
4264  {
4265#line 890
4266  ldv_check_alloc_flags(ldv_func_arg2);
4267#line 892
4268  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
4269  }
4270#line 893
4271  return ((void *)0);
4272}
4273}
4274#line 895 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5920/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/comedi_parport.c.p"
4275__inline static void *kzalloc(size_t size , gfp_t flags ) 
4276{ void *tmp ;
4277
4278  {
4279  {
4280#line 901
4281  ldv_check_alloc_flags(flags);
4282#line 902
4283  tmp = __VERIFIER_nondet_pointer();
4284  }
4285#line 902
4286  return (tmp);
4287}
4288}