Showing error 610

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-test.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3121
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 1 "<compiler builtins>"
2141long __builtin_expect(long val , long res ) ;
2142#line 320 "include/linux/kernel.h"
2143extern int ( /* format attribute */  sprintf)(char *buf , char const   *fmt  , ...) ;
2144#line 45 "include/linux/string.h"
2145extern int strncmp(char const   * , char const   * , __kernel_size_t  ) ;
2146#line 27 "include/linux/err.h"
2147__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
2148#line 27 "include/linux/err.h"
2149__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr ) 
2150{ 
2151
2152  {
2153#line 29
2154  return ((long )ptr);
2155}
2156}
2157#line 32
2158__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
2159#line 32 "include/linux/err.h"
2160__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr ) 
2161{ long tmp ;
2162  unsigned long __cil_tmp3 ;
2163  int __cil_tmp4 ;
2164  int __cil_tmp5 ;
2165  int __cil_tmp6 ;
2166  long __cil_tmp7 ;
2167
2168  {
2169  {
2170#line 34
2171  __cil_tmp3 = (unsigned long )ptr;
2172#line 34
2173  __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
2174#line 34
2175  __cil_tmp5 = ! __cil_tmp4;
2176#line 34
2177  __cil_tmp6 = ! __cil_tmp5;
2178#line 34
2179  __cil_tmp7 = (long )__cil_tmp6;
2180#line 34
2181  tmp = __builtin_expect(__cil_tmp7, 0L);
2182  }
2183#line 34
2184  return (tmp);
2185}
2186}
2187#line 122 "include/linux/time.h"
2188extern unsigned long get_seconds(void) ;
2189#line 152 "include/linux/mutex.h"
2190void mutex_lock(struct mutex *lock ) ;
2191#line 153
2192int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2193#line 154
2194int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2195#line 168
2196int mutex_trylock(struct mutex *lock ) ;
2197#line 169
2198void mutex_unlock(struct mutex *lock ) ;
2199#line 170
2200int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2201#line 26 "include/linux/export.h"
2202extern struct module __this_module ;
2203#line 67 "include/linux/module.h"
2204int init_module(void) ;
2205#line 68
2206void cleanup_module(void) ;
2207#line 112 "include/linux/rtc.h"
2208extern void rtc_time_to_tm(unsigned long time , struct rtc_time *tm ) ;
2209#line 507 "include/linux/device.h"
2210extern int device_create_file(struct device *device , struct device_attribute  const  *entry ) ;
2211#line 509
2212extern void device_remove_file(struct device *dev , struct device_attribute  const  *attr ) ;
2213#line 792
2214extern void *dev_get_drvdata(struct device  const  *dev ) ;
2215#line 793
2216extern int dev_set_drvdata(struct device *dev , void *data ) ;
2217#line 897
2218extern int ( /* format attribute */  _dev_info)(struct device  const  *dev , char const   *fmt 
2219                                                , ...) ;
2220#line 88 "include/linux/seq_file.h"
2221extern int ( /* format attribute */  seq_printf)(struct seq_file * , char const   * 
2222                                                 , ...) ;
2223#line 221 "include/linux/rtc.h"
2224extern struct rtc_device *rtc_device_register(char const   *name , struct device *dev ,
2225                                              struct rtc_class_ops  const  *ops ,
2226                                              struct module *owner ) ;
2227#line 225
2228extern void rtc_device_unregister(struct rtc_device *rtc ) ;
2229#line 231
2230extern int rtc_read_alarm(struct rtc_device *rtc , struct rtc_wkalrm *alrm ) ;
2231#line 237
2232extern void rtc_update_irq(struct rtc_device *rtc , unsigned long num , unsigned long events ) ;
2233#line 40 "include/linux/platform_device.h"
2234extern void platform_device_unregister(struct platform_device * ) ;
2235#line 155
2236extern struct platform_device *platform_device_alloc(char const   *name , int id ) ;
2237#line 160
2238extern int platform_device_add(struct platform_device *pdev ) ;
2239#line 162
2240extern void platform_device_put(struct platform_device *pdev ) ;
2241#line 174
2242extern int platform_driver_register(struct platform_driver * ) ;
2243#line 175
2244extern void platform_driver_unregister(struct platform_driver * ) ;
2245#line 183
2246__inline static void *platform_get_drvdata(struct platform_device  const  *pdev )  __attribute__((__no_instrument_function__)) ;
2247#line 183 "include/linux/platform_device.h"
2248__inline static void *platform_get_drvdata(struct platform_device  const  *pdev ) 
2249{ void *tmp ;
2250  unsigned long __cil_tmp3 ;
2251  unsigned long __cil_tmp4 ;
2252  struct device  const  *__cil_tmp5 ;
2253
2254  {
2255  {
2256#line 185
2257  __cil_tmp3 = (unsigned long )pdev;
2258#line 185
2259  __cil_tmp4 = __cil_tmp3 + 16;
2260#line 185
2261  __cil_tmp5 = (struct device  const  *)__cil_tmp4;
2262#line 185
2263  tmp = dev_get_drvdata(__cil_tmp5);
2264  }
2265#line 185
2266  return (tmp);
2267}
2268}
2269#line 188
2270__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )  __attribute__((__no_instrument_function__)) ;
2271#line 188 "include/linux/platform_device.h"
2272__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) 
2273{ unsigned long __cil_tmp3 ;
2274  unsigned long __cil_tmp4 ;
2275  struct device *__cil_tmp5 ;
2276
2277  {
2278  {
2279#line 190
2280  __cil_tmp3 = (unsigned long )pdev;
2281#line 190
2282  __cil_tmp4 = __cil_tmp3 + 16;
2283#line 190
2284  __cil_tmp5 = (struct device *)__cil_tmp4;
2285#line 190
2286  dev_set_drvdata(__cil_tmp5, data);
2287  }
2288#line 191
2289  return;
2290}
2291}
2292#line 17 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2293static struct platform_device *test0  =    (struct platform_device *)((void *)0);
2294#line 17 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2295static struct platform_device *test1  =    (struct platform_device *)((void *)0);
2296#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2297static int test_rtc_read_alarm(struct device *dev , struct rtc_wkalrm *alrm ) 
2298{ 
2299
2300  {
2301#line 22
2302  return (0);
2303}
2304}
2305#line 25 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2306static int test_rtc_set_alarm(struct device *dev , struct rtc_wkalrm *alrm ) 
2307{ 
2308
2309  {
2310#line 28
2311  return (0);
2312}
2313}
2314#line 31 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2315static int test_rtc_read_time(struct device *dev , struct rtc_time *tm ) 
2316{ unsigned long tmp ;
2317
2318  {
2319  {
2320#line 34
2321  tmp = get_seconds();
2322#line 34
2323  rtc_time_to_tm(tmp, tm);
2324  }
2325#line 35
2326  return (0);
2327}
2328}
2329#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2330static int test_rtc_set_mmss(struct device *dev , unsigned long secs ) 
2331{ struct device  const  *__cil_tmp3 ;
2332
2333  {
2334  {
2335#line 40
2336  __cil_tmp3 = (struct device  const  *)dev;
2337#line 40
2338  _dev_info(__cil_tmp3, "%s, secs = %lu\n", "test_rtc_set_mmss", secs);
2339  }
2340#line 41
2341  return (0);
2342}
2343}
2344#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2345static int test_rtc_proc(struct device *dev , struct seq_file *seq ) 
2346{ struct platform_device *plat_dev ;
2347  struct device  const  *__mptr ;
2348  struct platform_device *__cil_tmp5 ;
2349  unsigned long __cil_tmp6 ;
2350  unsigned long __cil_tmp7 ;
2351  struct device *__cil_tmp8 ;
2352  unsigned int __cil_tmp9 ;
2353  char *__cil_tmp10 ;
2354  char *__cil_tmp11 ;
2355  unsigned long __cil_tmp12 ;
2356  unsigned long __cil_tmp13 ;
2357  int __cil_tmp14 ;
2358
2359  {
2360  {
2361#line 46
2362  __mptr = (struct device  const  *)dev;
2363#line 46
2364  __cil_tmp5 = (struct platform_device *)0;
2365#line 46
2366  __cil_tmp6 = (unsigned long )__cil_tmp5;
2367#line 46
2368  __cil_tmp7 = __cil_tmp6 + 16;
2369#line 46
2370  __cil_tmp8 = (struct device *)__cil_tmp7;
2371#line 46
2372  __cil_tmp9 = (unsigned int )__cil_tmp8;
2373#line 46
2374  __cil_tmp10 = (char *)__mptr;
2375#line 46
2376  __cil_tmp11 = __cil_tmp10 - __cil_tmp9;
2377#line 46
2378  plat_dev = (struct platform_device *)__cil_tmp11;
2379#line 48
2380  seq_printf(seq, "test\t\t: yes\n");
2381#line 49
2382  __cil_tmp12 = (unsigned long )plat_dev;
2383#line 49
2384  __cil_tmp13 = __cil_tmp12 + 8;
2385#line 49
2386  __cil_tmp14 = *((int *)__cil_tmp13);
2387#line 49
2388  seq_printf(seq, "id\t\t: %d\n", __cil_tmp14);
2389  }
2390#line 51
2391  return (0);
2392}
2393}
2394#line 54 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2395static int test_rtc_alarm_irq_enable(struct device *dev , unsigned int enable ) 
2396{ 
2397
2398  {
2399#line 56
2400  return (0);
2401}
2402}
2403#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2404static struct rtc_class_ops  const  test_rtc_ops  = 
2405#line 59
2406     {(int (*)(struct device * ))0, (void (*)(struct device * ))0, (int (*)(struct device * ,
2407                                                                          unsigned int  ,
2408                                                                          unsigned long  ))0,
2409    & test_rtc_read_time, (int (*)(struct device * , struct rtc_time * ))0, & test_rtc_read_alarm,
2410    & test_rtc_set_alarm, & test_rtc_proc, & test_rtc_set_mmss, (int (*)(struct device * ,
2411                                                                         int data ))0,
2412    & test_rtc_alarm_irq_enable};
2413#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2414static ssize_t test_irq_show(struct device *dev , struct device_attribute *attr ,
2415                             char *buf ) 
2416{ int tmp ;
2417
2418  {
2419  {
2420#line 71
2421  tmp = sprintf(buf, "%d\n", 42);
2422  }
2423#line 71
2424  return ((ssize_t )tmp);
2425}
2426}
2427#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2428static ssize_t test_irq_store(struct device *dev , struct device_attribute *attr ,
2429                              char const   *buf , size_t count ) 
2430{ int retval ;
2431  struct platform_device *plat_dev ;
2432  struct device  const  *__mptr ;
2433  struct rtc_device *rtc ;
2434  void *tmp ;
2435  struct rtc_wkalrm alrm ;
2436  int err ;
2437  int tmp___0 ;
2438  int tmp___1 ;
2439  int tmp___2 ;
2440  int tmp___3 ;
2441  struct platform_device *__cil_tmp16 ;
2442  unsigned long __cil_tmp17 ;
2443  unsigned long __cil_tmp18 ;
2444  struct device *__cil_tmp19 ;
2445  unsigned int __cil_tmp20 ;
2446  char *__cil_tmp21 ;
2447  char *__cil_tmp22 ;
2448  struct platform_device  const  *__cil_tmp23 ;
2449  __kernel_size_t __cil_tmp24 ;
2450  unsigned long __cil_tmp25 ;
2451  unsigned long __cil_tmp26 ;
2452  __kernel_size_t __cil_tmp27 ;
2453  struct rtc_wkalrm *__cil_tmp28 ;
2454  __kernel_size_t __cil_tmp29 ;
2455  unsigned long __cil_tmp30 ;
2456  unsigned long __cil_tmp31 ;
2457  unsigned long __cil_tmp32 ;
2458
2459  {
2460  {
2461#line 78
2462  __mptr = (struct device  const  *)dev;
2463#line 78
2464  __cil_tmp16 = (struct platform_device *)0;
2465#line 78
2466  __cil_tmp17 = (unsigned long )__cil_tmp16;
2467#line 78
2468  __cil_tmp18 = __cil_tmp17 + 16;
2469#line 78
2470  __cil_tmp19 = (struct device *)__cil_tmp18;
2471#line 78
2472  __cil_tmp20 = (unsigned int )__cil_tmp19;
2473#line 78
2474  __cil_tmp21 = (char *)__mptr;
2475#line 78
2476  __cil_tmp22 = __cil_tmp21 - __cil_tmp20;
2477#line 78
2478  plat_dev = (struct platform_device *)__cil_tmp22;
2479#line 79
2480  __cil_tmp23 = (struct platform_device  const  *)plat_dev;
2481#line 79
2482  tmp = platform_get_drvdata(__cil_tmp23);
2483#line 79
2484  rtc = (struct rtc_device *)tmp;
2485#line 81
2486  retval = (int )count;
2487#line 82
2488  __cil_tmp24 = (__kernel_size_t )4;
2489#line 82
2490  tmp___3 = strncmp(buf, "tick", __cil_tmp24);
2491  }
2492#line 82
2493  if (tmp___3 == 0) {
2494    {
2495#line 82
2496    __cil_tmp25 = (unsigned long )rtc;
2497#line 82
2498    __cil_tmp26 = __cil_tmp25 + 1352;
2499#line 82
2500    if (*((int *)__cil_tmp26)) {
2501      {
2502#line 83
2503      rtc_update_irq(rtc, 1UL, 192UL);
2504      }
2505    } else {
2506#line 82
2507      goto _L;
2508    }
2509    }
2510  } else {
2511    _L: /* CIL Label */ 
2512    {
2513#line 84
2514    __cil_tmp27 = (__kernel_size_t )5;
2515#line 84
2516    tmp___2 = strncmp(buf, "alarm", __cil_tmp27);
2517    }
2518#line 84
2519    if (tmp___2 == 0) {
2520      {
2521#line 86
2522      tmp___0 = rtc_read_alarm(rtc, & alrm);
2523#line 86
2524      err = tmp___0;
2525      }
2526#line 88
2527      if (! err) {
2528        {
2529#line 88
2530        __cil_tmp28 = & alrm;
2531#line 88
2532        if (*((unsigned char *)__cil_tmp28)) {
2533          {
2534#line 89
2535          rtc_update_irq(rtc, 1UL, 160UL);
2536          }
2537        } else {
2538
2539        }
2540        }
2541      } else {
2542
2543      }
2544    } else {
2545      {
2546#line 91
2547      __cil_tmp29 = (__kernel_size_t )6;
2548#line 91
2549      tmp___1 = strncmp(buf, "update", __cil_tmp29);
2550      }
2551#line 91
2552      if (tmp___1 == 0) {
2553        {
2554#line 91
2555        __cil_tmp30 = 1192 + 56;
2556#line 91
2557        __cil_tmp31 = (unsigned long )rtc;
2558#line 91
2559        __cil_tmp32 = __cil_tmp31 + __cil_tmp30;
2560#line 91
2561        if (*((int *)__cil_tmp32)) {
2562          {
2563#line 92
2564          rtc_update_irq(rtc, 1UL, 144UL);
2565          }
2566        } else {
2567#line 94
2568          retval = -22;
2569        }
2570        }
2571      } else {
2572#line 94
2573        retval = -22;
2574      }
2575    }
2576  }
2577#line 96
2578  return ((ssize_t )retval);
2579}
2580}
2581#line 98 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2582static struct device_attribute dev_attr_irq  =    {{"irq", (umode_t )420}, & test_irq_show, & test_irq_store};
2583#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2584static int test_probe(struct platform_device *plat_dev ) 
2585{ int err ;
2586  struct rtc_device *rtc ;
2587  struct rtc_device *tmp ;
2588  long tmp___0 ;
2589  long tmp___1 ;
2590  unsigned long __cil_tmp7 ;
2591  unsigned long __cil_tmp8 ;
2592  struct device *__cil_tmp9 ;
2593  void const   *__cil_tmp10 ;
2594  void const   *__cil_tmp11 ;
2595  unsigned long __cil_tmp12 ;
2596  unsigned long __cil_tmp13 ;
2597  struct device *__cil_tmp14 ;
2598  struct device_attribute  const  *__cil_tmp15 ;
2599  void *__cil_tmp16 ;
2600
2601  {
2602  {
2603#line 103
2604  __cil_tmp7 = (unsigned long )plat_dev;
2605#line 103
2606  __cil_tmp8 = __cil_tmp7 + 16;
2607#line 103
2608  __cil_tmp9 = (struct device *)__cil_tmp8;
2609#line 103
2610  tmp = rtc_device_register("test", __cil_tmp9, & test_rtc_ops, & __this_module);
2611#line 103
2612  rtc = tmp;
2613#line 105
2614  __cil_tmp10 = (void const   *)rtc;
2615#line 105
2616  tmp___1 = (long )IS_ERR(__cil_tmp10);
2617  }
2618#line 105
2619  if (tmp___1) {
2620    {
2621#line 106
2622    __cil_tmp11 = (void const   *)rtc;
2623#line 106
2624    tmp___0 = (long )PTR_ERR(__cil_tmp11);
2625#line 106
2626    err = (int )tmp___0;
2627    }
2628#line 107
2629    return (err);
2630  } else {
2631
2632  }
2633  {
2634#line 110
2635  __cil_tmp12 = (unsigned long )plat_dev;
2636#line 110
2637  __cil_tmp13 = __cil_tmp12 + 16;
2638#line 110
2639  __cil_tmp14 = (struct device *)__cil_tmp13;
2640#line 110
2641  __cil_tmp15 = (struct device_attribute  const  *)(& dev_attr_irq);
2642#line 110
2643  err = device_create_file(__cil_tmp14, __cil_tmp15);
2644  }
2645#line 111
2646  if (err) {
2647#line 112
2648    goto err;
2649  } else {
2650
2651  }
2652  {
2653#line 114
2654  __cil_tmp16 = (void *)rtc;
2655#line 114
2656  platform_set_drvdata(plat_dev, __cil_tmp16);
2657  }
2658#line 116
2659  return (0);
2660  err: 
2661  {
2662#line 119
2663  rtc_device_unregister(rtc);
2664  }
2665#line 120
2666  return (err);
2667}
2668}
2669#line 123
2670static int test_remove(struct platform_device *plat_dev )  __attribute__((__section__(".devexit.text"),
2671__no_instrument_function__)) ;
2672#line 123 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2673static int test_remove(struct platform_device *plat_dev ) 
2674{ struct rtc_device *rtc ;
2675  void *tmp ;
2676  struct platform_device  const  *__cil_tmp4 ;
2677  unsigned long __cil_tmp5 ;
2678  unsigned long __cil_tmp6 ;
2679  struct device *__cil_tmp7 ;
2680  struct device_attribute  const  *__cil_tmp8 ;
2681
2682  {
2683  {
2684#line 125
2685  __cil_tmp4 = (struct platform_device  const  *)plat_dev;
2686#line 125
2687  tmp = platform_get_drvdata(__cil_tmp4);
2688#line 125
2689  rtc = (struct rtc_device *)tmp;
2690#line 127
2691  rtc_device_unregister(rtc);
2692#line 128
2693  __cil_tmp5 = (unsigned long )plat_dev;
2694#line 128
2695  __cil_tmp6 = __cil_tmp5 + 16;
2696#line 128
2697  __cil_tmp7 = (struct device *)__cil_tmp6;
2698#line 128
2699  __cil_tmp8 = (struct device_attribute  const  *)(& dev_attr_irq);
2700#line 128
2701  device_remove_file(__cil_tmp7, __cil_tmp8);
2702  }
2703#line 130
2704  return (0);
2705}
2706}
2707#line 133 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2708static struct platform_driver test_driver  =    {& test_probe, & test_remove, (void (*)(struct platform_device * ))0, (int (*)(struct platform_device * ,
2709                                                                                  pm_message_t state ))0,
2710    (int (*)(struct platform_device * ))0, {"rtc-test", (struct bus_type *)0, & __this_module,
2711                                            (char const   *)0, (_Bool)0, (struct of_device_id  const  *)0,
2712                                            (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
2713                                            (void (*)(struct device *dev ))0, (int (*)(struct device *dev ,
2714                                                                                       pm_message_t state ))0,
2715                                            (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0,
2716                                            (struct dev_pm_ops  const  *)0, (struct driver_private *)0},
2717    (struct platform_device_id  const  *)0};
2718#line 142
2719static int test_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
2720#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2721static int test_init(void) 
2722{ int err ;
2723  void *__cil_tmp2 ;
2724  unsigned long __cil_tmp3 ;
2725  unsigned long __cil_tmp4 ;
2726  void *__cil_tmp5 ;
2727  unsigned long __cil_tmp6 ;
2728  unsigned long __cil_tmp7 ;
2729
2730  {
2731  {
2732#line 146
2733  err = platform_driver_register(& test_driver);
2734  }
2735#line 146
2736  if (err) {
2737#line 147
2738    return (err);
2739  } else {
2740
2741  }
2742  {
2743#line 149
2744  test0 = platform_device_alloc("rtc-test", 0);
2745  }
2746  {
2747#line 149
2748  __cil_tmp2 = (void *)0;
2749#line 149
2750  __cil_tmp3 = (unsigned long )__cil_tmp2;
2751#line 149
2752  __cil_tmp4 = (unsigned long )test0;
2753#line 149
2754  if (__cil_tmp4 == __cil_tmp3) {
2755#line 150
2756    err = -12;
2757#line 151
2758    goto exit_driver_unregister;
2759  } else {
2760
2761  }
2762  }
2763  {
2764#line 154
2765  test1 = platform_device_alloc("rtc-test", 1);
2766  }
2767  {
2768#line 154
2769  __cil_tmp5 = (void *)0;
2770#line 154
2771  __cil_tmp6 = (unsigned long )__cil_tmp5;
2772#line 154
2773  __cil_tmp7 = (unsigned long )test1;
2774#line 154
2775  if (__cil_tmp7 == __cil_tmp6) {
2776#line 155
2777    err = -12;
2778#line 156
2779    goto exit_free_test0;
2780  } else {
2781
2782  }
2783  }
2784  {
2785#line 159
2786  err = platform_device_add(test0);
2787  }
2788#line 159
2789  if (err) {
2790#line 160
2791    goto exit_free_test1;
2792  } else {
2793
2794  }
2795  {
2796#line 162
2797  err = platform_device_add(test1);
2798  }
2799#line 162
2800  if (err) {
2801#line 163
2802    goto exit_device_unregister;
2803  } else {
2804
2805  }
2806#line 165
2807  return (0);
2808  exit_device_unregister: 
2809  {
2810#line 168
2811  platform_device_unregister(test0);
2812  }
2813  exit_free_test1: 
2814  {
2815#line 171
2816  platform_device_put(test1);
2817  }
2818  exit_free_test0: 
2819  {
2820#line 174
2821  platform_device_put(test0);
2822  }
2823  exit_driver_unregister: 
2824  {
2825#line 177
2826  platform_driver_unregister(& test_driver);
2827  }
2828#line 178
2829  return (err);
2830}
2831}
2832#line 181
2833static void test_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
2834#line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2835static void test_exit(void) 
2836{ 
2837
2838  {
2839  {
2840#line 183
2841  platform_device_unregister(test0);
2842#line 184
2843  platform_device_unregister(test1);
2844#line 185
2845  platform_driver_unregister(& test_driver);
2846  }
2847#line 186
2848  return;
2849}
2850}
2851#line 188 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2852static char const   __mod_author188[47]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2853__aligned__(1)))  = 
2854#line 188
2855  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
2856        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'A', 
2857        (char const   )'l',      (char const   )'e',      (char const   )'s',      (char const   )'s', 
2858        (char const   )'a',      (char const   )'n',      (char const   )'d',      (char const   )'r', 
2859        (char const   )'o',      (char const   )' ',      (char const   )'Z',      (char const   )'u', 
2860        (char const   )'m',      (char const   )'m',      (char const   )'o',      (char const   )' ', 
2861        (char const   )'<',      (char const   )'a',      (char const   )'.',      (char const   )'z', 
2862        (char const   )'u',      (char const   )'m',      (char const   )'m',      (char const   )'o', 
2863        (char const   )'@',      (char const   )'t',      (char const   )'o',      (char const   )'w', 
2864        (char const   )'e',      (char const   )'r',      (char const   )'t',      (char const   )'e', 
2865        (char const   )'c',      (char const   )'h',      (char const   )'.',      (char const   )'i', 
2866        (char const   )'t',      (char const   )'>',      (char const   )'\000'};
2867#line 189 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2868static char const   __mod_description189[35]  __attribute__((__used__, __unused__,
2869__section__(".modinfo"), __aligned__(1)))  = 
2870#line 189
2871  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
2872        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
2873        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
2874        (char const   )'R',      (char const   )'T',      (char const   )'C',      (char const   )' ', 
2875        (char const   )'t',      (char const   )'e',      (char const   )'s',      (char const   )'t', 
2876        (char const   )' ',      (char const   )'d',      (char const   )'r',      (char const   )'i', 
2877        (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )'/', 
2878        (char const   )'d',      (char const   )'e',      (char const   )'v',      (char const   )'i', 
2879        (char const   )'c',      (char const   )'e',      (char const   )'\000'};
2880#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2881static char const   __mod_license190[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2882__aligned__(1)))  = 
2883#line 190
2884  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
2885        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
2886        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
2887#line 192 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2888int init_module(void) 
2889{ int tmp ;
2890
2891  {
2892  {
2893#line 192
2894  tmp = test_init();
2895  }
2896#line 192
2897  return (tmp);
2898}
2899}
2900#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2901void cleanup_module(void) 
2902{ 
2903
2904  {
2905  {
2906#line 193
2907  test_exit();
2908  }
2909#line 193
2910  return;
2911}
2912}
2913#line 211
2914void ldv_check_final_state(void) ;
2915#line 214
2916extern void ldv_check_return_value(int res ) ;
2917#line 217
2918extern void ldv_initialize(void) ;
2919#line 220
2920extern int __VERIFIER_nondet_int(void) ;
2921#line 223 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2922int LDV_IN_INTERRUPT  ;
2923#line 264 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2924static int res_test_probe_8  ;
2925#line 226 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
2926void main(void) 
2927{ struct device *var_group1 ;
2928  struct seq_file *var_group2 ;
2929  struct rtc_time *var_group3 ;
2930  struct rtc_wkalrm *var_group4 ;
2931  unsigned long var_test_rtc_set_mmss_3_p1 ;
2932  unsigned int var_test_rtc_alarm_irq_enable_5_p1 ;
2933  struct platform_device *var_group5 ;
2934  int tmp ;
2935  int ldv_s_test_driver_platform_driver ;
2936  int tmp___0 ;
2937  int tmp___1 ;
2938  int __cil_tmp12 ;
2939
2940  {
2941  {
2942#line 272
2943  LDV_IN_INTERRUPT = 1;
2944#line 281
2945  ldv_initialize();
2946#line 287
2947  tmp = test_init();
2948  }
2949#line 287
2950  if (tmp) {
2951#line 288
2952    goto ldv_final;
2953  } else {
2954
2955  }
2956#line 291
2957  ldv_s_test_driver_platform_driver = 0;
2958  {
2959#line 294
2960  while (1) {
2961    while_continue: /* CIL Label */ ;
2962    {
2963#line 294
2964    tmp___1 = __VERIFIER_nondet_int();
2965    }
2966#line 294
2967    if (tmp___1) {
2968
2969    } else {
2970      {
2971#line 294
2972      __cil_tmp12 = ldv_s_test_driver_platform_driver == 0;
2973#line 294
2974      if (! __cil_tmp12) {
2975
2976      } else {
2977#line 294
2978        goto while_break;
2979      }
2980      }
2981    }
2982    {
2983#line 298
2984    tmp___0 = __VERIFIER_nondet_int();
2985    }
2986#line 300
2987    if (tmp___0 == 0) {
2988#line 300
2989      goto case_0;
2990    } else
2991#line 316
2992    if (tmp___0 == 1) {
2993#line 316
2994      goto case_1;
2995    } else
2996#line 332
2997    if (tmp___0 == 2) {
2998#line 332
2999      goto case_2;
3000    } else
3001#line 348
3002    if (tmp___0 == 3) {
3003#line 348
3004      goto case_3;
3005    } else
3006#line 364
3007    if (tmp___0 == 4) {
3008#line 364
3009      goto case_4;
3010    } else
3011#line 380
3012    if (tmp___0 == 5) {
3013#line 380
3014      goto case_5;
3015    } else
3016#line 396
3017    if (tmp___0 == 6) {
3018#line 396
3019      goto case_6;
3020    } else {
3021      {
3022#line 415
3023      goto switch_default;
3024#line 298
3025      if (0) {
3026        case_0: /* CIL Label */ 
3027        {
3028#line 308
3029        test_rtc_proc(var_group1, var_group2);
3030        }
3031#line 315
3032        goto switch_break;
3033        case_1: /* CIL Label */ 
3034        {
3035#line 324
3036        test_rtc_read_time(var_group1, var_group3);
3037        }
3038#line 331
3039        goto switch_break;
3040        case_2: /* CIL Label */ 
3041        {
3042#line 340
3043        test_rtc_read_alarm(var_group1, var_group4);
3044        }
3045#line 347
3046        goto switch_break;
3047        case_3: /* CIL Label */ 
3048        {
3049#line 356
3050        test_rtc_set_alarm(var_group1, var_group4);
3051        }
3052#line 363
3053        goto switch_break;
3054        case_4: /* CIL Label */ 
3055        {
3056#line 372
3057        test_rtc_set_mmss(var_group1, var_test_rtc_set_mmss_3_p1);
3058        }
3059#line 379
3060        goto switch_break;
3061        case_5: /* CIL Label */ 
3062        {
3063#line 388
3064        test_rtc_alarm_irq_enable(var_group1, var_test_rtc_alarm_irq_enable_5_p1);
3065        }
3066#line 395
3067        goto switch_break;
3068        case_6: /* CIL Label */ 
3069#line 399
3070        if (ldv_s_test_driver_platform_driver == 0) {
3071          {
3072#line 404
3073          res_test_probe_8 = test_probe(var_group5);
3074#line 405
3075          ldv_check_return_value(res_test_probe_8);
3076          }
3077#line 406
3078          if (res_test_probe_8) {
3079#line 407
3080            goto ldv_module_exit;
3081          } else {
3082
3083          }
3084#line 408
3085          ldv_s_test_driver_platform_driver = 0;
3086        } else {
3087
3088        }
3089#line 414
3090        goto switch_break;
3091        switch_default: /* CIL Label */ 
3092#line 415
3093        goto switch_break;
3094      } else {
3095        switch_break: /* CIL Label */ ;
3096      }
3097      }
3098    }
3099  }
3100  while_break: /* CIL Label */ ;
3101  }
3102  ldv_module_exit: 
3103  {
3104#line 427
3105  test_exit();
3106  }
3107  ldv_final: 
3108  {
3109#line 430
3110  ldv_check_final_state();
3111  }
3112#line 433
3113  return;
3114}
3115}
3116#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3117void ldv_blast_assert(void) 
3118{ 
3119
3120  {
3121  ERROR: 
3122#line 6
3123  goto ERROR;
3124}
3125}
3126#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3127extern int __VERIFIER_nondet_int(void) ;
3128#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3129int ldv_mutex  =    1;
3130#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3131int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
3132{ int nondetermined ;
3133
3134  {
3135#line 29
3136  if (ldv_mutex == 1) {
3137
3138  } else {
3139    {
3140#line 29
3141    ldv_blast_assert();
3142    }
3143  }
3144  {
3145#line 32
3146  nondetermined = __VERIFIER_nondet_int();
3147  }
3148#line 35
3149  if (nondetermined) {
3150#line 38
3151    ldv_mutex = 2;
3152#line 40
3153    return (0);
3154  } else {
3155#line 45
3156    return (-4);
3157  }
3158}
3159}
3160#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3161int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
3162{ int nondetermined ;
3163
3164  {
3165#line 57
3166  if (ldv_mutex == 1) {
3167
3168  } else {
3169    {
3170#line 57
3171    ldv_blast_assert();
3172    }
3173  }
3174  {
3175#line 60
3176  nondetermined = __VERIFIER_nondet_int();
3177  }
3178#line 63
3179  if (nondetermined) {
3180#line 66
3181    ldv_mutex = 2;
3182#line 68
3183    return (0);
3184  } else {
3185#line 73
3186    return (-4);
3187  }
3188}
3189}
3190#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3191int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
3192{ int atomic_value_after_dec ;
3193
3194  {
3195#line 83
3196  if (ldv_mutex == 1) {
3197
3198  } else {
3199    {
3200#line 83
3201    ldv_blast_assert();
3202    }
3203  }
3204  {
3205#line 86
3206  atomic_value_after_dec = __VERIFIER_nondet_int();
3207  }
3208#line 89
3209  if (atomic_value_after_dec == 0) {
3210#line 92
3211    ldv_mutex = 2;
3212#line 94
3213    return (1);
3214  } else {
3215
3216  }
3217#line 98
3218  return (0);
3219}
3220}
3221#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3222void mutex_lock(struct mutex *lock ) 
3223{ 
3224
3225  {
3226#line 108
3227  if (ldv_mutex == 1) {
3228
3229  } else {
3230    {
3231#line 108
3232    ldv_blast_assert();
3233    }
3234  }
3235#line 110
3236  ldv_mutex = 2;
3237#line 111
3238  return;
3239}
3240}
3241#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3242int mutex_trylock(struct mutex *lock ) 
3243{ int nondetermined ;
3244
3245  {
3246#line 121
3247  if (ldv_mutex == 1) {
3248
3249  } else {
3250    {
3251#line 121
3252    ldv_blast_assert();
3253    }
3254  }
3255  {
3256#line 124
3257  nondetermined = __VERIFIER_nondet_int();
3258  }
3259#line 127
3260  if (nondetermined) {
3261#line 130
3262    ldv_mutex = 2;
3263#line 132
3264    return (1);
3265  } else {
3266#line 137
3267    return (0);
3268  }
3269}
3270}
3271#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3272void mutex_unlock(struct mutex *lock ) 
3273{ 
3274
3275  {
3276#line 147
3277  if (ldv_mutex == 2) {
3278
3279  } else {
3280    {
3281#line 147
3282    ldv_blast_assert();
3283    }
3284  }
3285#line 149
3286  ldv_mutex = 1;
3287#line 150
3288  return;
3289}
3290}
3291#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3292void ldv_check_final_state(void) 
3293{ 
3294
3295  {
3296#line 156
3297  if (ldv_mutex == 1) {
3298
3299  } else {
3300    {
3301#line 156
3302    ldv_blast_assert();
3303    }
3304  }
3305#line 157
3306  return;
3307}
3308}
3309#line 442 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6262/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-test.c.common.c"
3310long s__builtin_expect(long val , long res ) 
3311{ 
3312
3313  {
3314#line 443
3315  return (val);
3316}
3317}