Showing error 1069

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--mfd--rdc321x-southbridge.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1851
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 181 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/x86_init.h"
 300struct pci_dev;
 301#line 181
 302struct pci_dev;
 303#line 312 "include/linux/jiffies.h"
 304union ktime {
 305   s64 tv64 ;
 306};
 307#line 59 "include/linux/ktime.h"
 308typedef union ktime ktime_t;
 309#line 341
 310struct tvec_base;
 311#line 341
 312struct tvec_base;
 313#line 342 "include/linux/ktime.h"
 314struct timer_list {
 315   struct list_head entry ;
 316   unsigned long expires ;
 317   struct tvec_base *base ;
 318   void (*function)(unsigned long  ) ;
 319   unsigned long data ;
 320   int slack ;
 321   int start_pid ;
 322   void *start_site ;
 323   char start_comm[16U] ;
 324   struct lockdep_map lockdep_map ;
 325};
 326#line 302 "include/linux/timer.h"
 327struct work_struct;
 328#line 302
 329struct work_struct;
 330#line 45 "include/linux/workqueue.h"
 331struct work_struct {
 332   atomic_long_t data ;
 333   struct list_head entry ;
 334   void (*func)(struct work_struct * ) ;
 335   struct lockdep_map lockdep_map ;
 336};
 337#line 46 "include/linux/pm.h"
 338struct pm_message {
 339   int event ;
 340};
 341#line 52 "include/linux/pm.h"
 342typedef struct pm_message pm_message_t;
 343#line 53 "include/linux/pm.h"
 344struct dev_pm_ops {
 345   int (*prepare)(struct device * ) ;
 346   void (*complete)(struct device * ) ;
 347   int (*suspend)(struct device * ) ;
 348   int (*resume)(struct device * ) ;
 349   int (*freeze)(struct device * ) ;
 350   int (*thaw)(struct device * ) ;
 351   int (*poweroff)(struct device * ) ;
 352   int (*restore)(struct device * ) ;
 353   int (*suspend_late)(struct device * ) ;
 354   int (*resume_early)(struct device * ) ;
 355   int (*freeze_late)(struct device * ) ;
 356   int (*thaw_early)(struct device * ) ;
 357   int (*poweroff_late)(struct device * ) ;
 358   int (*restore_early)(struct device * ) ;
 359   int (*suspend_noirq)(struct device * ) ;
 360   int (*resume_noirq)(struct device * ) ;
 361   int (*freeze_noirq)(struct device * ) ;
 362   int (*thaw_noirq)(struct device * ) ;
 363   int (*poweroff_noirq)(struct device * ) ;
 364   int (*restore_noirq)(struct device * ) ;
 365   int (*runtime_suspend)(struct device * ) ;
 366   int (*runtime_resume)(struct device * ) ;
 367   int (*runtime_idle)(struct device * ) ;
 368};
 369#line 289
 370enum rpm_status {
 371    RPM_ACTIVE = 0,
 372    RPM_RESUMING = 1,
 373    RPM_SUSPENDED = 2,
 374    RPM_SUSPENDING = 3
 375} ;
 376#line 296
 377enum rpm_request {
 378    RPM_REQ_NONE = 0,
 379    RPM_REQ_IDLE = 1,
 380    RPM_REQ_SUSPEND = 2,
 381    RPM_REQ_AUTOSUSPEND = 3,
 382    RPM_REQ_RESUME = 4
 383} ;
 384#line 304
 385struct wakeup_source;
 386#line 304
 387struct wakeup_source;
 388#line 494 "include/linux/pm.h"
 389struct pm_subsys_data {
 390   spinlock_t lock ;
 391   unsigned int refcount ;
 392};
 393#line 499
 394struct dev_pm_qos_request;
 395#line 499
 396struct pm_qos_constraints;
 397#line 499 "include/linux/pm.h"
 398struct dev_pm_info {
 399   pm_message_t power_state ;
 400   unsigned char can_wakeup : 1 ;
 401   unsigned char async_suspend : 1 ;
 402   bool is_prepared ;
 403   bool is_suspended ;
 404   bool ignore_children ;
 405   spinlock_t lock ;
 406   struct list_head entry ;
 407   struct completion completion ;
 408   struct wakeup_source *wakeup ;
 409   bool wakeup_path ;
 410   struct timer_list suspend_timer ;
 411   unsigned long timer_expires ;
 412   struct work_struct work ;
 413   wait_queue_head_t wait_queue ;
 414   atomic_t usage_count ;
 415   atomic_t child_count ;
 416   unsigned char disable_depth : 3 ;
 417   unsigned char idle_notification : 1 ;
 418   unsigned char request_pending : 1 ;
 419   unsigned char deferred_resume : 1 ;
 420   unsigned char run_wake : 1 ;
 421   unsigned char runtime_auto : 1 ;
 422   unsigned char no_callbacks : 1 ;
 423   unsigned char irq_safe : 1 ;
 424   unsigned char use_autosuspend : 1 ;
 425   unsigned char timer_autosuspends : 1 ;
 426   enum rpm_request request ;
 427   enum rpm_status runtime_status ;
 428   int runtime_error ;
 429   int autosuspend_delay ;
 430   unsigned long last_busy ;
 431   unsigned long active_jiffies ;
 432   unsigned long suspended_jiffies ;
 433   unsigned long accounting_timestamp ;
 434   ktime_t suspend_time ;
 435   s64 max_time_suspended_ns ;
 436   struct dev_pm_qos_request *pq_req ;
 437   struct pm_subsys_data *subsys_data ;
 438   struct pm_qos_constraints *constraints ;
 439};
 440#line 558 "include/linux/pm.h"
 441struct dev_pm_domain {
 442   struct dev_pm_ops ops ;
 443};
 444#line 173 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/topology.h"
 445struct pci_bus;
 446#line 173
 447struct pci_bus;
 448#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 449struct __anonstruct_mm_context_t_101 {
 450   void *ldt ;
 451   int size ;
 452   unsigned short ia32_compat ;
 453   struct mutex lock ;
 454   void *vdso ;
 455};
 456#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 457typedef struct __anonstruct_mm_context_t_101 mm_context_t;
 458#line 18 "include/asm-generic/pci_iomap.h"
 459struct vm_area_struct;
 460#line 18
 461struct vm_area_struct;
 462#line 835 "include/linux/sysctl.h"
 463struct rb_node {
 464   unsigned long rb_parent_color ;
 465   struct rb_node *rb_right ;
 466   struct rb_node *rb_left ;
 467};
 468#line 108 "include/linux/rbtree.h"
 469struct rb_root {
 470   struct rb_node *rb_node ;
 471};
 472#line 18 "include/linux/elf.h"
 473typedef __u64 Elf64_Addr;
 474#line 19 "include/linux/elf.h"
 475typedef __u16 Elf64_Half;
 476#line 23 "include/linux/elf.h"
 477typedef __u32 Elf64_Word;
 478#line 24 "include/linux/elf.h"
 479typedef __u64 Elf64_Xword;
 480#line 193 "include/linux/elf.h"
 481struct elf64_sym {
 482   Elf64_Word st_name ;
 483   unsigned char st_info ;
 484   unsigned char st_other ;
 485   Elf64_Half st_shndx ;
 486   Elf64_Addr st_value ;
 487   Elf64_Xword st_size ;
 488};
 489#line 201 "include/linux/elf.h"
 490typedef struct elf64_sym Elf64_Sym;
 491#line 445
 492struct sock;
 493#line 445
 494struct sock;
 495#line 446
 496struct kobject;
 497#line 446
 498struct kobject;
 499#line 447
 500enum kobj_ns_type {
 501    KOBJ_NS_TYPE_NONE = 0,
 502    KOBJ_NS_TYPE_NET = 1,
 503    KOBJ_NS_TYPES = 2
 504} ;
 505#line 453 "include/linux/elf.h"
 506struct kobj_ns_type_operations {
 507   enum kobj_ns_type type ;
 508   void *(*grab_current_ns)(void) ;
 509   void const   *(*netlink_ns)(struct sock * ) ;
 510   void const   *(*initial_ns)(void) ;
 511   void (*drop_ns)(void * ) ;
 512};
 513#line 57 "include/linux/kobject_ns.h"
 514struct attribute {
 515   char const   *name ;
 516   umode_t mode ;
 517   struct lock_class_key *key ;
 518   struct lock_class_key skey ;
 519};
 520#line 33 "include/linux/sysfs.h"
 521struct attribute_group {
 522   char const   *name ;
 523   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 524   struct attribute **attrs ;
 525};
 526#line 62 "include/linux/sysfs.h"
 527struct bin_attribute {
 528   struct attribute attr ;
 529   size_t size ;
 530   void *private ;
 531   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 532                   loff_t  , size_t  ) ;
 533   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 534                    loff_t  , size_t  ) ;
 535   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
 536};
 537#line 98 "include/linux/sysfs.h"
 538struct sysfs_ops {
 539   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 540   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 541   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 542};
 543#line 117
 544struct sysfs_dirent;
 545#line 117
 546struct sysfs_dirent;
 547#line 182 "include/linux/sysfs.h"
 548struct kref {
 549   atomic_t refcount ;
 550};
 551#line 49 "include/linux/kobject.h"
 552struct kset;
 553#line 49
 554struct kobj_type;
 555#line 49 "include/linux/kobject.h"
 556struct kobject {
 557   char const   *name ;
 558   struct list_head entry ;
 559   struct kobject *parent ;
 560   struct kset *kset ;
 561   struct kobj_type *ktype ;
 562   struct sysfs_dirent *sd ;
 563   struct kref kref ;
 564   unsigned char state_initialized : 1 ;
 565   unsigned char state_in_sysfs : 1 ;
 566   unsigned char state_add_uevent_sent : 1 ;
 567   unsigned char state_remove_uevent_sent : 1 ;
 568   unsigned char uevent_suppress : 1 ;
 569};
 570#line 107 "include/linux/kobject.h"
 571struct kobj_type {
 572   void (*release)(struct kobject * ) ;
 573   struct sysfs_ops  const  *sysfs_ops ;
 574   struct attribute **default_attrs ;
 575   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 576   void const   *(*namespace)(struct kobject * ) ;
 577};
 578#line 115 "include/linux/kobject.h"
 579struct kobj_uevent_env {
 580   char *envp[32U] ;
 581   int envp_idx ;
 582   char buf[2048U] ;
 583   int buflen ;
 584};
 585#line 122 "include/linux/kobject.h"
 586struct kset_uevent_ops {
 587   int (* const  filter)(struct kset * , struct kobject * ) ;
 588   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 589   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 590};
 591#line 139 "include/linux/kobject.h"
 592struct kset {
 593   struct list_head list ;
 594   spinlock_t list_lock ;
 595   struct kobject kobj ;
 596   struct kset_uevent_ops  const  *uevent_ops ;
 597};
 598#line 215
 599struct kernel_param;
 600#line 215
 601struct kernel_param;
 602#line 216 "include/linux/kobject.h"
 603struct kernel_param_ops {
 604   int (*set)(char const   * , struct kernel_param  const  * ) ;
 605   int (*get)(char * , struct kernel_param  const  * ) ;
 606   void (*free)(void * ) ;
 607};
 608#line 49 "include/linux/moduleparam.h"
 609struct kparam_string;
 610#line 49
 611struct kparam_array;
 612#line 49 "include/linux/moduleparam.h"
 613union __anonunion_ldv_13363_134 {
 614   void *arg ;
 615   struct kparam_string  const  *str ;
 616   struct kparam_array  const  *arr ;
 617};
 618#line 49 "include/linux/moduleparam.h"
 619struct kernel_param {
 620   char const   *name ;
 621   struct kernel_param_ops  const  *ops ;
 622   u16 perm ;
 623   s16 level ;
 624   union __anonunion_ldv_13363_134 ldv_13363 ;
 625};
 626#line 61 "include/linux/moduleparam.h"
 627struct kparam_string {
 628   unsigned int maxlen ;
 629   char *string ;
 630};
 631#line 67 "include/linux/moduleparam.h"
 632struct kparam_array {
 633   unsigned int max ;
 634   unsigned int elemsize ;
 635   unsigned int *num ;
 636   struct kernel_param_ops  const  *ops ;
 637   void *elem ;
 638};
 639#line 458 "include/linux/moduleparam.h"
 640struct static_key {
 641   atomic_t enabled ;
 642};
 643#line 225 "include/linux/jump_label.h"
 644struct tracepoint;
 645#line 225
 646struct tracepoint;
 647#line 226 "include/linux/jump_label.h"
 648struct tracepoint_func {
 649   void *func ;
 650   void *data ;
 651};
 652#line 29 "include/linux/tracepoint.h"
 653struct tracepoint {
 654   char const   *name ;
 655   struct static_key key ;
 656   void (*regfunc)(void) ;
 657   void (*unregfunc)(void) ;
 658   struct tracepoint_func *funcs ;
 659};
 660#line 86 "include/linux/tracepoint.h"
 661struct kernel_symbol {
 662   unsigned long value ;
 663   char const   *name ;
 664};
 665#line 27 "include/linux/export.h"
 666struct mod_arch_specific {
 667
 668};
 669#line 34 "include/linux/module.h"
 670struct module_param_attrs;
 671#line 34 "include/linux/module.h"
 672struct module_kobject {
 673   struct kobject kobj ;
 674   struct module *mod ;
 675   struct kobject *drivers_dir ;
 676   struct module_param_attrs *mp ;
 677};
 678#line 43 "include/linux/module.h"
 679struct module_attribute {
 680   struct attribute attr ;
 681   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 682   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 683                    size_t  ) ;
 684   void (*setup)(struct module * , char const   * ) ;
 685   int (*test)(struct module * ) ;
 686   void (*free)(struct module * ) ;
 687};
 688#line 69
 689struct exception_table_entry;
 690#line 69
 691struct exception_table_entry;
 692#line 198
 693enum module_state {
 694    MODULE_STATE_LIVE = 0,
 695    MODULE_STATE_COMING = 1,
 696    MODULE_STATE_GOING = 2
 697} ;
 698#line 204 "include/linux/module.h"
 699struct module_ref {
 700   unsigned long incs ;
 701   unsigned long decs ;
 702};
 703#line 219
 704struct module_sect_attrs;
 705#line 219
 706struct module_notes_attrs;
 707#line 219
 708struct ftrace_event_call;
 709#line 219 "include/linux/module.h"
 710struct module {
 711   enum module_state state ;
 712   struct list_head list ;
 713   char name[56U] ;
 714   struct module_kobject mkobj ;
 715   struct module_attribute *modinfo_attrs ;
 716   char const   *version ;
 717   char const   *srcversion ;
 718   struct kobject *holders_dir ;
 719   struct kernel_symbol  const  *syms ;
 720   unsigned long const   *crcs ;
 721   unsigned int num_syms ;
 722   struct kernel_param *kp ;
 723   unsigned int num_kp ;
 724   unsigned int num_gpl_syms ;
 725   struct kernel_symbol  const  *gpl_syms ;
 726   unsigned long const   *gpl_crcs ;
 727   struct kernel_symbol  const  *unused_syms ;
 728   unsigned long const   *unused_crcs ;
 729   unsigned int num_unused_syms ;
 730   unsigned int num_unused_gpl_syms ;
 731   struct kernel_symbol  const  *unused_gpl_syms ;
 732   unsigned long const   *unused_gpl_crcs ;
 733   struct kernel_symbol  const  *gpl_future_syms ;
 734   unsigned long const   *gpl_future_crcs ;
 735   unsigned int num_gpl_future_syms ;
 736   unsigned int num_exentries ;
 737   struct exception_table_entry *extable ;
 738   int (*init)(void) ;
 739   void *module_init ;
 740   void *module_core ;
 741   unsigned int init_size ;
 742   unsigned int core_size ;
 743   unsigned int init_text_size ;
 744   unsigned int core_text_size ;
 745   unsigned int init_ro_size ;
 746   unsigned int core_ro_size ;
 747   struct mod_arch_specific arch ;
 748   unsigned int taints ;
 749   unsigned int num_bugs ;
 750   struct list_head bug_list ;
 751   struct bug_entry *bug_table ;
 752   Elf64_Sym *symtab ;
 753   Elf64_Sym *core_symtab ;
 754   unsigned int num_symtab ;
 755   unsigned int core_num_syms ;
 756   char *strtab ;
 757   char *core_strtab ;
 758   struct module_sect_attrs *sect_attrs ;
 759   struct module_notes_attrs *notes_attrs ;
 760   char *args ;
 761   void *percpu ;
 762   unsigned int percpu_size ;
 763   unsigned int num_tracepoints ;
 764   struct tracepoint * const  *tracepoints_ptrs ;
 765   unsigned int num_trace_bprintk_fmt ;
 766   char const   **trace_bprintk_fmt_start ;
 767   struct ftrace_event_call **trace_events ;
 768   unsigned int num_trace_events ;
 769   struct list_head source_list ;
 770   struct list_head target_list ;
 771   struct task_struct *waiter ;
 772   void (*exit)(void) ;
 773   struct module_ref *refptr ;
 774   ctor_fn_t (**ctors)(void) ;
 775   unsigned int num_ctors ;
 776};
 777#line 88 "include/linux/kmemleak.h"
 778struct kmem_cache_cpu {
 779   void **freelist ;
 780   unsigned long tid ;
 781   struct page *page ;
 782   struct page *partial ;
 783   int node ;
 784   unsigned int stat[26U] ;
 785};
 786#line 55 "include/linux/slub_def.h"
 787struct kmem_cache_node {
 788   spinlock_t list_lock ;
 789   unsigned long nr_partial ;
 790   struct list_head partial ;
 791   atomic_long_t nr_slabs ;
 792   atomic_long_t total_objects ;
 793   struct list_head full ;
 794};
 795#line 66 "include/linux/slub_def.h"
 796struct kmem_cache_order_objects {
 797   unsigned long x ;
 798};
 799#line 76 "include/linux/slub_def.h"
 800struct kmem_cache {
 801   struct kmem_cache_cpu *cpu_slab ;
 802   unsigned long flags ;
 803   unsigned long min_partial ;
 804   int size ;
 805   int objsize ;
 806   int offset ;
 807   int cpu_partial ;
 808   struct kmem_cache_order_objects oo ;
 809   struct kmem_cache_order_objects max ;
 810   struct kmem_cache_order_objects min ;
 811   gfp_t allocflags ;
 812   int refcount ;
 813   void (*ctor)(void * ) ;
 814   int inuse ;
 815   int align ;
 816   int reserved ;
 817   char const   *name ;
 818   struct list_head list ;
 819   struct kobject kobj ;
 820   int remote_node_defrag_ratio ;
 821   struct kmem_cache_node *node[1024U] ;
 822};
 823#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
 824struct klist_node;
 825#line 15
 826struct klist_node;
 827#line 37 "include/linux/klist.h"
 828struct klist_node {
 829   void *n_klist ;
 830   struct list_head n_node ;
 831   struct kref n_ref ;
 832};
 833#line 67
 834struct dma_map_ops;
 835#line 67 "include/linux/klist.h"
 836struct dev_archdata {
 837   void *acpi_handle ;
 838   struct dma_map_ops *dma_ops ;
 839   void *iommu ;
 840};
 841#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 842struct pdev_archdata {
 843
 844};
 845#line 17
 846struct device_private;
 847#line 17
 848struct device_private;
 849#line 18
 850struct device_driver;
 851#line 18
 852struct device_driver;
 853#line 19
 854struct driver_private;
 855#line 19
 856struct driver_private;
 857#line 20
 858struct class;
 859#line 20
 860struct class;
 861#line 21
 862struct subsys_private;
 863#line 21
 864struct subsys_private;
 865#line 22
 866struct bus_type;
 867#line 22
 868struct bus_type;
 869#line 23
 870struct device_node;
 871#line 23
 872struct device_node;
 873#line 24
 874struct iommu_ops;
 875#line 24
 876struct iommu_ops;
 877#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 878struct bus_attribute {
 879   struct attribute attr ;
 880   ssize_t (*show)(struct bus_type * , char * ) ;
 881   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
 882};
 883#line 51 "include/linux/device.h"
 884struct device_attribute;
 885#line 51
 886struct driver_attribute;
 887#line 51 "include/linux/device.h"
 888struct bus_type {
 889   char const   *name ;
 890   char const   *dev_name ;
 891   struct device *dev_root ;
 892   struct bus_attribute *bus_attrs ;
 893   struct device_attribute *dev_attrs ;
 894   struct driver_attribute *drv_attrs ;
 895   int (*match)(struct device * , struct device_driver * ) ;
 896   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 897   int (*probe)(struct device * ) ;
 898   int (*remove)(struct device * ) ;
 899   void (*shutdown)(struct device * ) ;
 900   int (*suspend)(struct device * , pm_message_t  ) ;
 901   int (*resume)(struct device * ) ;
 902   struct dev_pm_ops  const  *pm ;
 903   struct iommu_ops *iommu_ops ;
 904   struct subsys_private *p ;
 905};
 906#line 125
 907struct device_type;
 908#line 182
 909struct of_device_id;
 910#line 182 "include/linux/device.h"
 911struct device_driver {
 912   char const   *name ;
 913   struct bus_type *bus ;
 914   struct module *owner ;
 915   char const   *mod_name ;
 916   bool suppress_bind_attrs ;
 917   struct of_device_id  const  *of_match_table ;
 918   int (*probe)(struct device * ) ;
 919   int (*remove)(struct device * ) ;
 920   void (*shutdown)(struct device * ) ;
 921   int (*suspend)(struct device * , pm_message_t  ) ;
 922   int (*resume)(struct device * ) ;
 923   struct attribute_group  const  **groups ;
 924   struct dev_pm_ops  const  *pm ;
 925   struct driver_private *p ;
 926};
 927#line 245 "include/linux/device.h"
 928struct driver_attribute {
 929   struct attribute attr ;
 930   ssize_t (*show)(struct device_driver * , char * ) ;
 931   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
 932};
 933#line 299
 934struct class_attribute;
 935#line 299 "include/linux/device.h"
 936struct class {
 937   char const   *name ;
 938   struct module *owner ;
 939   struct class_attribute *class_attrs ;
 940   struct device_attribute *dev_attrs ;
 941   struct bin_attribute *dev_bin_attrs ;
 942   struct kobject *dev_kobj ;
 943   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
 944   char *(*devnode)(struct device * , umode_t * ) ;
 945   void (*class_release)(struct class * ) ;
 946   void (*dev_release)(struct device * ) ;
 947   int (*suspend)(struct device * , pm_message_t  ) ;
 948   int (*resume)(struct device * ) ;
 949   struct kobj_ns_type_operations  const  *ns_type ;
 950   void const   *(*namespace)(struct device * ) ;
 951   struct dev_pm_ops  const  *pm ;
 952   struct subsys_private *p ;
 953};
 954#line 394 "include/linux/device.h"
 955struct class_attribute {
 956   struct attribute attr ;
 957   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
 958   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
 959   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
 960};
 961#line 447 "include/linux/device.h"
 962struct device_type {
 963   char const   *name ;
 964   struct attribute_group  const  **groups ;
 965   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 966   char *(*devnode)(struct device * , umode_t * ) ;
 967   void (*release)(struct device * ) ;
 968   struct dev_pm_ops  const  *pm ;
 969};
 970#line 474 "include/linux/device.h"
 971struct device_attribute {
 972   struct attribute attr ;
 973   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
 974   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
 975                    size_t  ) ;
 976};
 977#line 557 "include/linux/device.h"
 978struct device_dma_parameters {
 979   unsigned int max_segment_size ;
 980   unsigned long segment_boundary_mask ;
 981};
 982#line 567
 983struct dma_coherent_mem;
 984#line 567 "include/linux/device.h"
 985struct device {
 986   struct device *parent ;
 987   struct device_private *p ;
 988   struct kobject kobj ;
 989   char const   *init_name ;
 990   struct device_type  const  *type ;
 991   struct mutex mutex ;
 992   struct bus_type *bus ;
 993   struct device_driver *driver ;
 994   void *platform_data ;
 995   struct dev_pm_info power ;
 996   struct dev_pm_domain *pm_domain ;
 997   int numa_node ;
 998   u64 *dma_mask ;
 999   u64 coherent_dma_mask ;
1000   struct device_dma_parameters *dma_parms ;
1001   struct list_head dma_pools ;
1002   struct dma_coherent_mem *dma_mem ;
1003   struct dev_archdata archdata ;
1004   struct device_node *of_node ;
1005   dev_t devt ;
1006   u32 id ;
1007   spinlock_t devres_lock ;
1008   struct list_head devres_head ;
1009   struct klist_node knode_class ;
1010   struct class *class ;
1011   struct attribute_group  const  **groups ;
1012   void (*release)(struct device * ) ;
1013};
1014#line 681 "include/linux/device.h"
1015struct wakeup_source {
1016   char const   *name ;
1017   struct list_head entry ;
1018   spinlock_t lock ;
1019   struct timer_list timer ;
1020   unsigned long timer_expires ;
1021   ktime_t total_time ;
1022   ktime_t max_time ;
1023   ktime_t last_time ;
1024   unsigned long event_count ;
1025   unsigned long active_count ;
1026   unsigned long relax_count ;
1027   unsigned long hit_count ;
1028   unsigned char active : 1 ;
1029};
1030#line 12 "include/linux/mod_devicetable.h"
1031typedef unsigned long kernel_ulong_t;
1032#line 13 "include/linux/mod_devicetable.h"
1033struct pci_device_id {
1034   __u32 vendor ;
1035   __u32 device ;
1036   __u32 subvendor ;
1037   __u32 subdevice ;
1038   __u32 class ;
1039   __u32 class_mask ;
1040   kernel_ulong_t driver_data ;
1041};
1042#line 215 "include/linux/mod_devicetable.h"
1043struct of_device_id {
1044   char name[32U] ;
1045   char type[32U] ;
1046   char compatible[128U] ;
1047   void *data ;
1048};
1049#line 492 "include/linux/mod_devicetable.h"
1050struct platform_device_id {
1051   char name[20U] ;
1052   kernel_ulong_t driver_data ;
1053};
1054#line 584
1055struct mfd_cell;
1056#line 584
1057struct mfd_cell;
1058#line 585 "include/linux/mod_devicetable.h"
1059struct platform_device {
1060   char const   *name ;
1061   int id ;
1062   struct device dev ;
1063   u32 num_resources ;
1064   struct resource *resource ;
1065   struct platform_device_id  const  *id_entry ;
1066   struct mfd_cell *mfd_cell ;
1067   struct pdev_archdata archdata ;
1068};
1069#line 17 "include/linux/irqreturn.h"
1070struct hotplug_slot;
1071#line 17 "include/linux/irqreturn.h"
1072struct pci_slot {
1073   struct pci_bus *bus ;
1074   struct list_head list ;
1075   struct hotplug_slot *hotplug ;
1076   unsigned char number ;
1077   struct kobject kobj ;
1078};
1079#line 117 "include/linux/pci.h"
1080typedef int pci_power_t;
1081#line 143 "include/linux/pci.h"
1082typedef unsigned int pci_channel_state_t;
1083#line 144
1084enum pci_channel_state {
1085    pci_channel_io_normal = 1,
1086    pci_channel_io_frozen = 2,
1087    pci_channel_io_perm_failure = 3
1088} ;
1089#line 169 "include/linux/pci.h"
1090typedef unsigned short pci_dev_flags_t;
1091#line 186 "include/linux/pci.h"
1092typedef unsigned short pci_bus_flags_t;
1093#line 229
1094struct pcie_link_state;
1095#line 229
1096struct pcie_link_state;
1097#line 230
1098struct pci_vpd;
1099#line 230
1100struct pci_vpd;
1101#line 231
1102struct pci_sriov;
1103#line 231
1104struct pci_sriov;
1105#line 232
1106struct pci_ats;
1107#line 232
1108struct pci_ats;
1109#line 233
1110struct proc_dir_entry;
1111#line 233
1112struct pci_driver;
1113#line 233 "include/linux/pci.h"
1114union __anonunion_ldv_15471_136 {
1115   struct pci_sriov *sriov ;
1116   struct pci_dev *physfn ;
1117};
1118#line 233 "include/linux/pci.h"
1119struct pci_dev {
1120   struct list_head bus_list ;
1121   struct pci_bus *bus ;
1122   struct pci_bus *subordinate ;
1123   void *sysdata ;
1124   struct proc_dir_entry *procent ;
1125   struct pci_slot *slot ;
1126   unsigned int devfn ;
1127   unsigned short vendor ;
1128   unsigned short device ;
1129   unsigned short subsystem_vendor ;
1130   unsigned short subsystem_device ;
1131   unsigned int class ;
1132   u8 revision ;
1133   u8 hdr_type ;
1134   u8 pcie_cap ;
1135   unsigned char pcie_type : 4 ;
1136   unsigned char pcie_mpss : 3 ;
1137   u8 rom_base_reg ;
1138   u8 pin ;
1139   struct pci_driver *driver ;
1140   u64 dma_mask ;
1141   struct device_dma_parameters dma_parms ;
1142   pci_power_t current_state ;
1143   int pm_cap ;
1144   unsigned char pme_support : 5 ;
1145   unsigned char pme_interrupt : 1 ;
1146   unsigned char pme_poll : 1 ;
1147   unsigned char d1_support : 1 ;
1148   unsigned char d2_support : 1 ;
1149   unsigned char no_d1d2 : 1 ;
1150   unsigned char mmio_always_on : 1 ;
1151   unsigned char wakeup_prepared : 1 ;
1152   unsigned int d3_delay ;
1153   struct pcie_link_state *link_state ;
1154   pci_channel_state_t error_state ;
1155   struct device dev ;
1156   int cfg_size ;
1157   unsigned int irq ;
1158   struct resource resource[17U] ;
1159   unsigned char transparent : 1 ;
1160   unsigned char multifunction : 1 ;
1161   unsigned char is_added : 1 ;
1162   unsigned char is_busmaster : 1 ;
1163   unsigned char no_msi : 1 ;
1164   unsigned char block_cfg_access : 1 ;
1165   unsigned char broken_parity_status : 1 ;
1166   unsigned char irq_reroute_variant : 2 ;
1167   unsigned char msi_enabled : 1 ;
1168   unsigned char msix_enabled : 1 ;
1169   unsigned char ari_enabled : 1 ;
1170   unsigned char is_managed : 1 ;
1171   unsigned char is_pcie : 1 ;
1172   unsigned char needs_freset : 1 ;
1173   unsigned char state_saved : 1 ;
1174   unsigned char is_physfn : 1 ;
1175   unsigned char is_virtfn : 1 ;
1176   unsigned char reset_fn : 1 ;
1177   unsigned char is_hotplug_bridge : 1 ;
1178   unsigned char __aer_firmware_first_valid : 1 ;
1179   unsigned char __aer_firmware_first : 1 ;
1180   pci_dev_flags_t dev_flags ;
1181   atomic_t enable_cnt ;
1182   u32 saved_config_space[16U] ;
1183   struct hlist_head saved_cap_space ;
1184   struct bin_attribute *rom_attr ;
1185   int rom_attr_enabled ;
1186   struct bin_attribute *res_attr[17U] ;
1187   struct bin_attribute *res_attr_wc[17U] ;
1188   struct list_head msi_list ;
1189   struct kset *msi_kset ;
1190   struct pci_vpd *vpd ;
1191   union __anonunion_ldv_15471_136 ldv_15471 ;
1192   struct pci_ats *ats ;
1193};
1194#line 403
1195struct pci_ops;
1196#line 403 "include/linux/pci.h"
1197struct pci_bus {
1198   struct list_head node ;
1199   struct pci_bus *parent ;
1200   struct list_head children ;
1201   struct list_head devices ;
1202   struct pci_dev *self ;
1203   struct list_head slots ;
1204   struct resource *resource[4U] ;
1205   struct list_head resources ;
1206   struct pci_ops *ops ;
1207   void *sysdata ;
1208   struct proc_dir_entry *procdir ;
1209   unsigned char number ;
1210   unsigned char primary ;
1211   unsigned char secondary ;
1212   unsigned char subordinate ;
1213   unsigned char max_bus_speed ;
1214   unsigned char cur_bus_speed ;
1215   char name[48U] ;
1216   unsigned short bridge_ctl ;
1217   pci_bus_flags_t bus_flags ;
1218   struct device *bridge ;
1219   struct device dev ;
1220   struct bin_attribute *legacy_io ;
1221   struct bin_attribute *legacy_mem ;
1222   unsigned char is_added : 1 ;
1223};
1224#line 455 "include/linux/pci.h"
1225struct pci_ops {
1226   int (*read)(struct pci_bus * , unsigned int  , int  , int  , u32 * ) ;
1227   int (*write)(struct pci_bus * , unsigned int  , int  , int  , u32  ) ;
1228};
1229#line 490 "include/linux/pci.h"
1230struct pci_dynids {
1231   spinlock_t lock ;
1232   struct list_head list ;
1233};
1234#line 503 "include/linux/pci.h"
1235typedef unsigned int pci_ers_result_t;
1236#line 512 "include/linux/pci.h"
1237struct pci_error_handlers {
1238   pci_ers_result_t (*error_detected)(struct pci_dev * , enum pci_channel_state  ) ;
1239   pci_ers_result_t (*mmio_enabled)(struct pci_dev * ) ;
1240   pci_ers_result_t (*link_reset)(struct pci_dev * ) ;
1241   pci_ers_result_t (*slot_reset)(struct pci_dev * ) ;
1242   void (*resume)(struct pci_dev * ) ;
1243};
1244#line 540 "include/linux/pci.h"
1245struct pci_driver {
1246   struct list_head node ;
1247   char const   *name ;
1248   struct pci_device_id  const  *id_table ;
1249   int (*probe)(struct pci_dev * , struct pci_device_id  const  * ) ;
1250   void (*remove)(struct pci_dev * ) ;
1251   int (*suspend)(struct pci_dev * , pm_message_t  ) ;
1252   int (*suspend_late)(struct pci_dev * , pm_message_t  ) ;
1253   int (*resume_early)(struct pci_dev * ) ;
1254   int (*resume)(struct pci_dev * ) ;
1255   void (*shutdown)(struct pci_dev * ) ;
1256   struct pci_error_handlers *err_handler ;
1257   struct device_driver driver ;
1258   struct pci_dynids dynids ;
1259};
1260#line 986 "include/linux/pci.h"
1261struct scatterlist {
1262   unsigned long sg_magic ;
1263   unsigned long page_link ;
1264   unsigned int offset ;
1265   unsigned int length ;
1266   dma_addr_t dma_address ;
1267   unsigned int dma_length ;
1268};
1269#line 1134
1270struct prio_tree_node;
1271#line 1134 "include/linux/pci.h"
1272struct raw_prio_tree_node {
1273   struct prio_tree_node *left ;
1274   struct prio_tree_node *right ;
1275   struct prio_tree_node *parent ;
1276};
1277#line 19 "include/linux/prio_tree.h"
1278struct prio_tree_node {
1279   struct prio_tree_node *left ;
1280   struct prio_tree_node *right ;
1281   struct prio_tree_node *parent ;
1282   unsigned long start ;
1283   unsigned long last ;
1284};
1285#line 116
1286struct address_space;
1287#line 116
1288struct address_space;
1289#line 117 "include/linux/prio_tree.h"
1290union __anonunion_ldv_16343_138 {
1291   unsigned long index ;
1292   void *freelist ;
1293};
1294#line 117 "include/linux/prio_tree.h"
1295struct __anonstruct_ldv_16353_142 {
1296   unsigned short inuse ;
1297   unsigned short objects : 15 ;
1298   unsigned char frozen : 1 ;
1299};
1300#line 117 "include/linux/prio_tree.h"
1301union __anonunion_ldv_16354_141 {
1302   atomic_t _mapcount ;
1303   struct __anonstruct_ldv_16353_142 ldv_16353 ;
1304};
1305#line 117 "include/linux/prio_tree.h"
1306struct __anonstruct_ldv_16356_140 {
1307   union __anonunion_ldv_16354_141 ldv_16354 ;
1308   atomic_t _count ;
1309};
1310#line 117 "include/linux/prio_tree.h"
1311union __anonunion_ldv_16357_139 {
1312   unsigned long counters ;
1313   struct __anonstruct_ldv_16356_140 ldv_16356 ;
1314};
1315#line 117 "include/linux/prio_tree.h"
1316struct __anonstruct_ldv_16358_137 {
1317   union __anonunion_ldv_16343_138 ldv_16343 ;
1318   union __anonunion_ldv_16357_139 ldv_16357 ;
1319};
1320#line 117 "include/linux/prio_tree.h"
1321struct __anonstruct_ldv_16365_144 {
1322   struct page *next ;
1323   int pages ;
1324   int pobjects ;
1325};
1326#line 117 "include/linux/prio_tree.h"
1327union __anonunion_ldv_16366_143 {
1328   struct list_head lru ;
1329   struct __anonstruct_ldv_16365_144 ldv_16365 ;
1330};
1331#line 117 "include/linux/prio_tree.h"
1332union __anonunion_ldv_16371_145 {
1333   unsigned long private ;
1334   struct kmem_cache *slab ;
1335   struct page *first_page ;
1336};
1337#line 117 "include/linux/prio_tree.h"
1338struct page {
1339   unsigned long flags ;
1340   struct address_space *mapping ;
1341   struct __anonstruct_ldv_16358_137 ldv_16358 ;
1342   union __anonunion_ldv_16366_143 ldv_16366 ;
1343   union __anonunion_ldv_16371_145 ldv_16371 ;
1344   unsigned long debug_flags ;
1345};
1346#line 192 "include/linux/mm_types.h"
1347struct __anonstruct_vm_set_147 {
1348   struct list_head list ;
1349   void *parent ;
1350   struct vm_area_struct *head ;
1351};
1352#line 192 "include/linux/mm_types.h"
1353union __anonunion_shared_146 {
1354   struct __anonstruct_vm_set_147 vm_set ;
1355   struct raw_prio_tree_node prio_tree_node ;
1356};
1357#line 192
1358struct anon_vma;
1359#line 192
1360struct vm_operations_struct;
1361#line 192
1362struct mempolicy;
1363#line 192 "include/linux/mm_types.h"
1364struct vm_area_struct {
1365   struct mm_struct *vm_mm ;
1366   unsigned long vm_start ;
1367   unsigned long vm_end ;
1368   struct vm_area_struct *vm_next ;
1369   struct vm_area_struct *vm_prev ;
1370   pgprot_t vm_page_prot ;
1371   unsigned long vm_flags ;
1372   struct rb_node vm_rb ;
1373   union __anonunion_shared_146 shared ;
1374   struct list_head anon_vma_chain ;
1375   struct anon_vma *anon_vma ;
1376   struct vm_operations_struct  const  *vm_ops ;
1377   unsigned long vm_pgoff ;
1378   struct file *vm_file ;
1379   void *vm_private_data ;
1380   struct mempolicy *vm_policy ;
1381};
1382#line 255 "include/linux/mm_types.h"
1383struct core_thread {
1384   struct task_struct *task ;
1385   struct core_thread *next ;
1386};
1387#line 261 "include/linux/mm_types.h"
1388struct core_state {
1389   atomic_t nr_threads ;
1390   struct core_thread dumper ;
1391   struct completion startup ;
1392};
1393#line 274 "include/linux/mm_types.h"
1394struct mm_rss_stat {
1395   atomic_long_t count[3U] ;
1396};
1397#line 287
1398struct linux_binfmt;
1399#line 287
1400struct mmu_notifier_mm;
1401#line 287 "include/linux/mm_types.h"
1402struct mm_struct {
1403   struct vm_area_struct *mmap ;
1404   struct rb_root mm_rb ;
1405   struct vm_area_struct *mmap_cache ;
1406   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1407                                      unsigned long  , unsigned long  ) ;
1408   void (*unmap_area)(struct mm_struct * , unsigned long  ) ;
1409   unsigned long mmap_base ;
1410   unsigned long task_size ;
1411   unsigned long cached_hole_size ;
1412   unsigned long free_area_cache ;
1413   pgd_t *pgd ;
1414   atomic_t mm_users ;
1415   atomic_t mm_count ;
1416   int map_count ;
1417   spinlock_t page_table_lock ;
1418   struct rw_semaphore mmap_sem ;
1419   struct list_head mmlist ;
1420   unsigned long hiwater_rss ;
1421   unsigned long hiwater_vm ;
1422   unsigned long total_vm ;
1423   unsigned long locked_vm ;
1424   unsigned long pinned_vm ;
1425   unsigned long shared_vm ;
1426   unsigned long exec_vm ;
1427   unsigned long stack_vm ;
1428   unsigned long reserved_vm ;
1429   unsigned long def_flags ;
1430   unsigned long nr_ptes ;
1431   unsigned long start_code ;
1432   unsigned long end_code ;
1433   unsigned long start_data ;
1434   unsigned long end_data ;
1435   unsigned long start_brk ;
1436   unsigned long brk ;
1437   unsigned long start_stack ;
1438   unsigned long arg_start ;
1439   unsigned long arg_end ;
1440   unsigned long env_start ;
1441   unsigned long env_end ;
1442   unsigned long saved_auxv[44U] ;
1443   struct mm_rss_stat rss_stat ;
1444   struct linux_binfmt *binfmt ;
1445   cpumask_var_t cpu_vm_mask_var ;
1446   mm_context_t context ;
1447   unsigned int faultstamp ;
1448   unsigned int token_priority ;
1449   unsigned int last_interval ;
1450   unsigned long flags ;
1451   struct core_state *core_state ;
1452   spinlock_t ioctx_lock ;
1453   struct hlist_head ioctx_list ;
1454   struct task_struct *owner ;
1455   struct file *exe_file ;
1456   unsigned long num_exe_file_vmas ;
1457   struct mmu_notifier_mm *mmu_notifier_mm ;
1458   pgtable_t pmd_huge_pte ;
1459   struct cpumask cpumask_allocation ;
1460};
1461#line 178 "include/linux/mm.h"
1462struct vm_fault {
1463   unsigned int flags ;
1464   unsigned long pgoff ;
1465   void *virtual_address ;
1466   struct page *page ;
1467};
1468#line 195 "include/linux/mm.h"
1469struct vm_operations_struct {
1470   void (*open)(struct vm_area_struct * ) ;
1471   void (*close)(struct vm_area_struct * ) ;
1472   int (*fault)(struct vm_area_struct * , struct vm_fault * ) ;
1473   int (*page_mkwrite)(struct vm_area_struct * , struct vm_fault * ) ;
1474   int (*access)(struct vm_area_struct * , unsigned long  , void * , int  , int  ) ;
1475   int (*set_policy)(struct vm_area_struct * , struct mempolicy * ) ;
1476   struct mempolicy *(*get_policy)(struct vm_area_struct * , unsigned long  ) ;
1477   int (*migrate)(struct vm_area_struct * , nodemask_t const   * , nodemask_t const   * ,
1478                  unsigned long  ) ;
1479};
1480#line 31 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pci_64.h"
1481struct dma_attrs {
1482   unsigned long flags[1U] ;
1483};
1484#line 67 "include/linux/dma-attrs.h"
1485enum dma_data_direction {
1486    DMA_BIDIRECTIONAL = 0,
1487    DMA_TO_DEVICE = 1,
1488    DMA_FROM_DEVICE = 2,
1489    DMA_NONE = 3
1490} ;
1491#line 268 "include/linux/scatterlist.h"
1492struct dma_map_ops {
1493   void *(*alloc)(struct device * , size_t  , dma_addr_t * , gfp_t  , struct dma_attrs * ) ;
1494   void (*free)(struct device * , size_t  , void * , dma_addr_t  , struct dma_attrs * ) ;
1495   int (*mmap)(struct device * , struct vm_area_struct * , void * , dma_addr_t  ,
1496               size_t  , struct dma_attrs * ) ;
1497   dma_addr_t (*map_page)(struct device * , struct page * , unsigned long  , size_t  ,
1498                          enum dma_data_direction  , struct dma_attrs * ) ;
1499   void (*unmap_page)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ,
1500                      struct dma_attrs * ) ;
1501   int (*map_sg)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ,
1502                 struct dma_attrs * ) ;
1503   void (*unmap_sg)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ,
1504                    struct dma_attrs * ) ;
1505   void (*sync_single_for_cpu)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ) ;
1506   void (*sync_single_for_device)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ) ;
1507   void (*sync_sg_for_cpu)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ) ;
1508   void (*sync_sg_for_device)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ) ;
1509   int (*mapping_error)(struct device * , dma_addr_t  ) ;
1510   int (*dma_supported)(struct device * , u64  ) ;
1511   int (*set_dma_mask)(struct device * , u64  ) ;
1512   int is_phys ;
1513};
1514#line 1722 "include/linux/pci.h"
1515struct mfd_cell {
1516   char const   *name ;
1517   int id ;
1518   atomic_t *usage_count ;
1519   int (*enable)(struct platform_device * ) ;
1520   int (*disable)(struct platform_device * ) ;
1521   int (*suspend)(struct platform_device * ) ;
1522   int (*resume)(struct platform_device * ) ;
1523   void *platform_data ;
1524   size_t pdata_size ;
1525   int num_resources ;
1526   struct resource  const  *resources ;
1527   bool ignore_resource_conflicts ;
1528   bool pm_runtime_no_callbacks ;
1529};
1530#line 99 "include/linux/mfd/core.h"
1531struct rdc321x_gpio_pdata {
1532   struct pci_dev *sb_pdev ;
1533   unsigned int max_gpios ;
1534};
1535#line 21 "include/linux/mfd/rdc321x.h"
1536struct rdc321x_wdt_pdata {
1537   struct pci_dev *sb_pdev ;
1538};
1539#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1540void ldv_spin_lock(void) ;
1541#line 3
1542void ldv_spin_unlock(void) ;
1543#line 4
1544int ldv_spin_trylock(void) ;
1545#line 26 "include/linux/export.h"
1546extern struct module __this_module ;
1547#line 220 "include/linux/slub_def.h"
1548extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1549#line 223
1550void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1551#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1552void ldv_check_alloc_flags(gfp_t flags ) ;
1553#line 12
1554void ldv_check_alloc_nonatomic(void) ;
1555#line 14
1556struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1557#line 892 "include/linux/device.h"
1558extern int dev_err(struct device  const  * , char const   *  , ...) ;
1559#line 773 "include/linux/pci.h"
1560extern int pci_enable_device(struct pci_dev * ) ;
1561#line 940
1562extern int __pci_register_driver(struct pci_driver * , struct module * , char const   * ) ;
1563#line 949
1564extern void pci_unregister_driver(struct pci_driver * ) ;
1565#line 93 "include/linux/mfd/core.h"
1566extern int mfd_add_devices(struct device * , int  , struct mfd_cell * , int  , struct resource * ,
1567                           int  ) ;
1568#line 98
1569extern void mfd_remove_devices(struct device * ) ;
1570#line 45 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1571static struct rdc321x_wdt_pdata rdc321x_wdt_pdata  ;
1572#line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1573static struct resource rdc321x_wdt_resource[1U]  = {      {68ULL, 71ULL, "wdt-reg", 256UL, (struct resource *)0, (struct resource *)0,
1574      (struct resource *)0}};
1575#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1576static struct rdc321x_gpio_pdata rdc321x_gpio_pdata  =    {(struct pci_dev *)0, 58U};
1577#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1578static struct resource rdc321x_gpio_resources[2U]  = {      {72ULL, 79ULL, "gpio-reg1", 256UL, (struct resource *)0, (struct resource *)0,
1579      (struct resource *)0}, 
1580        {132ULL, 139ULL, "gpio-reg2", 256UL, (struct resource *)0, (struct resource *)0,
1581      (struct resource *)0}};
1582#line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1583static struct mfd_cell rdc321x_sb_cells[2U]  = {      {"rdc321x-wdt", 0, (atomic_t *)0, (int (*)(struct platform_device * ))0, (int (*)(struct platform_device * ))0,
1584      (int (*)(struct platform_device * ))0, (int (*)(struct platform_device * ))0,
1585      (void *)(& rdc321x_wdt_pdata), 8UL, 1, (struct resource  const  *)(& rdc321x_wdt_resource),
1586      (_Bool)0, (_Bool)0}, 
1587        {"rdc321x-gpio", 0, (atomic_t *)0, (int (*)(struct platform_device * ))0, (int (*)(struct platform_device * ))0,
1588      (int (*)(struct platform_device * ))0, (int (*)(struct platform_device * ))0,
1589      (void *)(& rdc321x_gpio_pdata), 16UL, 2, (struct resource  const  *)(& rdc321x_gpio_resources),
1590      (_Bool)0, (_Bool)0}};
1591#line 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1592static int rdc321x_sb_probe(struct pci_dev *pdev , struct pci_device_id  const  *ent ) 
1593{ int err ;
1594  int tmp ;
1595  unsigned long __cil_tmp5 ;
1596  unsigned long __cil_tmp6 ;
1597  struct device *__cil_tmp7 ;
1598  struct device  const  *__cil_tmp8 ;
1599  struct rdc321x_gpio_pdata *__cil_tmp9 ;
1600  struct rdc321x_wdt_pdata *__cil_tmp10 ;
1601  unsigned long __cil_tmp11 ;
1602  unsigned long __cil_tmp12 ;
1603  struct device *__cil_tmp13 ;
1604  struct mfd_cell *__cil_tmp14 ;
1605  struct resource *__cil_tmp15 ;
1606
1607  {
1608  {
1609#line 95
1610  err = pci_enable_device(pdev);
1611  }
1612#line 96
1613  if (err != 0) {
1614    {
1615#line 97
1616    __cil_tmp5 = (unsigned long )pdev;
1617#line 97
1618    __cil_tmp6 = __cil_tmp5 + 144;
1619#line 97
1620    __cil_tmp7 = (struct device *)__cil_tmp6;
1621#line 97
1622    __cil_tmp8 = (struct device  const  *)__cil_tmp7;
1623#line 97
1624    dev_err(__cil_tmp8, "failed to enable device\n");
1625    }
1626#line 98
1627    return (err);
1628  } else {
1629
1630  }
1631  {
1632#line 101
1633  __cil_tmp9 = & rdc321x_gpio_pdata;
1634#line 101
1635  *((struct pci_dev **)__cil_tmp9) = pdev;
1636#line 102
1637  __cil_tmp10 = & rdc321x_wdt_pdata;
1638#line 102
1639  *((struct pci_dev **)__cil_tmp10) = pdev;
1640#line 104
1641  __cil_tmp11 = (unsigned long )pdev;
1642#line 104
1643  __cil_tmp12 = __cil_tmp11 + 144;
1644#line 104
1645  __cil_tmp13 = (struct device *)__cil_tmp12;
1646#line 104
1647  __cil_tmp14 = (struct mfd_cell *)(& rdc321x_sb_cells);
1648#line 104
1649  __cil_tmp15 = (struct resource *)0;
1650#line 104
1651  tmp = mfd_add_devices(__cil_tmp13, -1, __cil_tmp14, 2, __cil_tmp15, 0);
1652  }
1653#line 104
1654  return (tmp);
1655}
1656}
1657#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1658static void rdc321x_sb_remove(struct pci_dev *pdev ) 
1659{ unsigned long __cil_tmp2 ;
1660  unsigned long __cil_tmp3 ;
1661  struct device *__cil_tmp4 ;
1662
1663  {
1664  {
1665#line 110
1666  __cil_tmp2 = (unsigned long )pdev;
1667#line 110
1668  __cil_tmp3 = __cil_tmp2 + 144;
1669#line 110
1670  __cil_tmp4 = (struct device *)__cil_tmp3;
1671#line 110
1672  mfd_remove_devices(__cil_tmp4);
1673  }
1674#line 111
1675  return;
1676}
1677}
1678#line 113 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1679static struct pci_device_id  const  rdc321x_sb_table[2U]  = {      {6131U, 24624U, 4294967295U, 4294967295U, 0U, 0U, 0UL}, 
1680        {0U, 0U, 0U, 0U, 0U, 0U, 0UL}};
1681#line 117 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1682struct pci_device_id  const  __mod_pci_device_table  ;
1683#line 119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1684static struct pci_driver rdc321x_sb_driver  = 
1685#line 119
1686     {{(struct list_head *)0, (struct list_head *)0}, "RDC321x Southbridge", (struct pci_device_id  const  *)(& rdc321x_sb_table),
1687    & rdc321x_sb_probe, & rdc321x_sb_remove, (int (*)(struct pci_dev * , pm_message_t  ))0,
1688    (int (*)(struct pci_dev * , pm_message_t  ))0, (int (*)(struct pci_dev * ))0,
1689    (int (*)(struct pci_dev * ))0, (void (*)(struct pci_dev * ))0, (struct pci_error_handlers *)0,
1690    {(char const   *)0, (struct bus_type *)0, (struct module *)0, (char const   *)0,
1691     (_Bool)0, (struct of_device_id  const  *)0, (int (*)(struct device * ))0, (int (*)(struct device * ))0,
1692     (void (*)(struct device * ))0, (int (*)(struct device * , pm_message_t  ))0,
1693     (int (*)(struct device * ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
1694     (struct driver_private *)0}, {{{{{{0U}}, 0U, 0U, (void *)0, {(struct lock_class_key *)0,
1695                                                                  {(struct lock_class *)0,
1696                                                                   (struct lock_class *)0},
1697                                                                  (char const   *)0,
1698                                                                  0, 0UL}}}}, {(struct list_head *)0,
1699                                                                               (struct list_head *)0}}};
1700#line 126 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1701static int rdc321x_sb_init(void) 
1702{ int tmp ;
1703
1704  {
1705  {
1706#line 128
1707  tmp = __pci_register_driver(& rdc321x_sb_driver, & __this_module, "rdc321x_southbridge");
1708  }
1709#line 128
1710  return (tmp);
1711}
1712}
1713#line 131 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1714static void rdc321x_sb_exit(void) 
1715{ 
1716
1717  {
1718  {
1719#line 133
1720  pci_unregister_driver(& rdc321x_sb_driver);
1721  }
1722#line 134
1723  return;
1724}
1725}
1726#line 159
1727extern void ldv_check_final_state(void) ;
1728#line 162
1729extern void ldv_check_return_value(int  ) ;
1730#line 165
1731extern void ldv_initialize(void) ;
1732#line 168
1733extern int __VERIFIER_nondet_int(void) ;
1734#line 171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1735int LDV_IN_INTERRUPT  ;
1736#line 174 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1737void main(void) 
1738{ struct pci_dev *var_group1 ;
1739  struct pci_device_id  const  *var_rdc321x_sb_probe_0_p1 ;
1740  int res_rdc321x_sb_probe_0 ;
1741  int ldv_s_rdc321x_sb_driver_pci_driver ;
1742  int tmp ;
1743  int tmp___0 ;
1744  int tmp___1 ;
1745
1746  {
1747  {
1748#line 213
1749  ldv_s_rdc321x_sb_driver_pci_driver = 0;
1750#line 196
1751  LDV_IN_INTERRUPT = 1;
1752#line 205
1753  ldv_initialize();
1754#line 211
1755  tmp = rdc321x_sb_init();
1756  }
1757#line 211
1758  if (tmp != 0) {
1759#line 212
1760    goto ldv_final;
1761  } else {
1762
1763  }
1764#line 216
1765  goto ldv_20100;
1766  ldv_20099: 
1767  {
1768#line 220
1769  tmp___0 = __VERIFIER_nondet_int();
1770  }
1771#line 222
1772  if (tmp___0 == 0) {
1773#line 222
1774    goto case_0;
1775  } else {
1776    {
1777#line 241
1778    goto switch_default;
1779#line 220
1780    if (0) {
1781      case_0: /* CIL Label */ ;
1782#line 225
1783      if (ldv_s_rdc321x_sb_driver_pci_driver == 0) {
1784        {
1785#line 230
1786        res_rdc321x_sb_probe_0 = rdc321x_sb_probe(var_group1, var_rdc321x_sb_probe_0_p1);
1787#line 231
1788        ldv_check_return_value(res_rdc321x_sb_probe_0);
1789        }
1790#line 232
1791        if (res_rdc321x_sb_probe_0 != 0) {
1792#line 233
1793          goto ldv_module_exit;
1794        } else {
1795
1796        }
1797#line 234
1798        ldv_s_rdc321x_sb_driver_pci_driver = 0;
1799      } else {
1800
1801      }
1802#line 240
1803      goto ldv_20097;
1804      switch_default: /* CIL Label */ ;
1805#line 241
1806      goto ldv_20097;
1807    } else {
1808      switch_break: /* CIL Label */ ;
1809    }
1810    }
1811  }
1812  ldv_20097: ;
1813  ldv_20100: 
1814  {
1815#line 216
1816  tmp___1 = __VERIFIER_nondet_int();
1817  }
1818#line 216
1819  if (tmp___1 != 0) {
1820#line 218
1821    goto ldv_20099;
1822  } else
1823#line 216
1824  if (ldv_s_rdc321x_sb_driver_pci_driver != 0) {
1825#line 218
1826    goto ldv_20099;
1827  } else {
1828#line 220
1829    goto ldv_20101;
1830  }
1831  ldv_20101: ;
1832  ldv_module_exit: 
1833  {
1834#line 253
1835  rdc321x_sb_exit();
1836  }
1837  ldv_final: 
1838  {
1839#line 256
1840  ldv_check_final_state();
1841  }
1842#line 259
1843  return;
1844}
1845}
1846#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1847void ldv_blast_assert(void) 
1848{ 
1849
1850  {
1851  ERROR: ;
1852#line 6
1853  goto ERROR;
1854}
1855}
1856#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1857extern int __VERIFIER_nondet_int(void) ;
1858#line 280 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1859int ldv_spin  =    0;
1860#line 284 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1861void ldv_check_alloc_flags(gfp_t flags ) 
1862{ 
1863
1864  {
1865#line 287
1866  if (ldv_spin != 0) {
1867#line 287
1868    if (flags != 32U) {
1869      {
1870#line 287
1871      ldv_blast_assert();
1872      }
1873    } else {
1874
1875    }
1876  } else {
1877
1878  }
1879#line 290
1880  return;
1881}
1882}
1883#line 290
1884extern struct page *ldv_some_page(void) ;
1885#line 293 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1886struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
1887{ struct page *tmp ;
1888
1889  {
1890#line 296
1891  if (ldv_spin != 0) {
1892#line 296
1893    if (flags != 32U) {
1894      {
1895#line 296
1896      ldv_blast_assert();
1897      }
1898    } else {
1899
1900    }
1901  } else {
1902
1903  }
1904  {
1905#line 298
1906  tmp = ldv_some_page();
1907  }
1908#line 298
1909  return (tmp);
1910}
1911}
1912#line 302 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1913void ldv_check_alloc_nonatomic(void) 
1914{ 
1915
1916  {
1917#line 305
1918  if (ldv_spin != 0) {
1919    {
1920#line 305
1921    ldv_blast_assert();
1922    }
1923  } else {
1924
1925  }
1926#line 308
1927  return;
1928}
1929}
1930#line 309 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1931void ldv_spin_lock(void) 
1932{ 
1933
1934  {
1935#line 312
1936  ldv_spin = 1;
1937#line 313
1938  return;
1939}
1940}
1941#line 316 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1942void ldv_spin_unlock(void) 
1943{ 
1944
1945  {
1946#line 319
1947  ldv_spin = 0;
1948#line 320
1949  return;
1950}
1951}
1952#line 323 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1953int ldv_spin_trylock(void) 
1954{ int is_lock ;
1955
1956  {
1957  {
1958#line 328
1959  is_lock = __VERIFIER_nondet_int();
1960  }
1961#line 330
1962  if (is_lock != 0) {
1963#line 333
1964    return (0);
1965  } else {
1966#line 338
1967    ldv_spin = 1;
1968#line 340
1969    return (1);
1970  }
1971}
1972}
1973#line 507 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1974void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
1975{ 
1976
1977  {
1978  {
1979#line 513
1980  ldv_check_alloc_flags(ldv_func_arg2);
1981#line 515
1982  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1983  }
1984#line 516
1985  return ((void *)0);
1986}
1987}