Showing error 496

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