Showing error 870

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