Showing error 605

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-pcap.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3464
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 19 "include/asm-generic/int-ll64.h"
   5typedef signed char __s8;
   6#line 22 "include/asm-generic/int-ll64.h"
   7typedef short __s16;
   8#line 23 "include/asm-generic/int-ll64.h"
   9typedef unsigned short __u16;
  10#line 25 "include/asm-generic/int-ll64.h"
  11typedef int __s32;
  12#line 26 "include/asm-generic/int-ll64.h"
  13typedef unsigned int __u32;
  14#line 30 "include/asm-generic/int-ll64.h"
  15typedef unsigned long long __u64;
  16#line 43 "include/asm-generic/int-ll64.h"
  17typedef unsigned char u8;
  18#line 45 "include/asm-generic/int-ll64.h"
  19typedef short s16;
  20#line 46 "include/asm-generic/int-ll64.h"
  21typedef unsigned short u16;
  22#line 48 "include/asm-generic/int-ll64.h"
  23typedef int s32;
  24#line 49 "include/asm-generic/int-ll64.h"
  25typedef unsigned int u32;
  26#line 51 "include/asm-generic/int-ll64.h"
  27typedef long long s64;
  28#line 52 "include/asm-generic/int-ll64.h"
  29typedef unsigned long long u64;
  30#line 14 "include/asm-generic/posix_types.h"
  31typedef long __kernel_long_t;
  32#line 15 "include/asm-generic/posix_types.h"
  33typedef unsigned long __kernel_ulong_t;
  34#line 52 "include/asm-generic/posix_types.h"
  35typedef unsigned int __kernel_uid32_t;
  36#line 53 "include/asm-generic/posix_types.h"
  37typedef unsigned int __kernel_gid32_t;
  38#line 75 "include/asm-generic/posix_types.h"
  39typedef __kernel_ulong_t __kernel_size_t;
  40#line 76 "include/asm-generic/posix_types.h"
  41typedef __kernel_long_t __kernel_ssize_t;
  42#line 91 "include/asm-generic/posix_types.h"
  43typedef long long __kernel_loff_t;
  44#line 92 "include/asm-generic/posix_types.h"
  45typedef __kernel_long_t __kernel_time_t;
  46#line 95 "include/asm-generic/posix_types.h"
  47typedef int __kernel_clockid_t;
  48#line 21 "include/linux/types.h"
  49typedef __u32 __kernel_dev_t;
  50#line 24 "include/linux/types.h"
  51typedef __kernel_dev_t dev_t;
  52#line 27 "include/linux/types.h"
  53typedef unsigned short umode_t;
  54#line 35 "include/linux/types.h"
  55typedef __kernel_clockid_t clockid_t;
  56#line 38 "include/linux/types.h"
  57typedef _Bool bool;
  58#line 40 "include/linux/types.h"
  59typedef __kernel_uid32_t uid_t;
  60#line 41 "include/linux/types.h"
  61typedef __kernel_gid32_t gid_t;
  62#line 54 "include/linux/types.h"
  63typedef __kernel_loff_t loff_t;
  64#line 63 "include/linux/types.h"
  65typedef __kernel_size_t size_t;
  66#line 68 "include/linux/types.h"
  67typedef __kernel_ssize_t ssize_t;
  68#line 78 "include/linux/types.h"
  69typedef __kernel_time_t time_t;
  70#line 142 "include/linux/types.h"
  71typedef unsigned long sector_t;
  72#line 143 "include/linux/types.h"
  73typedef unsigned long blkcnt_t;
  74#line 202 "include/linux/types.h"
  75typedef unsigned int gfp_t;
  76#line 203 "include/linux/types.h"
  77typedef unsigned int fmode_t;
  78#line 206 "include/linux/types.h"
  79typedef u64 phys_addr_t;
  80#line 211 "include/linux/types.h"
  81typedef phys_addr_t resource_size_t;
  82#line 219 "include/linux/types.h"
  83struct __anonstruct_atomic_t_7 {
  84   int counter ;
  85};
  86#line 219 "include/linux/types.h"
  87typedef struct __anonstruct_atomic_t_7 atomic_t;
  88#line 224 "include/linux/types.h"
  89struct __anonstruct_atomic64_t_8 {
  90   long counter ;
  91};
  92#line 224 "include/linux/types.h"
  93typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  94#line 229 "include/linux/types.h"
  95struct list_head {
  96   struct list_head *next ;
  97   struct list_head *prev ;
  98};
  99#line 233
 100struct hlist_node;
 101#line 233 "include/linux/types.h"
 102struct hlist_head {
 103   struct hlist_node *first ;
 104};
 105#line 237 "include/linux/types.h"
 106struct hlist_node {
 107   struct hlist_node *next ;
 108   struct hlist_node **pprev ;
 109};
 110#line 253 "include/linux/types.h"
 111struct rcu_head {
 112   struct rcu_head *next ;
 113   void (*func)(struct rcu_head *head ) ;
 114};
 115#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 116struct module;
 117#line 56
 118struct module;
 119#line 146 "include/linux/init.h"
 120typedef void (*ctor_fn_t)(void);
 121#line 47 "include/linux/dynamic_debug.h"
 122struct device;
 123#line 47
 124struct device;
 125#line 135 "include/linux/kernel.h"
 126struct completion;
 127#line 135
 128struct completion;
 129#line 349
 130struct pid;
 131#line 349
 132struct pid;
 133#line 12 "include/linux/thread_info.h"
 134struct timespec;
 135#line 12
 136struct timespec;
 137#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 138struct page;
 139#line 18
 140struct page;
 141#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 142struct task_struct;
 143#line 20
 144struct task_struct;
 145#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 146struct task_struct;
 147#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 148struct file;
 149#line 295
 150struct file;
 151#line 313
 152struct seq_file;
 153#line 313
 154struct seq_file;
 155#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 156struct page;
 157#line 52
 158struct task_struct;
 159#line 329
 160struct arch_spinlock;
 161#line 329
 162struct arch_spinlock;
 163#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 164struct task_struct;
 165#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 166struct task_struct;
 167#line 10 "include/asm-generic/bug.h"
 168struct bug_entry {
 169   int bug_addr_disp ;
 170   int file_disp ;
 171   unsigned short line ;
 172   unsigned short flags ;
 173};
 174#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 175struct static_key;
 176#line 234
 177struct static_key;
 178#line 153 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 179struct seq_operations;
 180#line 433
 181struct kmem_cache;
 182#line 23 "include/asm-generic/atomic-long.h"
 183typedef atomic64_t atomic_long_t;
 184#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 185typedef u16 __ticket_t;
 186#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 187typedef u32 __ticketpair_t;
 188#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 189struct __raw_tickets {
 190   __ticket_t head ;
 191   __ticket_t tail ;
 192};
 193#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 194union __anonunion____missing_field_name_36 {
 195   __ticketpair_t head_tail ;
 196   struct __raw_tickets tickets ;
 197};
 198#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 199struct arch_spinlock {
 200   union __anonunion____missing_field_name_36 __annonCompField17 ;
 201};
 202#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 203typedef struct arch_spinlock arch_spinlock_t;
 204#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 205struct __anonstruct____missing_field_name_38 {
 206   u32 read ;
 207   s32 write ;
 208};
 209#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 210union __anonunion_arch_rwlock_t_37 {
 211   s64 lock ;
 212   struct __anonstruct____missing_field_name_38 __annonCompField18 ;
 213};
 214#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 215typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
 216#line 12 "include/linux/lockdep.h"
 217struct task_struct;
 218#line 391 "include/linux/lockdep.h"
 219struct lock_class_key {
 220
 221};
 222#line 20 "include/linux/spinlock_types.h"
 223struct raw_spinlock {
 224   arch_spinlock_t raw_lock ;
 225   unsigned int magic ;
 226   unsigned int owner_cpu ;
 227   void *owner ;
 228};
 229#line 20 "include/linux/spinlock_types.h"
 230typedef struct raw_spinlock raw_spinlock_t;
 231#line 64 "include/linux/spinlock_types.h"
 232union __anonunion____missing_field_name_39 {
 233   struct raw_spinlock rlock ;
 234};
 235#line 64 "include/linux/spinlock_types.h"
 236struct spinlock {
 237   union __anonunion____missing_field_name_39 __annonCompField19 ;
 238};
 239#line 64 "include/linux/spinlock_types.h"
 240typedef struct spinlock spinlock_t;
 241#line 11 "include/linux/rwlock_types.h"
 242struct __anonstruct_rwlock_t_40 {
 243   arch_rwlock_t raw_lock ;
 244   unsigned int magic ;
 245   unsigned int owner_cpu ;
 246   void *owner ;
 247};
 248#line 11 "include/linux/rwlock_types.h"
 249typedef struct __anonstruct_rwlock_t_40 rwlock_t;
 250#line 119 "include/linux/seqlock.h"
 251struct seqcount {
 252   unsigned int sequence ;
 253};
 254#line 119 "include/linux/seqlock.h"
 255typedef struct seqcount seqcount_t;
 256#line 14 "include/linux/time.h"
 257struct timespec {
 258   __kernel_time_t tv_sec ;
 259   long tv_nsec ;
 260};
 261#line 62 "include/linux/stat.h"
 262struct kstat {
 263   u64 ino ;
 264   dev_t dev ;
 265   umode_t mode ;
 266   unsigned int nlink ;
 267   uid_t uid ;
 268   gid_t gid ;
 269   dev_t rdev ;
 270   loff_t size ;
 271   struct timespec atime ;
 272   struct timespec mtime ;
 273   struct timespec ctime ;
 274   unsigned long blksize ;
 275   unsigned long long blocks ;
 276};
 277#line 49 "include/linux/wait.h"
 278struct __wait_queue_head {
 279   spinlock_t lock ;
 280   struct list_head task_list ;
 281};
 282#line 53 "include/linux/wait.h"
 283typedef struct __wait_queue_head wait_queue_head_t;
 284#line 55
 285struct task_struct;
 286#line 60 "include/linux/pageblock-flags.h"
 287struct page;
 288#line 48 "include/linux/mutex.h"
 289struct mutex {
 290   atomic_t count ;
 291   spinlock_t wait_lock ;
 292   struct list_head wait_list ;
 293   struct task_struct *owner ;
 294   char const   *name ;
 295   void *magic ;
 296};
 297#line 19 "include/linux/rwsem.h"
 298struct rw_semaphore;
 299#line 19
 300struct rw_semaphore;
 301#line 25 "include/linux/rwsem.h"
 302struct rw_semaphore {
 303   long count ;
 304   raw_spinlock_t wait_lock ;
 305   struct list_head wait_list ;
 306};
 307#line 25 "include/linux/completion.h"
 308struct completion {
 309   unsigned int done ;
 310   wait_queue_head_t wait ;
 311};
 312#line 9 "include/linux/memory_hotplug.h"
 313struct page;
 314#line 18 "include/linux/ioport.h"
 315struct resource {
 316   resource_size_t start ;
 317   resource_size_t end ;
 318   char const   *name ;
 319   unsigned long flags ;
 320   struct resource *parent ;
 321   struct resource *sibling ;
 322   struct resource *child ;
 323};
 324#line 202
 325struct device;
 326#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 327struct device;
 328#line 46 "include/linux/ktime.h"
 329union ktime {
 330   s64 tv64 ;
 331};
 332#line 59 "include/linux/ktime.h"
 333typedef union ktime ktime_t;
 334#line 10 "include/linux/timer.h"
 335struct tvec_base;
 336#line 10
 337struct tvec_base;
 338#line 12 "include/linux/timer.h"
 339struct timer_list {
 340   struct list_head entry ;
 341   unsigned long expires ;
 342   struct tvec_base *base ;
 343   void (*function)(unsigned long  ) ;
 344   unsigned long data ;
 345   int slack ;
 346   int start_pid ;
 347   void *start_site ;
 348   char start_comm[16] ;
 349};
 350#line 289
 351struct hrtimer;
 352#line 289
 353struct hrtimer;
 354#line 290
 355enum hrtimer_restart;
 356#line 17 "include/linux/workqueue.h"
 357struct work_struct;
 358#line 17
 359struct work_struct;
 360#line 79 "include/linux/workqueue.h"
 361struct work_struct {
 362   atomic_long_t data ;
 363   struct list_head entry ;
 364   void (*func)(struct work_struct *work ) ;
 365};
 366#line 42 "include/linux/pm.h"
 367struct device;
 368#line 50 "include/linux/pm.h"
 369struct pm_message {
 370   int event ;
 371};
 372#line 50 "include/linux/pm.h"
 373typedef struct pm_message pm_message_t;
 374#line 264 "include/linux/pm.h"
 375struct dev_pm_ops {
 376   int (*prepare)(struct device *dev ) ;
 377   void (*complete)(struct device *dev ) ;
 378   int (*suspend)(struct device *dev ) ;
 379   int (*resume)(struct device *dev ) ;
 380   int (*freeze)(struct device *dev ) ;
 381   int (*thaw)(struct device *dev ) ;
 382   int (*poweroff)(struct device *dev ) ;
 383   int (*restore)(struct device *dev ) ;
 384   int (*suspend_late)(struct device *dev ) ;
 385   int (*resume_early)(struct device *dev ) ;
 386   int (*freeze_late)(struct device *dev ) ;
 387   int (*thaw_early)(struct device *dev ) ;
 388   int (*poweroff_late)(struct device *dev ) ;
 389   int (*restore_early)(struct device *dev ) ;
 390   int (*suspend_noirq)(struct device *dev ) ;
 391   int (*resume_noirq)(struct device *dev ) ;
 392   int (*freeze_noirq)(struct device *dev ) ;
 393   int (*thaw_noirq)(struct device *dev ) ;
 394   int (*poweroff_noirq)(struct device *dev ) ;
 395   int (*restore_noirq)(struct device *dev ) ;
 396   int (*runtime_suspend)(struct device *dev ) ;
 397   int (*runtime_resume)(struct device *dev ) ;
 398   int (*runtime_idle)(struct device *dev ) ;
 399};
 400#line 458
 401enum rpm_status {
 402    RPM_ACTIVE = 0,
 403    RPM_RESUMING = 1,
 404    RPM_SUSPENDED = 2,
 405    RPM_SUSPENDING = 3
 406} ;
 407#line 480
 408enum rpm_request {
 409    RPM_REQ_NONE = 0,
 410    RPM_REQ_IDLE = 1,
 411    RPM_REQ_SUSPEND = 2,
 412    RPM_REQ_AUTOSUSPEND = 3,
 413    RPM_REQ_RESUME = 4
 414} ;
 415#line 488
 416struct wakeup_source;
 417#line 488
 418struct wakeup_source;
 419#line 495 "include/linux/pm.h"
 420struct pm_subsys_data {
 421   spinlock_t lock ;
 422   unsigned int refcount ;
 423};
 424#line 506
 425struct dev_pm_qos_request;
 426#line 506
 427struct pm_qos_constraints;
 428#line 506 "include/linux/pm.h"
 429struct dev_pm_info {
 430   pm_message_t power_state ;
 431   unsigned int can_wakeup : 1 ;
 432   unsigned int async_suspend : 1 ;
 433   bool is_prepared : 1 ;
 434   bool is_suspended : 1 ;
 435   bool ignore_children : 1 ;
 436   spinlock_t lock ;
 437   struct list_head entry ;
 438   struct completion completion ;
 439   struct wakeup_source *wakeup ;
 440   bool wakeup_path : 1 ;
 441   struct timer_list suspend_timer ;
 442   unsigned long timer_expires ;
 443   struct work_struct work ;
 444   wait_queue_head_t wait_queue ;
 445   atomic_t usage_count ;
 446   atomic_t child_count ;
 447   unsigned int disable_depth : 3 ;
 448   unsigned int idle_notification : 1 ;
 449   unsigned int request_pending : 1 ;
 450   unsigned int deferred_resume : 1 ;
 451   unsigned int run_wake : 1 ;
 452   unsigned int runtime_auto : 1 ;
 453   unsigned int no_callbacks : 1 ;
 454   unsigned int irq_safe : 1 ;
 455   unsigned int use_autosuspend : 1 ;
 456   unsigned int timer_autosuspends : 1 ;
 457   enum rpm_request request ;
 458   enum rpm_status runtime_status ;
 459   int runtime_error ;
 460   int autosuspend_delay ;
 461   unsigned long last_busy ;
 462   unsigned long active_jiffies ;
 463   unsigned long suspended_jiffies ;
 464   unsigned long accounting_timestamp ;
 465   ktime_t suspend_time ;
 466   s64 max_time_suspended_ns ;
 467   struct dev_pm_qos_request *pq_req ;
 468   struct pm_subsys_data *subsys_data ;
 469   struct pm_qos_constraints *constraints ;
 470};
 471#line 564 "include/linux/pm.h"
 472struct dev_pm_domain {
 473   struct dev_pm_ops ops ;
 474};
 475#line 8 "include/linux/vmalloc.h"
 476struct vm_area_struct;
 477#line 8
 478struct vm_area_struct;
 479#line 994 "include/linux/mmzone.h"
 480struct page;
 481#line 10 "include/linux/gfp.h"
 482struct vm_area_struct;
 483#line 29 "include/linux/sysctl.h"
 484struct completion;
 485#line 100 "include/linux/rbtree.h"
 486struct rb_node {
 487   unsigned long rb_parent_color ;
 488   struct rb_node *rb_right ;
 489   struct rb_node *rb_left ;
 490} __attribute__((__aligned__(sizeof(long )))) ;
 491#line 110 "include/linux/rbtree.h"
 492struct rb_root {
 493   struct rb_node *rb_node ;
 494};
 495#line 48 "include/linux/kmod.h"
 496struct cred;
 497#line 48
 498struct cred;
 499#line 49
 500struct file;
 501#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 502struct task_struct;
 503#line 18 "include/linux/elf.h"
 504typedef __u64 Elf64_Addr;
 505#line 19 "include/linux/elf.h"
 506typedef __u16 Elf64_Half;
 507#line 23 "include/linux/elf.h"
 508typedef __u32 Elf64_Word;
 509#line 24 "include/linux/elf.h"
 510typedef __u64 Elf64_Xword;
 511#line 194 "include/linux/elf.h"
 512struct elf64_sym {
 513   Elf64_Word st_name ;
 514   unsigned char st_info ;
 515   unsigned char st_other ;
 516   Elf64_Half st_shndx ;
 517   Elf64_Addr st_value ;
 518   Elf64_Xword st_size ;
 519};
 520#line 194 "include/linux/elf.h"
 521typedef struct elf64_sym Elf64_Sym;
 522#line 438
 523struct file;
 524#line 20 "include/linux/kobject_ns.h"
 525struct sock;
 526#line 20
 527struct sock;
 528#line 21
 529struct kobject;
 530#line 21
 531struct kobject;
 532#line 27
 533enum kobj_ns_type {
 534    KOBJ_NS_TYPE_NONE = 0,
 535    KOBJ_NS_TYPE_NET = 1,
 536    KOBJ_NS_TYPES = 2
 537} ;
 538#line 40 "include/linux/kobject_ns.h"
 539struct kobj_ns_type_operations {
 540   enum kobj_ns_type type ;
 541   void *(*grab_current_ns)(void) ;
 542   void const   *(*netlink_ns)(struct sock *sk ) ;
 543   void const   *(*initial_ns)(void) ;
 544   void (*drop_ns)(void * ) ;
 545};
 546#line 22 "include/linux/sysfs.h"
 547struct kobject;
 548#line 23
 549struct module;
 550#line 24
 551enum kobj_ns_type;
 552#line 26 "include/linux/sysfs.h"
 553struct attribute {
 554   char const   *name ;
 555   umode_t mode ;
 556};
 557#line 56 "include/linux/sysfs.h"
 558struct attribute_group {
 559   char const   *name ;
 560   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 561   struct attribute **attrs ;
 562};
 563#line 85
 564struct file;
 565#line 86
 566struct vm_area_struct;
 567#line 88 "include/linux/sysfs.h"
 568struct bin_attribute {
 569   struct attribute attr ;
 570   size_t size ;
 571   void *private ;
 572   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 573                   loff_t  , size_t  ) ;
 574   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 575                    loff_t  , size_t  ) ;
 576   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 577};
 578#line 112 "include/linux/sysfs.h"
 579struct sysfs_ops {
 580   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 581   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 582   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 583};
 584#line 118
 585struct sysfs_dirent;
 586#line 118
 587struct sysfs_dirent;
 588#line 22 "include/linux/kref.h"
 589struct kref {
 590   atomic_t refcount ;
 591};
 592#line 60 "include/linux/kobject.h"
 593struct kset;
 594#line 60
 595struct kobj_type;
 596#line 60 "include/linux/kobject.h"
 597struct kobject {
 598   char const   *name ;
 599   struct list_head entry ;
 600   struct kobject *parent ;
 601   struct kset *kset ;
 602   struct kobj_type *ktype ;
 603   struct sysfs_dirent *sd ;
 604   struct kref kref ;
 605   unsigned int state_initialized : 1 ;
 606   unsigned int state_in_sysfs : 1 ;
 607   unsigned int state_add_uevent_sent : 1 ;
 608   unsigned int state_remove_uevent_sent : 1 ;
 609   unsigned int uevent_suppress : 1 ;
 610};
 611#line 108 "include/linux/kobject.h"
 612struct kobj_type {
 613   void (*release)(struct kobject *kobj ) ;
 614   struct sysfs_ops  const  *sysfs_ops ;
 615   struct attribute **default_attrs ;
 616   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 617   void const   *(*namespace)(struct kobject *kobj ) ;
 618};
 619#line 116 "include/linux/kobject.h"
 620struct kobj_uevent_env {
 621   char *envp[32] ;
 622   int envp_idx ;
 623   char buf[2048] ;
 624   int buflen ;
 625};
 626#line 123 "include/linux/kobject.h"
 627struct kset_uevent_ops {
 628   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 629   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 630   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 631};
 632#line 140
 633struct sock;
 634#line 159 "include/linux/kobject.h"
 635struct kset {
 636   struct list_head list ;
 637   spinlock_t list_lock ;
 638   struct kobject kobj ;
 639   struct kset_uevent_ops  const  *uevent_ops ;
 640};
 641#line 39 "include/linux/moduleparam.h"
 642struct kernel_param;
 643#line 39
 644struct kernel_param;
 645#line 41 "include/linux/moduleparam.h"
 646struct kernel_param_ops {
 647   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 648   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 649   void (*free)(void *arg ) ;
 650};
 651#line 50
 652struct kparam_string;
 653#line 50
 654struct kparam_array;
 655#line 50 "include/linux/moduleparam.h"
 656union __anonunion____missing_field_name_199 {
 657   void *arg ;
 658   struct kparam_string  const  *str ;
 659   struct kparam_array  const  *arr ;
 660};
 661#line 50 "include/linux/moduleparam.h"
 662struct kernel_param {
 663   char const   *name ;
 664   struct kernel_param_ops  const  *ops ;
 665   u16 perm ;
 666   s16 level ;
 667   union __anonunion____missing_field_name_199 __annonCompField32 ;
 668};
 669#line 63 "include/linux/moduleparam.h"
 670struct kparam_string {
 671   unsigned int maxlen ;
 672   char *string ;
 673};
 674#line 69 "include/linux/moduleparam.h"
 675struct kparam_array {
 676   unsigned int max ;
 677   unsigned int elemsize ;
 678   unsigned int *num ;
 679   struct kernel_param_ops  const  *ops ;
 680   void *elem ;
 681};
 682#line 445
 683struct module;
 684#line 80 "include/linux/jump_label.h"
 685struct module;
 686#line 143 "include/linux/jump_label.h"
 687struct static_key {
 688   atomic_t enabled ;
 689};
 690#line 22 "include/linux/tracepoint.h"
 691struct module;
 692#line 23
 693struct tracepoint;
 694#line 23
 695struct tracepoint;
 696#line 25 "include/linux/tracepoint.h"
 697struct tracepoint_func {
 698   void *func ;
 699   void *data ;
 700};
 701#line 30 "include/linux/tracepoint.h"
 702struct tracepoint {
 703   char const   *name ;
 704   struct static_key key ;
 705   void (*regfunc)(void) ;
 706   void (*unregfunc)(void) ;
 707   struct tracepoint_func *funcs ;
 708};
 709#line 19 "include/linux/export.h"
 710struct kernel_symbol {
 711   unsigned long value ;
 712   char const   *name ;
 713};
 714#line 8 "include/asm-generic/module.h"
 715struct mod_arch_specific {
 716
 717};
 718#line 35 "include/linux/module.h"
 719struct module;
 720#line 37
 721struct module_param_attrs;
 722#line 37 "include/linux/module.h"
 723struct module_kobject {
 724   struct kobject kobj ;
 725   struct module *mod ;
 726   struct kobject *drivers_dir ;
 727   struct module_param_attrs *mp ;
 728};
 729#line 44 "include/linux/module.h"
 730struct module_attribute {
 731   struct attribute attr ;
 732   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 733   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 734                    size_t count ) ;
 735   void (*setup)(struct module * , char const   * ) ;
 736   int (*test)(struct module * ) ;
 737   void (*free)(struct module * ) ;
 738};
 739#line 71
 740struct exception_table_entry;
 741#line 71
 742struct exception_table_entry;
 743#line 199
 744enum module_state {
 745    MODULE_STATE_LIVE = 0,
 746    MODULE_STATE_COMING = 1,
 747    MODULE_STATE_GOING = 2
 748} ;
 749#line 215 "include/linux/module.h"
 750struct module_ref {
 751   unsigned long incs ;
 752   unsigned long decs ;
 753} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 754#line 220
 755struct module_sect_attrs;
 756#line 220
 757struct module_notes_attrs;
 758#line 220
 759struct ftrace_event_call;
 760#line 220 "include/linux/module.h"
 761struct module {
 762   enum module_state state ;
 763   struct list_head list ;
 764   char name[64UL - sizeof(unsigned long )] ;
 765   struct module_kobject mkobj ;
 766   struct module_attribute *modinfo_attrs ;
 767   char const   *version ;
 768   char const   *srcversion ;
 769   struct kobject *holders_dir ;
 770   struct kernel_symbol  const  *syms ;
 771   unsigned long const   *crcs ;
 772   unsigned int num_syms ;
 773   struct kernel_param *kp ;
 774   unsigned int num_kp ;
 775   unsigned int num_gpl_syms ;
 776   struct kernel_symbol  const  *gpl_syms ;
 777   unsigned long const   *gpl_crcs ;
 778   struct kernel_symbol  const  *unused_syms ;
 779   unsigned long const   *unused_crcs ;
 780   unsigned int num_unused_syms ;
 781   unsigned int num_unused_gpl_syms ;
 782   struct kernel_symbol  const  *unused_gpl_syms ;
 783   unsigned long const   *unused_gpl_crcs ;
 784   struct kernel_symbol  const  *gpl_future_syms ;
 785   unsigned long const   *gpl_future_crcs ;
 786   unsigned int num_gpl_future_syms ;
 787   unsigned int num_exentries ;
 788   struct exception_table_entry *extable ;
 789   int (*init)(void) ;
 790   void *module_init ;
 791   void *module_core ;
 792   unsigned int init_size ;
 793   unsigned int core_size ;
 794   unsigned int init_text_size ;
 795   unsigned int core_text_size ;
 796   unsigned int init_ro_size ;
 797   unsigned int core_ro_size ;
 798   struct mod_arch_specific arch ;
 799   unsigned int taints ;
 800   unsigned int num_bugs ;
 801   struct list_head bug_list ;
 802   struct bug_entry *bug_table ;
 803   Elf64_Sym *symtab ;
 804   Elf64_Sym *core_symtab ;
 805   unsigned int num_symtab ;
 806   unsigned int core_num_syms ;
 807   char *strtab ;
 808   char *core_strtab ;
 809   struct module_sect_attrs *sect_attrs ;
 810   struct module_notes_attrs *notes_attrs ;
 811   char *args ;
 812   void *percpu ;
 813   unsigned int percpu_size ;
 814   unsigned int num_tracepoints ;
 815   struct tracepoint * const  *tracepoints_ptrs ;
 816   unsigned int num_trace_bprintk_fmt ;
 817   char const   **trace_bprintk_fmt_start ;
 818   struct ftrace_event_call **trace_events ;
 819   unsigned int num_trace_events ;
 820   struct list_head source_list ;
 821   struct list_head target_list ;
 822   struct task_struct *waiter ;
 823   void (*exit)(void) ;
 824   struct module_ref *refptr ;
 825   ctor_fn_t *ctors ;
 826   unsigned int num_ctors ;
 827};
 828#line 24 "include/linux/mfd/ezx-pcap.h"
 829struct pcap_chip;
 830#line 24
 831struct pcap_chip;
 832#line 20 "include/linux/rtc.h"
 833struct rtc_time {
 834   int tm_sec ;
 835   int tm_min ;
 836   int tm_hour ;
 837   int tm_mday ;
 838   int tm_mon ;
 839   int tm_year ;
 840   int tm_wday ;
 841   int tm_yday ;
 842   int tm_isdst ;
 843};
 844#line 36 "include/linux/rtc.h"
 845struct rtc_wkalrm {
 846   unsigned char enabled ;
 847   unsigned char pending ;
 848   struct rtc_time time ;
 849};
 850#line 10 "include/linux/irqreturn.h"
 851enum irqreturn {
 852    IRQ_NONE = 0,
 853    IRQ_HANDLED = 1,
 854    IRQ_WAKE_THREAD = 2
 855} ;
 856#line 16 "include/linux/irqreturn.h"
 857typedef enum irqreturn irqreturn_t;
 858#line 31 "include/linux/irq.h"
 859struct seq_file;
 860#line 32
 861struct module;
 862#line 14 "include/linux/irqdesc.h"
 863struct module;
 864#line 65 "include/linux/profile.h"
 865struct task_struct;
 866#line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess.h"
 867struct exception_table_entry {
 868   unsigned long insn ;
 869   unsigned long fixup ;
 870};
 871#line 132 "include/linux/hardirq.h"
 872struct task_struct;
 873#line 8 "include/linux/timerqueue.h"
 874struct timerqueue_node {
 875   struct rb_node node ;
 876   ktime_t expires ;
 877};
 878#line 13 "include/linux/timerqueue.h"
 879struct timerqueue_head {
 880   struct rb_root head ;
 881   struct timerqueue_node *next ;
 882};
 883#line 27 "include/linux/hrtimer.h"
 884struct hrtimer_clock_base;
 885#line 27
 886struct hrtimer_clock_base;
 887#line 28
 888struct hrtimer_cpu_base;
 889#line 28
 890struct hrtimer_cpu_base;
 891#line 44
 892enum hrtimer_restart {
 893    HRTIMER_NORESTART = 0,
 894    HRTIMER_RESTART = 1
 895} ;
 896#line 108 "include/linux/hrtimer.h"
 897struct hrtimer {
 898   struct timerqueue_node node ;
 899   ktime_t _softexpires ;
 900   enum hrtimer_restart (*function)(struct hrtimer * ) ;
 901   struct hrtimer_clock_base *base ;
 902   unsigned long state ;
 903   int start_pid ;
 904   void *start_site ;
 905   char start_comm[16] ;
 906};
 907#line 145 "include/linux/hrtimer.h"
 908struct hrtimer_clock_base {
 909   struct hrtimer_cpu_base *cpu_base ;
 910   int index ;
 911   clockid_t clockid ;
 912   struct timerqueue_head active ;
 913   ktime_t resolution ;
 914   ktime_t (*get_time)(void) ;
 915   ktime_t softirq_time ;
 916   ktime_t offset ;
 917};
 918#line 178 "include/linux/hrtimer.h"
 919struct hrtimer_cpu_base {
 920   raw_spinlock_t lock ;
 921   unsigned long active_bases ;
 922   ktime_t expires_next ;
 923   int hres_active ;
 924   int hang_detected ;
 925   unsigned long nr_events ;
 926   unsigned long nr_retries ;
 927   unsigned long nr_hangs ;
 928   ktime_t max_hang_time ;
 929   struct hrtimer_clock_base clock_base[3] ;
 930};
 931#line 187 "include/linux/interrupt.h"
 932struct device;
 933#line 695
 934struct seq_file;
 935#line 19 "include/linux/klist.h"
 936struct klist_node;
 937#line 19
 938struct klist_node;
 939#line 39 "include/linux/klist.h"
 940struct klist_node {
 941   void *n_klist ;
 942   struct list_head n_node ;
 943   struct kref n_ref ;
 944};
 945#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 946struct dma_map_ops;
 947#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 948struct dev_archdata {
 949   void *acpi_handle ;
 950   struct dma_map_ops *dma_ops ;
 951   void *iommu ;
 952};
 953#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 954struct pdev_archdata {
 955
 956};
 957#line 28 "include/linux/device.h"
 958struct device;
 959#line 29
 960struct device_private;
 961#line 29
 962struct device_private;
 963#line 30
 964struct device_driver;
 965#line 30
 966struct device_driver;
 967#line 31
 968struct driver_private;
 969#line 31
 970struct driver_private;
 971#line 32
 972struct module;
 973#line 33
 974struct class;
 975#line 33
 976struct class;
 977#line 34
 978struct subsys_private;
 979#line 34
 980struct subsys_private;
 981#line 35
 982struct bus_type;
 983#line 35
 984struct bus_type;
 985#line 36
 986struct device_node;
 987#line 36
 988struct device_node;
 989#line 37
 990struct iommu_ops;
 991#line 37
 992struct iommu_ops;
 993#line 39 "include/linux/device.h"
 994struct bus_attribute {
 995   struct attribute attr ;
 996   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
 997   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 998};
 999#line 89
