Showing error 604

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