Showing error 838

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