Showing error 619

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