1000struct device_attribute;
1001#line 89
1002struct driver_attribute;
1003#line 89 "include/linux/device.h"
1004struct bus_type {
1005   char const   *name ;
1006   char const   *dev_name ;
1007   struct device *dev_root ;
1008   struct bus_attribute *bus_attrs ;
1009   struct device_attribute *dev_attrs ;
1010   struct driver_attribute *drv_attrs ;
1011   int (*match)(struct device *dev , struct device_driver *drv ) ;
1012   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1013   int (*probe)(struct device *dev ) ;
1014   int (*remove)(struct device *dev ) ;
1015   void (*shutdown)(struct device *dev ) ;
1016   int (*suspend)(struct device *dev , pm_message_t state ) ;
1017   int (*resume)(struct device *dev ) ;
1018   struct dev_pm_ops  const  *pm ;
1019   struct iommu_ops *iommu_ops ;
1020   struct subsys_private *p ;
1021};
1022#line 127
1023struct device_type;
1024#line 214
1025struct of_device_id;
1026#line 214 "include/linux/device.h"
1027struct device_driver {
1028   char const   *name ;
1029   struct bus_type *bus ;
1030   struct module *owner ;
1031   char const   *mod_name ;
1032   bool suppress_bind_attrs ;
1033   struct of_device_id  const  *of_match_table ;
1034   int (*probe)(struct device *dev ) ;
1035   int (*remove)(struct device *dev ) ;
1036   void (*shutdown)(struct device *dev ) ;
1037   int (*suspend)(struct device *dev , pm_message_t state ) ;
1038   int (*resume)(struct device *dev ) ;
1039   struct attribute_group  const  **groups ;
1040   struct dev_pm_ops  const  *pm ;
1041   struct driver_private *p ;
1042};
1043#line 249 "include/linux/device.h"
1044struct driver_attribute {
1045   struct attribute attr ;
1046   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1047   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
1048};
1049#line 330
1050struct class_attribute;
1051#line 330 "include/linux/device.h"
1052struct class {
1053   char const   *name ;
1054   struct module *owner ;
1055   struct class_attribute *class_attrs ;
1056   struct device_attribute *dev_attrs ;
1057   struct bin_attribute *dev_bin_attrs ;
1058   struct kobject *dev_kobj ;
1059   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1060   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1061   void (*class_release)(struct class *class ) ;
1062   void (*dev_release)(struct device *dev ) ;
1063   int (*suspend)(struct device *dev , pm_message_t state ) ;
1064   int (*resume)(struct device *dev ) ;
1065   struct kobj_ns_type_operations  const  *ns_type ;
1066   void const   *(*namespace)(struct device *dev ) ;
1067   struct dev_pm_ops  const  *pm ;
1068   struct subsys_private *p ;
1069};
1070#line 397 "include/linux/device.h"
1071struct class_attribute {
1072   struct attribute attr ;
1073   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1074   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
1075                    size_t count ) ;
1076   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
1077};
1078#line 465 "include/linux/device.h"
1079struct device_type {
1080   char const   *name ;
1081   struct attribute_group  const  **groups ;
1082   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1083   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1084   void (*release)(struct device *dev ) ;
1085   struct dev_pm_ops  const  *pm ;
1086};
1087#line 476 "include/linux/device.h"
1088struct device_attribute {
1089   struct attribute attr ;
1090   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1091   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
1092                    size_t count ) ;
1093};
1094#line 559 "include/linux/device.h"
1095struct device_dma_parameters {
1096   unsigned int max_segment_size ;
1097   unsigned long segment_boundary_mask ;
1098};
1099#line 627
1100struct dma_coherent_mem;
1101#line 627 "include/linux/device.h"
1102struct device {
1103   struct device *parent ;
1104   struct device_private *p ;
1105   struct kobject kobj ;
1106   char const   *init_name ;
1107   struct device_type  const  *type ;
1108   struct mutex mutex ;
1109   struct bus_type *bus ;
1110   struct device_driver *driver ;
1111   void *platform_data ;
1112   struct dev_pm_info power ;
1113   struct dev_pm_domain *pm_domain ;
1114   int numa_node ;
1115   u64 *dma_mask ;
1116   u64 coherent_dma_mask ;
1117   struct device_dma_parameters *dma_parms ;
1118   struct list_head dma_pools ;
1119   struct dma_coherent_mem *dma_mem ;
1120   struct dev_archdata archdata ;
1121   struct device_node *of_node ;
1122   dev_t devt ;
1123   u32 id ;
1124   spinlock_t devres_lock ;
1125   struct list_head devres_head ;
1126   struct klist_node knode_class ;
1127   struct class *class ;
1128   struct attribute_group  const  **groups ;
1129   void (*release)(struct device *dev ) ;
1130};
1131#line 43 "include/linux/pm_wakeup.h"
1132struct wakeup_source {
1133   char const   *name ;
1134   struct list_head entry ;
1135   spinlock_t lock ;
1136   struct timer_list timer ;
1137   unsigned long timer_expires ;
1138   ktime_t total_time ;
1139   ktime_t max_time ;
1140   ktime_t last_time ;
1141   unsigned long event_count ;
1142   unsigned long active_count ;
1143   unsigned long relax_count ;
1144   unsigned long hit_count ;
1145   unsigned int active : 1 ;
1146};
1147#line 11 "include/linux/seq_file.h"
1148struct seq_operations;
1149#line 12
1150struct file;
1151#line 13
1152struct path;
1153#line 13
1154struct path;
1155#line 14
1156struct inode;
1157#line 14
1158struct inode;
1159#line 15
1160struct dentry;
1161#line 15
1162struct dentry;
1163#line 17 "include/linux/seq_file.h"
1164struct seq_file {
1165   char *buf ;
1166   size_t size ;
1167   size_t from ;
1168   size_t count ;
1169   loff_t index ;
1170   loff_t read_pos ;
1171   u64 version ;
1172   struct mutex lock ;
1173   struct seq_operations  const  *op ;
1174   int poll_event ;
1175   void *private ;
1176};
1177#line 31 "include/linux/seq_file.h"
1178struct seq_operations {
1179   void *(*start)(struct seq_file *m , loff_t *pos ) ;
1180   void (*stop)(struct seq_file *m , void *v ) ;
1181   void *(*next)(struct seq_file *m , void *v , loff_t *pos ) ;
1182   int (*show)(struct seq_file *m , void *v ) ;
1183};
1184#line 8 "include/linux/cdev.h"
1185struct file_operations;
1186#line 8
1187struct file_operations;
1188#line 9
1189struct inode;
1190#line 10
1191struct module;
1192#line 12 "include/linux/cdev.h"
1193struct cdev {
1194   struct kobject kobj ;
1195   struct module *owner ;
1196   struct file_operations  const  *ops ;
1197   struct list_head list ;
1198   dev_t dev ;
1199   unsigned int count ;
1200};
1201#line 33
1202struct backing_dev_info;
1203#line 15 "include/linux/blk_types.h"
1204struct page;
1205#line 16
1206struct block_device;
1207#line 16
1208struct block_device;
1209#line 33 "include/linux/list_bl.h"
1210struct hlist_bl_node;
1211#line 33 "include/linux/list_bl.h"
1212struct hlist_bl_head {
1213   struct hlist_bl_node *first ;
1214};
1215#line 37 "include/linux/list_bl.h"
1216struct hlist_bl_node {
1217   struct hlist_bl_node *next ;
1218   struct hlist_bl_node **pprev ;
1219};
1220#line 13 "include/linux/dcache.h"
1221struct nameidata;
1222#line 13
1223struct nameidata;
1224#line 14
1225struct path;
1226#line 15
1227struct vfsmount;
1228#line 15
1229struct vfsmount;
1230#line 35 "include/linux/dcache.h"
1231struct qstr {
1232   unsigned int hash ;
1233   unsigned int len ;
1234   unsigned char const   *name ;
1235};
1236#line 88
1237struct dentry_operations;
1238#line 88
1239struct super_block;
1240#line 88 "include/linux/dcache.h"
1241union __anonunion_d_u_209 {
1242   struct list_head d_child ;
1243   struct rcu_head d_rcu ;
1244};
1245#line 88 "include/linux/dcache.h"
1246struct dentry {
1247   unsigned int d_flags ;
1248   seqcount_t d_seq ;
1249   struct hlist_bl_node d_hash ;
1250   struct dentry *d_parent ;
1251   struct qstr d_name ;
1252   struct inode *d_inode ;
1253   unsigned char d_iname[32] ;
1254   unsigned int d_count ;
1255   spinlock_t d_lock ;
1256   struct dentry_operations  const  *d_op ;
1257   struct super_block *d_sb ;
1258   unsigned long d_time ;
1259   void *d_fsdata ;
1260   struct list_head d_lru ;
1261   union __anonunion_d_u_209 d_u ;
1262   struct list_head d_subdirs ;
1263   struct list_head d_alias ;
1264};
1265#line 131 "include/linux/dcache.h"
1266struct dentry_operations {
1267   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1268   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
1269   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
1270                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
1271   int (*d_delete)(struct dentry  const  * ) ;
1272   void (*d_release)(struct dentry * ) ;
1273   void (*d_prune)(struct dentry * ) ;
1274   void (*d_iput)(struct dentry * , struct inode * ) ;
1275   char *(*d_dname)(struct dentry * , char * , int  ) ;
1276   struct vfsmount *(*d_automount)(struct path * ) ;
1277   int (*d_manage)(struct dentry * , bool  ) ;
1278} __attribute__((__aligned__((1) <<  (6) ))) ;
1279#line 4 "include/linux/path.h"
1280struct dentry;
1281#line 5
1282struct vfsmount;
1283#line 7 "include/linux/path.h"
1284struct path {
1285   struct vfsmount *mnt ;
1286   struct dentry *dentry ;
1287};
1288#line 64 "include/linux/radix-tree.h"
1289struct radix_tree_node;
1290#line 64 "include/linux/radix-tree.h"
1291struct radix_tree_root {
1292   unsigned int height ;
1293   gfp_t gfp_mask ;
1294   struct radix_tree_node *rnode ;
1295};
1296#line 14 "include/linux/prio_tree.h"
1297struct prio_tree_node;
1298#line 20 "include/linux/prio_tree.h"
1299struct prio_tree_node {
1300   struct prio_tree_node *left ;
1301   struct prio_tree_node *right ;
1302   struct prio_tree_node *parent ;
1303   unsigned long start ;
1304   unsigned long last ;
1305};
1306#line 28 "include/linux/prio_tree.h"
1307struct prio_tree_root {
1308   struct prio_tree_node *prio_tree_node ;
1309   unsigned short index_bits ;
1310   unsigned short raw ;
1311};
1312#line 6 "include/linux/pid.h"
1313enum pid_type {
1314    PIDTYPE_PID = 0,
1315    PIDTYPE_PGID = 1,
1316    PIDTYPE_SID = 2,
1317    PIDTYPE_MAX = 3
1318} ;
1319#line 50
1320struct pid_namespace;
1321#line 50 "include/linux/pid.h"
1322struct upid {
1323   int nr ;
1324   struct pid_namespace *ns ;
1325   struct hlist_node pid_chain ;
1326};
1327#line 57 "include/linux/pid.h"
1328struct pid {
1329   atomic_t count ;
1330   unsigned int level ;
1331   struct hlist_head tasks[3] ;
1332   struct rcu_head rcu ;
1333   struct upid numbers[1] ;
1334};
1335#line 100
1336struct pid_namespace;
1337#line 18 "include/linux/capability.h"
1338struct task_struct;
1339#line 377
1340struct dentry;
1341#line 16 "include/linux/fiemap.h"
1342struct fiemap_extent {
1343   __u64 fe_logical ;
1344   __u64 fe_physical ;
1345   __u64 fe_length ;
1346   __u64 fe_reserved64[2] ;
1347   __u32 fe_flags ;
1348   __u32 fe_reserved[3] ;
1349};
1350#line 8 "include/linux/shrinker.h"
1351struct shrink_control {
1352   gfp_t gfp_mask ;
1353   unsigned long nr_to_scan ;
1354};
1355#line 31 "include/linux/shrinker.h"
1356struct shrinker {
1357   int (*shrink)(struct shrinker * , struct shrink_control *sc ) ;
1358   int seeks ;
1359   long batch ;
1360   struct list_head list ;
1361   atomic_long_t nr_in_batch ;
1362};
1363#line 10 "include/linux/migrate_mode.h"
1364enum migrate_mode {
1365    MIGRATE_ASYNC = 0,
1366    MIGRATE_SYNC_LIGHT = 1,
1367    MIGRATE_SYNC = 2
1368} ;
1369#line 408 "include/linux/fs.h"
1370struct export_operations;
1371#line 408
1372struct export_operations;
1373#line 410
1374struct iovec;
1375#line 410
1376struct iovec;
1377#line 411
1378struct nameidata;
1379#line 412
1380struct kiocb;
1381#line 412
1382struct kiocb;
1383#line 413
1384struct kobject;
1385#line 414
1386struct pipe_inode_info;
1387#line 414
1388struct pipe_inode_info;
1389#line 415
1390struct poll_table_struct;
1391#line 415
1392struct poll_table_struct;
1393#line 416
1394struct kstatfs;
1395#line 416
1396struct kstatfs;
1397#line 417
1398struct vm_area_struct;
1399#line 418
1400struct vfsmount;
1401#line 419
1402struct cred;
1403#line 469 "include/linux/fs.h"
1404struct iattr {
1405   unsigned int ia_valid ;
1406   umode_t ia_mode ;
1407   uid_t ia_uid ;
1408   gid_t ia_gid ;
1409   loff_t ia_size ;
1410   struct timespec ia_atime ;
1411   struct timespec ia_mtime ;
1412   struct timespec ia_ctime ;
1413   struct file *ia_file ;
1414};
1415#line 129 "include/linux/quota.h"
1416struct if_dqinfo {
1417   __u64 dqi_bgrace ;
1418   __u64 dqi_igrace ;
1419   __u32 dqi_flags ;
1420   __u32 dqi_valid ;
1421};
1422#line 50 "include/linux/dqblk_xfs.h"
1423struct fs_disk_quota {
1424   __s8 d_version ;
1425   __s8 d_flags ;
1426   __u16 d_fieldmask ;
1427   __u32 d_id ;
1428   __u64 d_blk_hardlimit ;
1429   __u64 d_blk_softlimit ;
1430   __u64 d_ino_hardlimit ;
1431   __u64 d_ino_softlimit ;
1432   __u64 d_bcount ;
1433   __u64 d_icount ;
1434   __s32 d_itimer ;
1435   __s32 d_btimer ;
1436   __u16 d_iwarns ;
1437   __u16 d_bwarns ;
1438   __s32 d_padding2 ;
1439   __u64 d_rtb_hardlimit ;
1440   __u64 d_rtb_softlimit ;
1441   __u64 d_rtbcount ;
1442   __s32 d_rtbtimer ;
1443   __u16 d_rtbwarns ;
1444   __s16 d_padding3 ;
1445   char d_padding4[8] ;
1446};
1447#line 146 "include/linux/dqblk_xfs.h"
1448struct fs_qfilestat {
1449   __u64 qfs_ino ;
1450   __u64 qfs_nblks ;
1451   __u32 qfs_nextents ;
1452};
1453#line 146 "include/linux/dqblk_xfs.h"
1454typedef struct fs_qfilestat fs_qfilestat_t;
1455#line 152 "include/linux/dqblk_xfs.h"
1456struct fs_quota_stat {
1457   __s8 qs_version ;
1458   __u16 qs_flags ;
1459   __s8 qs_pad ;
1460   fs_qfilestat_t qs_uquota ;
1461   fs_qfilestat_t qs_gquota ;
1462   __u32 qs_incoredqs ;
1463   __s32 qs_btimelimit ;
1464   __s32 qs_itimelimit ;
1465   __s32 qs_rtbtimelimit ;
1466   __u16 qs_bwarnlimit ;
1467   __u16 qs_iwarnlimit ;
1468};
1469#line 17 "include/linux/dqblk_qtree.h"
1470struct dquot;
1471#line 17
1472struct dquot;
1473#line 185 "include/linux/quota.h"
1474typedef __kernel_uid32_t qid_t;
1475#line 186 "include/linux/quota.h"
1476typedef long long qsize_t;
1477#line 200 "include/linux/quota.h"
1478struct mem_dqblk {
1479   qsize_t dqb_bhardlimit ;
1480   qsize_t dqb_bsoftlimit ;
1481   qsize_t dqb_curspace ;
1482   qsize_t dqb_rsvspace ;
1483   qsize_t dqb_ihardlimit ;
1484   qsize_t dqb_isoftlimit ;
1485   qsize_t dqb_curinodes ;
1486   time_t dqb_btime ;
1487   time_t dqb_itime ;
1488};
1489#line 215
1490struct quota_format_type;
1491#line 215
1492struct quota_format_type;
1493#line 217 "include/linux/quota.h"
1494struct mem_dqinfo {
1495   struct quota_format_type *dqi_format ;
1496   int dqi_fmt_id ;
1497   struct list_head dqi_dirty_list ;
1498   unsigned long dqi_flags ;
1499   unsigned int dqi_bgrace ;
1500   unsigned int dqi_igrace ;
1501   qsize_t dqi_maxblimit ;
1502   qsize_t dqi_maxilimit ;
1503   void *dqi_priv ;
1504};
1505#line 230
1506struct super_block;
1507#line 288 "include/linux/quota.h"
1508struct dquot {
1509   struct hlist_node dq_hash ;
1510   struct list_head dq_inuse ;
1511   struct list_head dq_free ;
1512   struct list_head dq_dirty ;
1513   struct mutex dq_lock ;
1514   atomic_t dq_count ;
1515   wait_queue_head_t dq_wait_unused ;
1516   struct super_block *dq_sb ;
1517   unsigned int dq_id ;
1518   loff_t dq_off ;
1519   unsigned long dq_flags ;
1520   short dq_type ;
1521   struct mem_dqblk dq_dqb ;
1522};
1523#line 305 "include/linux/quota.h"
1524struct quota_format_ops {
1525   int (*check_quota_file)(struct super_block *sb , int type ) ;
1526   int (*read_file_info)(struct super_block *sb , int type ) ;
1527   int (*write_file_info)(struct super_block *sb , int type ) ;
1528   int (*free_file_info)(struct super_block *sb , int type ) ;
1529   int (*read_dqblk)(struct dquot *dquot ) ;
1530   int (*commit_dqblk)(struct dquot *dquot ) ;
1531   int (*release_dqblk)(struct dquot *dquot ) ;
1532};
1533#line 316 "include/linux/quota.h"
1534struct dquot_operations {
1535   int (*write_dquot)(struct dquot * ) ;
1536   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
1537   void (*destroy_dquot)(struct dquot * ) ;
1538   int (*acquire_dquot)(struct dquot * ) ;
1539   int (*release_dquot)(struct dquot * ) ;
1540   int (*mark_dirty)(struct dquot * ) ;
1541   int (*write_info)(struct super_block * , int  ) ;
1542   qsize_t *(*get_reserved_space)(struct inode * ) ;
1543};
1544#line 329
1545struct path;
1546#line 332 "include/linux/quota.h"
1547struct quotactl_ops {
1548   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
1549   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
1550   int (*quota_off)(struct super_block * , int  ) ;
1551   int (*quota_sync)(struct super_block * , int  , int  ) ;
1552   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1553   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1554   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1555   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1556   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1557   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
1558};
1559#line 345 "include/linux/quota.h"
1560struct quota_format_type {
1561   int qf_fmt_id ;
1562   struct quota_format_ops  const  *qf_ops ;
1563   struct module *qf_owner ;
1564   struct quota_format_type *qf_next ;
1565};
1566#line 399 "include/linux/quota.h"
1567struct quota_info {
1568   unsigned int flags ;
1569   struct mutex dqio_mutex ;
1570   struct mutex dqonoff_mutex ;
1571   struct rw_semaphore dqptr_sem ;
1572   struct inode *files[2] ;
1573   struct mem_dqinfo info[2] ;
1574   struct quota_format_ops  const  *ops[2] ;
1575};
1576#line 532 "include/linux/fs.h"
1577struct page;
1578#line 533
1579struct address_space;
1580#line 533
1581struct address_space;
1582#line 534
1583struct writeback_control;
1584#line 534
1585struct writeback_control;
1586#line 577 "include/linux/fs.h"
1587union __anonunion_arg_217 {
1588   char *buf ;
1589   void *data ;
1590};
1591#line 577 "include/linux/fs.h"
1592struct __anonstruct_read_descriptor_t_216 {
1593   size_t written ;
1594   size_t count ;
1595   union __anonunion_arg_217 arg ;
1596   int error ;
1597};
1598#line 577 "include/linux/fs.h"
1599typedef struct __anonstruct_read_descriptor_t_216 read_descriptor_t;
1600#line 590 "include/linux/fs.h"
1601struct address_space_operations {
1602   int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
1603   int (*readpage)(struct file * , struct page * ) ;
1604   int (*writepages)(struct address_space * , struct writeback_control * ) ;
1605   int (*set_page_dirty)(struct page *page ) ;
1606   int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
1607                    unsigned int nr_pages ) ;
1608   int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
1609                      unsigned int len , unsigned int flags , struct page **pagep ,
1610                      void **fsdata ) ;
1611   int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
1612                    unsigned int copied , struct page *page , void *fsdata ) ;
1613   sector_t (*bmap)(struct address_space * , sector_t  ) ;
1614   void (*invalidatepage)(struct page * , unsigned long  ) ;
1615   int (*releasepage)(struct page * , gfp_t  ) ;
1616   void (*freepage)(struct page * ) ;
1617   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  *iov , loff_t offset ,
1618                        unsigned long nr_segs ) ;
1619   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
1620   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
1621   int (*launder_page)(struct page * ) ;
1622   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
1623   int (*error_remove_page)(struct address_space * , struct page * ) ;
1624};
1625#line 645
1626struct backing_dev_info;
1627#line 646 "include/linux/fs.h"
1628struct address_space {
1629   struct inode *host ;
1630   struct radix_tree_root page_tree ;
1631   spinlock_t tree_lock ;
1632   unsigned int i_mmap_writable ;
1633   struct prio_tree_root i_mmap ;
1634   struct list_head i_mmap_nonlinear ;
1635   struct mutex i_mmap_mutex ;
1636   unsigned long nrpages ;
1637   unsigned long writeback_index ;
1638   struct address_space_operations  const  *a_ops ;
1639   unsigned long flags ;
1640   struct backing_dev_info *backing_dev_info ;
1641   spinlock_t private_lock ;
1642   struct list_head private_list ;
1643   struct address_space *assoc_mapping ;
1644} __attribute__((__aligned__(sizeof(long )))) ;
1645#line 669
1646struct request_queue;
1647#line 669
1648struct request_queue;
1649#line 671
1650struct hd_struct;
1651#line 671
1652struct gendisk;
1653#line 671 "include/linux/fs.h"
1654struct block_device {
1655   dev_t bd_dev ;
1656   int bd_openers ;
1657   struct inode *bd_inode ;
1658   struct super_block *bd_super ;
1659   struct mutex bd_mutex ;
1660   struct list_head bd_inodes ;
1661   void *bd_claiming ;
1662   void *bd_holder ;
1663   int bd_holders ;
1664   bool bd_write_holder ;
1665   struct list_head bd_holder_disks ;
1666   struct block_device *bd_contains ;
1667   unsigned int bd_block_size ;
1668   struct hd_struct *bd_part ;
1669   unsigned int bd_part_count ;
1670   int bd_invalidated ;
1671   struct gendisk *bd_disk ;
1672   struct request_queue *bd_queue ;
1673   struct list_head bd_list ;
1674   unsigned long bd_private ;
1675   int bd_fsfreeze_count ;
1676   struct mutex bd_fsfreeze_mutex ;
1677};
1678#line 749
1679struct posix_acl;
1680#line 749
1681struct posix_acl;
1682#line 761
1683struct inode_operations;
1684#line 761 "include/linux/fs.h"
1685union __anonunion____missing_field_name_218 {
1686   unsigned int const   i_nlink ;
1687   unsigned int __i_nlink ;
1688};
1689#line 761 "include/linux/fs.h"
1690union __anonunion____missing_field_name_219 {
1691   struct list_head i_dentry ;
1692   struct rcu_head i_rcu ;
1693};
1694#line 761
1695struct file_lock;
1696#line 761 "include/linux/fs.h"
1697union __anonunion____missing_field_name_220 {
1698   struct pipe_inode_info *i_pipe ;
1699   struct block_device *i_bdev ;
1700   struct cdev *i_cdev ;
1701};
1702#line 761 "include/linux/fs.h"
1703struct inode {
1704   umode_t i_mode ;
1705   unsigned short i_opflags ;
1706   uid_t i_uid ;
1707   gid_t i_gid ;
1708   unsigned int i_flags ;
1709   struct posix_acl *i_acl ;
1710   struct posix_acl *i_default_acl ;
1711   struct inode_operations  const  *i_op ;
1712   struct super_block *i_sb ;
1713   struct address_space *i_mapping ;
1714   void *i_security ;
1715   unsigned long i_ino ;
1716   union __anonunion____missing_field_name_218 __annonCompField33 ;
1717   dev_t i_rdev ;
1718   struct timespec i_atime ;
1719   struct timespec i_mtime ;
1720   struct timespec i_ctime ;
1721   spinlock_t i_lock ;
1722   unsigned short i_bytes ;
1723   blkcnt_t i_blocks ;
1724   loff_t i_size ;
1725   unsigned long i_state ;
1726   struct mutex i_mutex ;
1727   unsigned long dirtied_when ;
1728   struct hlist_node i_hash ;
1729   struct list_head i_wb_list ;
1730   struct list_head i_lru ;
1731   struct list_head i_sb_list ;
1732   union __anonunion____missing_field_name_219 __annonCompField34 ;
1733   atomic_t i_count ;
1734   unsigned int i_blkbits ;
1735   u64 i_version ;
1736   atomic_t i_dio_count ;
1737   atomic_t i_writecount ;
1738   struct file_operations  const  *i_fop ;
1739   struct file_lock *i_flock ;
1740   struct address_space i_data ;
1741   struct dquot *i_dquot[2] ;
1742   struct list_head i_devices ;
1743   union __anonunion____missing_field_name_220 __annonCompField35 ;
1744   __u32 i_generation ;
1745   __u32 i_fsnotify_mask ;
1746   struct hlist_head i_fsnotify_marks ;
1747   atomic_t i_readcount ;
1748   void *i_private ;
1749};
1750#line 942 "include/linux/fs.h"
1751struct fown_struct {
1752   rwlock_t lock ;
1753   struct pid *pid ;
1754   enum pid_type pid_type ;
1755   uid_t uid ;
1756   uid_t euid ;
1757   int signum ;
1758};
1759#line 953 "include/linux/fs.h"
1760struct file_ra_state {
1761   unsigned long start ;
1762   unsigned int size ;
1763   unsigned int async_size ;
1764   unsigned int ra_pages ;
1765   unsigned int mmap_miss ;
1766   loff_t prev_pos ;
1767};
1768#line 976 "include/linux/fs.h"
1769union __anonunion_f_u_221 {
1770   struct list_head fu_list ;
1771   struct rcu_head fu_rcuhead ;
1772};
1773#line 976 "include/linux/fs.h"
1774struct file {
1775   union __anonunion_f_u_221 f_u ;
1776   struct path f_path ;
1777   struct file_operations  const  *f_op ;
1778   spinlock_t f_lock ;
1779   int f_sb_list_cpu ;
1780   atomic_long_t f_count ;
1781   unsigned int f_flags ;
1782   fmode_t f_mode ;
1783   loff_t f_pos ;
1784   struct fown_struct f_owner ;
1785   struct cred  const  *f_cred ;
1786   struct file_ra_state f_ra ;
1787   u64 f_version ;
1788   void *f_security ;
1789   void *private_data ;
1790   struct list_head f_ep_links ;
1791   struct list_head f_tfile_llink ;
1792   struct address_space *f_mapping ;
1793   unsigned long f_mnt_write_state ;
1794};
1795#line 1111
1796struct files_struct;
1797#line 1111 "include/linux/fs.h"
1798typedef struct files_struct *fl_owner_t;
1799#line 1113 "include/linux/fs.h"
1800struct file_lock_operations {
1801   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1802   void (*fl_release_private)(struct file_lock * ) ;
1803};
1804#line 1118 "include/linux/fs.h"
1805struct lock_manager_operations {
1806   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1807   void (*lm_notify)(struct file_lock * ) ;
1808   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
1809   void (*lm_release_private)(struct file_lock * ) ;
1810   void (*lm_break)(struct file_lock * ) ;
1811   int (*lm_change)(struct file_lock ** , int  ) ;
1812};
1813#line 4 "include/linux/nfs_fs_i.h"
1814struct nlm_lockowner;
1815#line 4
1816struct nlm_lockowner;
1817#line 9 "include/linux/nfs_fs_i.h"
1818struct nfs_lock_info {
1819   u32 state ;
1820   struct nlm_lockowner *owner ;
1821   struct list_head list ;
1822};
1823#line 15
1824struct nfs4_lock_state;
1825#line 15
1826struct nfs4_lock_state;
1827#line 16 "include/linux/nfs_fs_i.h"
1828struct nfs4_lock_info {
1829   struct nfs4_lock_state *owner ;
1830};
1831#line 1138 "include/linux/fs.h"
1832struct fasync_struct;
1833#line 1138 "include/linux/fs.h"
1834struct __anonstruct_afs_223 {
1835   struct list_head link ;
1836   int state ;
1837};
1838#line 1138 "include/linux/fs.h"
1839union __anonunion_fl_u_222 {
1840   struct nfs_lock_info nfs_fl ;
1841   struct nfs4_lock_info nfs4_fl ;
1842   struct __anonstruct_afs_223 afs ;
1843};
1844#line 1138 "include/linux/fs.h"
1845struct file_lock {
1846   struct file_lock *fl_next ;
1847   struct list_head fl_link ;
1848   struct list_head fl_block ;
1849   fl_owner_t fl_owner ;
1850   unsigned int fl_flags ;
1851   unsigned char fl_type ;
1852   unsigned int fl_pid ;
1853   struct pid *fl_nspid ;
1854   wait_queue_head_t fl_wait ;
1855   struct file *fl_file ;
1856   loff_t fl_start ;
1857   loff_t fl_end ;
1858   struct fasync_struct *fl_fasync ;
1859   unsigned long fl_break_time ;
1860   unsigned long fl_downgrade_time ;
1861   struct file_lock_operations  const  *fl_ops ;
1862   struct lock_manager_operations  const  *fl_lmops ;
1863   union __anonunion_fl_u_222 fl_u ;
1864};
1865#line 1378 "include/linux/fs.h"
1866struct fasync_struct {
1867   spinlock_t fa_lock ;
1868   int magic ;
1869   int fa_fd ;
1870   struct fasync_struct *fa_next ;
1871   struct file *fa_file ;
1872   struct rcu_head fa_rcu ;
1873};
1874#line 1418
1875struct file_system_type;
1876#line 1418
1877struct super_operations;
1878#line 1418
1879struct xattr_handler;
1880#line 1418
1881struct mtd_info;
1882#line 1418 "include/linux/fs.h"
1883struct super_block {
1884   struct list_head s_list ;
1885   dev_t s_dev ;
1886   unsigned char s_dirt ;
1887   unsigned char s_blocksize_bits ;
1888   unsigned long s_blocksize ;
1889   loff_t s_maxbytes ;
1890   struct file_system_type *s_type ;
1891   struct super_operations  const  *s_op ;
1892   struct dquot_operations  const  *dq_op ;
1893   struct quotactl_ops  const  *s_qcop ;
1894   struct export_operations  const  *s_export_op ;
1895   unsigned long s_flags ;
1896   unsigned long s_magic ;
1897   struct dentry *s_root ;
1898   struct rw_semaphore s_umount ;
1899   struct mutex s_lock ;
1900   int s_count ;
1901   atomic_t s_active ;
1902   void *s_security ;
1903   struct xattr_handler  const  **s_xattr ;
1904   struct list_head s_inodes ;
1905   struct hlist_bl_head s_anon ;
1906   struct list_head *s_files ;
1907   struct list_head s_mounts ;
1908   struct list_head s_dentry_lru ;
1909   int s_nr_dentry_unused ;
1910   spinlock_t s_inode_lru_lock  __attribute__((__aligned__((1) <<  (6) ))) ;
1911   struct list_head s_inode_lru ;
1912   int s_nr_inodes_unused ;
1913   struct block_device *s_bdev ;
1914   struct backing_dev_info *s_bdi ;
1915   struct mtd_info *s_mtd ;
1916   struct hlist_node s_instances ;
1917   struct quota_info s_dquot ;
1918   int s_frozen ;
1919   wait_queue_head_t s_wait_unfrozen ;
1920   char s_id[32] ;
1921   u8 s_uuid[16] ;
1922   void *s_fs_info ;
1923   unsigned int s_max_links ;
1924   fmode_t s_mode ;
1925   u32 s_time_gran ;
1926   struct mutex s_vfs_rename_mutex ;
1927   char *s_subtype ;
1928   char *s_options ;
1929   struct dentry_operations  const  *s_d_op ;
1930   int cleancache_poolid ;
1931   struct shrinker s_shrink ;
1932   atomic_long_t s_remove_count ;
1933   int s_readonly_remount ;
1934};
1935#line 1567 "include/linux/fs.h"
1936struct fiemap_extent_info {
1937   unsigned int fi_flags ;
1938   unsigned int fi_extents_mapped ;
1939   unsigned int fi_extents_max ;
1940   struct fiemap_extent *fi_extents_start ;
1941};
1942#line 1609 "include/linux/fs.h"
1943struct file_operations {
1944   struct module *owner ;
1945   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
1946   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
1947   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
1948   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1949                       loff_t  ) ;
1950   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1951                        loff_t  ) ;
1952   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
1953                                                   loff_t  , u64  , unsigned int  ) ) ;
1954   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1955   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1956   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1957   int (*mmap)(struct file * , struct vm_area_struct * ) ;
1958   int (*open)(struct inode * , struct file * ) ;
1959   int (*flush)(struct file * , fl_owner_t id ) ;
1960   int (*release)(struct inode * , struct file * ) ;
1961   int (*fsync)(struct file * , loff_t  , loff_t  , int datasync ) ;
1962   int (*aio_fsync)(struct kiocb * , int datasync ) ;
1963   int (*fasync)(int  , struct file * , int  ) ;
1964   int (*lock)(struct file * , int  , struct file_lock * ) ;
1965   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
1966                       int  ) ;
1967   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1968                                      unsigned long  , unsigned long  ) ;
1969   int (*check_flags)(int  ) ;
1970   int (*flock)(struct file * , int  , struct file_lock * ) ;
1971   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
1972                           unsigned int  ) ;
1973   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
1974                          unsigned int  ) ;
1975   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
1976   long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
1977};
1978#line 1639 "include/linux/fs.h"
1979struct inode_operations {
1980   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1981   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1982   int (*permission)(struct inode * , int  ) ;
1983   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
1984   int (*readlink)(struct dentry * , char * , int  ) ;
1985   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1986   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
1987   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1988   int (*unlink)(struct inode * , struct dentry * ) ;
1989   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
1990   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
1991   int (*rmdir)(struct inode * , struct dentry * ) ;
1992   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
1993   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1994   void (*truncate)(struct inode * ) ;
1995   int (*setattr)(struct dentry * , struct iattr * ) ;
1996   int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
1997   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
1998   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
1999   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
2000   int (*removexattr)(struct dentry * , char const   * ) ;
2001   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
2002   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
2003} __attribute__((__aligned__((1) <<  (6) ))) ;
2004#line 1669
2005struct seq_file;
2006#line 1684 "include/linux/fs.h"
2007struct super_operations {
2008   struct inode *(*alloc_inode)(struct super_block *sb ) ;
2009   void (*destroy_inode)(struct inode * ) ;
2010   void (*dirty_inode)(struct inode * , int flags ) ;
2011   int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
2012   int (*drop_inode)(struct inode * ) ;
2013   void (*evict_inode)(struct inode * ) ;
2014   void (*put_super)(struct super_block * ) ;
2015   void (*write_super)(struct super_block * ) ;
2016   int (*sync_fs)(struct super_block *sb , int wait ) ;
2017   int (*freeze_fs)(struct super_block * ) ;
2018   int (*unfreeze_fs)(struct super_block * ) ;
2019   int (*statfs)(struct dentry * , struct kstatfs * ) ;
2020   int (*remount_fs)(struct super_block * , int * , char * ) ;
2021   void (*umount_begin)(struct super_block * ) ;
2022   int (*show_options)(struct seq_file * , struct dentry * ) ;
2023   int (*show_devname)(struct seq_file * , struct dentry * ) ;
2024   int (*show_path)(struct seq_file * , struct dentry * ) ;
2025   int (*show_stats)(struct seq_file * , struct dentry * ) ;
2026   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
2027   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
2028                          loff_t  ) ;
2029   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
2030   int (*nr_cached_objects)(struct super_block * ) ;
2031   void (*free_cached_objects)(struct super_block * , int  ) ;
2032};
2033#line 1835 "include/linux/fs.h"
2034struct file_system_type {
2035   char const   *name ;
2036   int fs_flags ;
2037   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
2038   void (*kill_sb)(struct super_block * ) ;
2039   struct module *owner ;
2040   struct file_system_type *next ;
2041   struct hlist_head fs_supers ;
2042   struct lock_class_key s_lock_key ;
2043   struct lock_class_key s_umount_key ;
2044   struct lock_class_key s_vfs_rename_key ;
2045   struct lock_class_key i_lock_key ;
2046   struct lock_class_key i_mutex_key ;
2047   struct lock_class_key i_mutex_dir_key ;
2048};
2049#line 28 "include/linux/poll.h"
2050struct poll_table_struct;
2051#line 39 "include/linux/poll.h"
2052struct poll_table_struct {
2053   void (*_qproc)(struct file * , wait_queue_head_t * , struct poll_table_struct * ) ;
2054   unsigned long _key ;
2055};
2056#line 143 "include/linux/rtc.h"
2057struct rtc_class_ops {
2058   int (*open)(struct device * ) ;
2059   void (*release)(struct device * ) ;
2060   int (*ioctl)(struct device * , unsigned int  , unsigned long  ) ;
2061   int (*read_time)(struct device * , struct rtc_time * ) ;
2062   int (*set_time)(struct device * , struct rtc_time * ) ;
2063   int (*read_alarm)(struct device * , struct rtc_wkalrm * ) ;
2064   int (*set_alarm)(struct device * , struct rtc_wkalrm * ) ;
2065   int (*proc)(struct device * , struct seq_file * ) ;
2066   int (*set_mmss)(struct device * , unsigned long secs ) ;
2067   int (*read_callback)(struct device * , int data ) ;
2068   int (*alarm_irq_enable)(struct device * , unsigned int enabled ) ;
2069};
2070#line 158 "include/linux/rtc.h"
2071struct rtc_task {
2072   void (*func)(void *private_data ) ;
2073   void *private_data ;
2074};
2075#line 164 "include/linux/rtc.h"
2076struct rtc_timer {
2077   struct rtc_task task ;
2078   struct timerqueue_node node ;
2079   ktime_t period ;
2080   int enabled ;
2081};
2082#line 175 "include/linux/rtc.h"
2083struct rtc_device {
2084   struct device dev ;
2085   struct module *owner ;
2086   int id ;
2087   char name[20] ;
2088   struct rtc_class_ops  const  *ops ;
2089   struct mutex ops_lock ;
2090   struct cdev char_dev ;
2091   unsigned long flags ;
2092   unsigned long irq_data ;
2093   spinlock_t irq_lock ;
2094   wait_queue_head_t irq_queue ;
2095   struct fasync_struct *async_queue ;
2096   struct rtc_task *irq_task ;
2097   spinlock_t irq_task_lock ;
2098   int irq_freq ;
2099   int max_user_freq ;
2100   struct timerqueue_head timerqueue ;
2101   struct rtc_timer aie_timer ;
2102   struct rtc_timer uie_rtctimer ;
2103   struct hrtimer pie_timer ;
2104   int pie_enabled ;
2105   struct work_struct irqwork ;
2106   int uie_unsupported ;
2107   struct work_struct uie_task ;
2108   struct timer_list uie_timer ;
2109   unsigned int oldsecs ;
2110   unsigned int uie_irq_active : 1 ;
2111   unsigned int stop_uie_polling : 1 ;
2112   unsigned int uie_task_active : 1 ;
2113   unsigned int uie_timer_active : 1 ;
2114};
2115#line 46 "include/linux/slub_def.h"
2116struct kmem_cache_cpu {
2117   void **freelist ;
2118   unsigned long tid ;
2119   struct page *page ;
2120   struct page *partial ;
2121   int node ;
2122   unsigned int stat[26] ;
2123};
2124#line 57 "include/linux/slub_def.h"
2125struct kmem_cache_node {
2126   spinlock_t list_lock ;
2127   unsigned long nr_partial ;
2128   struct list_head partial ;
2129   atomic_long_t nr_slabs ;
2130   atomic_long_t total_objects ;
2131   struct list_head full ;
2132};
2133#line 73 "include/linux/slub_def.h"
2134struct kmem_cache_order_objects {
2135   unsigned long x ;
2136};
2137#line 80 "include/linux/slub_def.h"
2138struct kmem_cache {
2139   struct kmem_cache_cpu *cpu_slab ;
2140   unsigned long flags ;
2141   unsigned long min_partial ;
2142   int size ;
2143   int objsize ;
2144   int offset ;
2145   int cpu_partial ;
2146   struct kmem_cache_order_objects oo ;
2147   struct kmem_cache_order_objects max ;
2148   struct kmem_cache_order_objects min ;
2149   gfp_t allocflags ;
2150   int refcount ;
2151   void (*ctor)(void * ) ;
2152   int inuse ;
2153   int align ;
2154   int reserved ;
2155   char const   *name ;
2156   struct list_head list ;
2157   struct kobject kobj ;
2158   int remote_node_defrag_ratio ;
2159   struct kmem_cache_node *node[1 << 10] ;
2160};
2161#line 12 "include/linux/mod_devicetable.h"
2162typedef unsigned long kernel_ulong_t;
2163#line 219 "include/linux/mod_devicetable.h"
2164struct of_device_id {
2165   char name[32] ;
2166   char type[32] ;
2167   char compatible[128] ;
2168   void *data ;
2169};
2170#line 506 "include/linux/mod_devicetable.h"
2171struct platform_device_id {
2172   char name[20] ;
2173   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
2174};
2175#line 17 "include/linux/platform_device.h"
2176struct mfd_cell;
2177#line 17
2178struct mfd_cell;
2179#line 19 "include/linux/platform_device.h"
2180struct platform_device {
2181   char const   *name ;
2182   int id ;
2183   struct device dev ;
2184   u32 num_resources ;
2185   struct resource *resource ;
2186   struct platform_device_id  const  *id_entry ;
2187   struct mfd_cell *mfd_cell ;
2188   struct pdev_archdata archdata ;
2189};
2190#line 164 "include/linux/platform_device.h"
2191struct platform_driver {
2192   int (*probe)(struct platform_device * ) ;
2193   int (*remove)(struct platform_device * ) ;
2194   void (*shutdown)(struct platform_device * ) ;
2195   int (*suspend)(struct platform_device * , pm_message_t state ) ;
2196   int (*resume)(struct platform_device * ) ;
2197   struct device_driver driver ;
2198   struct platform_device_id  const  *id_table ;
2199};
2200#line 24 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2201struct pcap_rtc {
2202   struct pcap_chip *pcap ;
2203   struct rtc_device *rtc ;
2204};
2205#line 1 "<compiler builtins>"
2206long __builtin_expect(long val , long res ) ;
2207#line 27 "include/linux/err.h"
2208__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
2209#line 27 "include/linux/err.h"
2210__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr ) 
2211{ 
2212
2213  {
2214#line 29
2215  return ((long )ptr);
2216}
2217}
2218#line 32
2219__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
2220#line 32 "include/linux/err.h"
2221__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr ) 
2222{ long tmp ;
2223  unsigned long __cil_tmp3 ;
2224  int __cil_tmp4 ;
2225  int __cil_tmp5 ;
2226  int __cil_tmp6 ;
2227  long __cil_tmp7 ;
2228
2229  {
2230  {
2231#line 34
2232  __cil_tmp3 = (unsigned long )ptr;
2233#line 34
2234  __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
2235#line 34
2236  __cil_tmp5 = ! __cil_tmp4;
2237#line 34
2238  __cil_tmp6 = ! __cil_tmp5;
2239#line 34
2240  __cil_tmp7 = (long )__cil_tmp6;
2241#line 34
2242  tmp = __builtin_expect(__cil_tmp7, 0L);
2243  }
2244#line 34
2245  return (tmp);
2246}
2247}
2248#line 152 "include/linux/mutex.h"
2249void mutex_lock(struct mutex *lock ) ;
2250#line 153
2251int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2252#line 154
2253int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2254#line 168
2255int mutex_trylock(struct mutex *lock ) ;
2256#line 169
2257void mutex_unlock(struct mutex *lock ) ;
2258#line 170
2259int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2260#line 26 "include/linux/export.h"
2261extern struct module __this_module ;
2262#line 67 "include/linux/module.h"
2263int init_module(void) ;
2264#line 68
2265void cleanup_module(void) ;
2266#line 26 "include/linux/mfd/ezx-pcap.h"
2267extern int ezx_pcap_write(struct pcap_chip * , u8  , u32  ) ;
2268#line 27
2269extern int ezx_pcap_read(struct pcap_chip * , u8  , u32 * ) ;
2270#line 29
2271extern int pcap_to_irq(struct pcap_chip * , int  ) ;
2272#line 126 "include/linux/interrupt.h"
2273extern int __attribute__((__warn_unused_result__))  request_threaded_irq(unsigned int irq ,
2274                                                                         irqreturn_t (*handler)(int  ,
2275                                                                                                void * ) ,
2276                                                                         irqreturn_t (*thread_fn)(int  ,
2277                                                                                                  void * ) ,
2278                                                                         unsigned long flags ,
2279                                                                         char const   *name ,
2280                                                                         void *dev ) ;
2281#line 131
2282__inline static int __attribute__((__warn_unused_result__))  request_irq(unsigned int irq ,
2283                                                                         irqreturn_t (*handler)(int  ,
2284                                                                                                void * ) ,
2285                                                                         unsigned long flags ,
2286                                                                         char const   *name ,
2287                                                                         void *dev )  __attribute__((__no_instrument_function__)) ;
2288#line 131 "include/linux/interrupt.h"
2289__inline static int __attribute__((__warn_unused_result__))  request_irq(unsigned int irq ,
2290                                                                         irqreturn_t (*handler)(int  ,
2291                                                                                                void * ) ,
2292                                                                         unsigned long flags ,
2293                                                                         char const   *name ,
2294                                                                         void *dev ) 
2295{ int tmp ;
2296  void *__cil_tmp7 ;
2297  irqreturn_t (*__cil_tmp8)(int  , void * ) ;
2298
2299  {
2300  {
2301#line 135
2302  __cil_tmp7 = (void *)0;
2303#line 135
2304  __cil_tmp8 = (irqreturn_t (*)(int  , void * ))__cil_tmp7;
2305#line 135
2306  tmp = (int )request_threaded_irq(irq, handler, __cil_tmp8, flags, name, dev);
2307  }
2308#line 135
2309  return (tmp);
2310}
2311}
2312#line 184
2313extern void free_irq(unsigned int  , void * ) ;
2314#line 224
2315extern void disable_irq(unsigned int irq ) ;
2316#line 226
2317extern void enable_irq(unsigned int irq ) ;
2318#line 110 "include/linux/rtc.h"
2319extern int rtc_valid_tm(struct rtc_time *tm ) ;
2320#line 111
2321extern int rtc_tm_to_time(struct rtc_time *tm , unsigned long *time ) ;
2322#line 112
2323extern void rtc_time_to_tm(unsigned long time , struct rtc_time *tm ) ;
2324#line 792 "include/linux/device.h"
2325extern void *dev_get_drvdata(struct device  const  *dev ) ;
2326#line 793
2327extern int dev_set_drvdata(struct device *dev , void *data ) ;
2328#line 221 "include/linux/rtc.h"
2329extern struct rtc_device *rtc_device_register(char const   *name , struct device *dev ,
2330                                              struct rtc_class_ops  const  *ops ,
2331                                              struct module *owner ) ;
2332#line 225
2333extern void rtc_device_unregister(struct rtc_device *rtc ) ;
2334#line 237
2335extern void rtc_update_irq(struct rtc_device *rtc , unsigned long num , unsigned long events ) ;
2336#line 161 "include/linux/slab.h"
2337extern void kfree(void const   * ) ;
2338#line 221 "include/linux/slub_def.h"
2339extern void *__kmalloc(size_t size , gfp_t flags ) ;
2340#line 268
2341__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2342                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2343#line 268 "include/linux/slub_def.h"
2344__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2345                                                                    gfp_t flags ) 
2346{ void *tmp___2 ;
2347
2348  {
2349  {
2350#line 283
2351  tmp___2 = __kmalloc(size, flags);
2352  }
2353#line 283
2354  return (tmp___2);
2355}
2356}
2357#line 175 "include/linux/platform_device.h"
2358extern void platform_driver_unregister(struct platform_driver * ) ;
2359#line 180
2360extern int platform_driver_probe(struct platform_driver *driver , int (*probe)(struct platform_device * ) ) ;
2361#line 183
2362__inline static void *platform_get_drvdata(struct platform_device  const  *pdev )  __attribute__((__no_instrument_function__)) ;
2363#line 183 "include/linux/platform_device.h"
2364__inline static void *platform_get_drvdata(struct platform_device  const  *pdev ) 
2365{ void *tmp ;
2366  unsigned long __cil_tmp3 ;
2367  unsigned long __cil_tmp4 ;
2368  struct device  const  *__cil_tmp5 ;
2369
2370  {
2371  {
2372#line 185
2373  __cil_tmp3 = (unsigned long )pdev;
2374#line 185
2375  __cil_tmp4 = __cil_tmp3 + 16;
2376#line 185
2377  __cil_tmp5 = (struct device  const  *)__cil_tmp4;
2378#line 185
2379  tmp = dev_get_drvdata(__cil_tmp5);
2380  }
2381#line 185
2382  return (tmp);
2383}
2384}
2385#line 188
2386__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )  __attribute__((__no_instrument_function__)) ;
2387#line 188 "include/linux/platform_device.h"
2388__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) 
2389{ unsigned long __cil_tmp3 ;
2390  unsigned long __cil_tmp4 ;
2391  struct device *__cil_tmp5 ;
2392
2393  {
2394  {
2395#line 190
2396  __cil_tmp3 = (unsigned long )pdev;
2397#line 190
2398  __cil_tmp4 = __cil_tmp3 + 16;
2399#line 190
2400  __cil_tmp5 = (struct device *)__cil_tmp4;
2401#line 190
2402  dev_set_drvdata(__cil_tmp5, data);
2403  }
2404#line 191
2405  return;
2406}
2407}
2408#line 29 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2409static irqreturn_t pcap_rtc_irq(int irq , void *_pcap_rtc ) 
2410{ struct pcap_rtc *pcap_rtc ;
2411  unsigned long rtc_events ;
2412  int tmp ;
2413  int tmp___0 ;
2414  struct pcap_chip *__cil_tmp7 ;
2415  struct pcap_chip *__cil_tmp8 ;
2416  unsigned long __cil_tmp9 ;
2417  unsigned long __cil_tmp10 ;
2418  struct rtc_device *__cil_tmp11 ;
2419
2420  {
2421  {
2422#line 31
2423  pcap_rtc = (struct pcap_rtc *)_pcap_rtc;
2424#line 34
2425  __cil_tmp7 = *((struct pcap_chip **)pcap_rtc);
2426#line 34
2427  tmp___0 = pcap_to_irq(__cil_tmp7, 2);
2428  }
2429#line 34
2430  if (irq == tmp___0) {
2431#line 35
2432    rtc_events = 144UL;
2433  } else {
2434    {
2435#line 36
2436    __cil_tmp8 = *((struct pcap_chip **)pcap_rtc);
2437#line 36
2438    tmp = pcap_to_irq(__cil_tmp8, 5);
2439    }
2440#line 36
2441    if (irq == tmp) {
2442#line 37
2443      rtc_events = 160UL;
2444    } else {
2445#line 39
2446      rtc_events = 0UL;
2447    }
2448  }
2449  {
2450#line 41
2451  __cil_tmp9 = (unsigned long )pcap_rtc;
2452#line 41
2453  __cil_tmp10 = __cil_tmp9 + 8;
2454#line 41
2455  __cil_tmp11 = *((struct rtc_device **)__cil_tmp10);
2456#line 41
2457  rtc_update_irq(__cil_tmp11, 1UL, rtc_events);
2458  }
2459#line 42
2460  return ((irqreturn_t )1);
2461}
2462}
2463#line 45 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2464static int pcap_rtc_read_alarm(struct device *dev , struct rtc_wkalrm *alrm ) 
2465{ struct platform_device *pdev ;
2466  struct device  const  *__mptr ;
2467  struct pcap_rtc *pcap_rtc ;
2468  void *tmp ;
2469  struct rtc_time *tm ;
2470  unsigned long secs ;
2471  u32 tod ;
2472  u32 days ;
2473  struct platform_device *__cil_tmp11 ;
2474  unsigned long __cil_tmp12 ;
2475  unsigned long __cil_tmp13 ;
2476  struct device *__cil_tmp14 ;
2477  unsigned int __cil_tmp15 ;
2478  char *__cil_tmp16 ;
2479  char *__cil_tmp17 ;
2480  struct platform_device  const  *__cil_tmp18 ;
2481  unsigned long __cil_tmp19 ;
2482  unsigned long __cil_tmp20 ;
2483  struct pcap_chip *__cil_tmp21 ;
2484  u8 __cil_tmp22 ;
2485  u32 *__cil_tmp23 ;
2486  u32 __cil_tmp24 ;
2487  unsigned int __cil_tmp25 ;
2488  struct pcap_chip *__cil_tmp26 ;
2489  u8 __cil_tmp27 ;
2490  u32 *__cil_tmp28 ;
2491  u32 __cil_tmp29 ;
2492  unsigned int __cil_tmp30 ;
2493  unsigned int __cil_tmp31 ;
2494  unsigned long __cil_tmp32 ;
2495
2496  {
2497  {
2498#line 47
2499  __mptr = (struct device  const  *)dev;
2500#line 47
2501  __cil_tmp11 = (struct platform_device *)0;
2502#line 47
2503  __cil_tmp12 = (unsigned long )__cil_tmp11;
2504#line 47
2505  __cil_tmp13 = __cil_tmp12 + 16;
2506#line 47
2507  __cil_tmp14 = (struct device *)__cil_tmp13;
2508#line 47
2509  __cil_tmp15 = (unsigned int )__cil_tmp14;
2510#line 47
2511  __cil_tmp16 = (char *)__mptr;
2512#line 47
2513  __cil_tmp17 = __cil_tmp16 - __cil_tmp15;
2514#line 47
2515  pdev = (struct platform_device *)__cil_tmp17;
2516#line 48
2517  __cil_tmp18 = (struct platform_device  const  *)pdev;
2518#line 48
2519  tmp = platform_get_drvdata(__cil_tmp18);
2520#line 48
2521  pcap_rtc = (struct pcap_rtc *)tmp;
2522#line 49
2523  __cil_tmp19 = (unsigned long )alrm;
2524#line 49
2525  __cil_tmp20 = __cil_tmp19 + 4;
2526#line 49
2527  tm = (struct rtc_time *)__cil_tmp20;
2528#line 54
2529  __cil_tmp21 = *((struct pcap_chip **)pcap_rtc);
2530#line 54
2531  __cil_tmp22 = (u8 )15;
2532#line 54
2533  ezx_pcap_read(__cil_tmp21, __cil_tmp22, & tod);
2534#line 55
2535  __cil_tmp23 = & tod;
2536#line 55
2537  __cil_tmp24 = *__cil_tmp23;
2538#line 55
2539  __cil_tmp25 = __cil_tmp24 & 65535U;
2540#line 55
2541  secs = (unsigned long )__cil_tmp25;
2542#line 57
2543  __cil_tmp26 = *((struct pcap_chip **)pcap_rtc);
2544#line 57
2545  __cil_tmp27 = (u8 )17;
2546#line 57
2547  ezx_pcap_read(__cil_tmp26, __cil_tmp27, & days);
2548#line 58
2549  __cil_tmp28 = & days;
2550#line 58
2551  __cil_tmp29 = *__cil_tmp28;
2552#line 58
2553  __cil_tmp30 = __cil_tmp29 & 16383U;
2554#line 58
2555  __cil_tmp31 = __cil_tmp30 * 86400U;
2556#line 58
2557  __cil_tmp32 = (unsigned long )__cil_tmp31;
2558#line 58
2559  secs = secs + __cil_tmp32;
2560#line 60
2561  rtc_time_to_tm(secs, tm);
2562  }
2563#line 62
2564  return (0);
2565}
2566}
2567#line 65 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2568static int pcap_rtc_set_alarm(struct device *dev , struct rtc_wkalrm *alrm ) 
2569{ struct platform_device *pdev ;
2570  struct device  const  *__mptr ;
2571  struct pcap_rtc *pcap_rtc ;
2572  void *tmp ;
2573  struct rtc_time *tm ;
2574  unsigned long secs ;
2575  u32 tod ;
2576  u32 days ;
2577  struct platform_device *__cil_tmp11 ;
2578  unsigned long __cil_tmp12 ;
2579  unsigned long __cil_tmp13 ;
2580  struct device *__cil_tmp14 ;
2581  unsigned int __cil_tmp15 ;
2582  char *__cil_tmp16 ;
2583  char *__cil_tmp17 ;
2584  struct platform_device  const  *__cil_tmp18 ;
2585  unsigned long __cil_tmp19 ;
2586  unsigned long __cil_tmp20 ;
2587  unsigned long *__cil_tmp21 ;
2588  unsigned long __cil_tmp22 ;
2589  unsigned long __cil_tmp23 ;
2590  struct pcap_chip *__cil_tmp24 ;
2591  u8 __cil_tmp25 ;
2592  unsigned long *__cil_tmp26 ;
2593  unsigned long __cil_tmp27 ;
2594  unsigned long __cil_tmp28 ;
2595  struct pcap_chip *__cil_tmp29 ;
2596  u8 __cil_tmp30 ;
2597
2598  {
2599  {
2600#line 67
2601  __mptr = (struct device  const  *)dev;
2602#line 67
2603  __cil_tmp11 = (struct platform_device *)0;
2604#line 67
2605  __cil_tmp12 = (unsigned long )__cil_tmp11;
2606#line 67
2607  __cil_tmp13 = __cil_tmp12 + 16;
2608#line 67
2609  __cil_tmp14 = (struct device *)__cil_tmp13;
2610#line 67
2611  __cil_tmp15 = (unsigned int )__cil_tmp14;
2612#line 67
2613  __cil_tmp16 = (char *)__mptr;
2614#line 67
2615  __cil_tmp17 = __cil_tmp16 - __cil_tmp15;
2616#line 67
2617  pdev = (struct platform_device *)__cil_tmp17;
2618#line 68
2619  __cil_tmp18 = (struct platform_device  const  *)pdev;
2620#line 68
2621  tmp = platform_get_drvdata(__cil_tmp18);
2622#line 68
2623  pcap_rtc = (struct pcap_rtc *)tmp;
2624#line 69
2625  __cil_tmp19 = (unsigned long )alrm;
2626#line 69
2627  __cil_tmp20 = __cil_tmp19 + 4;
2628#line 69
2629  tm = (struct rtc_time *)__cil_tmp20;
2630#line 73
2631  rtc_tm_to_time(tm, & secs);
2632#line 75
2633  __cil_tmp21 = & secs;
2634#line 75
2635  __cil_tmp22 = *__cil_tmp21;
2636#line 75
2637  __cil_tmp23 = __cil_tmp22 % 86400UL;
2638#line 75
2639  tod = (u32 )__cil_tmp23;
2640#line 76
2641  __cil_tmp24 = *((struct pcap_chip **)pcap_rtc);
2642#line 76
2643  __cil_tmp25 = (u8 )15;
2644#line 76
2645  ezx_pcap_write(__cil_tmp24, __cil_tmp25, tod);
2646#line 78
2647  __cil_tmp26 = & secs;
2648#line 78
2649  __cil_tmp27 = *__cil_tmp26;
2650#line 78
2651  __cil_tmp28 = __cil_tmp27 / 86400UL;
2652#line 78
2653  days = (u32 )__cil_tmp28;
2654#line 79
2655  __cil_tmp29 = *((struct pcap_chip **)pcap_rtc);
2656#line 79
2657  __cil_tmp30 = (u8 )17;
2658#line 79
2659  ezx_pcap_write(__cil_tmp29, __cil_tmp30, days);
2660  }
2661#line 81
2662  return (0);
2663}
2664}
2665#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2666static int pcap_rtc_read_time(struct device *dev , struct rtc_time *tm ) 
2667{ struct platform_device *pdev ;
2668  struct device  const  *__mptr ;
2669  struct pcap_rtc *pcap_rtc ;
2670  void *tmp ;
2671  unsigned long secs ;
2672  u32 tod ;
2673  u32 days ;
2674  int tmp___0 ;
2675  struct platform_device *__cil_tmp11 ;
2676  unsigned long __cil_tmp12 ;
2677  unsigned long __cil_tmp13 ;
2678  struct device *__cil_tmp14 ;
2679  unsigned int __cil_tmp15 ;
2680  char *__cil_tmp16 ;
2681  char *__cil_tmp17 ;
2682  struct platform_device  const  *__cil_tmp18 ;
2683  struct pcap_chip *__cil_tmp19 ;
2684  u8 __cil_tmp20 ;
2685  u32 *__cil_tmp21 ;
2686  u32 __cil_tmp22 ;
2687  unsigned int __cil_tmp23 ;
2688  struct pcap_chip *__cil_tmp24 ;
2689  u8 __cil_tmp25 ;
2690  u32 *__cil_tmp26 ;
2691  u32 __cil_tmp27 ;
2692  unsigned int __cil_tmp28 ;
2693  unsigned int __cil_tmp29 ;
2694  unsigned long __cil_tmp30 ;
2695
2696  {
2697  {
2698#line 86
2699  __mptr = (struct device  const  *)dev;
2700#line 86
2701  __cil_tmp11 = (struct platform_device *)0;
2702#line 86
2703  __cil_tmp12 = (unsigned long )__cil_tmp11;
2704#line 86
2705  __cil_tmp13 = __cil_tmp12 + 16;
2706#line 86
2707  __cil_tmp14 = (struct device *)__cil_tmp13;
2708#line 86
2709  __cil_tmp15 = (unsigned int )__cil_tmp14;
2710#line 86
2711  __cil_tmp16 = (char *)__mptr;
2712#line 86
2713  __cil_tmp17 = __cil_tmp16 - __cil_tmp15;
2714#line 86
2715  pdev = (struct platform_device *)__cil_tmp17;
2716#line 87
2717  __cil_tmp18 = (struct platform_device  const  *)pdev;
2718#line 87
2719  tmp = platform_get_drvdata(__cil_tmp18);
2720#line 87
2721  pcap_rtc = (struct pcap_rtc *)tmp;
2722#line 91
2723  __cil_tmp19 = *((struct pcap_chip **)pcap_rtc);
2724#line 91
2725  __cil_tmp20 = (u8 )14;
2726#line 91
2727  ezx_pcap_read(__cil_tmp19, __cil_tmp20, & tod);
2728#line 92
2729  __cil_tmp21 = & tod;
2730#line 92
2731  __cil_tmp22 = *__cil_tmp21;
2732#line 92
2733  __cil_tmp23 = __cil_tmp22 & 65535U;
2734#line 92
2735  secs = (unsigned long )__cil_tmp23;
2736#line 94
2737  __cil_tmp24 = *((struct pcap_chip **)pcap_rtc);
2738#line 94
2739  __cil_tmp25 = (u8 )16;
2740#line 94
2741  ezx_pcap_read(__cil_tmp24, __cil_tmp25, & days);
2742#line 95
2743  __cil_tmp26 = & days;
2744#line 95
2745  __cil_tmp27 = *__cil_tmp26;
2746#line 95
2747  __cil_tmp28 = __cil_tmp27 & 16383U;
2748#line 95
2749  __cil_tmp29 = __cil_tmp28 * 86400U;
2750#line 95
2751  __cil_tmp30 = (unsigned long )__cil_tmp29;
2752#line 95
2753  secs = secs + __cil_tmp30;
2754#line 97
2755  rtc_time_to_tm(secs, tm);
2756#line 99
2757  tmp___0 = rtc_valid_tm(tm);
2758  }
2759#line 99
2760  return (tmp___0);
2761}
2762}
2763#line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2764static int pcap_rtc_set_mmss(struct device *dev , unsigned long secs ) 
2765{ struct platform_device *pdev ;
2766  struct device  const  *__mptr ;
2767  struct pcap_rtc *pcap_rtc ;
2768  void *tmp ;
2769  u32 tod ;
2770  u32 days ;
2771  struct platform_device *__cil_tmp9 ;
2772  unsigned long __cil_tmp10 ;
2773  unsigned long __cil_tmp11 ;
2774  struct device *__cil_tmp12 ;
2775  unsigned int __cil_tmp13 ;
2776  char *__cil_tmp14 ;
2777  char *__cil_tmp15 ;
2778  struct platform_device  const  *__cil_tmp16 ;
2779  unsigned long __cil_tmp17 ;
2780  struct pcap_chip *__cil_tmp18 ;
2781  u8 __cil_tmp19 ;
2782  unsigned long __cil_tmp20 ;
2783  struct pcap_chip *__cil_tmp21 ;
2784  u8 __cil_tmp22 ;
2785
2786  {
2787  {
2788#line 104
2789  __mptr = (struct device  const  *)dev;
2790#line 104
2791  __cil_tmp9 = (struct platform_device *)0;
2792#line 104
2793  __cil_tmp10 = (unsigned long )__cil_tmp9;
2794#line 104
2795  __cil_tmp11 = __cil_tmp10 + 16;
2796#line 104
2797  __cil_tmp12 = (struct device *)__cil_tmp11;
2798#line 104
2799  __cil_tmp13 = (unsigned int )__cil_tmp12;
2800#line 104
2801  __cil_tmp14 = (char *)__mptr;
2802#line 104
2803  __cil_tmp15 = __cil_tmp14 - __cil_tmp13;
2804#line 104
2805  pdev = (struct platform_device *)__cil_tmp15;
2806#line 105
2807  __cil_tmp16 = (struct platform_device  const  *)pdev;
2808#line 105
2809  tmp = platform_get_drvdata(__cil_tmp16);
2810#line 105
2811  pcap_rtc = (struct pcap_rtc *)tmp;
2812#line 108
2813  __cil_tmp17 = secs % 86400UL;
2814#line 108
2815  tod = (u32 )__cil_tmp17;
2816#line 109
2817  __cil_tmp18 = *((struct pcap_chip **)pcap_rtc);
2818#line 109
2819  __cil_tmp19 = (u8 )14;
2820#line 109
2821  ezx_pcap_write(__cil_tmp18, __cil_tmp19, tod);
2822#line 111
2823  __cil_tmp20 = secs / 86400UL;
2824#line 111
2825  days = (u32 )__cil_tmp20;
2826#line 112
2827  __cil_tmp21 = *((struct pcap_chip **)pcap_rtc);
2828#line 112
2829  __cil_tmp22 = (u8 )16;
2830#line 112
2831  ezx_pcap_write(__cil_tmp21, __cil_tmp22, days);
2832  }
2833#line 114
2834  return (0);
2835}
2836}
2837#line 117 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2838static int pcap_rtc_irq_enable(struct device *dev , int pirq , unsigned int en ) 
2839{ struct platform_device *pdev ;
2840  struct device  const  *__mptr ;
2841  struct pcap_rtc *pcap_rtc ;
2842  void *tmp ;
2843  int tmp___0 ;
2844  int tmp___1 ;
2845  struct platform_device *__cil_tmp10 ;
2846  unsigned long __cil_tmp11 ;
2847  unsigned long __cil_tmp12 ;
2848  struct device *__cil_tmp13 ;
2849  unsigned int __cil_tmp14 ;
2850  char *__cil_tmp15 ;
2851  char *__cil_tmp16 ;
2852  struct platform_device  const  *__cil_tmp17 ;
2853  struct pcap_chip *__cil_tmp18 ;
2854  unsigned int __cil_tmp19 ;
2855  struct pcap_chip *__cil_tmp20 ;
2856  unsigned int __cil_tmp21 ;
2857
2858  {
2859  {
2860#line 119
2861  __mptr = (struct device  const  *)dev;
2862#line 119
2863  __cil_tmp10 = (struct platform_device *)0;
2864#line 119
2865  __cil_tmp11 = (unsigned long )__cil_tmp10;
2866#line 119
2867  __cil_tmp12 = __cil_tmp11 + 16;
2868#line 119
2869  __cil_tmp13 = (struct device *)__cil_tmp12;
2870#line 119
2871  __cil_tmp14 = (unsigned int )__cil_tmp13;
2872#line 119
2873  __cil_tmp15 = (char *)__mptr;
2874#line 119
2875  __cil_tmp16 = __cil_tmp15 - __cil_tmp14;
2876#line 119
2877  pdev = (struct platform_device *)__cil_tmp16;
2878#line 120
2879  __cil_tmp17 = (struct platform_device  const  *)pdev;
2880#line 120
2881  tmp = platform_get_drvdata(__cil_tmp17);
2882#line 120
2883  pcap_rtc = (struct pcap_rtc *)tmp;
2884  }
2885#line 122
2886  if (en) {
2887    {
2888#line 123
2889    __cil_tmp18 = *((struct pcap_chip **)pcap_rtc);
2890#line 123
2891    tmp___0 = pcap_to_irq(__cil_tmp18, pirq);
2892#line 123
2893    __cil_tmp19 = (unsigned int )tmp___0;
2894#line 123
2895    enable_irq(__cil_tmp19);
2896    }
2897  } else {
2898    {
2899#line 125
2900    __cil_tmp20 = *((struct pcap_chip **)pcap_rtc);
2901#line 125
2902    tmp___1 = pcap_to_irq(__cil_tmp20, pirq);
2903#line 125
2904    __cil_tmp21 = (unsigned int )tmp___1;
2905#line 125
2906    disable_irq(__cil_tmp21);
2907    }
2908  }
2909#line 127
2910  return (0);
2911}
2912}
2913#line 130 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2914static int pcap_rtc_alarm_irq_enable(struct device *dev , unsigned int en ) 
2915{ int tmp ;
2916
2917  {
2918  {
2919#line 132
2920  tmp = pcap_rtc_irq_enable(dev, 5, en);
2921  }
2922#line 132
2923  return (tmp);
2924}
2925}
2926#line 135 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2927static struct rtc_class_ops  const  pcap_rtc_ops  = 
2928#line 135
2929     {(int (*)(struct device * ))0, (void (*)(struct device * ))0, (int (*)(struct device * ,
2930                                                                          unsigned int  ,
2931                                                                          unsigned long  ))0,
2932    & pcap_rtc_read_time, (int (*)(struct device * , struct rtc_time * ))0, & pcap_rtc_read_alarm,
2933    & pcap_rtc_set_alarm, (int (*)(struct device * , struct seq_file * ))0, & pcap_rtc_set_mmss,
2934    (int (*)(struct device * , int data ))0, & pcap_rtc_alarm_irq_enable};
2935#line 143
2936static int pcap_rtc_probe(struct platform_device *pdev )  __attribute__((__section__(".devinit.text"),
2937__no_instrument_function__)) ;
2938#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
2939static int pcap_rtc_probe(struct platform_device *pdev ) 
2940{ struct pcap_rtc *pcap_rtc ;
2941  int timer_irq ;
2942  int alarm_irq ;
2943  int err ;
2944  void *tmp ;
2945  void *tmp___0 ;
2946  long tmp___1 ;
2947  long tmp___2 ;
2948  unsigned long __cil_tmp10 ;
2949  unsigned long __cil_tmp11 ;
2950  struct device *__cil_tmp12 ;
2951  struct device  const  *__cil_tmp13 ;
2952  void *__cil_tmp14 ;
2953  unsigned long __cil_tmp15 ;
2954  unsigned long __cil_tmp16 ;
2955  unsigned long __cil_tmp17 ;
2956  unsigned long __cil_tmp18 ;
2957  struct device *__cil_tmp19 ;
2958  unsigned long __cil_tmp20 ;
2959  unsigned long __cil_tmp21 ;
2960  struct rtc_device *__cil_tmp22 ;
2961  void const   *__cil_tmp23 ;
2962  unsigned long __cil_tmp24 ;
2963  unsigned long __cil_tmp25 ;
2964  struct rtc_device *__cil_tmp26 ;
2965  void const   *__cil_tmp27 ;
2966  struct pcap_chip *__cil_tmp28 ;
2967  struct pcap_chip *__cil_tmp29 ;
2968  unsigned int __cil_tmp30 ;
2969  void *__cil_tmp31 ;
2970  unsigned int __cil_tmp32 ;
2971  void *__cil_tmp33 ;
2972  unsigned int __cil_tmp34 ;
2973  void *__cil_tmp35 ;
2974  unsigned long __cil_tmp36 ;
2975  unsigned long __cil_tmp37 ;
2976  struct rtc_device *__cil_tmp38 ;
2977  void *__cil_tmp39 ;
2978  void const   *__cil_tmp40 ;
2979
2980  {
2981  {
2982#line 147
2983  err = -12;
2984#line 149
2985  tmp = kmalloc(16UL, 208U);
2986#line 149
2987  pcap_rtc = (struct pcap_rtc *)tmp;
2988  }
2989#line 150
2990  if (! pcap_rtc) {
2991#line 151
2992    return (err);
2993  } else {
2994
2995  }
2996  {
2997#line 153
2998  __cil_tmp10 = (unsigned long )pdev;
2999#line 153
3000  __cil_tmp11 = __cil_tmp10 + 16;
3001#line 153
3002  __cil_tmp12 = *((struct device **)__cil_tmp11);
3003#line 153
3004  __cil_tmp13 = (struct device  const  *)__cil_tmp12;
3005#line 153
3006  tmp___0 = dev_get_drvdata(__cil_tmp13);
3007#line 153
3008  *((struct pcap_chip **)pcap_rtc) = (struct pcap_chip *)tmp___0;
3009#line 155
3010  __cil_tmp14 = (void *)pcap_rtc;
3011#line 155
3012  platform_set_drvdata(pdev, __cil_tmp14);
3013#line 157
3014  __cil_tmp15 = (unsigned long )pcap_rtc;
3015#line 157
3016  __cil_tmp16 = __cil_tmp15 + 8;
3017#line 157
3018  __cil_tmp17 = (unsigned long )pdev;
3019#line 157
3020  __cil_tmp18 = __cil_tmp17 + 16;
3021#line 157
3022  __cil_tmp19 = (struct device *)__cil_tmp18;
3023#line 157
3024  *((struct rtc_device **)__cil_tmp16) = rtc_device_register("pcap", __cil_tmp19,
3025                                                             & pcap_rtc_ops, & __this_module);
3026#line 159
3027  __cil_tmp20 = (unsigned long )pcap_rtc;
3028#line 159
3029  __cil_tmp21 = __cil_tmp20 + 8;
3030#line 159
3031  __cil_tmp22 = *((struct rtc_device **)__cil_tmp21);
3032#line 159
3033  __cil_tmp23 = (void const   *)__cil_tmp22;
3034#line 159
3035  tmp___2 = (long )IS_ERR(__cil_tmp23);
3036  }
3037#line 159
3038  if (tmp___2) {
3039    {
3040#line 160
3041    __cil_tmp24 = (unsigned long )pcap_rtc;
3042#line 160
3043    __cil_tmp25 = __cil_tmp24 + 8;
3044#line 160
3045    __cil_tmp26 = *((struct rtc_device **)__cil_tmp25);
3046#line 160
3047    __cil_tmp27 = (void const   *)__cil_tmp26;
3048#line 160
3049    tmp___1 = (long )PTR_ERR(__cil_tmp27);
3050#line 160
3051    err = (int )tmp___1;
3052    }
3053#line 161
3054    goto fail_rtc;
3055  } else {
3056
3057  }
3058  {
3059#line 165
3060  __cil_tmp28 = *((struct pcap_chip **)pcap_rtc);
3061#line 165
3062  timer_irq = pcap_to_irq(__cil_tmp28, 2);
3063#line 166
3064  __cil_tmp29 = *((struct pcap_chip **)pcap_rtc);
3065#line 166
3066  alarm_irq = pcap_to_irq(__cil_tmp29, 5);
3067#line 168
3068  __cil_tmp30 = (unsigned int )timer_irq;
3069#line 168
3070  __cil_tmp31 = (void *)pcap_rtc;
3071#line 168
3072  err = (int )request_irq(__cil_tmp30, & pcap_rtc_irq, 0UL, "RTC Timer", __cil_tmp31);
3073  }
3074#line 169
3075  if (err) {
3076#line 170
3077    goto fail_timer;
3078  } else {
3079
3080  }
3081  {
3082#line 172
3083  __cil_tmp32 = (unsigned int )alarm_irq;
3084#line 172
3085  __cil_tmp33 = (void *)pcap_rtc;
3086#line 172
3087  err = (int )request_irq(__cil_tmp32, & pcap_rtc_irq, 0UL, "RTC Alarm", __cil_tmp33);
3088  }
3089#line 173
3090  if (err) {
3091#line 174
3092    goto fail_alarm;
3093  } else {
3094
3095  }
3096#line 176
3097  return (0);
3098  fail_alarm: 
3099  {
3100#line 178
3101  __cil_tmp34 = (unsigned int )timer_irq;
3102#line 178
3103  __cil_tmp35 = (void *)pcap_rtc;
3104#line 178
3105  free_irq(__cil_tmp34, __cil_tmp35);
3106  }
3107  fail_timer: 
3108  {
3109#line 180
3110  __cil_tmp36 = (unsigned long )pcap_rtc;
3111#line 180
3112  __cil_tmp37 = __cil_tmp36 + 8;
3113#line 180
3114  __cil_tmp38 = *((struct rtc_device **)__cil_tmp37);
3115#line 180
3116  rtc_device_unregister(__cil_tmp38);
3117  }
3118  fail_rtc: 
3119  {
3120#line 182
3121  __cil_tmp39 = (void *)0;
3122#line 182
3123  platform_set_drvdata(pdev, __cil_tmp39);
3124#line 183
3125  __cil_tmp40 = (void const   *)pcap_rtc;
3126#line 183
3127  kfree(__cil_tmp40);
3128  }
3129#line 184
3130  return (err);
3131}
3132}
3133#line 187
3134static int pcap_rtc_remove(struct platform_device *pdev )  __attribute__((__section__(".devexit.text"),
3135__no_instrument_function__)) ;
3136#line 187 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3137static int pcap_rtc_remove(struct platform_device *pdev ) 
3138{ struct pcap_rtc *pcap_rtc ;
3139  void *tmp ;
3140  int tmp___0 ;
3141  int tmp___1 ;
3142  struct platform_device  const  *__cil_tmp6 ;
3143  struct pcap_chip *__cil_tmp7 ;
3144  unsigned int __cil_tmp8 ;
3145  void *__cil_tmp9 ;
3146  struct pcap_chip *__cil_tmp10 ;
3147  unsigned int __cil_tmp11 ;
3148  void *__cil_tmp12 ;
3149  unsigned long __cil_tmp13 ;
3150  unsigned long __cil_tmp14 ;
3151  struct rtc_device *__cil_tmp15 ;
3152  void const   *__cil_tmp16 ;
3153
3154  {
3155  {
3156#line 189
3157  __cil_tmp6 = (struct platform_device  const  *)pdev;
3158#line 189
3159  tmp = platform_get_drvdata(__cil_tmp6);
3160#line 189
3161  pcap_rtc = (struct pcap_rtc *)tmp;
3162#line 191
3163  __cil_tmp7 = *((struct pcap_chip **)pcap_rtc);
3164#line 191
3165  tmp___0 = pcap_to_irq(__cil_tmp7, 2);
3166#line 191
3167  __cil_tmp8 = (unsigned int )tmp___0;
3168#line 191
3169  __cil_tmp9 = (void *)pcap_rtc;
3170#line 191
3171  free_irq(__cil_tmp8, __cil_tmp9);
3172#line 192
3173  __cil_tmp10 = *((struct pcap_chip **)pcap_rtc);
3174#line 192
3175  tmp___1 = pcap_to_irq(__cil_tmp10, 5);
3176#line 192
3177  __cil_tmp11 = (unsigned int )tmp___1;
3178#line 192
3179  __cil_tmp12 = (void *)pcap_rtc;
3180#line 192
3181  free_irq(__cil_tmp11, __cil_tmp12);
3182#line 193
3183  __cil_tmp13 = (unsigned long )pcap_rtc;
3184#line 193
3185  __cil_tmp14 = __cil_tmp13 + 8;
3186#line 193
3187  __cil_tmp15 = *((struct rtc_device **)__cil_tmp14);
3188#line 193
3189  rtc_device_unregister(__cil_tmp15);
3190#line 194
3191  __cil_tmp16 = (void const   *)pcap_rtc;
3192#line 194
3193  kfree(__cil_tmp16);
3194  }
3195#line 196
3196  return (0);
3197}
3198}
3199#line 199 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3200static struct platform_driver pcap_rtc_driver  =    {(int (*)(struct platform_device * ))0, & pcap_rtc_remove, (void (*)(struct platform_device * ))0,
3201    (int (*)(struct platform_device * , pm_message_t state ))0, (int (*)(struct platform_device * ))0,
3202    {"pcap-rtc", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
3203     (struct of_device_id  const  *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3204     (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
3205     (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
3206     (struct driver_private *)0}, (struct platform_device_id  const  *)0};
3207#line 207
3208static int rtc_pcap_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
3209#line 207 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3210static int rtc_pcap_init(void) 
3211{ int tmp ;
3212
3213  {
3214  {
3215#line 209
3216  tmp = platform_driver_probe(& pcap_rtc_driver, & pcap_rtc_probe);
3217  }
3218#line 209
3219  return (tmp);
3220}
3221}
3222#line 212
3223static void rtc_pcap_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
3224#line 212 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3225static void rtc_pcap_exit(void) 
3226{ 
3227
3228  {
3229  {
3230#line 214
3231  platform_driver_unregister(& pcap_rtc_driver);
3232  }
3233#line 215
3234  return;
3235}
3236}
3237#line 217 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3238int init_module(void) 
3239{ int tmp ;
3240
3241  {
3242  {
3243#line 217
3244  tmp = rtc_pcap_init();
3245  }
3246#line 217
3247  return (tmp);
3248}
3249}
3250#line 218 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3251void cleanup_module(void) 
3252{ 
3253
3254  {
3255  {
3256#line 218
3257  rtc_pcap_exit();
3258  }
3259#line 218
3260  return;
3261}
3262}
3263#line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3264static char const   __mod_description220[37]  __attribute__((__used__, __unused__,
3265__section__(".modinfo"), __aligned__(1)))  = 
3266#line 220
3267  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
3268        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
3269        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
3270        (char const   )'M',      (char const   )'o',      (char const   )'t',      (char const   )'o', 
3271        (char const   )'r',      (char const   )'o',      (char const   )'l',      (char const   )'a', 
3272        (char const   )' ',      (char const   )'p',      (char const   )'c',      (char const   )'a', 
3273        (char const   )'p',      (char const   )' ',      (char const   )'r',      (char const   )'t', 
3274        (char const   )'c',      (char const   )' ',      (char const   )'d',      (char const   )'r', 
3275        (char const   )'i',      (char const   )'v',      (char const   )'e',      (char const   )'r', 
3276        (char const   )'\000'};
3277#line 221 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3278static char const   __mod_author221[39]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3279__aligned__(1)))  = 
3280#line 221
3281  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
3282        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'g', 
3283        (char const   )'u',      (char const   )'i',      (char const   )'m',      (char const   )'i', 
3284        (char const   )'n',      (char const   )'g',      (char const   )' ',      (char const   )'z', 
3285        (char const   )'h',      (char const   )'u',      (char const   )'o',      (char const   )' ', 
3286        (char const   )'<',      (char const   )'g',      (char const   )'m',      (char const   )'z', 
3287        (char const   )'h',      (char const   )'u',      (char const   )'o',      (char const   )'@', 
3288        (char const   )'g',      (char const   )'m',      (char const   )'a',      (char const   )'i', 
3289        (char const   )'l',      (char const   )'.',      (char const   )'c',      (char const   )'o', 
3290        (char const   )'m',      (char const   )'>',      (char const   )'\000'};
3291#line 222 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3292static char const   __mod_license222[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3293__aligned__(1)))  = 
3294#line 222
3295  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
3296        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
3297        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
3298#line 240
3299void ldv_check_final_state(void) ;
3300#line 246
3301extern void ldv_initialize(void) ;
3302#line 249
3303extern int __VERIFIER_nondet_int(void) ;
3304#line 252 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3305int LDV_IN_INTERRUPT  ;
3306#line 255 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3307void main(void) 
3308{ struct device *var_group1 ;
3309  struct rtc_time *var_group2 ;
3310  struct rtc_wkalrm *var_group3 ;
3311  unsigned long var_pcap_rtc_set_mmss_4_p1 ;
3312  unsigned int var_pcap_rtc_alarm_irq_enable_6_p1 ;
3313  int var_pcap_rtc_irq_0_p0 ;
3314  void *var_pcap_rtc_irq_0_p1 ;
3315  int tmp ;
3316  int tmp___0 ;
3317  int tmp___1 ;
3318
3319  {
3320  {
3321#line 297
3322  LDV_IN_INTERRUPT = 1;
3323#line 306
3324  ldv_initialize();
3325#line 312
3326  tmp = rtc_pcap_init();
3327  }
3328#line 312
3329  if (tmp) {
3330#line 313
3331    goto ldv_final;
3332  } else {
3333
3334  }
3335  {
3336#line 319
3337  while (1) {
3338    while_continue: /* CIL Label */ ;
3339    {
3340#line 319
3341    tmp___1 = __VERIFIER_nondet_int();
3342    }
3343#line 319
3344    if (tmp___1) {
3345
3346    } else {
3347#line 319
3348      goto while_break;
3349    }
3350    {
3351#line 322
3352    tmp___0 = __VERIFIER_nondet_int();
3353    }
3354#line 324
3355    if (tmp___0 == 0) {
3356#line 324
3357      goto case_0;
3358    } else
3359#line 340
3360    if (tmp___0 == 1) {
3361#line 340
3362      goto case_1;
3363    } else
3364#line 356
3365    if (tmp___0 == 2) {
3366#line 356
3367      goto case_2;
3368    } else
3369#line 372
3370    if (tmp___0 == 3) {
3371#line 372
3372      goto case_3;
3373    } else
3374#line 388
3375    if (tmp___0 == 4) {
3376#line 388
3377      goto case_4;
3378    } else
3379#line 404
3380    if (tmp___0 == 5) {
3381#line 404
3382      goto case_5;
3383    } else {
3384      {
3385#line 420
3386      goto switch_default;
3387#line 322
3388      if (0) {
3389        case_0: /* CIL Label */ 
3390        {
3391#line 332
3392        pcap_rtc_read_time(var_group1, var_group2);
3393        }
3394#line 339
3395        goto switch_break;
3396        case_1: /* CIL Label */ 
3397        {
3398#line 348
3399        pcap_rtc_read_alarm(var_group1, var_group3);
3400        }
3401#line 355
3402        goto switch_break;
3403        case_2: /* CIL Label */ 
3404        {
3405#line 364
3406        pcap_rtc_set_alarm(var_group1, var_group3);
3407        }
3408#line 371
3409        goto switch_break;
3410        case_3: /* CIL Label */ 
3411        {
3412#line 380
3413        pcap_rtc_set_mmss(var_group1, var_pcap_rtc_set_mmss_4_p1);
3414        }
3415#line 387
3416        goto switch_break;
3417        case_4: /* CIL Label */ 
3418        {
3419#line 396
3420        pcap_rtc_alarm_irq_enable(var_group1, var_pcap_rtc_alarm_irq_enable_6_p1);
3421        }
3422#line 403
3423        goto switch_break;
3424        case_5: /* CIL Label */ 
3425        {
3426#line 407
3427        LDV_IN_INTERRUPT = 2;
3428#line 412
3429        pcap_rtc_irq(var_pcap_rtc_irq_0_p0, var_pcap_rtc_irq_0_p1);
3430#line 413
3431        LDV_IN_INTERRUPT = 1;
3432        }
3433#line 419
3434        goto switch_break;
3435        switch_default: /* CIL Label */ 
3436#line 420
3437        goto switch_break;
3438      } else {
3439        switch_break: /* CIL Label */ ;
3440      }
3441      }
3442    }
3443  }
3444  while_break: /* CIL Label */ ;
3445  }
3446  {
3447#line 432
3448  rtc_pcap_exit();
3449  }
3450  ldv_final: 
3451  {
3452#line 435
3453  ldv_check_final_state();
3454  }
3455#line 438
3456  return;
3457}
3458}
3459#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3460void ldv_blast_assert(void) 
3461{ 
3462
3463  {
3464  ERROR: 
3465#line 6
3466  goto ERROR;
3467}
3468}
3469#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3470extern int __VERIFIER_nondet_int(void) ;
3471#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3472int ldv_mutex  =    1;
3473#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3474int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
3475{ int nondetermined ;
3476
3477  {
3478#line 29
3479  if (ldv_mutex == 1) {
3480
3481  } else {
3482    {
3483#line 29
3484    ldv_blast_assert();
3485    }
3486  }
3487  {
3488#line 32
3489  nondetermined = __VERIFIER_nondet_int();
3490  }
3491#line 35
3492  if (nondetermined) {
3493#line 38
3494    ldv_mutex = 2;
3495#line 40
3496    return (0);
3497  } else {
3498#line 45
3499    return (-4);
3500  }
3501}
3502}
3503#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3504int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
3505{ int nondetermined ;
3506
3507  {
3508#line 57
3509  if (ldv_mutex == 1) {
3510
3511  } else {
3512    {
3513#line 57
3514    ldv_blast_assert();
3515    }
3516  }
3517  {
3518#line 60
3519  nondetermined = __VERIFIER_nondet_int();
3520  }
3521#line 63
3522  if (nondetermined) {
3523#line 66
3524    ldv_mutex = 2;
3525#line 68
3526    return (0);
3527  } else {
3528#line 73
3529    return (-4);
3530  }
3531}
3532}
3533#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3534int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
3535{ int atomic_value_after_dec ;
3536
3537  {
3538#line 83
3539  if (ldv_mutex == 1) {
3540
3541  } else {
3542    {
3543#line 83
3544    ldv_blast_assert();
3545    }
3546  }
3547  {
3548#line 86
3549  atomic_value_after_dec = __VERIFIER_nondet_int();
3550  }
3551#line 89
3552  if (atomic_value_after_dec == 0) {
3553#line 92
3554    ldv_mutex = 2;
3555#line 94
3556    return (1);
3557  } else {
3558
3559  }
3560#line 98
3561  return (0);
3562}
3563}
3564#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3565void mutex_lock(struct mutex *lock ) 
3566{ 
3567
3568  {
3569#line 108
3570  if (ldv_mutex == 1) {
3571
3572  } else {
3573    {
3574#line 108
3575    ldv_blast_assert();
3576    }
3577  }
3578#line 110
3579  ldv_mutex = 2;
3580#line 111
3581  return;
3582}
3583}
3584#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3585int mutex_trylock(struct mutex *lock ) 
3586{ int nondetermined ;
3587
3588  {
3589#line 121
3590  if (ldv_mutex == 1) {
3591
3592  } else {
3593    {
3594#line 121
3595    ldv_blast_assert();
3596    }
3597  }
3598  {
3599#line 124
3600  nondetermined = __VERIFIER_nondet_int();
3601  }
3602#line 127
3603  if (nondetermined) {
3604#line 130
3605    ldv_mutex = 2;
3606#line 132
3607    return (1);
3608  } else {
3609#line 137
3610    return (0);
3611  }
3612}
3613}
3614#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3615void mutex_unlock(struct mutex *lock ) 
3616{ 
3617
3618  {
3619#line 147
3620  if (ldv_mutex == 2) {
3621
3622  } else {
3623    {
3624#line 147
3625    ldv_blast_assert();
3626    }
3627  }
3628#line 149
3629  ldv_mutex = 1;
3630#line 150
3631  return;
3632}
3633}
3634#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3635void ldv_check_final_state(void) 
3636{ 
3637
3638  {
3639#line 156
3640  if (ldv_mutex == 1) {
3641
3642  } else {
3643    {
3644#line 156
3645    ldv_blast_assert();
3646    }
3647  }
3648#line 157
3649  return;
3650}
3651}
3652#line 447 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6248/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcap.c.common.c"
3653long s__builtin_expect(long val , long res ) 
3654{ 
3655
3656  {
3657#line 448
3658  return (val);
3659}
3660}