Showing error 606

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-pcf2123.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 6593
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 19 "include/asm-generic/int-ll64.h"
   5typedef signed char __s8;
   6#line 22 "include/asm-generic/int-ll64.h"
   7typedef short __s16;
   8#line 23 "include/asm-generic/int-ll64.h"
   9typedef unsigned short __u16;
  10#line 25 "include/asm-generic/int-ll64.h"
  11typedef int __s32;
  12#line 26 "include/asm-generic/int-ll64.h"
  13typedef unsigned int __u32;
  14#line 29 "include/asm-generic/int-ll64.h"
  15typedef long long __s64;
  16#line 30 "include/asm-generic/int-ll64.h"
  17typedef unsigned long long __u64;
  18#line 43 "include/asm-generic/int-ll64.h"
  19typedef unsigned char u8;
  20#line 45 "include/asm-generic/int-ll64.h"
  21typedef short s16;
  22#line 46 "include/asm-generic/int-ll64.h"
  23typedef unsigned short u16;
  24#line 48 "include/asm-generic/int-ll64.h"
  25typedef int s32;
  26#line 49 "include/asm-generic/int-ll64.h"
  27typedef unsigned int u32;
  28#line 51 "include/asm-generic/int-ll64.h"
  29typedef long long s64;
  30#line 52 "include/asm-generic/int-ll64.h"
  31typedef unsigned long long u64;
  32#line 14 "include/asm-generic/posix_types.h"
  33typedef long __kernel_long_t;
  34#line 15 "include/asm-generic/posix_types.h"
  35typedef unsigned long __kernel_ulong_t;
  36#line 31 "include/asm-generic/posix_types.h"
  37typedef int __kernel_pid_t;
  38#line 52 "include/asm-generic/posix_types.h"
  39typedef unsigned int __kernel_uid32_t;
  40#line 53 "include/asm-generic/posix_types.h"
  41typedef unsigned int __kernel_gid32_t;
  42#line 75 "include/asm-generic/posix_types.h"
  43typedef __kernel_ulong_t __kernel_size_t;
  44#line 76 "include/asm-generic/posix_types.h"
  45typedef __kernel_long_t __kernel_ssize_t;
  46#line 91 "include/asm-generic/posix_types.h"
  47typedef long long __kernel_loff_t;
  48#line 92 "include/asm-generic/posix_types.h"
  49typedef __kernel_long_t __kernel_time_t;
  50#line 93 "include/asm-generic/posix_types.h"
  51typedef __kernel_long_t __kernel_clock_t;
  52#line 94 "include/asm-generic/posix_types.h"
  53typedef int __kernel_timer_t;
  54#line 95 "include/asm-generic/posix_types.h"
  55typedef int __kernel_clockid_t;
  56#line 21 "include/linux/types.h"
  57typedef __u32 __kernel_dev_t;
  58#line 24 "include/linux/types.h"
  59typedef __kernel_dev_t dev_t;
  60#line 27 "include/linux/types.h"
  61typedef unsigned short umode_t;
  62#line 30 "include/linux/types.h"
  63typedef __kernel_pid_t pid_t;
  64#line 35 "include/linux/types.h"
  65typedef __kernel_clockid_t clockid_t;
  66#line 38 "include/linux/types.h"
  67typedef _Bool bool;
  68#line 40 "include/linux/types.h"
  69typedef __kernel_uid32_t uid_t;
  70#line 41 "include/linux/types.h"
  71typedef __kernel_gid32_t gid_t;
  72#line 54 "include/linux/types.h"
  73typedef __kernel_loff_t loff_t;
  74#line 63 "include/linux/types.h"
  75typedef __kernel_size_t size_t;
  76#line 68 "include/linux/types.h"
  77typedef __kernel_ssize_t ssize_t;
  78#line 78 "include/linux/types.h"
  79typedef __kernel_time_t time_t;
  80#line 111 "include/linux/types.h"
  81typedef __s32 int32_t;
  82#line 117 "include/linux/types.h"
  83typedef __u32 uint32_t;
  84#line 142 "include/linux/types.h"
  85typedef unsigned long sector_t;
  86#line 143 "include/linux/types.h"
  87typedef unsigned long blkcnt_t;
  88#line 155 "include/linux/types.h"
  89typedef u64 dma_addr_t;
  90#line 202 "include/linux/types.h"
  91typedef unsigned int gfp_t;
  92#line 203 "include/linux/types.h"
  93typedef unsigned int fmode_t;
  94#line 219 "include/linux/types.h"
  95struct __anonstruct_atomic_t_7 {
  96   int counter ;
  97};
  98#line 219 "include/linux/types.h"
  99typedef struct __anonstruct_atomic_t_7 atomic_t;
 100#line 224 "include/linux/types.h"
 101struct __anonstruct_atomic64_t_8 {
 102   long counter ;
 103};
 104#line 224 "include/linux/types.h"
 105typedef struct __anonstruct_atomic64_t_8 atomic64_t;
 106#line 229 "include/linux/types.h"
 107struct list_head {
 108   struct list_head *next ;
 109   struct list_head *prev ;
 110};
 111#line 233
 112struct hlist_node;
 113#line 233 "include/linux/types.h"
 114struct hlist_head {
 115   struct hlist_node *first ;
 116};
 117#line 237 "include/linux/types.h"
 118struct hlist_node {
 119   struct hlist_node *next ;
 120   struct hlist_node **pprev ;
 121};
 122#line 253 "include/linux/types.h"
 123struct rcu_head {
 124   struct rcu_head *next ;
 125   void (*func)(struct rcu_head *head ) ;
 126};
 127#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 128struct module;
 129#line 56
 130struct module;
 131#line 146 "include/linux/init.h"
 132typedef void (*ctor_fn_t)(void);
 133#line 9 "include/linux/dynamic_debug.h"
 134struct _ddebug {
 135   char const   *modname ;
 136   char const   *function ;
 137   char const   *filename ;
 138   char const   *format ;
 139   unsigned int lineno : 18 ;
 140   unsigned int flags : 8 ;
 141} __attribute__((__aligned__(8))) ;
 142#line 47
 143struct device;
 144#line 47
 145struct device;
 146#line 135 "include/linux/kernel.h"
 147struct completion;
 148#line 135
 149struct completion;
 150#line 136
 151struct pt_regs;
 152#line 136
 153struct pt_regs;
 154#line 349
 155struct pid;
 156#line 349
 157struct pid;
 158#line 202 "include/linux/ioport.h"
 159struct device;
 160#line 12 "include/linux/lockdep.h"
 161struct task_struct;
 162#line 12
 163struct task_struct;
 164#line 391 "include/linux/lockdep.h"
 165struct lock_class_key {
 166
 167};
 168#line 20 "include/linux/kobject_ns.h"
 169struct sock;
 170#line 20
 171struct sock;
 172#line 21
 173struct kobject;
 174#line 21
 175struct kobject;
 176#line 27
 177enum kobj_ns_type {
 178    KOBJ_NS_TYPE_NONE = 0,
 179    KOBJ_NS_TYPE_NET = 1,
 180    KOBJ_NS_TYPES = 2
 181} ;
 182#line 40 "include/linux/kobject_ns.h"
 183struct kobj_ns_type_operations {
 184   enum kobj_ns_type type ;
 185   void *(*grab_current_ns)(void) ;
 186   void const   *(*netlink_ns)(struct sock *sk ) ;
 187   void const   *(*initial_ns)(void) ;
 188   void (*drop_ns)(void * ) ;
 189};
 190#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 191struct task_struct;
 192#line 8
 193struct mm_struct;
 194#line 8
 195struct mm_struct;
 196#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 197struct pt_regs {
 198   unsigned long r15 ;
 199   unsigned long r14 ;
 200   unsigned long r13 ;
 201   unsigned long r12 ;
 202   unsigned long bp ;
 203   unsigned long bx ;
 204   unsigned long r11 ;
 205   unsigned long r10 ;
 206   unsigned long r9 ;
 207   unsigned long r8 ;
 208   unsigned long ax ;
 209   unsigned long cx ;
 210   unsigned long dx ;
 211   unsigned long si ;
 212   unsigned long di ;
 213   unsigned long orig_ax ;
 214   unsigned long ip ;
 215   unsigned long cs ;
 216   unsigned long flags ;
 217   unsigned long sp ;
 218   unsigned long ss ;
 219};
 220#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 221struct __anonstruct____missing_field_name_11 {
 222   unsigned int a ;
 223   unsigned int b ;
 224};
 225#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 226struct __anonstruct____missing_field_name_12 {
 227   u16 limit0 ;
 228   u16 base0 ;
 229   unsigned int base1 : 8 ;
 230   unsigned int type : 4 ;
 231   unsigned int s : 1 ;
 232   unsigned int dpl : 2 ;
 233   unsigned int p : 1 ;
 234   unsigned int limit : 4 ;
 235   unsigned int avl : 1 ;
 236   unsigned int l : 1 ;
 237   unsigned int d : 1 ;
 238   unsigned int g : 1 ;
 239   unsigned int base2 : 8 ;
 240};
 241#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 242union __anonunion____missing_field_name_10 {
 243   struct __anonstruct____missing_field_name_11 __annonCompField4 ;
 244   struct __anonstruct____missing_field_name_12 __annonCompField5 ;
 245};
 246#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 247struct desc_struct {
 248   union __anonunion____missing_field_name_10 __annonCompField6 ;
 249} __attribute__((__packed__)) ;
 250#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 251typedef unsigned long pgdval_t;
 252#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 253typedef unsigned long pgprotval_t;
 254#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 255struct pgprot {
 256   pgprotval_t pgprot ;
 257};
 258#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 259typedef struct pgprot pgprot_t;
 260#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 261struct __anonstruct_pgd_t_16 {
 262   pgdval_t pgd ;
 263};
 264#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 265typedef struct __anonstruct_pgd_t_16 pgd_t;
 266#line 282
 267struct page;
 268#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 269typedef struct page *pgtable_t;
 270#line 295
 271struct file;
 272#line 295
 273struct file;
 274#line 313
 275struct seq_file;
 276#line 313
 277struct seq_file;
 278#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 279struct page;
 280#line 47
 281struct thread_struct;
 282#line 47
 283struct thread_struct;
 284#line 50
 285struct mm_struct;
 286#line 51
 287struct desc_struct;
 288#line 52
 289struct task_struct;
 290#line 53
 291struct cpumask;
 292#line 53
 293struct cpumask;
 294#line 329
 295struct arch_spinlock;
 296#line 329
 297struct arch_spinlock;
 298#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 299struct task_struct;
 300#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 301struct kernel_vm86_regs {
 302   struct pt_regs pt ;
 303   unsigned short es ;
 304   unsigned short __esh ;
 305   unsigned short ds ;
 306   unsigned short __dsh ;
 307   unsigned short fs ;
 308   unsigned short __fsh ;
 309   unsigned short gs ;
 310   unsigned short __gsh ;
 311};
 312#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 313union __anonunion____missing_field_name_20 {
 314   struct pt_regs *regs ;
 315   struct kernel_vm86_regs *vm86 ;
 316};
 317#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 318struct math_emu_info {
 319   long ___orig_eip ;
 320   union __anonunion____missing_field_name_20 __annonCompField7 ;
 321};
 322#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 323struct task_struct;
 324#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 325struct page;
 326#line 10 "include/asm-generic/bug.h"
 327struct bug_entry {
 328   int bug_addr_disp ;
 329   int file_disp ;
 330   unsigned short line ;
 331   unsigned short flags ;
 332};
 333#line 12 "include/linux/bug.h"
 334struct pt_regs;
 335#line 14 "include/linux/cpumask.h"
 336struct cpumask {
 337   unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 338};
 339#line 14 "include/linux/cpumask.h"
 340typedef struct cpumask cpumask_t;
 341#line 637 "include/linux/cpumask.h"
 342typedef struct cpumask *cpumask_var_t;
 343#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 344struct static_key;
 345#line 234
 346struct static_key;
 347#line 11 "include/linux/personality.h"
 348struct pt_regs;
 349#line 153 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 350struct seq_operations;
 351#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 352struct i387_fsave_struct {
 353   u32 cwd ;
 354   u32 swd ;
 355   u32 twd ;
 356   u32 fip ;
 357   u32 fcs ;
 358   u32 foo ;
 359   u32 fos ;
 360   u32 st_space[20] ;
 361   u32 status ;
 362};
 363#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 364struct __anonstruct____missing_field_name_27 {
 365   u64 rip ;
 366   u64 rdp ;
 367};
 368#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 369struct __anonstruct____missing_field_name_28 {
 370   u32 fip ;
 371   u32 fcs ;
 372   u32 foo ;
 373   u32 fos ;
 374};
 375#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 376union __anonunion____missing_field_name_26 {
 377   struct __anonstruct____missing_field_name_27 __annonCompField11 ;
 378   struct __anonstruct____missing_field_name_28 __annonCompField12 ;
 379};
 380#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 381union __anonunion____missing_field_name_29 {
 382   u32 padding1[12] ;
 383   u32 sw_reserved[12] ;
 384};
 385#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 386struct i387_fxsave_struct {
 387   u16 cwd ;
 388   u16 swd ;
 389   u16 twd ;
 390   u16 fop ;
 391   union __anonunion____missing_field_name_26 __annonCompField13 ;
 392   u32 mxcsr ;
 393   u32 mxcsr_mask ;
 394   u32 st_space[32] ;
 395   u32 xmm_space[64] ;
 396   u32 padding[12] ;
 397   union __anonunion____missing_field_name_29 __annonCompField14 ;
 398} __attribute__((__aligned__(16))) ;
 399#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 400struct i387_soft_struct {
 401   u32 cwd ;
 402   u32 swd ;
 403   u32 twd ;
 404   u32 fip ;
 405   u32 fcs ;
 406   u32 foo ;
 407   u32 fos ;
 408   u32 st_space[20] ;
 409   u8 ftop ;
 410   u8 changed ;
 411   u8 lookahead ;
 412   u8 no_update ;
 413   u8 rm ;
 414   u8 alimit ;
 415   struct math_emu_info *info ;
 416   u32 entry_eip ;
 417};
 418#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 419struct ymmh_struct {
 420   u32 ymmh_space[64] ;
 421};
 422#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 423struct xsave_hdr_struct {
 424   u64 xstate_bv ;
 425   u64 reserved1[2] ;
 426   u64 reserved2[5] ;
 427} __attribute__((__packed__)) ;
 428#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 429struct xsave_struct {
 430   struct i387_fxsave_struct i387 ;
 431   struct xsave_hdr_struct xsave_hdr ;
 432   struct ymmh_struct ymmh ;
 433} __attribute__((__packed__, __aligned__(64))) ;
 434#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 435union thread_xstate {
 436   struct i387_fsave_struct fsave ;
 437   struct i387_fxsave_struct fxsave ;
 438   struct i387_soft_struct soft ;
 439   struct xsave_struct xsave ;
 440};
 441#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 442struct fpu {
 443   unsigned int last_cpu ;
 444   unsigned int has_fpu ;
 445   union thread_xstate *state ;
 446};
 447#line 433
 448struct kmem_cache;
 449#line 435
 450struct perf_event;
 451#line 435
 452struct perf_event;
 453#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 454struct thread_struct {
 455   struct desc_struct tls_array[3] ;
 456   unsigned long sp0 ;
 457   unsigned long sp ;
 458   unsigned long usersp ;
 459   unsigned short es ;
 460   unsigned short ds ;
 461   unsigned short fsindex ;
 462   unsigned short gsindex ;
 463   unsigned long fs ;
 464   unsigned long gs ;
 465   struct perf_event *ptrace_bps[4] ;
 466   unsigned long debugreg6 ;
 467   unsigned long ptrace_dr7 ;
 468   unsigned long cr2 ;
 469   unsigned long trap_nr ;
 470   unsigned long error_code ;
 471   struct fpu fpu ;
 472   unsigned long *io_bitmap_ptr ;
 473   unsigned long iopl ;
 474   unsigned int io_bitmap_max ;
 475};
 476#line 23 "include/asm-generic/atomic-long.h"
 477typedef atomic64_t atomic_long_t;
 478#line 22 "include/linux/sysfs.h"
 479struct kobject;
 480#line 23
 481struct module;
 482#line 24
 483enum kobj_ns_type;
 484#line 26 "include/linux/sysfs.h"
 485struct attribute {
 486   char const   *name ;
 487   umode_t mode ;
 488};
 489#line 56 "include/linux/sysfs.h"
 490struct attribute_group {
 491   char const   *name ;
 492   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 493   struct attribute **attrs ;
 494};
 495#line 85
 496struct file;
 497#line 86
 498struct vm_area_struct;
 499#line 86
 500struct vm_area_struct;
 501#line 88 "include/linux/sysfs.h"
 502struct bin_attribute {
 503   struct attribute attr ;
 504   size_t size ;
 505   void *private ;
 506   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 507                   loff_t  , size_t  ) ;
 508   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 509                    loff_t  , size_t  ) ;
 510   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 511};
 512#line 112 "include/linux/sysfs.h"
 513struct sysfs_ops {
 514   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 515   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 516   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 517};
 518#line 118
 519struct sysfs_dirent;
 520#line 118
 521struct sysfs_dirent;
 522#line 12 "include/linux/thread_info.h"
 523struct timespec;
 524#line 12
 525struct timespec;
 526#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 527struct task_struct;
 528#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 529typedef u16 __ticket_t;
 530#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 531typedef u32 __ticketpair_t;
 532#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 533struct __raw_tickets {
 534   __ticket_t head ;
 535   __ticket_t tail ;
 536};
 537#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 538union __anonunion____missing_field_name_36 {
 539   __ticketpair_t head_tail ;
 540   struct __raw_tickets tickets ;
 541};
 542#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 543struct arch_spinlock {
 544   union __anonunion____missing_field_name_36 __annonCompField17 ;
 545};
 546#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 547typedef struct arch_spinlock arch_spinlock_t;
 548#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 549struct __anonstruct____missing_field_name_38 {
 550   u32 read ;
 551   s32 write ;
 552};
 553#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 554union __anonunion_arch_rwlock_t_37 {
 555   s64 lock ;
 556   struct __anonstruct____missing_field_name_38 __annonCompField18 ;
 557};
 558#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 559typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
 560#line 20 "include/linux/spinlock_types.h"
 561struct raw_spinlock {
 562   arch_spinlock_t raw_lock ;
 563   unsigned int magic ;
 564   unsigned int owner_cpu ;
 565   void *owner ;
 566};
 567#line 20 "include/linux/spinlock_types.h"
 568typedef struct raw_spinlock raw_spinlock_t;
 569#line 64 "include/linux/spinlock_types.h"
 570union __anonunion____missing_field_name_39 {
 571   struct raw_spinlock rlock ;
 572};
 573#line 64 "include/linux/spinlock_types.h"
 574struct spinlock {
 575   union __anonunion____missing_field_name_39 __annonCompField19 ;
 576};
 577#line 64 "include/linux/spinlock_types.h"
 578typedef struct spinlock spinlock_t;
 579#line 11 "include/linux/rwlock_types.h"
 580struct __anonstruct_rwlock_t_40 {
 581   arch_rwlock_t raw_lock ;
 582   unsigned int magic ;
 583   unsigned int owner_cpu ;
 584   void *owner ;
 585};
 586#line 11 "include/linux/rwlock_types.h"
 587typedef struct __anonstruct_rwlock_t_40 rwlock_t;
 588#line 22 "include/linux/kref.h"
 589struct kref {
 590   atomic_t refcount ;
 591};
 592#line 49 "include/linux/wait.h"
 593struct __wait_queue_head {
 594   spinlock_t lock ;
 595   struct list_head task_list ;
 596};
 597#line 53 "include/linux/wait.h"
 598typedef struct __wait_queue_head wait_queue_head_t;
 599#line 55
 600struct task_struct;
 601#line 60 "include/linux/kobject.h"
 602struct kset;
 603#line 60
 604struct kobj_type;
 605#line 60 "include/linux/kobject.h"
 606struct kobject {
 607   char const   *name ;
 608   struct list_head entry ;
 609   struct kobject *parent ;
 610   struct kset *kset ;
 611   struct kobj_type *ktype ;
 612   struct sysfs_dirent *sd ;
 613   struct kref kref ;
 614   unsigned int state_initialized : 1 ;
 615   unsigned int state_in_sysfs : 1 ;
 616   unsigned int state_add_uevent_sent : 1 ;
 617   unsigned int state_remove_uevent_sent : 1 ;
 618   unsigned int uevent_suppress : 1 ;
 619};
 620#line 108 "include/linux/kobject.h"
 621struct kobj_type {
 622   void (*release)(struct kobject *kobj ) ;
 623   struct sysfs_ops  const  *sysfs_ops ;
 624   struct attribute **default_attrs ;
 625   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 626   void const   *(*namespace)(struct kobject *kobj ) ;
 627};
 628#line 116 "include/linux/kobject.h"
 629struct kobj_uevent_env {
 630   char *envp[32] ;
 631   int envp_idx ;
 632   char buf[2048] ;
 633   int buflen ;
 634};
 635#line 123 "include/linux/kobject.h"
 636struct kset_uevent_ops {
 637   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 638   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 639   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 640};
 641#line 140
 642struct sock;
 643#line 159 "include/linux/kobject.h"
 644struct kset {
 645   struct list_head list ;
 646   spinlock_t list_lock ;
 647   struct kobject kobj ;
 648   struct kset_uevent_ops  const  *uevent_ops ;
 649};
 650#line 19 "include/linux/klist.h"
 651struct klist_node;
 652#line 19
 653struct klist_node;
 654#line 39 "include/linux/klist.h"
 655struct klist_node {
 656   void *n_klist ;
 657   struct list_head n_node ;
 658   struct kref n_ref ;
 659};
 660#line 48 "include/linux/mutex.h"
 661struct mutex {
 662   atomic_t count ;
 663   spinlock_t wait_lock ;
 664   struct list_head wait_list ;
 665   struct task_struct *owner ;
 666   char const   *name ;
 667   void *magic ;
 668};
 669#line 69 "include/linux/mutex.h"
 670struct mutex_waiter {
 671   struct list_head list ;
 672   struct task_struct *task ;
 673   void *magic ;
 674};
 675#line 119 "include/linux/seqlock.h"
 676struct seqcount {
 677   unsigned int sequence ;
 678};
 679#line 119 "include/linux/seqlock.h"
 680typedef struct seqcount seqcount_t;
 681#line 14 "include/linux/time.h"
 682struct timespec {
 683   __kernel_time_t tv_sec ;
 684   long tv_nsec ;
 685};
 686#line 46 "include/linux/ktime.h"
 687union ktime {
 688   s64 tv64 ;
 689};
 690#line 59 "include/linux/ktime.h"
 691typedef union ktime ktime_t;
 692#line 10 "include/linux/timer.h"
 693struct tvec_base;
 694#line 10
 695struct tvec_base;
 696#line 12 "include/linux/timer.h"
 697struct timer_list {
 698   struct list_head entry ;
 699   unsigned long expires ;
 700   struct tvec_base *base ;
 701   void (*function)(unsigned long  ) ;
 702   unsigned long data ;
 703   int slack ;
 704   int start_pid ;
 705   void *start_site ;
 706   char start_comm[16] ;
 707};
 708#line 289
 709struct hrtimer;
 710#line 289
 711struct hrtimer;
 712#line 290
 713enum hrtimer_restart;
 714#line 17 "include/linux/workqueue.h"
 715struct work_struct;
 716#line 17
 717struct work_struct;
 718#line 79 "include/linux/workqueue.h"
 719struct work_struct {
 720   atomic_long_t data ;
 721   struct list_head entry ;
 722   void (*func)(struct work_struct *work ) ;
 723};
 724#line 92 "include/linux/workqueue.h"
 725struct delayed_work {
 726   struct work_struct work ;
 727   struct timer_list timer ;
 728};
 729#line 25 "include/linux/completion.h"
 730struct completion {
 731   unsigned int done ;
 732   wait_queue_head_t wait ;
 733};
 734#line 42 "include/linux/pm.h"
 735struct device;
 736#line 50 "include/linux/pm.h"
 737struct pm_message {
 738   int event ;
 739};
 740#line 50 "include/linux/pm.h"
 741typedef struct pm_message pm_message_t;
 742#line 264 "include/linux/pm.h"
 743struct dev_pm_ops {
 744   int (*prepare)(struct device *dev ) ;
 745   void (*complete)(struct device *dev ) ;
 746   int (*suspend)(struct device *dev ) ;
 747   int (*resume)(struct device *dev ) ;
 748   int (*freeze)(struct device *dev ) ;
 749   int (*thaw)(struct device *dev ) ;
 750   int (*poweroff)(struct device *dev ) ;
 751   int (*restore)(struct device *dev ) ;
 752   int (*suspend_late)(struct device *dev ) ;
 753   int (*resume_early)(struct device *dev ) ;
 754   int (*freeze_late)(struct device *dev ) ;
 755   int (*thaw_early)(struct device *dev ) ;
 756   int (*poweroff_late)(struct device *dev ) ;
 757   int (*restore_early)(struct device *dev ) ;
 758   int (*suspend_noirq)(struct device *dev ) ;
 759   int (*resume_noirq)(struct device *dev ) ;
 760   int (*freeze_noirq)(struct device *dev ) ;
 761   int (*thaw_noirq)(struct device *dev ) ;
 762   int (*poweroff_noirq)(struct device *dev ) ;
 763   int (*restore_noirq)(struct device *dev ) ;
 764   int (*runtime_suspend)(struct device *dev ) ;
 765   int (*runtime_resume)(struct device *dev ) ;
 766   int (*runtime_idle)(struct device *dev ) ;
 767};
 768#line 458
 769enum rpm_status {
 770    RPM_ACTIVE = 0,
 771    RPM_RESUMING = 1,
 772    RPM_SUSPENDED = 2,
 773    RPM_SUSPENDING = 3
 774} ;
 775#line 480
 776enum rpm_request {
 777    RPM_REQ_NONE = 0,
 778    RPM_REQ_IDLE = 1,
 779    RPM_REQ_SUSPEND = 2,
 780    RPM_REQ_AUTOSUSPEND = 3,
 781    RPM_REQ_RESUME = 4
 782} ;
 783#line 488
 784struct wakeup_source;
 785#line 488
 786struct wakeup_source;
 787#line 495 "include/linux/pm.h"
 788struct pm_subsys_data {
 789   spinlock_t lock ;
 790   unsigned int refcount ;
 791};
 792#line 506
 793struct dev_pm_qos_request;
 794#line 506
 795struct pm_qos_constraints;
 796#line 506 "include/linux/pm.h"
 797struct dev_pm_info {
 798   pm_message_t power_state ;
 799   unsigned int can_wakeup : 1 ;
 800   unsigned int async_suspend : 1 ;
 801   bool is_prepared : 1 ;
 802   bool is_suspended : 1 ;
 803   bool ignore_children : 1 ;
 804   spinlock_t lock ;
 805   struct list_head entry ;
 806   struct completion completion ;
 807   struct wakeup_source *wakeup ;
 808   bool wakeup_path : 1 ;
 809   struct timer_list suspend_timer ;
 810   unsigned long timer_expires ;
 811   struct work_struct work ;
 812   wait_queue_head_t wait_queue ;
 813   atomic_t usage_count ;
 814   atomic_t child_count ;
 815   unsigned int disable_depth : 3 ;
 816   unsigned int idle_notification : 1 ;
 817   unsigned int request_pending : 1 ;
 818   unsigned int deferred_resume : 1 ;
 819   unsigned int run_wake : 1 ;
 820   unsigned int runtime_auto : 1 ;
 821   unsigned int no_callbacks : 1 ;
 822   unsigned int irq_safe : 1 ;
 823   unsigned int use_autosuspend : 1 ;
 824   unsigned int timer_autosuspends : 1 ;
 825   enum rpm_request request ;
 826   enum rpm_status runtime_status ;
 827   int runtime_error ;
 828   int autosuspend_delay ;
 829   unsigned long last_busy ;
 830   unsigned long active_jiffies ;
 831   unsigned long suspended_jiffies ;
 832   unsigned long accounting_timestamp ;
 833   ktime_t suspend_time ;
 834   s64 max_time_suspended_ns ;
 835   struct dev_pm_qos_request *pq_req ;
 836   struct pm_subsys_data *subsys_data ;
 837   struct pm_qos_constraints *constraints ;
 838};
 839#line 564 "include/linux/pm.h"
 840struct dev_pm_domain {
 841   struct dev_pm_ops ops ;
 842};
 843#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 844struct dma_map_ops;
 845#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 846struct dev_archdata {
 847   void *acpi_handle ;
 848   struct dma_map_ops *dma_ops ;
 849   void *iommu ;
 850};
 851#line 28 "include/linux/device.h"
 852struct device;
 853#line 29
 854struct device_private;
 855#line 29
 856struct device_private;
 857#line 30
 858struct device_driver;
 859#line 30
 860struct device_driver;
 861#line 31
 862struct driver_private;
 863#line 31
 864struct driver_private;
 865#line 32
 866struct module;
 867#line 33
 868struct class;
 869#line 33
 870struct class;
 871#line 34
 872struct subsys_private;
 873#line 34
 874struct subsys_private;
 875#line 35
 876struct bus_type;
 877#line 35
 878struct bus_type;
 879#line 36
 880struct device_node;
 881#line 36
 882struct device_node;
 883#line 37
 884struct iommu_ops;
 885#line 37
 886struct iommu_ops;
 887#line 39 "include/linux/device.h"
 888struct bus_attribute {
 889   struct attribute attr ;
 890   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
 891   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 892};
 893#line 89
 894struct device_attribute;
 895#line 89
 896struct driver_attribute;
 897#line 89 "include/linux/device.h"
 898struct bus_type {
 899   char const   *name ;
 900   char const   *dev_name ;
 901   struct device *dev_root ;
 902   struct bus_attribute *bus_attrs ;
 903   struct device_attribute *dev_attrs ;
 904   struct driver_attribute *drv_attrs ;
 905   int (*match)(struct device *dev , struct device_driver *drv ) ;
 906   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 907   int (*probe)(struct device *dev ) ;
 908   int (*remove)(struct device *dev ) ;
 909   void (*shutdown)(struct device *dev ) ;
 910   int (*suspend)(struct device *dev , pm_message_t state ) ;
 911   int (*resume)(struct device *dev ) ;
 912   struct dev_pm_ops  const  *pm ;
 913   struct iommu_ops *iommu_ops ;
 914   struct subsys_private *p ;
 915};
 916#line 127
 917struct device_type;
 918#line 214
 919struct of_device_id;
 920#line 214 "include/linux/device.h"
 921struct device_driver {
 922   char const   *name ;
 923   struct bus_type *bus ;
 924   struct module *owner ;
 925   char const   *mod_name ;
 926   bool suppress_bind_attrs ;
 927   struct of_device_id  const  *of_match_table ;
 928   int (*probe)(struct device *dev ) ;
 929   int (*remove)(struct device *dev ) ;
 930   void (*shutdown)(struct device *dev ) ;
 931   int (*suspend)(struct device *dev , pm_message_t state ) ;
 932   int (*resume)(struct device *dev ) ;
 933   struct attribute_group  const  **groups ;
 934   struct dev_pm_ops  const  *pm ;
 935   struct driver_private *p ;
 936};
 937#line 249 "include/linux/device.h"
 938struct driver_attribute {
 939   struct attribute attr ;
 940   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
 941   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
 942};
 943#line 330
 944struct class_attribute;
 945#line 330 "include/linux/device.h"
 946struct class {
 947   char const   *name ;
 948   struct module *owner ;
 949   struct class_attribute *class_attrs ;
 950   struct device_attribute *dev_attrs ;
 951   struct bin_attribute *dev_bin_attrs ;
 952   struct kobject *dev_kobj ;
 953   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 954   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 955   void (*class_release)(struct class *class ) ;
 956   void (*dev_release)(struct device *dev ) ;
 957   int (*suspend)(struct device *dev , pm_message_t state ) ;
 958   int (*resume)(struct device *dev ) ;
 959   struct kobj_ns_type_operations  const  *ns_type ;
 960   void const   *(*namespace)(struct device *dev ) ;
 961   struct dev_pm_ops  const  *pm ;
 962   struct subsys_private *p ;
 963};
 964#line 397 "include/linux/device.h"
 965struct class_attribute {
 966   struct attribute attr ;
 967   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
 968   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
 969                    size_t count ) ;
 970   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
 971};
 972#line 465 "include/linux/device.h"
 973struct device_type {
 974   char const   *name ;
 975   struct attribute_group  const  **groups ;
 976   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 977   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 978   void (*release)(struct device *dev ) ;
 979   struct dev_pm_ops  const  *pm ;
 980};
 981#line 476 "include/linux/device.h"
 982struct device_attribute {
 983   struct attribute attr ;
 984   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
 985   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
 986                    size_t count ) ;
 987};
 988#line 559 "include/linux/device.h"
 989struct device_dma_parameters {
 990   unsigned int max_segment_size ;
 991   unsigned long segment_boundary_mask ;
 992};
 993#line 627
 994struct dma_coherent_mem;
 995#line 627 "include/linux/device.h"
 996struct device {
 997   struct device *parent ;
 998   struct device_private *p ;
 999   struct kobject kobj ;
1000   char const   *init_name ;
1001   struct device_type  const  *type ;
1002   struct mutex mutex ;
1003   struct bus_type *bus ;
1004   struct device_driver *driver ;
1005   void *platform_data ;
1006   struct dev_pm_info power ;
1007   struct dev_pm_domain *pm_domain ;
1008   int numa_node ;
1009   u64 *dma_mask ;
1010   u64 coherent_dma_mask ;
1011   struct device_dma_parameters *dma_parms ;
1012   struct list_head dma_pools ;
1013   struct dma_coherent_mem *dma_mem ;
1014   struct dev_archdata archdata ;
1015   struct device_node *of_node ;
1016   dev_t devt ;
1017   u32 id ;
1018   spinlock_t devres_lock ;
1019   struct list_head devres_head ;
1020   struct klist_node knode_class ;
1021   struct class *class ;
1022   struct attribute_group  const  **groups ;
1023   void (*release)(struct device *dev ) ;
1024};
1025#line 43 "include/linux/pm_wakeup.h"
1026struct wakeup_source {
1027   char const   *name ;
1028   struct list_head entry ;
1029   spinlock_t lock ;
1030   struct timer_list timer ;
1031   unsigned long timer_expires ;
1032   ktime_t total_time ;
1033   ktime_t max_time ;
1034   ktime_t last_time ;
1035   unsigned long event_count ;
1036   unsigned long active_count ;
1037   unsigned long relax_count ;
1038   unsigned long hit_count ;
1039   unsigned int active : 1 ;
1040};
1041#line 98 "include/linux/nodemask.h"
1042struct __anonstruct_nodemask_t_44 {
1043   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1044};
1045#line 98 "include/linux/nodemask.h"
1046typedef struct __anonstruct_nodemask_t_44 nodemask_t;
1047#line 60 "include/linux/pageblock-flags.h"
1048struct page;
1049#line 19 "include/linux/rwsem.h"
1050struct rw_semaphore;
1051#line 19
1052struct rw_semaphore;
1053#line 25 "include/linux/rwsem.h"
1054struct rw_semaphore {
1055   long count ;
1056   raw_spinlock_t wait_lock ;
1057   struct list_head wait_list ;
1058};
1059#line 9 "include/linux/memory_hotplug.h"
1060struct page;
1061#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
1062struct device;
1063#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
1064struct __anonstruct_mm_context_t_112 {
1065   void *ldt ;
1066   int size ;
1067   unsigned short ia32_compat ;
1068   struct mutex lock ;
1069   void *vdso ;
1070};
1071#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
1072typedef struct __anonstruct_mm_context_t_112 mm_context_t;
1073#line 8 "include/linux/vmalloc.h"
1074struct vm_area_struct;
1075#line 994 "include/linux/mmzone.h"
1076struct page;
1077#line 10 "include/linux/gfp.h"
1078struct vm_area_struct;
1079#line 46 "include/linux/slub_def.h"
1080struct kmem_cache_cpu {
1081   void **freelist ;
1082   unsigned long tid ;
1083   struct page *page ;
1084   struct page *partial ;
1085   int node ;
1086   unsigned int stat[26] ;
1087};
1088#line 57 "include/linux/slub_def.h"
1089struct kmem_cache_node {
1090   spinlock_t list_lock ;
1091   unsigned long nr_partial ;
1092   struct list_head partial ;
1093   atomic_long_t nr_slabs ;
1094   atomic_long_t total_objects ;
1095   struct list_head full ;
1096};
1097#line 73 "include/linux/slub_def.h"
1098struct kmem_cache_order_objects {
1099   unsigned long x ;
1100};
1101#line 80 "include/linux/slub_def.h"
1102struct kmem_cache {
1103   struct kmem_cache_cpu *cpu_slab ;
1104   unsigned long flags ;
1105   unsigned long min_partial ;
1106   int size ;
1107   int objsize ;
1108   int offset ;
1109   int cpu_partial ;
1110   struct kmem_cache_order_objects oo ;
1111   struct kmem_cache_order_objects max ;
1112   struct kmem_cache_order_objects min ;
1113   gfp_t allocflags ;
1114   int refcount ;
1115   void (*ctor)(void * ) ;
1116   int inuse ;
1117   int align ;
1118   int reserved ;
1119   char const   *name ;
1120   struct list_head list ;
1121   struct kobject kobj ;
1122   int remote_node_defrag_ratio ;
1123   struct kmem_cache_node *node[1 << 10] ;
1124};
1125#line 20 "include/linux/rtc.h"
1126struct rtc_time {
1127   int tm_sec ;
1128   int tm_min ;
1129   int tm_hour ;
1130   int tm_mday ;
1131   int tm_mon ;
1132   int tm_year ;
1133   int tm_wday ;
1134   int tm_yday ;
1135   int tm_isdst ;
1136};
1137#line 36 "include/linux/rtc.h"
1138struct rtc_wkalrm {
1139   unsigned char enabled ;
1140   unsigned char pending ;
1141   struct rtc_time time ;
1142};
1143#line 31 "include/linux/irq.h"
1144struct seq_file;
1145#line 32
1146struct module;
1147#line 14 "include/linux/irqdesc.h"
1148struct module;
1149#line 17 "include/linux/profile.h"
1150struct pt_regs;
1151#line 65
1152struct task_struct;
1153#line 66
1154struct mm_struct;
1155#line 88
1156struct pt_regs;
1157#line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess.h"
1158struct exception_table_entry {
1159   unsigned long insn ;
1160   unsigned long fixup ;
1161};
1162#line 132 "include/linux/hardirq.h"
1163struct task_struct;
1164#line 100 "include/linux/rbtree.h"
1165struct rb_node {
1166   unsigned long rb_parent_color ;
1167   struct rb_node *rb_right ;
1168   struct rb_node *rb_left ;
1169} __attribute__((__aligned__(sizeof(long )))) ;
1170#line 110 "include/linux/rbtree.h"
1171struct rb_root {
1172   struct rb_node *rb_node ;
1173};
1174#line 8 "include/linux/timerqueue.h"
1175struct timerqueue_node {
1176   struct rb_node node ;
1177   ktime_t expires ;
1178};
1179#line 13 "include/linux/timerqueue.h"
1180struct timerqueue_head {
1181   struct rb_root head ;
1182   struct timerqueue_node *next ;
1183};
1184#line 27 "include/linux/hrtimer.h"
1185struct hrtimer_clock_base;
1186#line 27
1187struct hrtimer_clock_base;
1188#line 28
1189struct hrtimer_cpu_base;
1190#line 28
1191struct hrtimer_cpu_base;
1192#line 44
1193enum hrtimer_restart {
1194    HRTIMER_NORESTART = 0,
1195    HRTIMER_RESTART = 1
1196} ;
1197#line 108 "include/linux/hrtimer.h"
1198struct hrtimer {
1199   struct timerqueue_node node ;
1200   ktime_t _softexpires ;
1201   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1202   struct hrtimer_clock_base *base ;
1203   unsigned long state ;
1204   int start_pid ;
1205   void *start_site ;
1206   char start_comm[16] ;
1207};
1208#line 145 "include/linux/hrtimer.h"
1209struct hrtimer_clock_base {
1210   struct hrtimer_cpu_base *cpu_base ;
1211   int index ;
1212   clockid_t clockid ;
1213   struct timerqueue_head active ;
1214   ktime_t resolution ;
1215   ktime_t (*get_time)(void) ;
1216   ktime_t softirq_time ;
1217   ktime_t offset ;
1218};
1219#line 178 "include/linux/hrtimer.h"
1220struct hrtimer_cpu_base {
1221   raw_spinlock_t lock ;
1222   unsigned long active_bases ;
1223   ktime_t expires_next ;
1224   int hres_active ;
1225   int hang_detected ;
1226   unsigned long nr_events ;
1227   unsigned long nr_retries ;
1228   unsigned long nr_hangs ;
1229   ktime_t max_hang_time ;
1230   struct hrtimer_clock_base clock_base[3] ;
1231};
1232#line 187 "include/linux/interrupt.h"
1233struct device;
1234#line 695
1235struct seq_file;
1236#line 11 "include/linux/seq_file.h"
1237struct seq_operations;
1238#line 12
1239struct file;
1240#line 13
1241struct path;
1242#line 13
1243struct path;
1244#line 14
1245struct inode;
1246#line 14
1247struct inode;
1248#line 15
1249struct dentry;
1250#line 15
1251struct dentry;
1252#line 17 "include/linux/seq_file.h"
1253struct seq_file {
1254   char *buf ;
1255   size_t size ;
1256   size_t from ;
1257   size_t count ;
1258   loff_t index ;
1259   loff_t read_pos ;
1260   u64 version ;
1261   struct mutex lock ;
1262   struct seq_operations  const  *op ;
1263   int poll_event ;
1264   void *private ;
1265};
1266#line 31 "include/linux/seq_file.h"
1267struct seq_operations {
1268   void *(*start)(struct seq_file *m , loff_t *pos ) ;
1269   void (*stop)(struct seq_file *m , void *v ) ;
1270   void *(*next)(struct seq_file *m , void *v , loff_t *pos ) ;
1271   int (*show)(struct seq_file *m , void *v ) ;
1272};
1273#line 8 "include/linux/cdev.h"
1274struct file_operations;
1275#line 8
1276struct file_operations;
1277#line 9
1278struct inode;
1279#line 10
1280struct module;
1281#line 12 "include/linux/cdev.h"
1282struct cdev {
1283   struct kobject kobj ;
1284   struct module *owner ;
1285   struct file_operations  const  *ops ;
1286   struct list_head list ;
1287   dev_t dev ;
1288   unsigned int count ;
1289};
1290#line 33
1291struct backing_dev_info;
1292#line 15 "include/linux/blk_types.h"
1293struct page;
1294#line 16
1295struct block_device;
1296#line 16
1297struct block_device;
1298#line 33 "include/linux/list_bl.h"
1299struct hlist_bl_node;
1300#line 33 "include/linux/list_bl.h"
1301struct hlist_bl_head {
1302   struct hlist_bl_node *first ;
1303};
1304#line 37 "include/linux/list_bl.h"
1305struct hlist_bl_node {
1306   struct hlist_bl_node *next ;
1307   struct hlist_bl_node **pprev ;
1308};
1309#line 13 "include/linux/dcache.h"
1310struct nameidata;
1311#line 13
1312struct nameidata;
1313#line 14
1314struct path;
1315#line 15
1316struct vfsmount;
1317#line 15
1318struct vfsmount;
1319#line 35 "include/linux/dcache.h"
1320struct qstr {
1321   unsigned int hash ;
1322   unsigned int len ;
1323   unsigned char const   *name ;
1324};
1325#line 88
1326struct dentry_operations;
1327#line 88
1328struct super_block;
1329#line 88 "include/linux/dcache.h"
1330union __anonunion_d_u_147 {
1331   struct list_head d_child ;
1332   struct rcu_head d_rcu ;
1333};
1334#line 88 "include/linux/dcache.h"
1335struct dentry {
1336   unsigned int d_flags ;
1337   seqcount_t d_seq ;
1338   struct hlist_bl_node d_hash ;
1339   struct dentry *d_parent ;
1340   struct qstr d_name ;
1341   struct inode *d_inode ;
1342   unsigned char d_iname[32] ;
1343   unsigned int d_count ;
1344   spinlock_t d_lock ;
1345   struct dentry_operations  const  *d_op ;
1346   struct super_block *d_sb ;
1347   unsigned long d_time ;
1348   void *d_fsdata ;
1349   struct list_head d_lru ;
1350   union __anonunion_d_u_147 d_u ;
1351   struct list_head d_subdirs ;
1352   struct list_head d_alias ;
1353};
1354#line 131 "include/linux/dcache.h"
1355struct dentry_operations {
1356   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1357   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
1358   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
1359                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
1360   int (*d_delete)(struct dentry  const  * ) ;
1361   void (*d_release)(struct dentry * ) ;
1362   void (*d_prune)(struct dentry * ) ;
1363   void (*d_iput)(struct dentry * , struct inode * ) ;
1364   char *(*d_dname)(struct dentry * , char * , int  ) ;
1365   struct vfsmount *(*d_automount)(struct path * ) ;
1366   int (*d_manage)(struct dentry * , bool  ) ;
1367} __attribute__((__aligned__((1) <<  (6) ))) ;
1368#line 4 "include/linux/path.h"
1369struct dentry;
1370#line 5
1371struct vfsmount;
1372#line 7 "include/linux/path.h"
1373struct path {
1374   struct vfsmount *mnt ;
1375   struct dentry *dentry ;
1376};
1377#line 62 "include/linux/stat.h"
1378struct kstat {
1379   u64 ino ;
1380   dev_t dev ;
1381   umode_t mode ;
1382   unsigned int nlink ;
1383   uid_t uid ;
1384   gid_t gid ;
1385   dev_t rdev ;
1386   loff_t size ;
1387   struct timespec atime ;
1388   struct timespec mtime ;
1389   struct timespec ctime ;
1390   unsigned long blksize ;
1391   unsigned long long blocks ;
1392};
1393#line 64 "include/linux/radix-tree.h"
1394struct radix_tree_node;
1395#line 64 "include/linux/radix-tree.h"
1396struct radix_tree_root {
1397   unsigned int height ;
1398   gfp_t gfp_mask ;
1399   struct radix_tree_node *rnode ;
1400};
1401#line 14 "include/linux/prio_tree.h"
1402struct prio_tree_node;
1403#line 14 "include/linux/prio_tree.h"
1404struct raw_prio_tree_node {
1405   struct prio_tree_node *left ;
1406   struct prio_tree_node *right ;
1407   struct prio_tree_node *parent ;
1408};
1409#line 20 "include/linux/prio_tree.h"
1410struct prio_tree_node {
1411   struct prio_tree_node *left ;
1412   struct prio_tree_node *right ;
1413   struct prio_tree_node *parent ;
1414   unsigned long start ;
1415   unsigned long last ;
1416};
1417#line 28 "include/linux/prio_tree.h"
1418struct prio_tree_root {
1419   struct prio_tree_node *prio_tree_node ;
1420   unsigned short index_bits ;
1421   unsigned short raw ;
1422};
1423#line 6 "include/linux/pid.h"
1424enum pid_type {
1425    PIDTYPE_PID = 0,
1426    PIDTYPE_PGID = 1,
1427    PIDTYPE_SID = 2,
1428    PIDTYPE_MAX = 3
1429} ;
1430#line 50
1431struct pid_namespace;
1432#line 50 "include/linux/pid.h"
1433struct upid {
1434   int nr ;
1435   struct pid_namespace *ns ;
1436   struct hlist_node pid_chain ;
1437};
1438#line 57 "include/linux/pid.h"
1439struct pid {
1440   atomic_t count ;
1441   unsigned int level ;
1442   struct hlist_head tasks[3] ;
1443   struct rcu_head rcu ;
1444   struct upid numbers[1] ;
1445};
1446#line 69 "include/linux/pid.h"
1447struct pid_link {
1448   struct hlist_node node ;
1449   struct pid *pid ;
1450};
1451#line 100
1452struct pid_namespace;
1453#line 18 "include/linux/capability.h"
1454struct task_struct;
1455#line 94 "include/linux/capability.h"
1456struct kernel_cap_struct {
1457   __u32 cap[2] ;
1458};
1459#line 94 "include/linux/capability.h"
1460typedef struct kernel_cap_struct kernel_cap_t;
1461#line 377
1462struct dentry;
1463#line 378
1464struct user_namespace;
1465#line 378
1466struct user_namespace;
1467#line 16 "include/linux/fiemap.h"
1468struct fiemap_extent {
1469   __u64 fe_logical ;
1470   __u64 fe_physical ;
1471   __u64 fe_length ;
1472   __u64 fe_reserved64[2] ;
1473   __u32 fe_flags ;
1474   __u32 fe_reserved[3] ;
1475};
1476#line 8 "include/linux/shrinker.h"
1477struct shrink_control {
1478   gfp_t gfp_mask ;
1479   unsigned long nr_to_scan ;
1480};
1481#line 31 "include/linux/shrinker.h"
1482struct shrinker {
1483   int (*shrink)(struct shrinker * , struct shrink_control *sc ) ;
1484   int seeks ;
1485   long batch ;
1486   struct list_head list ;
1487   atomic_long_t nr_in_batch ;
1488};
1489#line 10 "include/linux/migrate_mode.h"
1490enum migrate_mode {
1491    MIGRATE_ASYNC = 0,
1492    MIGRATE_SYNC_LIGHT = 1,
1493    MIGRATE_SYNC = 2
1494} ;
1495#line 408 "include/linux/fs.h"
1496struct export_operations;
1497#line 408
1498struct export_operations;
1499#line 410
1500struct iovec;
1501#line 410
1502struct iovec;
1503#line 411
1504struct nameidata;
1505#line 412
1506struct kiocb;
1507#line 412
1508struct kiocb;
1509#line 413
1510struct kobject;
1511#line 414
1512struct pipe_inode_info;
1513#line 414
1514struct pipe_inode_info;
1515#line 415
1516struct poll_table_struct;
1517#line 415
1518struct poll_table_struct;
1519#line 416
1520struct kstatfs;
1521#line 416
1522struct kstatfs;
1523#line 417
1524struct vm_area_struct;
1525#line 418
1526struct vfsmount;
1527#line 419
1528struct cred;
1529#line 419
1530struct cred;
1531#line 469 "include/linux/fs.h"
1532struct iattr {
1533   unsigned int ia_valid ;
1534   umode_t ia_mode ;
1535   uid_t ia_uid ;
1536   gid_t ia_gid ;
1537   loff_t ia_size ;
1538   struct timespec ia_atime ;
1539   struct timespec ia_mtime ;
1540   struct timespec ia_ctime ;
1541   struct file *ia_file ;
1542};
1543#line 129 "include/linux/quota.h"
1544struct if_dqinfo {
1545   __u64 dqi_bgrace ;
1546   __u64 dqi_igrace ;
1547   __u32 dqi_flags ;
1548   __u32 dqi_valid ;
1549};
1550#line 50 "include/linux/dqblk_xfs.h"
1551struct fs_disk_quota {
1552   __s8 d_version ;
1553   __s8 d_flags ;
1554   __u16 d_fieldmask ;
1555   __u32 d_id ;
1556   __u64 d_blk_hardlimit ;
1557   __u64 d_blk_softlimit ;
1558   __u64 d_ino_hardlimit ;
1559   __u64 d_ino_softlimit ;
1560   __u64 d_bcount ;
1561   __u64 d_icount ;
1562   __s32 d_itimer ;
1563   __s32 d_btimer ;
1564   __u16 d_iwarns ;
1565   __u16 d_bwarns ;
1566   __s32 d_padding2 ;
1567   __u64 d_rtb_hardlimit ;
1568   __u64 d_rtb_softlimit ;
1569   __u64 d_rtbcount ;
1570   __s32 d_rtbtimer ;
1571   __u16 d_rtbwarns ;
1572   __s16 d_padding3 ;
1573   char d_padding4[8] ;
1574};
1575#line 146 "include/linux/dqblk_xfs.h"
1576struct fs_qfilestat {
1577   __u64 qfs_ino ;
1578   __u64 qfs_nblks ;
1579   __u32 qfs_nextents ;
1580};
1581#line 146 "include/linux/dqblk_xfs.h"
1582typedef struct fs_qfilestat fs_qfilestat_t;
1583#line 152 "include/linux/dqblk_xfs.h"
1584struct fs_quota_stat {
1585   __s8 qs_version ;
1586   __u16 qs_flags ;
1587   __s8 qs_pad ;
1588   fs_qfilestat_t qs_uquota ;
1589   fs_qfilestat_t qs_gquota ;
1590   __u32 qs_incoredqs ;
1591   __s32 qs_btimelimit ;
1592   __s32 qs_itimelimit ;
1593   __s32 qs_rtbtimelimit ;
1594   __u16 qs_bwarnlimit ;
1595   __u16 qs_iwarnlimit ;
1596};
1597#line 17 "include/linux/dqblk_qtree.h"
1598struct dquot;
1599#line 17
1600struct dquot;
1601#line 185 "include/linux/quota.h"
1602typedef __kernel_uid32_t qid_t;
1603#line 186 "include/linux/quota.h"
1604typedef long long qsize_t;
1605#line 200 "include/linux/quota.h"
1606struct mem_dqblk {
1607   qsize_t dqb_bhardlimit ;
1608   qsize_t dqb_bsoftlimit ;
1609   qsize_t dqb_curspace ;
1610   qsize_t dqb_rsvspace ;
1611   qsize_t dqb_ihardlimit ;
1612   qsize_t dqb_isoftlimit ;
1613   qsize_t dqb_curinodes ;
1614   time_t dqb_btime ;
1615   time_t dqb_itime ;
1616};
1617#line 215
1618struct quota_format_type;
1619#line 215
1620struct quota_format_type;
1621#line 217 "include/linux/quota.h"
1622struct mem_dqinfo {
1623   struct quota_format_type *dqi_format ;
1624   int dqi_fmt_id ;
1625   struct list_head dqi_dirty_list ;
1626   unsigned long dqi_flags ;
1627   unsigned int dqi_bgrace ;
1628   unsigned int dqi_igrace ;
1629   qsize_t dqi_maxblimit ;
1630   qsize_t dqi_maxilimit ;
1631   void *dqi_priv ;
1632};
1633#line 230
1634struct super_block;
1635#line 288 "include/linux/quota.h"
1636struct dquot {
1637   struct hlist_node dq_hash ;
1638   struct list_head dq_inuse ;
1639   struct list_head dq_free ;
1640   struct list_head dq_dirty ;
1641   struct mutex dq_lock ;
1642   atomic_t dq_count ;
1643   wait_queue_head_t dq_wait_unused ;
1644   struct super_block *dq_sb ;
1645   unsigned int dq_id ;
1646   loff_t dq_off ;
1647   unsigned long dq_flags ;
1648   short dq_type ;
1649   struct mem_dqblk dq_dqb ;
1650};
1651#line 305 "include/linux/quota.h"
1652struct quota_format_ops {
1653   int (*check_quota_file)(struct super_block *sb , int type ) ;
1654   int (*read_file_info)(struct super_block *sb , int type ) ;
1655   int (*write_file_info)(struct super_block *sb , int type ) ;
1656   int (*free_file_info)(struct super_block *sb , int type ) ;
1657   int (*read_dqblk)(struct dquot *dquot ) ;
1658   int (*commit_dqblk)(struct dquot *dquot ) ;
1659   int (*release_dqblk)(struct dquot *dquot ) ;
1660};
1661#line 316 "include/linux/quota.h"
1662struct dquot_operations {
1663   int (*write_dquot)(struct dquot * ) ;
1664   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
1665   void (*destroy_dquot)(struct dquot * ) ;
1666   int (*acquire_dquot)(struct dquot * ) ;
1667   int (*release_dquot)(struct dquot * ) ;
1668   int (*mark_dirty)(struct dquot * ) ;
1669   int (*write_info)(struct super_block * , int  ) ;
1670   qsize_t *(*get_reserved_space)(struct inode * ) ;
1671};
1672#line 329
1673struct path;
1674#line 332 "include/linux/quota.h"
1675struct quotactl_ops {
1676   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
1677   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
1678   int (*quota_off)(struct super_block * , int  ) ;
1679   int (*quota_sync)(struct super_block * , int  , int  ) ;
1680   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1681   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1682   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1683   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1684   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1685   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
1686};
1687#line 345 "include/linux/quota.h"
1688struct quota_format_type {
1689   int qf_fmt_id ;
1690   struct quota_format_ops  const  *qf_ops ;
1691   struct module *qf_owner ;
1692   struct quota_format_type *qf_next ;
1693};
1694#line 399 "include/linux/quota.h"
1695struct quota_info {
1696   unsigned int flags ;
1697   struct mutex dqio_mutex ;
1698   struct mutex dqonoff_mutex ;
1699   struct rw_semaphore dqptr_sem ;
1700   struct inode *files[2] ;
1701   struct mem_dqinfo info[2] ;
1702   struct quota_format_ops  const  *ops[2] ;
1703};
1704#line 532 "include/linux/fs.h"
1705struct page;
1706#line 533
1707struct address_space;
1708#line 533
1709struct address_space;
1710#line 534
1711struct writeback_control;
1712#line 534
1713struct writeback_control;
1714#line 577 "include/linux/fs.h"
1715union __anonunion_arg_155 {
1716   char *buf ;
1717   void *data ;
1718};
1719#line 577 "include/linux/fs.h"
1720struct __anonstruct_read_descriptor_t_154 {
1721   size_t written ;
1722   size_t count ;
1723   union __anonunion_arg_155 arg ;
1724   int error ;
1725};
1726#line 577 "include/linux/fs.h"
1727typedef struct __anonstruct_read_descriptor_t_154 read_descriptor_t;
1728#line 590 "include/linux/fs.h"
1729struct address_space_operations {
1730   int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
1731   int (*readpage)(struct file * , struct page * ) ;
1732   int (*writepages)(struct address_space * , struct writeback_control * ) ;
1733   int (*set_page_dirty)(struct page *page ) ;
1734   int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
1735                    unsigned int nr_pages ) ;
1736   int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
1737                      unsigned int len , unsigned int flags , struct page **pagep ,
1738                      void **fsdata ) ;
1739   int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
1740                    unsigned int copied , struct page *page , void *fsdata ) ;
1741   sector_t (*bmap)(struct address_space * , sector_t  ) ;
1742   void (*invalidatepage)(struct page * , unsigned long  ) ;
1743   int (*releasepage)(struct page * , gfp_t  ) ;
1744   void (*freepage)(struct page * ) ;
1745   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  *iov , loff_t offset ,
1746                        unsigned long nr_segs ) ;
1747   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
1748   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
1749   int (*launder_page)(struct page * ) ;
1750   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
1751   int (*error_remove_page)(struct address_space * , struct page * ) ;
1752};
1753#line 645
1754struct backing_dev_info;
1755#line 646 "include/linux/fs.h"
1756struct address_space {
1757   struct inode *host ;
1758   struct radix_tree_root page_tree ;
1759   spinlock_t tree_lock ;
1760   unsigned int i_mmap_writable ;
1761   struct prio_tree_root i_mmap ;
1762   struct list_head i_mmap_nonlinear ;
1763   struct mutex i_mmap_mutex ;
1764   unsigned long nrpages ;
1765   unsigned long writeback_index ;
1766   struct address_space_operations  const  *a_ops ;
1767   unsigned long flags ;
1768   struct backing_dev_info *backing_dev_info ;
1769   spinlock_t private_lock ;
1770   struct list_head private_list ;
1771   struct address_space *assoc_mapping ;
1772} __attribute__((__aligned__(sizeof(long )))) ;
1773#line 669
1774struct request_queue;
1775#line 669
1776struct request_queue;
1777#line 671
1778struct hd_struct;
1779#line 671
1780struct gendisk;
1781#line 671 "include/linux/fs.h"
1782struct block_device {
1783   dev_t bd_dev ;
1784   int bd_openers ;
1785   struct inode *bd_inode ;
1786   struct super_block *bd_super ;
1787   struct mutex bd_mutex ;
1788   struct list_head bd_inodes ;
1789   void *bd_claiming ;
1790   void *bd_holder ;
1791   int bd_holders ;
1792   bool bd_write_holder ;
1793   struct list_head bd_holder_disks ;
1794   struct block_device *bd_contains ;
1795   unsigned int bd_block_size ;
1796   struct hd_struct *bd_part ;
1797   unsigned int bd_part_count ;
1798   int bd_invalidated ;
1799   struct gendisk *bd_disk ;
1800   struct request_queue *bd_queue ;
1801   struct list_head bd_list ;
1802   unsigned long bd_private ;
1803   int bd_fsfreeze_count ;
1804   struct mutex bd_fsfreeze_mutex ;
1805};
1806#line 749
1807struct posix_acl;
1808#line 749
1809struct posix_acl;
1810#line 761
1811struct inode_operations;
1812#line 761 "include/linux/fs.h"
1813union __anonunion____missing_field_name_156 {
1814   unsigned int const   i_nlink ;
1815   unsigned int __i_nlink ;
1816};
1817#line 761 "include/linux/fs.h"
1818union __anonunion____missing_field_name_157 {
1819   struct list_head i_dentry ;
1820   struct rcu_head i_rcu ;
1821};
1822#line 761
1823struct file_lock;
1824#line 761 "include/linux/fs.h"
1825union __anonunion____missing_field_name_158 {
1826   struct pipe_inode_info *i_pipe ;
1827   struct block_device *i_bdev ;
1828   struct cdev *i_cdev ;
1829};
1830#line 761 "include/linux/fs.h"
1831struct inode {
1832   umode_t i_mode ;
1833   unsigned short i_opflags ;
1834   uid_t i_uid ;
1835   gid_t i_gid ;
1836   unsigned int i_flags ;
1837   struct posix_acl *i_acl ;
1838   struct posix_acl *i_default_acl ;
1839   struct inode_operations  const  *i_op ;
1840   struct super_block *i_sb ;
1841   struct address_space *i_mapping ;
1842   void *i_security ;
1843   unsigned long i_ino ;
1844   union __anonunion____missing_field_name_156 __annonCompField30 ;
1845   dev_t i_rdev ;
1846   struct timespec i_atime ;
1847   struct timespec i_mtime ;
1848   struct timespec i_ctime ;
1849   spinlock_t i_lock ;
1850   unsigned short i_bytes ;
1851   blkcnt_t i_blocks ;
1852   loff_t i_size ;
1853   unsigned long i_state ;
1854   struct mutex i_mutex ;
1855   unsigned long dirtied_when ;
1856   struct hlist_node i_hash ;
1857   struct list_head i_wb_list ;
1858   struct list_head i_lru ;
1859   struct list_head i_sb_list ;
1860   union __anonunion____missing_field_name_157 __annonCompField31 ;
1861   atomic_t i_count ;
1862   unsigned int i_blkbits ;
1863   u64 i_version ;
1864   atomic_t i_dio_count ;
1865   atomic_t i_writecount ;
1866   struct file_operations  const  *i_fop ;
1867   struct file_lock *i_flock ;
1868   struct address_space i_data ;
1869   struct dquot *i_dquot[2] ;
1870   struct list_head i_devices ;
1871   union __anonunion____missing_field_name_158 __annonCompField32 ;
1872   __u32 i_generation ;
1873   __u32 i_fsnotify_mask ;
1874   struct hlist_head i_fsnotify_marks ;
1875   atomic_t i_readcount ;
1876   void *i_private ;
1877};
1878#line 942 "include/linux/fs.h"
1879struct fown_struct {
1880   rwlock_t lock ;
1881   struct pid *pid ;
1882   enum pid_type pid_type ;
1883   uid_t uid ;
1884   uid_t euid ;
1885   int signum ;
1886};
1887#line 953 "include/linux/fs.h"
1888struct file_ra_state {
1889   unsigned long start ;
1890   unsigned int size ;
1891   unsigned int async_size ;
1892   unsigned int ra_pages ;
1893   unsigned int mmap_miss ;
1894   loff_t prev_pos ;
1895};
1896#line 976 "include/linux/fs.h"
1897union __anonunion_f_u_159 {
1898   struct list_head fu_list ;
1899   struct rcu_head fu_rcuhead ;
1900};
1901#line 976 "include/linux/fs.h"
1902struct file {
1903   union __anonunion_f_u_159 f_u ;
1904   struct path f_path ;
1905   struct file_operations  const  *f_op ;
1906   spinlock_t f_lock ;
1907   int f_sb_list_cpu ;
1908   atomic_long_t f_count ;
1909   unsigned int f_flags ;
1910   fmode_t f_mode ;
1911   loff_t f_pos ;
1912   struct fown_struct f_owner ;
1913   struct cred  const  *f_cred ;
1914   struct file_ra_state f_ra ;
1915   u64 f_version ;
1916   void *f_security ;
1917   void *private_data ;
1918   struct list_head f_ep_links ;
1919   struct list_head f_tfile_llink ;
1920   struct address_space *f_mapping ;
1921   unsigned long f_mnt_write_state ;
1922};
1923#line 1111
1924struct files_struct;
1925#line 1111 "include/linux/fs.h"
1926typedef struct files_struct *fl_owner_t;
1927#line 1113 "include/linux/fs.h"
1928struct file_lock_operations {
1929   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1930   void (*fl_release_private)(struct file_lock * ) ;
1931};
1932#line 1118 "include/linux/fs.h"
1933struct lock_manager_operations {
1934   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1935   void (*lm_notify)(struct file_lock * ) ;
1936   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
1937   void (*lm_release_private)(struct file_lock * ) ;
1938   void (*lm_break)(struct file_lock * ) ;
1939   int (*lm_change)(struct file_lock ** , int  ) ;
1940};
1941#line 4 "include/linux/nfs_fs_i.h"
1942struct nlm_lockowner;
1943#line 4
1944struct nlm_lockowner;
1945#line 9 "include/linux/nfs_fs_i.h"
1946struct nfs_lock_info {
1947   u32 state ;
1948   struct nlm_lockowner *owner ;
1949   struct list_head list ;
1950};
1951#line 15
1952struct nfs4_lock_state;
1953#line 15
1954struct nfs4_lock_state;
1955#line 16 "include/linux/nfs_fs_i.h"
1956struct nfs4_lock_info {
1957   struct nfs4_lock_state *owner ;
1958};
1959#line 1138 "include/linux/fs.h"
1960struct fasync_struct;
1961#line 1138 "include/linux/fs.h"
1962struct __anonstruct_afs_161 {
1963   struct list_head link ;
1964   int state ;
1965};
1966#line 1138 "include/linux/fs.h"
1967union __anonunion_fl_u_160 {
1968   struct nfs_lock_info nfs_fl ;
1969   struct nfs4_lock_info nfs4_fl ;
1970   struct __anonstruct_afs_161 afs ;
1971};
1972#line 1138 "include/linux/fs.h"
1973struct file_lock {
1974   struct file_lock *fl_next ;
1975   struct list_head fl_link ;
1976   struct list_head fl_block ;
1977   fl_owner_t fl_owner ;
1978   unsigned int fl_flags ;
1979   unsigned char fl_type ;
1980   unsigned int fl_pid ;
1981   struct pid *fl_nspid ;
1982   wait_queue_head_t fl_wait ;
1983   struct file *fl_file ;
1984   loff_t fl_start ;
1985   loff_t fl_end ;
1986   struct fasync_struct *fl_fasync ;
1987   unsigned long fl_break_time ;
1988   unsigned long fl_downgrade_time ;
1989   struct file_lock_operations  const  *fl_ops ;
1990   struct lock_manager_operations  const  *fl_lmops ;
1991   union __anonunion_fl_u_160 fl_u ;
1992};
1993#line 1378 "include/linux/fs.h"
1994struct fasync_struct {
1995   spinlock_t fa_lock ;
1996   int magic ;
1997   int fa_fd ;
1998   struct fasync_struct *fa_next ;
1999   struct file *fa_file ;
2000   struct rcu_head fa_rcu ;
2001};
2002#line 1418
2003struct file_system_type;
2004#line 1418
2005struct super_operations;
2006#line 1418
2007struct xattr_handler;
2008#line 1418
2009struct mtd_info;
2010#line 1418 "include/linux/fs.h"
2011struct super_block {
2012   struct list_head s_list ;
2013   dev_t s_dev ;
2014   unsigned char s_dirt ;
2015   unsigned char s_blocksize_bits ;
2016   unsigned long s_blocksize ;
2017   loff_t s_maxbytes ;
2018   struct file_system_type *s_type ;
2019   struct super_operations  const  *s_op ;
2020   struct dquot_operations  const  *dq_op ;
2021   struct quotactl_ops  const  *s_qcop ;
2022   struct export_operations  const  *s_export_op ;
2023   unsigned long s_flags ;
2024   unsigned long s_magic ;
2025   struct dentry *s_root ;
2026   struct rw_semaphore s_umount ;
2027   struct mutex s_lock ;
2028   int s_count ;
2029   atomic_t s_active ;
2030   void *s_security ;
2031   struct xattr_handler  const  **s_xattr ;
2032   struct list_head s_inodes ;
2033   struct hlist_bl_head s_anon ;
2034   struct list_head *s_files ;
2035   struct list_head s_mounts ;
2036   struct list_head s_dentry_lru ;
2037   int s_nr_dentry_unused ;
2038   spinlock_t s_inode_lru_lock  __attribute__((__aligned__((1) <<  (6) ))) ;
2039   struct list_head s_inode_lru ;
2040   int s_nr_inodes_unused ;
2041   struct block_device *s_bdev ;
2042   struct backing_dev_info *s_bdi ;
2043   struct mtd_info *s_mtd ;
2044   struct hlist_node s_instances ;
2045   struct quota_info s_dquot ;
2046   int s_frozen ;
2047   wait_queue_head_t s_wait_unfrozen ;
2048   char s_id[32] ;
2049   u8 s_uuid[16] ;
2050   void *s_fs_info ;
2051   unsigned int s_max_links ;
2052   fmode_t s_mode ;
2053   u32 s_time_gran ;
2054   struct mutex s_vfs_rename_mutex ;
2055   char *s_subtype ;
2056   char *s_options ;
2057   struct dentry_operations  const  *s_d_op ;
2058   int cleancache_poolid ;
2059   struct shrinker s_shrink ;
2060   atomic_long_t s_remove_count ;
2061   int s_readonly_remount ;
2062};
2063#line 1567 "include/linux/fs.h"
2064struct fiemap_extent_info {
2065   unsigned int fi_flags ;
2066   unsigned int fi_extents_mapped ;
2067   unsigned int fi_extents_max ;
2068   struct fiemap_extent *fi_extents_start ;
2069};
2070#line 1609 "include/linux/fs.h"
2071struct file_operations {
2072   struct module *owner ;
2073   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
2074   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
2075   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
2076   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
2077                       loff_t  ) ;
2078   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
2079                        loff_t  ) ;
2080   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
2081                                                   loff_t  , u64  , unsigned int  ) ) ;
2082   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
2083   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
2084   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
2085   int (*mmap)(struct file * , struct vm_area_struct * ) ;
2086   int (*open)(struct inode * , struct file * ) ;
2087   int (*flush)(struct file * , fl_owner_t id ) ;
2088   int (*release)(struct inode * , struct file * ) ;
2089   int (*fsync)(struct file * , loff_t  , loff_t  , int datasync ) ;
2090   int (*aio_fsync)(struct kiocb * , int datasync ) ;
2091   int (*fasync)(int  , struct file * , int  ) ;
2092   int (*lock)(struct file * , int  , struct file_lock * ) ;
2093   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
2094                       int  ) ;
2095   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
2096                                      unsigned long  , unsigned long  ) ;
2097   int (*check_flags)(int  ) ;
2098   int (*flock)(struct file * , int  , struct file_lock * ) ;
2099   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
2100                           unsigned int  ) ;
2101   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
2102                          unsigned int  ) ;
2103   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
2104   long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
2105};
2106#line 1639 "include/linux/fs.h"
2107struct inode_operations {
2108   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
2109   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
2110   int (*permission)(struct inode * , int  ) ;
2111   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
2112   int (*readlink)(struct dentry * , char * , int  ) ;
2113   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
2114   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
2115   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
2116   int (*unlink)(struct inode * , struct dentry * ) ;
2117   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
2118   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
2119   int (*rmdir)(struct inode * , struct dentry * ) ;
2120   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
2121   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
2122   void (*truncate)(struct inode * ) ;
2123   int (*setattr)(struct dentry * , struct iattr * ) ;
2124   int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
2125   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
2126   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
2127   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
2128   int (*removexattr)(struct dentry * , char const   * ) ;
2129   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
2130   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
2131} __attribute__((__aligned__((1) <<  (6) ))) ;
2132#line 1669
2133struct seq_file;
2134#line 1684 "include/linux/fs.h"
2135struct super_operations {
2136   struct inode *(*alloc_inode)(struct super_block *sb ) ;
2137   void (*destroy_inode)(struct inode * ) ;
2138   void (*dirty_inode)(struct inode * , int flags ) ;
2139   int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
2140   int (*drop_inode)(struct inode * ) ;
2141   void (*evict_inode)(struct inode * ) ;
2142   void (*put_super)(struct super_block * ) ;
2143   void (*write_super)(struct super_block * ) ;
2144   int (*sync_fs)(struct super_block *sb , int wait ) ;
2145   int (*freeze_fs)(struct super_block * ) ;
2146   int (*unfreeze_fs)(struct super_block * ) ;
2147   int (*statfs)(struct dentry * , struct kstatfs * ) ;
2148   int (*remount_fs)(struct super_block * , int * , char * ) ;
2149   void (*umount_begin)(struct super_block * ) ;
2150   int (*show_options)(struct seq_file * , struct dentry * ) ;
2151   int (*show_devname)(struct seq_file * , struct dentry * ) ;
2152   int (*show_path)(struct seq_file * , struct dentry * ) ;
2153   int (*show_stats)(struct seq_file * , struct dentry * ) ;
2154   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
2155   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
2156                          loff_t  ) ;
2157   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
2158   int (*nr_cached_objects)(struct super_block * ) ;
2159   void (*free_cached_objects)(struct super_block * , int  ) ;
2160};
2161#line 1835 "include/linux/fs.h"
2162struct file_system_type {
2163   char const   *name ;
2164   int fs_flags ;
2165   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
2166   void (*kill_sb)(struct super_block * ) ;
2167   struct module *owner ;
2168   struct file_system_type *next ;
2169   struct hlist_head fs_supers ;
2170   struct lock_class_key s_lock_key ;
2171   struct lock_class_key s_umount_key ;
2172   struct lock_class_key s_vfs_rename_key ;
2173   struct lock_class_key i_lock_key ;
2174   struct lock_class_key i_mutex_key ;
2175   struct lock_class_key i_mutex_dir_key ;
2176};
2177#line 29 "include/linux/sysctl.h"
2178struct completion;
2179#line 939
2180struct nsproxy;
2181#line 939
2182struct nsproxy;
2183#line 28 "include/linux/poll.h"
2184struct poll_table_struct;
2185#line 39 "include/linux/poll.h"
2186struct poll_table_struct {
2187   void (*_qproc)(struct file * , wait_queue_head_t * , struct poll_table_struct * ) ;
2188   unsigned long _key ;
2189};
2190#line 143 "include/linux/rtc.h"
2191struct rtc_class_ops {
2192   int (*open)(struct device * ) ;
2193   void (*release)(struct device * ) ;
2194   int (*ioctl)(struct device * , unsigned int  , unsigned long  ) ;
2195   int (*read_time)(struct device * , struct rtc_time * ) ;
2196   int (*set_time)(struct device * , struct rtc_time * ) ;
2197   int (*read_alarm)(struct device * , struct rtc_wkalrm * ) ;
2198   int (*set_alarm)(struct device * , struct rtc_wkalrm * ) ;
2199   int (*proc)(struct device * , struct seq_file * ) ;
2200   int (*set_mmss)(struct device * , unsigned long secs ) ;
2201   int (*read_callback)(struct device * , int data ) ;
2202   int (*alarm_irq_enable)(struct device * , unsigned int enabled ) ;
2203};
2204#line 158 "include/linux/rtc.h"
2205struct rtc_task {
2206   void (*func)(void *private_data ) ;
2207   void *private_data ;
2208};
2209#line 164 "include/linux/rtc.h"
2210struct rtc_timer {
2211   struct rtc_task task ;
2212   struct timerqueue_node node ;
2213   ktime_t period ;
2214   int enabled ;
2215};
2216#line 175 "include/linux/rtc.h"
2217struct rtc_device {
2218   struct device dev ;
2219   struct module *owner ;
2220   int id ;
2221   char name[20] ;
2222   struct rtc_class_ops  const  *ops ;
2223   struct mutex ops_lock ;
2224   struct cdev char_dev ;
2225   unsigned long flags ;
2226   unsigned long irq_data ;
2227   spinlock_t irq_lock ;
2228   wait_queue_head_t irq_queue ;
2229   struct fasync_struct *async_queue ;
2230   struct rtc_task *irq_task ;
2231   spinlock_t irq_task_lock ;
2232   int irq_freq ;
2233   int max_user_freq ;
2234   struct timerqueue_head timerqueue ;
2235   struct rtc_timer aie_timer ;
2236   struct rtc_timer uie_rtctimer ;
2237   struct hrtimer pie_timer ;
2238   int pie_enabled ;
2239   struct work_struct irqwork ;
2240   int uie_unsupported ;
2241   struct work_struct uie_task ;
2242   struct timer_list uie_timer ;
2243   unsigned int oldsecs ;
2244   unsigned int uie_irq_active : 1 ;
2245   unsigned int stop_uie_polling : 1 ;
2246   unsigned int uie_task_active : 1 ;
2247   unsigned int uie_timer_active : 1 ;
2248};
2249#line 12 "include/linux/mod_devicetable.h"
2250typedef unsigned long kernel_ulong_t;
2251#line 219 "include/linux/mod_devicetable.h"
2252struct of_device_id {
2253   char name[32] ;
2254   char type[32] ;
2255   char compatible[128] ;
2256   void *data ;
2257};
2258#line 442 "include/linux/mod_devicetable.h"
2259struct spi_device_id {
2260   char name[32] ;
2261   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
2262};
2263#line 23 "include/linux/mm_types.h"
2264struct address_space;
2265#line 40 "include/linux/mm_types.h"
2266union __anonunion____missing_field_name_223 {
2267   unsigned long index ;
2268   void *freelist ;
2269};
2270#line 40 "include/linux/mm_types.h"
2271struct __anonstruct____missing_field_name_227 {
2272   unsigned int inuse : 16 ;
2273   unsigned int objects : 15 ;
2274   unsigned int frozen : 1 ;
2275};
2276#line 40 "include/linux/mm_types.h"
2277union __anonunion____missing_field_name_226 {
2278   atomic_t _mapcount ;
2279   struct __anonstruct____missing_field_name_227 __annonCompField36 ;
2280};
2281#line 40 "include/linux/mm_types.h"
2282struct __anonstruct____missing_field_name_225 {
2283   union __anonunion____missing_field_name_226 __annonCompField37 ;
2284   atomic_t _count ;
2285};
2286#line 40 "include/linux/mm_types.h"
2287union __anonunion____missing_field_name_224 {
2288   unsigned long counters ;
2289   struct __anonstruct____missing_field_name_225 __annonCompField38 ;
2290};
2291#line 40 "include/linux/mm_types.h"
2292struct __anonstruct____missing_field_name_222 {
2293   union __anonunion____missing_field_name_223 __annonCompField35 ;
2294   union __anonunion____missing_field_name_224 __annonCompField39 ;
2295};
2296#line 40 "include/linux/mm_types.h"
2297struct __anonstruct____missing_field_name_229 {
2298   struct page *next ;
2299   int pages ;
2300   int pobjects ;
2301};
2302#line 40 "include/linux/mm_types.h"
2303union __anonunion____missing_field_name_228 {
2304   struct list_head lru ;
2305   struct __anonstruct____missing_field_name_229 __annonCompField41 ;
2306};
2307#line 40 "include/linux/mm_types.h"
2308union __anonunion____missing_field_name_230 {
2309   unsigned long private ;
2310   struct kmem_cache *slab ;
2311   struct page *first_page ;
2312};
2313#line 40 "include/linux/mm_types.h"
2314struct page {
2315   unsigned long flags ;
2316   struct address_space *mapping ;
2317   struct __anonstruct____missing_field_name_222 __annonCompField40 ;
2318   union __anonunion____missing_field_name_228 __annonCompField42 ;
2319   union __anonunion____missing_field_name_230 __annonCompField43 ;
2320   unsigned long debug_flags ;
2321} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
2322#line 200 "include/linux/mm_types.h"
2323struct __anonstruct_vm_set_232 {
2324   struct list_head list ;
2325   void *parent ;
2326   struct vm_area_struct *head ;
2327};
2328#line 200 "include/linux/mm_types.h"
2329union __anonunion_shared_231 {
2330   struct __anonstruct_vm_set_232 vm_set ;
2331   struct raw_prio_tree_node prio_tree_node ;
2332};
2333#line 200
2334struct anon_vma;
2335#line 200
2336struct vm_operations_struct;
2337#line 200
2338struct mempolicy;
2339#line 200 "include/linux/mm_types.h"
2340struct vm_area_struct {
2341   struct mm_struct *vm_mm ;
2342   unsigned long vm_start ;
2343   unsigned long vm_end ;
2344   struct vm_area_struct *vm_next ;
2345   struct vm_area_struct *vm_prev ;
2346   pgprot_t vm_page_prot ;
2347   unsigned long vm_flags ;
2348   struct rb_node vm_rb ;
2349   union __anonunion_shared_231 shared ;
2350   struct list_head anon_vma_chain ;
2351   struct anon_vma *anon_vma ;
2352   struct vm_operations_struct  const  *vm_ops ;
2353   unsigned long vm_pgoff ;
2354   struct file *vm_file ;
2355   void *vm_private_data ;
2356   struct mempolicy *vm_policy ;
2357};
2358#line 257 "include/linux/mm_types.h"
2359struct core_thread {
2360   struct task_struct *task ;
2361   struct core_thread *next ;
2362};
2363#line 262 "include/linux/mm_types.h"
2364struct core_state {
2365   atomic_t nr_threads ;
2366   struct core_thread dumper ;
2367   struct completion startup ;
2368};
2369#line 284 "include/linux/mm_types.h"
2370struct mm_rss_stat {
2371   atomic_long_t count[3] ;
2372};
2373#line 288
2374struct linux_binfmt;
2375#line 288
2376struct mmu_notifier_mm;
2377#line 288 "include/linux/mm_types.h"
2378struct mm_struct {
2379   struct vm_area_struct *mmap ;
2380   struct rb_root mm_rb ;
2381   struct vm_area_struct *mmap_cache ;
2382   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
2383                                      unsigned long pgoff , unsigned long flags ) ;
2384   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
2385   unsigned long mmap_base ;
2386   unsigned long task_size ;
2387   unsigned long cached_hole_size ;
2388   unsigned long free_area_cache ;
2389   pgd_t *pgd ;
2390   atomic_t mm_users ;
2391   atomic_t mm_count ;
2392   int map_count ;
2393   spinlock_t page_table_lock ;
2394   struct rw_semaphore mmap_sem ;
2395   struct list_head mmlist ;
2396   unsigned long hiwater_rss ;
2397   unsigned long hiwater_vm ;
2398   unsigned long total_vm ;
2399   unsigned long locked_vm ;
2400   unsigned long pinned_vm ;
2401   unsigned long shared_vm ;
2402   unsigned long exec_vm ;
2403   unsigned long stack_vm ;
2404   unsigned long reserved_vm ;
2405   unsigned long def_flags ;
2406   unsigned long nr_ptes ;
2407   unsigned long start_code ;
2408   unsigned long end_code ;
2409   unsigned long start_data ;
2410   unsigned long end_data ;
2411   unsigned long start_brk ;
2412   unsigned long brk ;
2413   unsigned long start_stack ;
2414   unsigned long arg_start ;
2415   unsigned long arg_end ;
2416   unsigned long env_start ;
2417   unsigned long env_end ;
2418   unsigned long saved_auxv[44] ;
2419   struct mm_rss_stat rss_stat ;
2420   struct linux_binfmt *binfmt ;
2421   cpumask_var_t cpu_vm_mask_var ;
2422   mm_context_t context ;
2423   unsigned int faultstamp ;
2424   unsigned int token_priority ;
2425   unsigned int last_interval ;
2426   unsigned long flags ;
2427   struct core_state *core_state ;
2428   spinlock_t ioctx_lock ;
2429   struct hlist_head ioctx_list ;
2430   struct task_struct *owner ;
2431   struct file *exe_file ;
2432   unsigned long num_exe_file_vmas ;
2433   struct mmu_notifier_mm *mmu_notifier_mm ;
2434   pgtable_t pmd_huge_pte ;
2435   struct cpumask cpumask_allocation ;
2436};
2437#line 7 "include/asm-generic/cputime.h"
2438typedef unsigned long cputime_t;
2439#line 84 "include/linux/sem.h"
2440struct task_struct;
2441#line 101
2442struct sem_undo_list;
2443#line 101 "include/linux/sem.h"
2444struct sysv_sem {
2445   struct sem_undo_list *undo_list ;
2446};
2447#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2448struct siginfo;
2449#line 10
2450struct siginfo;
2451#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2452struct __anonstruct_sigset_t_234 {
2453   unsigned long sig[1] ;
2454};
2455#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2456typedef struct __anonstruct_sigset_t_234 sigset_t;
2457#line 17 "include/asm-generic/signal-defs.h"
2458typedef void __signalfn_t(int  );
2459#line 18 "include/asm-generic/signal-defs.h"
2460typedef __signalfn_t *__sighandler_t;
2461#line 20 "include/asm-generic/signal-defs.h"
2462typedef void __restorefn_t(void);
2463#line 21 "include/asm-generic/signal-defs.h"
2464typedef __restorefn_t *__sigrestore_t;
2465#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2466struct sigaction {
2467   __sighandler_t sa_handler ;
2468   unsigned long sa_flags ;
2469   __sigrestore_t sa_restorer ;
2470   sigset_t sa_mask ;
2471};
2472#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2473struct k_sigaction {
2474   struct sigaction sa ;
2475};
2476#line 7 "include/asm-generic/siginfo.h"
2477union sigval {
2478   int sival_int ;
2479   void *sival_ptr ;
2480};
2481#line 7 "include/asm-generic/siginfo.h"
2482typedef union sigval sigval_t;
2483#line 48 "include/asm-generic/siginfo.h"
2484struct __anonstruct__kill_236 {
2485   __kernel_pid_t _pid ;
2486   __kernel_uid32_t _uid ;
2487};
2488#line 48 "include/asm-generic/siginfo.h"
2489struct __anonstruct__timer_237 {
2490   __kernel_timer_t _tid ;
2491   int _overrun ;
2492   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
2493   sigval_t _sigval ;
2494   int _sys_private ;
2495};
2496#line 48 "include/asm-generic/siginfo.h"
2497struct __anonstruct__rt_238 {
2498   __kernel_pid_t _pid ;
2499   __kernel_uid32_t _uid ;
2500   sigval_t _sigval ;
2501};
2502#line 48 "include/asm-generic/siginfo.h"
2503struct __anonstruct__sigchld_239 {
2504   __kernel_pid_t _pid ;
2505   __kernel_uid32_t _uid ;
2506   int _status ;
2507   __kernel_clock_t _utime ;
2508   __kernel_clock_t _stime ;
2509};
2510#line 48 "include/asm-generic/siginfo.h"
2511struct __anonstruct__sigfault_240 {
2512   void *_addr ;
2513   short _addr_lsb ;
2514};
2515#line 48 "include/asm-generic/siginfo.h"
2516struct __anonstruct__sigpoll_241 {
2517   long _band ;
2518   int _fd ;
2519};
2520#line 48 "include/asm-generic/siginfo.h"
2521union __anonunion__sifields_235 {
2522   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
2523   struct __anonstruct__kill_236 _kill ;
2524   struct __anonstruct__timer_237 _timer ;
2525   struct __anonstruct__rt_238 _rt ;
2526   struct __anonstruct__sigchld_239 _sigchld ;
2527   struct __anonstruct__sigfault_240 _sigfault ;
2528   struct __anonstruct__sigpoll_241 _sigpoll ;
2529};
2530#line 48 "include/asm-generic/siginfo.h"
2531struct siginfo {
2532   int si_signo ;
2533   int si_errno ;
2534   int si_code ;
2535   union __anonunion__sifields_235 _sifields ;
2536};
2537#line 48 "include/asm-generic/siginfo.h"
2538typedef struct siginfo siginfo_t;
2539#line 288
2540struct siginfo;
2541#line 10 "include/linux/signal.h"
2542struct task_struct;
2543#line 18
2544struct user_struct;
2545#line 28 "include/linux/signal.h"
2546struct sigpending {
2547   struct list_head list ;
2548   sigset_t signal ;
2549};
2550#line 239
2551struct timespec;
2552#line 240
2553struct pt_regs;
2554#line 10 "include/linux/seccomp.h"
2555struct __anonstruct_seccomp_t_244 {
2556   int mode ;
2557};
2558#line 10 "include/linux/seccomp.h"
2559typedef struct __anonstruct_seccomp_t_244 seccomp_t;
2560#line 81 "include/linux/plist.h"
2561struct plist_head {
2562   struct list_head node_list ;
2563};
2564#line 85 "include/linux/plist.h"
2565struct plist_node {
2566   int prio ;
2567   struct list_head prio_list ;
2568   struct list_head node_list ;
2569};
2570#line 40 "include/linux/rtmutex.h"
2571struct rt_mutex_waiter;
2572#line 40
2573struct rt_mutex_waiter;
2574#line 42 "include/linux/resource.h"
2575struct rlimit {
2576   unsigned long rlim_cur ;
2577   unsigned long rlim_max ;
2578};
2579#line 81
2580struct task_struct;
2581#line 11 "include/linux/task_io_accounting.h"
2582struct task_io_accounting {
2583   u64 rchar ;
2584   u64 wchar ;
2585   u64 syscr ;
2586   u64 syscw ;
2587   u64 read_bytes ;
2588   u64 write_bytes ;
2589   u64 cancelled_write_bytes ;
2590};
2591#line 13 "include/linux/latencytop.h"
2592struct task_struct;
2593#line 20 "include/linux/latencytop.h"
2594struct latency_record {
2595   unsigned long backtrace[12] ;
2596   unsigned int count ;
2597   unsigned long time ;
2598   unsigned long max ;
2599};
2600#line 29 "include/linux/key.h"
2601typedef int32_t key_serial_t;
2602#line 32 "include/linux/key.h"
2603typedef uint32_t key_perm_t;
2604#line 34
2605struct key;
2606#line 34
2607struct key;
2608#line 74
2609struct seq_file;
2610#line 75
2611struct user_struct;
2612#line 76
2613struct signal_struct;
2614#line 76
2615struct signal_struct;
2616#line 77
2617struct cred;
2618#line 79
2619struct key_type;
2620#line 79
2621struct key_type;
2622#line 81
2623struct keyring_list;
2624#line 81
2625struct keyring_list;
2626#line 124
2627struct key_user;
2628#line 124 "include/linux/key.h"
2629union __anonunion____missing_field_name_245 {
2630   time_t expiry ;
2631   time_t revoked_at ;
2632};
2633#line 124 "include/linux/key.h"
2634union __anonunion_type_data_246 {
2635   struct list_head link ;
2636   unsigned long x[2] ;
2637   void *p[2] ;
2638   int reject_error ;
2639};
2640#line 124 "include/linux/key.h"
2641union __anonunion_payload_247 {
2642   unsigned long value ;
2643   void *rcudata ;
2644   void *data ;
2645   struct keyring_list *subscriptions ;
2646};
2647#line 124 "include/linux/key.h"
2648struct key {
2649   atomic_t usage ;
2650   key_serial_t serial ;
2651   struct rb_node serial_node ;
2652   struct key_type *type ;
2653   struct rw_semaphore sem ;
2654   struct key_user *user ;
2655   void *security ;
2656   union __anonunion____missing_field_name_245 __annonCompField44 ;
2657   uid_t uid ;
2658   gid_t gid ;
2659   key_perm_t perm ;
2660   unsigned short quotalen ;
2661   unsigned short datalen ;
2662   unsigned long flags ;
2663   char *description ;
2664   union __anonunion_type_data_246 type_data ;
2665   union __anonunion_payload_247 payload ;
2666};
2667#line 18 "include/linux/selinux.h"
2668struct audit_context;
2669#line 18
2670struct audit_context;
2671#line 21 "include/linux/cred.h"
2672struct user_struct;
2673#line 22
2674struct cred;
2675#line 23
2676struct inode;
2677#line 31 "include/linux/cred.h"
2678struct group_info {
2679   atomic_t usage ;
2680   int ngroups ;
2681   int nblocks ;
2682   gid_t small_block[32] ;
2683   gid_t *blocks[0] ;
2684};
2685#line 83 "include/linux/cred.h"
2686struct thread_group_cred {
2687   atomic_t usage ;
2688   pid_t tgid ;
2689   spinlock_t lock ;
2690   struct key *session_keyring ;
2691   struct key *process_keyring ;
2692   struct rcu_head rcu ;
2693};
2694#line 116 "include/linux/cred.h"
2695struct cred {
2696   atomic_t usage ;
2697   atomic_t subscribers ;
2698   void *put_addr ;
2699   unsigned int magic ;
2700   uid_t uid ;
2701   gid_t gid ;
2702   uid_t suid ;
2703   gid_t sgid ;
2704   uid_t euid ;
2705   gid_t egid ;
2706   uid_t fsuid ;
2707   gid_t fsgid ;
2708   unsigned int securebits ;
2709   kernel_cap_t cap_inheritable ;
2710   kernel_cap_t cap_permitted ;
2711   kernel_cap_t cap_effective ;
2712   kernel_cap_t cap_bset ;
2713   unsigned char jit_keyring ;
2714   struct key *thread_keyring ;
2715   struct key *request_key_auth ;
2716   struct thread_group_cred *tgcred ;
2717   void *security ;
2718   struct user_struct *user ;
2719   struct user_namespace *user_ns ;
2720   struct group_info *group_info ;
2721   struct rcu_head rcu ;
2722};
2723#line 61 "include/linux/llist.h"
2724struct llist_node;
2725#line 65 "include/linux/llist.h"
2726struct llist_node {
2727   struct llist_node *next ;
2728};
2729#line 97 "include/linux/sched.h"
2730struct futex_pi_state;
2731#line 97
2732struct futex_pi_state;
2733#line 98
2734struct robust_list_head;
2735#line 98
2736struct robust_list_head;
2737#line 99
2738struct bio_list;
2739#line 99
2740struct bio_list;
2741#line 100
2742struct fs_struct;
2743#line 100
2744struct fs_struct;
2745#line 101
2746struct perf_event_context;
2747#line 101
2748struct perf_event_context;
2749#line 102
2750struct blk_plug;
2751#line 102
2752struct blk_plug;
2753#line 150
2754struct seq_file;
2755#line 151
2756struct cfs_rq;
2757#line 151
2758struct cfs_rq;
2759#line 259
2760struct task_struct;
2761#line 366
2762struct nsproxy;
2763#line 367
2764struct user_namespace;
2765#line 58 "include/linux/aio_abi.h"
2766struct io_event {
2767   __u64 data ;
2768   __u64 obj ;
2769   __s64 res ;
2770   __s64 res2 ;
2771};
2772#line 16 "include/linux/uio.h"
2773struct iovec {
2774   void *iov_base ;
2775   __kernel_size_t iov_len ;
2776};
2777#line 15 "include/linux/aio.h"
2778struct kioctx;
2779#line 15
2780struct kioctx;
2781#line 87 "include/linux/aio.h"
2782union __anonunion_ki_obj_249 {
2783   void *user ;
2784   struct task_struct *tsk ;
2785};
2786#line 87
2787struct eventfd_ctx;
2788#line 87 "include/linux/aio.h"
2789struct kiocb {
2790   struct list_head ki_run_list ;
2791   unsigned long ki_flags ;
2792   int ki_users ;
2793   unsigned int ki_key ;
2794   struct file *ki_filp ;
2795   struct kioctx *ki_ctx ;
2796   int (*ki_cancel)(struct kiocb * , struct io_event * ) ;
2797   ssize_t (*ki_retry)(struct kiocb * ) ;
2798   void (*ki_dtor)(struct kiocb * ) ;
2799   union __anonunion_ki_obj_249 ki_obj ;
2800   __u64 ki_user_data ;
2801   loff_t ki_pos ;
2802   void *private ;
2803   unsigned short ki_opcode ;
2804   size_t ki_nbytes ;
2805   char *ki_buf ;
2806   size_t ki_left ;
2807   struct iovec ki_inline_vec ;
2808   struct iovec *ki_iovec ;
2809   unsigned long ki_nr_segs ;
2810   unsigned long ki_cur_seg ;
2811   struct list_head ki_list ;
2812   struct list_head ki_batch ;
2813   struct eventfd_ctx *ki_eventfd ;
2814};
2815#line 166 "include/linux/aio.h"
2816struct aio_ring_info {
2817   unsigned long mmap_base ;
2818   unsigned long mmap_size ;
2819   struct page **ring_pages ;
2820   spinlock_t ring_lock ;
2821   long nr_pages ;
2822   unsigned int nr ;
2823   unsigned int tail ;
2824   struct page *internal_pages[8] ;
2825};
2826#line 179 "include/linux/aio.h"
2827struct kioctx {
2828   atomic_t users ;
2829   int dead ;
2830   struct mm_struct *mm ;
2831   unsigned long user_id ;
2832   struct hlist_node list ;
2833   wait_queue_head_t wait ;
2834   spinlock_t ctx_lock ;
2835   int reqs_active ;
2836   struct list_head active_reqs ;
2837   struct list_head run_list ;
2838   unsigned int max_reqs ;
2839   struct aio_ring_info ring_info ;
2840   struct delayed_work wq ;
2841   struct rcu_head rcu_head ;
2842};
2843#line 214
2844struct mm_struct;
2845#line 443 "include/linux/sched.h"
2846struct sighand_struct {
2847   atomic_t count ;
2848   struct k_sigaction action[64] ;
2849   spinlock_t siglock ;
2850   wait_queue_head_t signalfd_wqh ;
2851};
2852#line 450 "include/linux/sched.h"
2853struct pacct_struct {
2854   int ac_flag ;
2855   long ac_exitcode ;
2856   unsigned long ac_mem ;
2857   cputime_t ac_utime ;
2858   cputime_t ac_stime ;
2859   unsigned long ac_minflt ;
2860   unsigned long ac_majflt ;
2861};
2862#line 458 "include/linux/sched.h"
2863struct cpu_itimer {
2864   cputime_t expires ;
2865   cputime_t incr ;
2866   u32 error ;
2867   u32 incr_error ;
2868};
2869#line 476 "include/linux/sched.h"
2870struct task_cputime {
2871   cputime_t utime ;
2872   cputime_t stime ;
2873   unsigned long long sum_exec_runtime ;
2874};
2875#line 512 "include/linux/sched.h"
2876struct thread_group_cputimer {
2877   struct task_cputime cputime ;
2878   int running ;
2879   raw_spinlock_t lock ;
2880};
2881#line 519
2882struct autogroup;
2883#line 519
2884struct autogroup;
2885#line 528
2886struct tty_struct;
2887#line 528
2888struct taskstats;
2889#line 528
2890struct tty_audit_buf;
2891#line 528 "include/linux/sched.h"
2892struct signal_struct {
2893   atomic_t sigcnt ;
2894   atomic_t live ;
2895   int nr_threads ;
2896   wait_queue_head_t wait_chldexit ;
2897   struct task_struct *curr_target ;
2898   struct sigpending shared_pending ;
2899   int group_exit_code ;
2900   int notify_count ;
2901   struct task_struct *group_exit_task ;
2902   int group_stop_count ;
2903   unsigned int flags ;
2904   unsigned int is_child_subreaper : 1 ;
2905   unsigned int has_child_subreaper : 1 ;
2906   struct list_head posix_timers ;
2907   struct hrtimer real_timer ;
2908   struct pid *leader_pid ;
2909   ktime_t it_real_incr ;
2910   struct cpu_itimer it[2] ;
2911   struct thread_group_cputimer cputimer ;
2912   struct task_cputime cputime_expires ;
2913   struct list_head cpu_timers[3] ;
2914   struct pid *tty_old_pgrp ;
2915   int leader ;
2916   struct tty_struct *tty ;
2917   struct autogroup *autogroup ;
2918   cputime_t utime ;
2919   cputime_t stime ;
2920   cputime_t cutime ;
2921   cputime_t cstime ;
2922   cputime_t gtime ;
2923   cputime_t cgtime ;
2924   cputime_t prev_utime ;
2925   cputime_t prev_stime ;
2926   unsigned long nvcsw ;
2927   unsigned long nivcsw ;
2928   unsigned long cnvcsw ;
2929   unsigned long cnivcsw ;
2930   unsigned long min_flt ;
2931   unsigned long maj_flt ;
2932   unsigned long cmin_flt ;
2933   unsigned long cmaj_flt ;
2934   unsigned long inblock ;
2935   unsigned long oublock ;
2936   unsigned long cinblock ;
2937   unsigned long coublock ;
2938   unsigned long maxrss ;
2939   unsigned long cmaxrss ;
2940   struct task_io_accounting ioac ;
2941   unsigned long long sum_sched_runtime ;
2942   struct rlimit rlim[16] ;
2943   struct pacct_struct pacct ;
2944   struct taskstats *stats ;
2945   unsigned int audit_tty ;
2946   struct tty_audit_buf *tty_audit_buf ;
2947   struct rw_semaphore group_rwsem ;
2948   int oom_adj ;
2949   int oom_score_adj ;
2950   int oom_score_adj_min ;
2951   struct mutex cred_guard_mutex ;
2952};
2953#line 703 "include/linux/sched.h"
2954struct user_struct {
2955   atomic_t __count ;
2956   atomic_t processes ;
2957   atomic_t files ;
2958   atomic_t sigpending ;
2959   atomic_t inotify_watches ;
2960   atomic_t inotify_devs ;
2961   atomic_t fanotify_listeners ;
2962   atomic_long_t epoll_watches ;
2963   unsigned long mq_bytes ;
2964   unsigned long locked_shm ;
2965   struct key *uid_keyring ;
2966   struct key *session_keyring ;
2967   struct hlist_node uidhash_node ;
2968   uid_t uid ;
2969   struct user_namespace *user_ns ;
2970   atomic_long_t locked_vm ;
2971};
2972#line 747
2973struct backing_dev_info;
2974#line 748
2975struct reclaim_state;
2976#line 748
2977struct reclaim_state;
2978#line 751 "include/linux/sched.h"
2979struct sched_info {
2980   unsigned long pcount ;
2981   unsigned long long run_delay ;
2982   unsigned long long last_arrival ;
2983   unsigned long long last_queued ;
2984};
2985#line 763 "include/linux/sched.h"
2986struct task_delay_info {
2987   spinlock_t lock ;
2988   unsigned int flags ;
2989   struct timespec blkio_start ;
2990   struct timespec blkio_end ;
2991   u64 blkio_delay ;
2992   u64 swapin_delay ;
2993   u32 blkio_count ;
2994   u32 swapin_count ;
2995   struct timespec freepages_start ;
2996   struct timespec freepages_end ;
2997   u64 freepages_delay ;
2998   u32 freepages_count ;
2999};
3000#line 1088
3001struct io_context;
3002#line 1088
3003struct io_context;
3004#line 1097
3005struct audit_context;
3006#line 1098
3007struct mempolicy;
3008#line 1099
3009struct pipe_inode_info;
3010#line 1102
3011struct rq;
3012#line 1102
3013struct rq;
3014#line 1122 "include/linux/sched.h"
3015struct sched_class {
3016   struct sched_class  const  *next ;
3017   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
3018   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
3019   void (*yield_task)(struct rq *rq ) ;
3020   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
3021   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
3022   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
3023   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
3024   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
3025   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
3026   void (*post_schedule)(struct rq *this_rq ) ;
3027   void (*task_waking)(struct task_struct *task ) ;
3028   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
3029   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
3030   void (*rq_online)(struct rq *rq ) ;
3031   void (*rq_offline)(struct rq *rq ) ;
3032   void (*set_curr_task)(struct rq *rq ) ;
3033   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
3034   void (*task_fork)(struct task_struct *p ) ;
3035   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
3036   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
3037   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
3038   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
3039   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
3040};
3041#line 1167 "include/linux/sched.h"
3042struct load_weight {
3043   unsigned long weight ;
3044   unsigned long inv_weight ;
3045};
3046#line 1172 "include/linux/sched.h"
3047struct sched_statistics {
3048   u64 wait_start ;
3049   u64 wait_max ;
3050   u64 wait_count ;
3051   u64 wait_sum ;
3052   u64 iowait_count ;
3053   u64 iowait_sum ;
3054   u64 sleep_start ;
3055   u64 sleep_max ;
3056   s64 sum_sleep_runtime ;
3057   u64 block_start ;
3058   u64 block_max ;
3059   u64 exec_max ;
3060   u64 slice_max ;
3061   u64 nr_migrations_cold ;
3062   u64 nr_failed_migrations_affine ;
3063   u64 nr_failed_migrations_running ;
3064   u64 nr_failed_migrations_hot ;
3065   u64 nr_forced_migrations ;
3066   u64 nr_wakeups ;
3067   u64 nr_wakeups_sync ;
3068   u64 nr_wakeups_migrate ;
3069   u64 nr_wakeups_local ;
3070   u64 nr_wakeups_remote ;
3071   u64 nr_wakeups_affine ;
3072   u64 nr_wakeups_affine_attempts ;
3073   u64 nr_wakeups_passive ;
3074   u64 nr_wakeups_idle ;
3075};
3076#line 1207 "include/linux/sched.h"
3077struct sched_entity {
3078   struct load_weight load ;
3079   struct rb_node run_node ;
3080   struct list_head group_node ;
3081   unsigned int on_rq ;
3082   u64 exec_start ;
3083   u64 sum_exec_runtime ;
3084   u64 vruntime ;
3085   u64 prev_sum_exec_runtime ;
3086   u64 nr_migrations ;
3087   struct sched_statistics statistics ;
3088   struct sched_entity *parent ;
3089   struct cfs_rq *cfs_rq ;
3090   struct cfs_rq *my_q ;
3091};
3092#line 1233
3093struct rt_rq;
3094#line 1233 "include/linux/sched.h"
3095struct sched_rt_entity {
3096   struct list_head run_list ;
3097   unsigned long timeout ;
3098   unsigned int time_slice ;
3099   int nr_cpus_allowed ;
3100   struct sched_rt_entity *back ;
3101   struct sched_rt_entity *parent ;
3102   struct rt_rq *rt_rq ;
3103   struct rt_rq *my_q ;
3104};
3105#line 1264
3106struct css_set;
3107#line 1264
3108struct compat_robust_list_head;
3109#line 1264
3110struct mem_cgroup;
3111#line 1264 "include/linux/sched.h"
3112struct memcg_batch_info {
3113   int do_batch ;
3114   struct mem_cgroup *memcg ;
3115   unsigned long nr_pages ;
3116   unsigned long memsw_nr_pages ;
3117};
3118#line 1264 "include/linux/sched.h"
3119struct task_struct {
3120   long volatile   state ;
3121   void *stack ;
3122   atomic_t usage ;
3123   unsigned int flags ;
3124   unsigned int ptrace ;
3125   struct llist_node wake_entry ;
3126   int on_cpu ;
3127   int on_rq ;
3128   int prio ;
3129   int static_prio ;
3130   int normal_prio ;
3131   unsigned int rt_priority ;
3132   struct sched_class  const  *sched_class ;
3133   struct sched_entity se ;
3134   struct sched_rt_entity rt ;
3135   struct hlist_head preempt_notifiers ;
3136   unsigned char fpu_counter ;
3137   unsigned int policy ;
3138   cpumask_t cpus_allowed ;
3139   struct sched_info sched_info ;
3140   struct list_head tasks ;
3141   struct plist_node pushable_tasks ;
3142   struct mm_struct *mm ;
3143   struct mm_struct *active_mm ;
3144   unsigned int brk_randomized : 1 ;
3145   int exit_state ;
3146   int exit_code ;
3147   int exit_signal ;
3148   int pdeath_signal ;
3149   unsigned int jobctl ;
3150   unsigned int personality ;
3151   unsigned int did_exec : 1 ;
3152   unsigned int in_execve : 1 ;
3153   unsigned int in_iowait : 1 ;
3154   unsigned int sched_reset_on_fork : 1 ;
3155   unsigned int sched_contributes_to_load : 1 ;
3156   unsigned int irq_thread : 1 ;
3157   pid_t pid ;
3158   pid_t tgid ;
3159   unsigned long stack_canary ;
3160   struct task_struct *real_parent ;
3161   struct task_struct *parent ;
3162   struct list_head children ;
3163   struct list_head sibling ;
3164   struct task_struct *group_leader ;
3165   struct list_head ptraced ;
3166   struct list_head ptrace_entry ;
3167   struct pid_link pids[3] ;
3168   struct list_head thread_group ;
3169   struct completion *vfork_done ;
3170   int *set_child_tid ;
3171   int *clear_child_tid ;
3172   cputime_t utime ;
3173   cputime_t stime ;
3174   cputime_t utimescaled ;
3175   cputime_t stimescaled ;
3176   cputime_t gtime ;
3177   cputime_t prev_utime ;
3178   cputime_t prev_stime ;
3179   unsigned long nvcsw ;
3180   unsigned long nivcsw ;
3181   struct timespec start_time ;
3182   struct timespec real_start_time ;
3183   unsigned long min_flt ;
3184   unsigned long maj_flt ;
3185   struct task_cputime cputime_expires ;
3186   struct list_head cpu_timers[3] ;
3187   struct cred  const  *real_cred ;
3188   struct cred  const  *cred ;
3189   struct cred *replacement_session_keyring ;
3190   char comm[16] ;
3191   int link_count ;
3192   int total_link_count ;
3193   struct sysv_sem sysvsem ;
3194   unsigned long last_switch_count ;
3195   struct thread_struct thread ;
3196   struct fs_struct *fs ;
3197   struct files_struct *files ;
3198   struct nsproxy *nsproxy ;
3199   struct signal_struct *signal ;
3200   struct sighand_struct *sighand ;
3201   sigset_t blocked ;
3202   sigset_t real_blocked ;
3203   sigset_t saved_sigmask ;
3204   struct sigpending pending ;
3205   unsigned long sas_ss_sp ;
3206   size_t sas_ss_size ;
3207   int (*notifier)(void *priv ) ;
3208   void *notifier_data ;
3209   sigset_t *notifier_mask ;
3210   struct audit_context *audit_context ;
3211   uid_t loginuid ;
3212   unsigned int sessionid ;
3213   seccomp_t seccomp ;
3214   u32 parent_exec_id ;
3215   u32 self_exec_id ;
3216   spinlock_t alloc_lock ;
3217   raw_spinlock_t pi_lock ;
3218   struct plist_head pi_waiters ;
3219   struct rt_mutex_waiter *pi_blocked_on ;
3220   struct mutex_waiter *blocked_on ;
3221   unsigned int irq_events ;
3222   unsigned long hardirq_enable_ip ;
3223   unsigned long hardirq_disable_ip ;
3224   unsigned int hardirq_enable_event ;
3225   unsigned int hardirq_disable_event ;
3226   int hardirqs_enabled ;
3227   int hardirq_context ;
3228   unsigned long softirq_disable_ip ;
3229   unsigned long softirq_enable_ip ;
3230   unsigned int softirq_disable_event ;
3231   unsigned int softirq_enable_event ;
3232   int softirqs_enabled ;
3233   int softirq_context ;
3234   void *journal_info ;
3235   struct bio_list *bio_list ;
3236   struct blk_plug *plug ;
3237   struct reclaim_state *reclaim_state ;
3238   struct backing_dev_info *backing_dev_info ;
3239   struct io_context *io_context ;
3240   unsigned long ptrace_message ;
3241   siginfo_t *last_siginfo ;
3242   struct task_io_accounting ioac ;
3243   u64 acct_rss_mem1 ;
3244   u64 acct_vm_mem1 ;
3245   cputime_t acct_timexpd ;
3246   nodemask_t mems_allowed ;
3247   seqcount_t mems_allowed_seq ;
3248   int cpuset_mem_spread_rotor ;
3249   int cpuset_slab_spread_rotor ;
3250   struct css_set *cgroups ;
3251   struct list_head cg_list ;
3252   struct robust_list_head *robust_list ;
3253   struct compat_robust_list_head *compat_robust_list ;
3254   struct list_head pi_state_list ;
3255   struct futex_pi_state *pi_state_cache ;
3256   struct perf_event_context *perf_event_ctxp[2] ;
3257   struct mutex perf_event_mutex ;
3258   struct list_head perf_event_list ;
3259   struct mempolicy *mempolicy ;
3260   short il_next ;
3261   short pref_node_fork ;
3262   struct rcu_head rcu ;
3263   struct pipe_inode_info *splice_pipe ;
3264   struct task_delay_info *delays ;
3265   int make_it_fail ;
3266   int nr_dirtied ;
3267   int nr_dirtied_pause ;
3268   unsigned long dirty_paused_when ;
3269   int latency_record_count ;
3270   struct latency_record latency_record[32] ;
3271   unsigned long timer_slack_ns ;
3272   unsigned long default_timer_slack_ns ;
3273   struct list_head *scm_work_list ;
3274   unsigned long trace ;
3275   unsigned long trace_recursion ;
3276   struct memcg_batch_info memcg_batch ;
3277   atomic_t ptrace_bp_refcnt ;
3278};
3279#line 1681
3280struct pid_namespace;
3281#line 55 "include/linux/kthread.h"
3282struct kthread_work;
3283#line 55
3284struct kthread_work;
3285#line 58 "include/linux/kthread.h"
3286struct kthread_worker {
3287   spinlock_t lock ;
3288   struct list_head work_list ;
3289   struct task_struct *task ;
3290};
3291#line 64 "include/linux/kthread.h"
3292struct kthread_work {
3293   struct list_head node ;
3294   void (*func)(struct kthread_work *work ) ;
3295   wait_queue_head_t done ;
3296   atomic_t flushing ;
3297   int queue_seq ;
3298   int done_seq ;
3299};
3300#line 70 "include/linux/spi/spi.h"
3301struct spi_master;
3302#line 70 "include/linux/spi/spi.h"
3303struct spi_device {
3304   struct device dev ;
3305   struct spi_master *master ;
3306   u32 max_speed_hz ;
3307   u8 chip_select ;
3308   u8 mode ;
3309   u8 bits_per_word ;
3310   int irq ;
3311   void *controller_state ;
3312   void *controller_data ;
3313   char modalias[32] ;
3314};
3315#line 145
3316struct spi_message;
3317#line 145
3318struct spi_message;
3319#line 176 "include/linux/spi/spi.h"
3320struct spi_driver {
3321   struct spi_device_id  const  *id_table ;
3322   int (*probe)(struct spi_device *spi ) ;
3323   int (*remove)(struct spi_device *spi ) ;
3324   void (*shutdown)(struct spi_device *spi ) ;
3325   int (*suspend)(struct spi_device *spi , pm_message_t mesg ) ;
3326   int (*resume)(struct spi_device *spi ) ;
3327   struct device_driver driver ;
3328};
3329#line 272 "include/linux/spi/spi.h"
3330struct spi_master {
3331   struct device dev ;
3332   struct list_head list ;
3333   s16 bus_num ;
3334   u16 num_chipselect ;
3335   u16 dma_alignment ;
3336   u16 mode_bits ;
3337   u16 flags ;
3338   spinlock_t bus_lock_spinlock ;
3339   struct mutex bus_lock_mutex ;
3340   bool bus_lock_flag ;
3341   int (*setup)(struct spi_device *spi ) ;
3342   int (*transfer)(struct spi_device *spi , struct spi_message *mesg ) ;
3343   void (*cleanup)(struct spi_device *spi ) ;
3344   bool queued ;
3345   struct kthread_worker kworker ;
3346   struct task_struct *kworker_task ;
3347   struct kthread_work pump_messages ;
3348   spinlock_t queue_lock ;
3349   struct list_head queue ;
3350   struct spi_message *cur_msg ;
3351   bool busy ;
3352   bool running ;
3353   bool rt ;
3354   int (*prepare_transfer_hardware)(struct spi_master *master ) ;
3355   int (*transfer_one_message)(struct spi_master *master , struct spi_message *mesg ) ;
3356   int (*unprepare_transfer_hardware)(struct spi_master *master ) ;
3357};
3358#line 492 "include/linux/spi/spi.h"
3359struct spi_transfer {
3360   void const   *tx_buf ;
3361   void *rx_buf ;
3362   unsigned int len ;
3363   dma_addr_t tx_dma ;
3364   dma_addr_t rx_dma ;
3365   unsigned int cs_change : 1 ;
3366   u8 bits_per_word ;
3367   u16 delay_usecs ;
3368   u32 speed_hz ;
3369   struct list_head transfer_list ;
3370};
3371#line 541 "include/linux/spi/spi.h"
3372struct spi_message {
3373   struct list_head transfers ;
3374   struct spi_device *spi ;
3375   unsigned int is_dma_mapped : 1 ;
3376   void (*complete)(void *context ) ;
3377   void *context ;
3378   unsigned int actual_length ;
3379   int status ;
3380   struct list_head queue ;
3381   void *state ;
3382};
3383#line 48 "include/linux/kmod.h"
3384struct cred;
3385#line 49
3386struct file;
3387#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
3388struct task_struct;
3389#line 18 "include/linux/elf.h"
3390typedef __u64 Elf64_Addr;
3391#line 19 "include/linux/elf.h"
3392typedef __u16 Elf64_Half;
3393#line 23 "include/linux/elf.h"
3394typedef __u32 Elf64_Word;
3395#line 24 "include/linux/elf.h"
3396typedef __u64 Elf64_Xword;
3397#line 194 "include/linux/elf.h"
3398struct elf64_sym {
3399   Elf64_Word st_name ;
3400   unsigned char st_info ;
3401   unsigned char st_other ;
3402   Elf64_Half st_shndx ;
3403   Elf64_Addr st_value ;
3404   Elf64_Xword st_size ;
3405};
3406#line 194 "include/linux/elf.h"
3407typedef struct elf64_sym Elf64_Sym;
3408#line 438
3409struct file;
3410#line 39 "include/linux/moduleparam.h"
3411struct kernel_param;
3412#line 39
3413struct kernel_param;
3414#line 41 "include/linux/moduleparam.h"
3415struct kernel_param_ops {
3416   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
3417   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
3418   void (*free)(void *arg ) ;
3419};
3420#line 50
3421struct kparam_string;
3422#line 50
3423struct kparam_array;
3424#line 50 "include/linux/moduleparam.h"
3425union __anonunion____missing_field_name_255 {
3426   void *arg ;
3427   struct kparam_string  const  *str ;
3428   struct kparam_array  const  *arr ;
3429};
3430#line 50 "include/linux/moduleparam.h"
3431struct kernel_param {
3432   char const   *name ;
3433   struct kernel_param_ops  const  *ops ;
3434   u16 perm ;
3435   s16 level ;
3436   union __anonunion____missing_field_name_255 __annonCompField46 ;
3437};
3438#line 63 "include/linux/moduleparam.h"
3439struct kparam_string {
3440   unsigned int maxlen ;
3441   char *string ;
3442};
3443#line 69 "include/linux/moduleparam.h"
3444struct kparam_array {
3445   unsigned int max ;
3446   unsigned int elemsize ;
3447   unsigned int *num ;
3448   struct kernel_param_ops  const  *ops ;
3449   void *elem ;
3450};
3451#line 445
3452struct module;
3453#line 80 "include/linux/jump_label.h"
3454struct module;
3455#line 143 "include/linux/jump_label.h"
3456struct static_key {
3457   atomic_t enabled ;
3458};
3459#line 22 "include/linux/tracepoint.h"
3460struct module;
3461#line 23
3462struct tracepoint;
3463#line 23
3464struct tracepoint;
3465#line 25 "include/linux/tracepoint.h"
3466struct tracepoint_func {
3467   void *func ;
3468   void *data ;
3469};
3470#line 30 "include/linux/tracepoint.h"
3471struct tracepoint {
3472   char const   *name ;
3473   struct static_key key ;
3474   void (*regfunc)(void) ;
3475   void (*unregfunc)(void) ;
3476   struct tracepoint_func *funcs ;
3477};
3478#line 19 "include/linux/export.h"
3479struct kernel_symbol {
3480   unsigned long value ;
3481   char const   *name ;
3482};
3483#line 8 "include/asm-generic/module.h"
3484struct mod_arch_specific {
3485
3486};
3487#line 35 "include/linux/module.h"
3488struct module;
3489#line 37
3490struct module_param_attrs;
3491#line 37 "include/linux/module.h"
3492struct module_kobject {
3493   struct kobject kobj ;
3494   struct module *mod ;
3495   struct kobject *drivers_dir ;
3496   struct module_param_attrs *mp ;
3497};
3498#line 44 "include/linux/module.h"
3499struct module_attribute {
3500   struct attribute attr ;
3501   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
3502   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
3503                    size_t count ) ;
3504   void (*setup)(struct module * , char const   * ) ;
3505   int (*test)(struct module * ) ;
3506   void (*free)(struct module * ) ;
3507};
3508#line 71
3509struct exception_table_entry;
3510#line 199
3511enum module_state {
3512    MODULE_STATE_LIVE = 0,
3513    MODULE_STATE_COMING = 1,
3514    MODULE_STATE_GOING = 2
3515} ;
3516#line 215 "include/linux/module.h"
3517struct module_ref {
3518   unsigned long incs ;
3519   unsigned long decs ;
3520} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
3521#line 220
3522struct module_sect_attrs;
3523#line 220
3524struct module_notes_attrs;
3525#line 220
3526struct ftrace_event_call;
3527#line 220 "include/linux/module.h"
3528struct module {
3529   enum module_state state ;
3530   struct list_head list ;
3531   char name[64UL - sizeof(unsigned long )] ;
3532   struct module_kobject mkobj ;
3533   struct module_attribute *modinfo_attrs ;
3534   char const   *version ;
3535   char const   *srcversion ;
3536   struct kobject *holders_dir ;
3537   struct kernel_symbol  const  *syms ;
3538   unsigned long const   *crcs ;
3539   unsigned int num_syms ;
3540   struct kernel_param *kp ;
3541   unsigned int num_kp ;
3542   unsigned int num_gpl_syms ;
3543   struct kernel_symbol  const  *gpl_syms ;
3544   unsigned long const   *gpl_crcs ;
3545   struct kernel_symbol  const  *unused_syms ;
3546   unsigned long const   *unused_crcs ;
3547   unsigned int num_unused_syms ;
3548   unsigned int num_unused_gpl_syms ;
3549   struct kernel_symbol  const  *unused_gpl_syms ;
3550   unsigned long const   *unused_gpl_crcs ;
3551   struct kernel_symbol  const  *gpl_future_syms ;
3552   unsigned long const   *gpl_future_crcs ;
3553   unsigned int num_gpl_future_syms ;
3554   unsigned int num_exentries ;
3555   struct exception_table_entry *extable ;
3556   int (*init)(void) ;
3557   void *module_init ;
3558   void *module_core ;
3559   unsigned int init_size ;
3560   unsigned int core_size ;
3561   unsigned int init_text_size ;
3562   unsigned int core_text_size ;
3563   unsigned int init_ro_size ;
3564   unsigned int core_ro_size ;
3565   struct mod_arch_specific arch ;
3566   unsigned int taints ;
3567   unsigned int num_bugs ;
3568   struct list_head bug_list ;
3569   struct bug_entry *bug_table ;
3570   Elf64_Sym *symtab ;
3571   Elf64_Sym *core_symtab ;
3572   unsigned int num_symtab ;
3573   unsigned int core_num_syms ;
3574   char *strtab ;
3575   char *core_strtab ;
3576   struct module_sect_attrs *sect_attrs ;
3577   struct module_notes_attrs *notes_attrs ;
3578   char *args ;
3579   void *percpu ;
3580   unsigned int percpu_size ;
3581   unsigned int num_tracepoints ;
3582   struct tracepoint * const  *tracepoints_ptrs ;
3583   unsigned int num_trace_bprintk_fmt ;
3584   char const   **trace_bprintk_fmt_start ;
3585   struct ftrace_event_call **trace_events ;
3586   unsigned int num_trace_events ;
3587   struct list_head source_list ;
3588   struct list_head target_list ;
3589   struct task_struct *waiter ;
3590   void (*exit)(void) ;
3591   struct module_ref *refptr ;
3592   ctor_fn_t *ctors ;
3593   unsigned int num_ctors ;
3594};
3595#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
3596struct pcf2123_sysfs_reg {
3597   struct device_attribute attr ;
3598   char name[2] ;
3599};
3600#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
3601struct pcf2123_plat_data {
3602   struct rtc_device *rtc ;
3603   struct pcf2123_sysfs_reg regs[16] ;
3604};
3605#line 1 "<compiler builtins>"
3606long __builtin_expect(long val , long res ) ;
3607#line 6 "include/linux/bcd.h"
3608extern unsigned int bcd2bin(unsigned char val )  __attribute__((__const__)) ;
3609#line 7
3610extern unsigned char bin2bcd(unsigned int val )  __attribute__((__const__)) ;
3611#line 49 "include/linux/dynamic_debug.h"
3612extern int ( /* format attribute */  __dynamic_dev_dbg)(struct _ddebug *descriptor ,
3613                                                        struct device  const  *dev ,
3614                                                        char const   *fmt  , ...) ;
3615#line 215 "include/linux/kernel.h"
3616extern int __attribute__((__warn_unused_result__))  _kstrtoul(char const   *s , unsigned int base ,
3617                                                              unsigned long *res ) ;
3618#line 218
3619extern int __attribute__((__warn_unused_result__))  kstrtoull(char const   *s , unsigned int base ,
3620                                                              unsigned long long *res ) ;
3621#line 220
3622__inline static int __attribute__((__warn_unused_result__))  kstrtoul(char const   *s ,
3623                                                                      unsigned int base ,
3624                                                                      unsigned long *res )  __attribute__((__no_instrument_function__)) ;
3625#line 220 "include/linux/kernel.h"
3626__inline static int __attribute__((__warn_unused_result__))  kstrtoul(char const   *s ,
3627                                                                      unsigned int base ,
3628                                                                      unsigned long *res ) 
3629{ int tmp ;
3630  int tmp___0 ;
3631  unsigned long long *__cil_tmp6 ;
3632
3633  {
3634#line 226
3635  if (8UL == 8UL) {
3636#line 226
3637    if (8UL == 8UL) {
3638      {
3639#line 228
3640      __cil_tmp6 = (unsigned long long *)res;
3641#line 228
3642      tmp = (int )kstrtoull(s, base, __cil_tmp6);
3643      }
3644#line 228
3645      return (tmp);
3646    } else {
3647      {
3648#line 230
3649      tmp___0 = (int )_kstrtoul(s, base, res);
3650      }
3651#line 230
3652      return (tmp___0);
3653    }
3654  } else {
3655    {
3656#line 230
3657    tmp___0 = (int )_kstrtoul(s, base, res);
3658    }
3659#line 230
3660    return (tmp___0);
3661  }
3662}
3663}
3664#line 320
3665extern int ( /* format attribute */  sprintf)(char *buf , char const   *fmt  , ...) ;
3666#line 10 "include/asm-generic/delay.h"
3667extern void __const_udelay(unsigned long xloops ) ;
3668#line 24 "include/linux/list.h"
3669__inline static void INIT_LIST_HEAD(struct list_head *list )  __attribute__((__no_instrument_function__)) ;
3670#line 24 "include/linux/list.h"
3671__inline static void INIT_LIST_HEAD(struct list_head *list ) 
3672{ unsigned long __cil_tmp2 ;
3673  unsigned long __cil_tmp3 ;
3674
3675  {
3676#line 26
3677  *((struct list_head **)list) = list;
3678#line 27
3679  __cil_tmp2 = (unsigned long )list;
3680#line 27
3681  __cil_tmp3 = __cil_tmp2 + 8;
3682#line 27
3683  *((struct list_head **)__cil_tmp3) = list;
3684#line 28
3685  return;
3686}
3687}
3688#line 47
3689extern void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next ) ;
3690#line 74
3691__inline static void list_add_tail(struct list_head *new , struct list_head *head )  __attribute__((__no_instrument_function__)) ;
3692#line 74 "include/linux/list.h"
3693__inline static void list_add_tail(struct list_head *new , struct list_head *head ) 
3694{ unsigned long __cil_tmp3 ;
3695  unsigned long __cil_tmp4 ;
3696  struct list_head *__cil_tmp5 ;
3697
3698  {
3699  {
3700#line 76
3701  __cil_tmp3 = (unsigned long )head;
3702#line 76
3703  __cil_tmp4 = __cil_tmp3 + 8;
3704#line 76
3705  __cil_tmp5 = *((struct list_head **)__cil_tmp4);
3706#line 76
3707  __list_add(new, __cil_tmp5, head);
3708  }
3709#line 77
3710  return;
3711}
3712}
3713#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
3714extern void *memset(void *s , int c , size_t n ) ;
3715#line 27 "include/linux/err.h"
3716__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
3717#line 27 "include/linux/err.h"
3718__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr ) 
3719{ 
3720
3721  {
3722#line 29
3723  return ((long )ptr);
3724}
3725}
3726#line 32
3727__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
3728#line 32 "include/linux/err.h"
3729__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr ) 
3730{ long tmp ;
3731  unsigned long __cil_tmp3 ;
3732  int __cil_tmp4 ;
3733  int __cil_tmp5 ;
3734  int __cil_tmp6 ;
3735  long __cil_tmp7 ;
3736
3737  {
3738  {
3739#line 34
3740  __cil_tmp3 = (unsigned long )ptr;
3741#line 34
3742  __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
3743#line 34
3744  __cil_tmp5 = ! __cil_tmp4;
3745#line 34
3746  __cil_tmp6 = ! __cil_tmp5;
3747#line 34
3748  __cil_tmp7 = (long )__cil_tmp6;
3749#line 34
3750  tmp = __builtin_expect(__cil_tmp7, 0L);
3751  }
3752#line 34
3753  return (tmp);
3754}
3755}
3756#line 152 "include/linux/mutex.h"
3757void mutex_lock(struct mutex *lock ) ;
3758#line 153
3759int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
3760#line 154
3761int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
3762#line 168
3763int mutex_trylock(struct mutex *lock ) ;
3764#line 169
3765void mutex_unlock(struct mutex *lock ) ;
3766#line 170
3767int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
3768#line 239 "include/linux/device.h"
3769extern void driver_unregister(struct device_driver *drv ) ;
3770#line 507
3771extern int device_create_file(struct device *device , struct device_attribute  const  *entry ) ;
3772#line 509
3773extern void device_remove_file(struct device *dev , struct device_attribute  const  *attr ) ;
3774#line 891
3775extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
3776                                              , ...) ;
3777#line 897
3778extern int ( /* format attribute */  _dev_info)(struct device  const  *dev , char const   *fmt 
3779                                                , ...) ;
3780#line 161 "include/linux/slab.h"
3781extern void kfree(void const   * ) ;
3782#line 221 "include/linux/slub_def.h"
3783extern void *__kmalloc(size_t size , gfp_t flags ) ;
3784#line 268
3785__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
3786                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
3787#line 268 "include/linux/slub_def.h"
3788__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
3789                                                                    gfp_t flags ) 
3790{ void *tmp___2 ;
3791
3792  {
3793  {
3794#line 283
3795  tmp___2 = __kmalloc(size, flags);
3796  }
3797#line 283
3798  return (tmp___2);
3799}
3800}
3801#line 349 "include/linux/slab.h"
3802__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
3803#line 349 "include/linux/slab.h"
3804__inline static void *kzalloc(size_t size , gfp_t flags ) 
3805{ void *tmp ;
3806  unsigned int __cil_tmp4 ;
3807
3808  {
3809  {
3810#line 351
3811  __cil_tmp4 = flags | 32768U;
3812#line 351
3813  tmp = kmalloc(size, __cil_tmp4);
3814  }
3815#line 351
3816  return (tmp);
3817}
3818}
3819#line 110 "include/linux/rtc.h"
3820extern int rtc_valid_tm(struct rtc_time *tm ) ;
3821#line 221
3822extern struct rtc_device *rtc_device_register(char const   *name , struct device *dev ,
3823                                              struct rtc_class_ops  const  *ops ,
3824                                              struct module *owner ) ;
3825#line 225
3826extern void rtc_device_unregister(struct rtc_device *rtc ) ;
3827#line 105 "include/linux/spi/spi.h"
3828__inline static struct spi_device *to_spi_device(struct device *dev )  __attribute__((__no_instrument_function__)) ;
3829#line 105 "include/linux/spi/spi.h"
3830__inline static struct spi_device *to_spi_device(struct device *dev ) 
3831{ struct device  const  *__mptr ;
3832  struct spi_device *tmp___7 ;
3833  struct spi_device *__cil_tmp4 ;
3834  struct device *__cil_tmp5 ;
3835  unsigned int __cil_tmp6 ;
3836  char *__cil_tmp7 ;
3837  char *__cil_tmp8 ;
3838  void *__cil_tmp9 ;
3839
3840  {
3841#line 107
3842  if (dev) {
3843#line 107
3844    __mptr = (struct device  const  *)dev;
3845#line 107
3846    __cil_tmp4 = (struct spi_device *)0;
3847#line 107
3848    __cil_tmp5 = (struct device *)__cil_tmp4;
3849#line 107
3850    __cil_tmp6 = (unsigned int )__cil_tmp5;
3851#line 107
3852    __cil_tmp7 = (char *)__mptr;
3853#line 107
3854    __cil_tmp8 = __cil_tmp7 - __cil_tmp6;
3855#line 107
3856    tmp___7 = (struct spi_device *)__cil_tmp8;
3857  } else {
3858#line 107
3859    __cil_tmp9 = (void *)0;
3860#line 107
3861    tmp___7 = (struct spi_device *)__cil_tmp9;
3862  }
3863#line 107
3864  return (tmp___7);
3865}
3866}
3867#line 191
3868extern int spi_register_driver(struct spi_driver *sdrv ) ;
3869#line 198
3870__inline static void spi_unregister_driver(struct spi_driver *sdrv )  __attribute__((__no_instrument_function__)) ;
3871#line 198 "include/linux/spi/spi.h"
3872__inline static void spi_unregister_driver(struct spi_driver *sdrv ) 
3873{ unsigned long __cil_tmp2 ;
3874  unsigned long __cil_tmp3 ;
3875  struct device_driver *__cil_tmp4 ;
3876
3877  {
3878#line 200
3879  if (sdrv) {
3880    {
3881#line 201
3882    __cil_tmp2 = (unsigned long )sdrv;
3883#line 201
3884    __cil_tmp3 = __cil_tmp2 + 48;
3885#line 201
3886    __cil_tmp4 = (struct device_driver *)__cil_tmp3;
3887#line 201
3888    driver_unregister(__cil_tmp4);
3889    }
3890  } else {
3891
3892  }
3893#line 202
3894  return;
3895}
3896}
3897#line 573
3898__inline static void spi_message_init(struct spi_message *m )  __attribute__((__no_instrument_function__)) ;
3899#line 573 "include/linux/spi/spi.h"
3900__inline static void spi_message_init(struct spi_message *m ) 
3901{ void *__cil_tmp2 ;
3902  struct list_head *__cil_tmp3 ;
3903
3904  {
3905  {
3906#line 575
3907  __cil_tmp2 = (void *)m;
3908#line 575
3909  memset(__cil_tmp2, 0, 80UL);
3910#line 576
3911  __cil_tmp3 = (struct list_head *)m;
3912#line 576
3913  INIT_LIST_HEAD(__cil_tmp3);
3914  }
3915#line 577
3916  return;
3917}
3918}
3919#line 579
3920__inline static void spi_message_add_tail(struct spi_transfer *t , struct spi_message *m )  __attribute__((__no_instrument_function__)) ;
3921#line 579 "include/linux/spi/spi.h"
3922__inline static void spi_message_add_tail(struct spi_transfer *t , struct spi_message *m ) 
3923{ unsigned long __cil_tmp3 ;
3924  unsigned long __cil_tmp4 ;
3925  struct list_head *__cil_tmp5 ;
3926  struct list_head *__cil_tmp6 ;
3927
3928  {
3929  {
3930#line 582
3931  __cil_tmp3 = (unsigned long )t;
3932#line 582
3933  __cil_tmp4 = __cil_tmp3 + 48;
3934#line 582
3935  __cil_tmp5 = (struct list_head *)__cil_tmp4;
3936#line 582
3937  __cil_tmp6 = (struct list_head *)m;
3938#line 582
3939  list_add_tail(__cil_tmp5, __cil_tmp6);
3940  }
3941#line 583
3942  return;
3943}
3944}
3945#line 630
3946extern int spi_sync(struct spi_device *spi , struct spi_message *message ) ;
3947#line 645
3948__inline static int spi_write(struct spi_device *spi , void const   *buf , size_t len )  __attribute__((__no_instrument_function__)) ;
3949#line 645 "include/linux/spi/spi.h"
3950__inline static int spi_write(struct spi_device *spi , void const   *buf , size_t len ) 
3951{ struct spi_transfer t ;
3952  struct spi_message m ;
3953  int tmp___7 ;
3954  struct spi_transfer *__cil_tmp7 ;
3955  unsigned long __cil_tmp8 ;
3956  unsigned long __cil_tmp9 ;
3957  unsigned long __cil_tmp10 ;
3958  unsigned long __cil_tmp11 ;
3959  unsigned long __cil_tmp12 ;
3960  unsigned long __cil_tmp13 ;
3961  unsigned long __cil_tmp14 ;
3962  unsigned long __cil_tmp15 ;
3963  unsigned long __cil_tmp16 ;
3964  unsigned long __cil_tmp17 ;
3965  unsigned long __cil_tmp18 ;
3966
3967  {
3968  {
3969#line 648
3970  __cil_tmp7 = & t;
3971#line 648
3972  *((void const   **)__cil_tmp7) = buf;
3973#line 648
3974  __cil_tmp8 = (unsigned long )(& t) + 8;
3975#line 648
3976  *((void **)__cil_tmp8) = (void *)0;
3977#line 648
3978  __cil_tmp9 = (unsigned long )(& t) + 16;
3979#line 648
3980  *((unsigned int *)__cil_tmp9) = (unsigned int )len;
3981#line 648
3982  __cil_tmp10 = (unsigned long )(& t) + 24;
3983#line 648
3984  *((dma_addr_t *)__cil_tmp10) = 0ULL;
3985#line 648
3986  __cil_tmp11 = (unsigned long )(& t) + 32;
3987#line 648
3988  *((dma_addr_t *)__cil_tmp11) = 0ULL;
3989#line 648
3990  __cil_tmp12 = (unsigned long )(& t) + 40;
3991#line 648
3992  *((unsigned int *)__cil_tmp12) = 0U;
3993#line 648
3994  __cil_tmp13 = (unsigned long )(& t) + 41;
3995#line 648
3996  *((u8 *)__cil_tmp13) = (unsigned char)0;
3997#line 648
3998  __cil_tmp14 = (unsigned long )(& t) + 42;
3999#line 648
4000  *((u16 *)__cil_tmp14) = (unsigned short)0;
4001#line 648
4002  __cil_tmp15 = (unsigned long )(& t) + 44;
4003#line 648
4004  *((u32 *)__cil_tmp15) = 0U;
4005#line 648
4006  __cil_tmp16 = (unsigned long )(& t) + 48;
4007#line 648
4008  *((struct list_head **)__cil_tmp16) = (struct list_head *)0;
4009#line 648
4010  __cil_tmp17 = 48 + 8;
4011#line 648
4012  __cil_tmp18 = (unsigned long )(& t) + __cil_tmp17;
4013#line 648
4014  *((struct list_head **)__cil_tmp18) = (struct list_head *)0;
4015#line 654
4016  spi_message_init(& m);
4017#line 655
4018  spi_message_add_tail(& t, & m);
4019#line 656
4020  tmp___7 = spi_sync(spi, & m);
4021  }
4022#line 656
4023  return (tmp___7);
4024}
4025}
4026#line 684
4027extern int spi_write_then_read(struct spi_device *spi , void const   *txbuf , unsigned int n_tx ,
4028                               void *rxbuf , unsigned int n_rx ) ;
4029#line 26 "include/linux/export.h"
4030extern struct module __this_module ;
4031#line 67 "include/linux/module.h"
4032int init_module(void) ;
4033#line 68
4034void cleanup_module(void) ;
4035#line 64 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
4036static struct spi_driver pcf2123_driver ;
4037#line 81
4038__inline static void pcf2123_delay_trec(void)  __attribute__((__no_instrument_function__)) ;
4039#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
4040__inline static void pcf2123_delay_trec(void) 
4041{ 
4042
4043  {
4044  {
4045#line 83
4046  __const_udelay(150UL);
4047  }
4048#line 84
4049  return;
4050}
4051}
4052#line 86 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
4053static ssize_t pcf2123_show(struct device *dev , struct device_attribute *attr , char *buffer ) 
4054{ struct spi_device *spi ;
4055  struct spi_device *tmp___7 ;
4056  struct pcf2123_sysfs_reg *r ;
4057  u8 txbuf[1] ;
4058  u8 rxbuf[1] ;
4059  unsigned long reg ;
4060  int ret ;
4061  struct device_attribute  const  *__mptr ;
4062  int tmp___8 ;
4063  int tmp___9 ;
4064  struct pcf2123_sysfs_reg *__cil_tmp14 ;
4065  struct device_attribute *__cil_tmp15 ;
4066  unsigned int __cil_tmp16 ;
4067  char *__cil_tmp17 ;
4068  char *__cil_tmp18 ;
4069  unsigned long __cil_tmp19 ;
4070  unsigned long __cil_tmp20 ;
4071  unsigned long __cil_tmp21 ;
4072  unsigned long __cil_tmp22 ;
4073  char *__cil_tmp23 ;
4074  char const   *__cil_tmp24 ;
4075  unsigned long __cil_tmp25 ;
4076  unsigned long __cil_tmp26 ;
4077  unsigned long *__cil_tmp27 ;
4078  unsigned long __cil_tmp28 ;
4079  int __cil_tmp29 ;
4080  int __cil_tmp30 ;
4081  int __cil_tmp31 ;
4082  unsigned long __cil_tmp32 ;
4083  unsigned long __cil_tmp33 ;
4084  unsigned long __cil_tmp34 ;
4085  unsigned long __cil_tmp35 ;
4086  u8 *__cil_tmp36 ;
4087  void const   *__cil_tmp37 ;
4088  unsigned long __cil_tmp38 ;
4089  unsigned long __cil_tmp39 ;
4090  u8 *__cil_tmp40 ;
4091  void *__cil_tmp41 ;
4092  unsigned long __cil_tmp42 ;
4093  unsigned long __cil_tmp43 ;
4094  u8 __cil_tmp44 ;
4095  int __cil_tmp45 ;
4096
4097  {
4098  {
4099#line 89
4100  tmp___7 = to_spi_device(dev);
4101#line 89
4102  spi = tmp___7;
4103#line 95
4104  __mptr = (struct device_attribute  const  *)attr;
4105#line 95
4106  __cil_tmp14 = (struct pcf2123_sysfs_reg *)0;
4107#line 95
4108  __cil_tmp15 = (struct device_attribute *)__cil_tmp14;
4109#line 95
4110  __cil_tmp16 = (unsigned int )__cil_tmp15;
4111#line 95
4112  __cil_tmp17 = (char *)__mptr;
4113#line 95
4114  __cil_tmp18 = __cil_tmp17 - __cil_tmp16;
4115#line 95
4116  r = (struct pcf2123_sysfs_reg *)__cil_tmp18;
4117#line 97
4118  __cil_tmp19 = 0 * 1UL;
4119#line 97
4120  __cil_tmp20 = 32 + __cil_tmp19;
4121#line 97
4122  __cil_tmp21 = (unsigned long )r;
4123#line 97
4124  __cil_tmp22 = __cil_tmp21 + __cil_tmp20;
4125#line 97
4126  __cil_tmp23 = (char *)__cil_tmp22;
4127#line 97
4128  __cil_tmp24 = (char const   *)__cil_tmp23;
4129#line 97
4130  tmp___8 = (int )kstrtoul(__cil_tmp24, 16U, & reg);
4131  }
4132#line 97
4133  if (tmp___8) {
4134#line 98
4135    return ((ssize_t )-22);
4136  } else {
4137
4138  }
4139  {
4140#line 100
4141  __cil_tmp25 = 0 * 1UL;
4142#line 100
4143  __cil_tmp26 = (unsigned long )(txbuf) + __cil_tmp25;
4144#line 100
4145  __cil_tmp27 = & reg;
4146#line 100
4147  __cil_tmp28 = *__cil_tmp27;
4148#line 100
4149  __cil_tmp29 = 1 << 4;
4150#line 100
4151  __cil_tmp30 = 1 << 7;
4152#line 100
4153  __cil_tmp31 = __cil_tmp30 | __cil_tmp29;
4154#line 100
4155  __cil_tmp32 = (unsigned long )__cil_tmp31;
4156#line 100
4157  __cil_tmp33 = __cil_tmp32 | __cil_tmp28;
4158#line 100
4159  *((u8 *)__cil_tmp26) = (u8 )__cil_tmp33;
4160#line 101
4161  __cil_tmp34 = 0 * 1UL;
4162#line 101
4163  __cil_tmp35 = (unsigned long )(txbuf) + __cil_tmp34;
4164#line 101
4165  __cil_tmp36 = (u8 *)__cil_tmp35;
4166#line 101
4167  __cil_tmp37 = (void const   *)__cil_tmp36;
4168#line 101
4169  __cil_tmp38 = 0 * 1UL;
4170#line 101
4171  __cil_tmp39 = (unsigned long )(rxbuf) + __cil_tmp38;
4172#line 101
4173  __cil_tmp40 = (u8 *)__cil_tmp39;
4174#line 101
4175  __cil_tmp41 = (void *)__cil_tmp40;
4176#line 101
4177  ret = spi_write_then_read(spi, __cil_tmp37, 1U, __cil_tmp41, 1U);
4178  }
4179#line 102
4180  if (ret < 0) {
4181#line 103
4182    return ((ssize_t )-5);
4183  } else {
4184
4185  }
4186  {
4187#line 104
4188  pcf2123_delay_trec();
4189#line 105
4190  __cil_tmp42 = 0 * 1UL;
4191#line 105
4192  __cil_tmp43 = (unsigned long )(rxbuf) + __cil_tmp42;
4193#line 105
4194  __cil_tmp44 = *((u8 *)__cil_tmp43);
4195#line 105
4196  __cil_tmp45 = (int )__cil_tmp44;
4197#line 105
4198  tmp___9 = sprintf(buffer, "0x%x\n", __cil_tmp45);
4199  }
4200#line 105
4201  return ((ssize_t )tmp___9);
4202}
4203}
4204#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
4205static ssize_t pcf2123_store(struct device *dev , struct device_attribute *attr ,
4206                             char const   *buffer , size_t count ) 
4207{ struct spi_device *spi ;
4208  struct spi_device *tmp___7 ;
4209  struct pcf2123_sysfs_reg *r ;
4210  u8 txbuf[2] ;
4211  unsigned long reg ;
4212  unsigned long val ;
4213  int ret ;
4214  struct device_attribute  const  *__mptr ;
4215  int tmp___8 ;
4216  int tmp___9 ;
4217  struct pcf2123_sysfs_reg *__cil_tmp15 ;
4218  struct device_attribute *__cil_tmp16 ;
4219  unsigned int __cil_tmp17 ;
4220  char *__cil_tmp18 ;
4221  char *__cil_tmp19 ;
4222  unsigned long __cil_tmp20 ;
4223  unsigned long __cil_tmp21 ;
4224  unsigned long __cil_tmp22 ;
4225  unsigned long __cil_tmp23 ;
4226  char *__cil_tmp24 ;
4227  char const   *__cil_tmp25 ;
4228  unsigned long __cil_tmp26 ;
4229  unsigned long __cil_tmp27 ;
4230  unsigned long *__cil_tmp28 ;
4231  unsigned long __cil_tmp29 ;
4232  int __cil_tmp30 ;
4233  unsigned long __cil_tmp31 ;
4234  unsigned long __cil_tmp32 ;
4235  unsigned long __cil_tmp33 ;
4236  unsigned long __cil_tmp34 ;
4237  unsigned long *__cil_tmp35 ;
4238  unsigned long __cil_tmp36 ;
4239  unsigned long __cil_tmp37 ;
4240  unsigned long __cil_tmp38 ;
4241  u8 *__cil_tmp39 ;
4242  void const   *__cil_tmp40 ;
4243
4244  {
4245  {
4246#line 110
4247  tmp___7 = to_spi_device(dev);
4248#line 110
4249  spi = tmp___7;
4250#line 118
4251  __mptr = (struct device_attribute  const  *)attr;
4252#line 118
4253  __cil_tmp15 = (struct pcf2123_sysfs_reg *)0;
4254#line 118
4255  __cil_tmp16 = (struct device_attribute *)__cil_tmp15;
4256#line 118
4257  __cil_tmp17 = (unsigned int )__cil_tmp16;
4258#line 118
4259  __cil_tmp18 = (char *)__mptr;
4260#line 118
4261  __cil_tmp19 = __cil_tmp18 - __cil_tmp17;
4262#line 118
4263  r = (struct pcf2123_sysfs_reg *)__cil_tmp19;
4264#line 120
4265  __cil_tmp20 = 0 * 1UL;
4266#line 120
4267  __cil_tmp21 = 32 + __cil_tmp20;
4268#line 120
4269  __cil_tmp22 = (unsigned long )r;
4270#line 120
4271  __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
4272#line 120
4273  __cil_tmp24 = (char *)__cil_tmp23;
4274#line 120
4275  __cil_tmp25 = (char const   *)__cil_tmp24;
4276#line 120
4277  tmp___8 = (int )kstrtoul(__cil_tmp25, 16U, & reg);
4278  }
4279#line 120
4280  if (tmp___8) {
4281#line 122
4282    return ((ssize_t )-22);
4283  } else {
4284    {
4285#line 120
4286    tmp___9 = (int )kstrtoul(buffer, 10U, & val);
4287    }
4288#line 120
4289    if (tmp___9) {
4290#line 122
4291      return ((ssize_t )-22);
4292    } else {
4293
4294    }
4295  }
4296  {
4297#line 124
4298  __cil_tmp26 = 0 * 1UL;
4299#line 124
4300  __cil_tmp27 = (unsigned long )(txbuf) + __cil_tmp26;
4301#line 124
4302  __cil_tmp28 = & reg;
4303#line 124
4304  __cil_tmp29 = *__cil_tmp28;
4305#line 124
4306  __cil_tmp30 = 1 << 4;
4307#line 124
4308  __cil_tmp31 = (unsigned long )__cil_tmp30;
4309#line 124
4310  __cil_tmp32 = __cil_tmp31 | __cil_tmp29;
4311#line 124
4312  *((u8 *)__cil_tmp27) = (u8 )__cil_tmp32;
4313#line 125
4314  __cil_tmp33 = 1 * 1UL;
4315#line 125
4316  __cil_tmp34 = (unsigned long )(txbuf) + __cil_tmp33;
4317#line 125
4318  __cil_tmp35 = & val;
4319#line 125
4320  __cil_tmp36 = *__cil_tmp35;
4321#line 125
4322  *((u8 *)__cil_tmp34) = (u8 )__cil_tmp36;
4323#line 126
4324  __cil_tmp37 = 0 * 1UL;
4325#line 126
4326  __cil_tmp38 = (unsigned long )(txbuf) + __cil_tmp37;
4327#line 126
4328  __cil_tmp39 = (u8 *)__cil_tmp38;
4329#line 126
4330  __cil_tmp40 = (void const   *)__cil_tmp39;
4331#line 126
4332  ret = spi_write(spi, __cil_tmp40, 2UL);
4333  }
4334#line 127
4335  if (ret < 0) {
4336#line 128
4337    return ((ssize_t )-5);
4338  } else {
4339
4340  }
4341  {
4342#line 129
4343  pcf2123_delay_trec();
4344  }
4345#line 130
4346  return ((ssize_t )count);
4347}
4348}
4349#line 156
4350static int pcf2123_rtc_read_time(struct device *dev , struct rtc_time *tm ) ;
4351#line 156 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
4352static struct _ddebug  __attribute__((__aligned__(8))) descriptor  __attribute__((__used__,
4353__section__("__verbose")))  =    {"rtc_pcf2123", "pcf2123_rtc_read_time", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c",
4354    "%s: tm is secs=%d, mins=%d, hours=%d, mday=%d, mon=%d, year=%d, wday=%d\n", 160U,
4355    1U};
4356#line 133 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
4357static int pcf2123_rtc_read_time(struct device *dev , struct rtc_time *tm ) 
4358{ struct spi_device *spi ;
4359  struct spi_device *tmp___7 ;
4360  u8 txbuf[1] ;
4361  u8 rxbuf[7] ;
4362  int ret ;
4363  unsigned int tmp___8 ;
4364  unsigned int tmp___9 ;
4365  unsigned int tmp___10 ;
4366  unsigned int tmp___11 ;
4367  unsigned int tmp___12 ;
4368  unsigned int tmp___13 ;
4369  long tmp___14 ;
4370  int tmp___15 ;
4371  unsigned long __cil_tmp16 ;
4372  unsigned long __cil_tmp17 ;
4373  int __cil_tmp18 ;
4374  int __cil_tmp19 ;
4375  int __cil_tmp20 ;
4376  int __cil_tmp21 ;
4377  unsigned long __cil_tmp22 ;
4378  unsigned long __cil_tmp23 ;
4379  u8 *__cil_tmp24 ;
4380  void const   *__cil_tmp25 ;
4381  unsigned int __cil_tmp26 ;
4382  unsigned long __cil_tmp27 ;
4383  unsigned long __cil_tmp28 ;
4384  u8 *__cil_tmp29 ;
4385  void *__cil_tmp30 ;
4386  unsigned int __cil_tmp31 ;
4387  unsigned long __cil_tmp32 ;
4388  unsigned long __cil_tmp33 ;
4389  u8 __cil_tmp34 ;
4390  int __cil_tmp35 ;
4391  int __cil_tmp36 ;
4392  unsigned char __cil_tmp37 ;
4393  unsigned long __cil_tmp38 ;
4394  unsigned long __cil_tmp39 ;
4395  u8 __cil_tmp40 ;
4396  int __cil_tmp41 ;
4397  int __cil_tmp42 ;
4398  unsigned char __cil_tmp43 ;
4399  unsigned long __cil_tmp44 ;
4400  unsigned long __cil_tmp45 ;
4401  unsigned long __cil_tmp46 ;
4402  unsigned long __cil_tmp47 ;
4403  u8 __cil_tmp48 ;
4404  int __cil_tmp49 ;
4405  int __cil_tmp50 ;
4406  unsigned char __cil_tmp51 ;
4407  unsigned long __cil_tmp52 ;
4408  unsigned long __cil_tmp53 ;
4409  unsigned long __cil_tmp54 ;
4410  unsigned long __cil_tmp55 ;
4411  u8 __cil_tmp56 ;
4412  int __cil_tmp57 ;
4413  int __cil_tmp58 ;
4414  unsigned char __cil_tmp59 ;
4415  unsigned long __cil_tmp60 ;
4416  unsigned long __cil_tmp61 ;
4417  unsigned long __cil_tmp62 ;
4418  unsigned long __cil_tmp63 ;
4419  unsigned long __cil_tmp64 ;
4420  unsigned long __cil_tmp65 ;
4421  u8 __cil_tmp66 ;
4422  int __cil_tmp67 ;
4423  unsigned long __cil_tmp68 ;
4424  unsigned long __cil_tmp69 ;
4425  u8 __cil_tmp70 ;
4426  int __cil_tmp71 ;
4427  int __cil_tmp72 ;
4428  unsigned char __cil_tmp73 ;
4429  unsigned long __cil_tmp74 ;
4430  unsigned long __cil_tmp75 ;
4431  unsigned int __cil_tmp76 ;
4432  unsigned long __cil_tmp77 ;
4433  unsigned long __cil_tmp78 ;
4434  u8 __cil_tmp79 ;
4435  unsigned long __cil_tmp80 ;
4436  unsigned long __cil_tmp81 ;
4437  unsigned long __cil_tmp82 ;
4438  unsigned long __cil_tmp83 ;
4439  int __cil_tmp84 ;
4440  unsigned long __cil_tmp85 ;
4441  unsigned long __cil_tmp86 ;
4442  unsigned long __cil_tmp87 ;
4443  unsigned long __cil_tmp88 ;
4444  int __cil_tmp89 ;
4445  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp90 ;
4446  unsigned int __cil_tmp91 ;
4447  unsigned int __cil_tmp92 ;
4448  int __cil_tmp93 ;
4449  int __cil_tmp94 ;
4450  long __cil_tmp95 ;
4451  struct device  const  *__cil_tmp96 ;
4452  int __cil_tmp97 ;
4453  unsigned long __cil_tmp98 ;
4454  unsigned long __cil_tmp99 ;
4455  int __cil_tmp100 ;
4456  unsigned long __cil_tmp101 ;
4457  unsigned long __cil_tmp102 ;
4458  int __cil_tmp103 ;
4459  unsigned long __cil_tmp104 ;
4460  unsigned long __cil_tmp105 ;
4461  int __cil_tmp106 ;
4462  unsigned long __cil_tmp107 ;
4463  unsigned long __cil_tmp108 ;
4464  int __cil_tmp109 ;
4465  unsigned long __cil_tmp110 ;
4466  unsigned long __cil_tmp111 ;
4467  int __cil_tmp112 ;
4468  unsigned long __cil_tmp113 ;
4469  unsigned long __cil_tmp114 ;
4470  int __cil_tmp115 ;
4471  struct device  const  *__cil_tmp116 ;
4472
4473  {
4474  {
4475#line 135
4476  tmp___7 = to_spi_device(dev);
4477#line 135
4478  spi = tmp___7;
4479#line 139
4480  __cil_tmp16 = 0 * 1UL;
4481#line 139
4482  __cil_tmp17 = (unsigned long )(txbuf) + __cil_tmp16;
4483#line 139
4484  __cil_tmp18 = 1 << 4;
4485#line 139
4486  __cil_tmp19 = 1 << 7;
4487#line 139
4488  __cil_tmp20 = __cil_tmp19 | __cil_tmp18;
4489#line 139
4490  __cil_tmp21 = __cil_tmp20 | 2;
4491#line 139
4492  *((u8 *)__cil_tmp17) = (u8 )__cil_tmp21;
4493#line 140
4494  __cil_tmp22 = 0 * 1UL;
4495#line 140
4496  __cil_tmp23 = (unsigned long )(txbuf) + __cil_tmp22;
4497#line 140
4498  __cil_tmp24 = (u8 *)__cil_tmp23;
4499#line 140
4500  __cil_tmp25 = (void const   *)__cil_tmp24;
4501#line 140
4502  __cil_tmp26 = (unsigned int )1UL;
4503#line 140
4504  __cil_tmp27 = 0 * 1UL;
4505#line 140
4506  __cil_tmp28 = (unsigned long )(rxbuf) + __cil_tmp27;
4507#line 140
4508  __cil_tmp29 = (u8 *)__cil_tmp28;
4509#line 140
4510  __cil_tmp30 = (void *)__cil_tmp29;
4511#line 140
4512  __cil_tmp31 = (unsigned int )7UL;
4513#line 140
4514  ret = spi_write_then_read(spi, __cil_tmp25, __cil_tmp26, __cil_tmp30, __cil_tmp31);
4515  }
4516#line 142
4517  if (ret < 0) {
4518#line 143
4519    return (ret);
4520  } else {
4521
4522  }
4523  {
4524#line 144
4525  pcf2123_delay_trec();
4526#line 146
4527  __cil_tmp32 = 0 * 1UL;
4528#line 146
4529  __cil_tmp33 = (unsigned long )(rxbuf) + __cil_tmp32;
4530#line 146
4531  __cil_tmp34 = *((u8 *)__cil_tmp33);
4532#line 146
4533  __cil_tmp35 = (int )__cil_tmp34;
4534#line 146
4535  __cil_tmp36 = __cil_tmp35 & 127;
4536#line 146
4537  __cil_tmp37 = (unsigned char )__cil_tmp36;
4538#line 146
4539  tmp___8 = bcd2bin(__cil_tmp37);
4540#line 146
4541  *((int *)tm) = (int )tmp___8;
4542#line 147
4543  __cil_tmp38 = 1 * 1UL;
4544#line 147
4545  __cil_tmp39 = (unsigned long )(rxbuf) + __cil_tmp38;
4546#line 147
4547  __cil_tmp40 = *((u8 *)__cil_tmp39);
4548#line 147
4549  __cil_tmp41 = (int )__cil_tmp40;
4550#line 147
4551  __cil_tmp42 = __cil_tmp41 & 127;
4552#line 147
4553  __cil_tmp43 = (unsigned char )__cil_tmp42;
4554#line 147
4555  tmp___9 = bcd2bin(__cil_tmp43);
4556#line 147
4557  __cil_tmp44 = (unsigned long )tm;
4558#line 147
4559  __cil_tmp45 = __cil_tmp44 + 4;
4560#line 147
4561  *((int *)__cil_tmp45) = (int )tmp___9;
4562#line 148
4563  __cil_tmp46 = 2 * 1UL;
4564#line 148
4565  __cil_tmp47 = (unsigned long )(rxbuf) + __cil_tmp46;
4566#line 148
4567  __cil_tmp48 = *((u8 *)__cil_tmp47);
4568#line 148
4569  __cil_tmp49 = (int )__cil_tmp48;
4570#line 148
4571  __cil_tmp50 = __cil_tmp49 & 63;
4572#line 148
4573  __cil_tmp51 = (unsigned char )__cil_tmp50;
4574#line 148
4575  tmp___10 = bcd2bin(__cil_tmp51);
4576#line 148
4577  __cil_tmp52 = (unsigned long )tm;
4578#line 148
4579  __cil_tmp53 = __cil_tmp52 + 8;
4580#line 148
4581  *((int *)__cil_tmp53) = (int )tmp___10;
4582#line 149
4583  __cil_tmp54 = 3 * 1UL;
4584#line 149
4585  __cil_tmp55 = (unsigned long )(rxbuf) + __cil_tmp54;
4586#line 149
4587  __cil_tmp56 = *((u8 *)__cil_tmp55);
4588#line 149
4589  __cil_tmp57 = (int )__cil_tmp56;
4590#line 149
4591  __cil_tmp58 = __cil_tmp57 & 63;
4592#line 149
4593  __cil_tmp59 = (unsigned char )__cil_tmp58;
4594#line 149
4595  tmp___11 = bcd2bin(__cil_tmp59);
4596#line 149
4597  __cil_tmp60 = (unsigned long )tm;
4598#line 149
4599  __cil_tmp61 = __cil_tmp60 + 12;
4600#line 149
4601  *((int *)__cil_tmp61) = (int )tmp___11;
4602#line 150
4603  __cil_tmp62 = (unsigned long )tm;
4604#line 150
4605  __cil_tmp63 = __cil_tmp62 + 24;
4606#line 150
4607  __cil_tmp64 = 4 * 1UL;
4608#line 150
4609  __cil_tmp65 = (unsigned long )(rxbuf) + __cil_tmp64;
4610#line 150
4611  __cil_tmp66 = *((u8 *)__cil_tmp65);
4612#line 150
4613  __cil_tmp67 = (int )__cil_tmp66;
4614#line 150
4615  *((int *)__cil_tmp63) = __cil_tmp67 & 7;
4616#line 151
4617  __cil_tmp68 = 5 * 1UL;
4618#line 151
4619  __cil_tmp69 = (unsigned long )(rxbuf) + __cil_tmp68;
4620#line 151
4621  __cil_tmp70 = *((u8 *)__cil_tmp69);
4622#line 151
4623  __cil_tmp71 = (int )__cil_tmp70;
4624#line 151
4625  __cil_tmp72 = __cil_tmp71 & 31;
4626#line 151
4627  __cil_tmp73 = (unsigned char )__cil_tmp72;
4628#line 151
4629  tmp___12 = bcd2bin(__cil_tmp73);
4630#line 151
4631  __cil_tmp74 = (unsigned long )tm;
4632#line 151
4633  __cil_tmp75 = __cil_tmp74 + 16;
4634#line 151
4635  __cil_tmp76 = tmp___12 - 1U;
4636#line 151
4637  *((int *)__cil_tmp75) = (int )__cil_tmp76;
4638#line 152
4639  __cil_tmp77 = 6 * 1UL;
4640#line 152
4641  __cil_tmp78 = (unsigned long )(rxbuf) + __cil_tmp77;
4642#line 152
4643  __cil_tmp79 = *((u8 *)__cil_tmp78);
4644#line 152
4645  tmp___13 = bcd2bin(__cil_tmp79);
4646#line 152
4647  __cil_tmp80 = (unsigned long )tm;
4648#line 152
4649  __cil_tmp81 = __cil_tmp80 + 20;
4650#line 152
4651  *((int *)__cil_tmp81) = (int )tmp___13;
4652  }
4653  {
4654#line 153
4655  __cil_tmp82 = (unsigned long )tm;
4656#line 153
4657  __cil_tmp83 = __cil_tmp82 + 20;
4658#line 153
4659  __cil_tmp84 = *((int *)__cil_tmp83);
4660#line 153
4661  if (__cil_tmp84 < 70) {
4662#line 154
4663    __cil_tmp85 = (unsigned long )tm;
4664#line 154
4665    __cil_tmp86 = __cil_tmp85 + 20;
4666#line 154
4667    __cil_tmp87 = (unsigned long )tm;
4668#line 154
4669    __cil_tmp88 = __cil_tmp87 + 20;
4670#line 154
4671    __cil_tmp89 = *((int *)__cil_tmp88);
4672#line 154
4673    *((int *)__cil_tmp86) = __cil_tmp89 + 100;
4674  } else {
4675
4676  }
4677  }
4678  {
4679#line 156
4680  while (1) {
4681    while_continue: /* CIL Label */ ;
4682    {
4683#line 156
4684    while (1) {
4685      while_continue___0: /* CIL Label */ ;
4686      {
4687#line 156
4688      __cil_tmp90 = & descriptor;
4689#line 156
4690      __cil_tmp91 = __cil_tmp90->flags;
4691#line 156
4692      __cil_tmp92 = __cil_tmp91 & 1U;
4693#line 156
4694      __cil_tmp93 = ! __cil_tmp92;
4695#line 156
4696      __cil_tmp94 = ! __cil_tmp93;
4697#line 156
4698      __cil_tmp95 = (long )__cil_tmp94;
4699#line 156
4700      tmp___14 = __builtin_expect(__cil_tmp95, 0L);
4701      }
4702#line 156
4703      if (tmp___14) {
4704        {
4705#line 156
4706        __cil_tmp96 = (struct device  const  *)dev;
4707#line 156
4708        __cil_tmp97 = *((int *)tm);
4709#line 156
4710        __cil_tmp98 = (unsigned long )tm;
4711#line 156
4712        __cil_tmp99 = __cil_tmp98 + 4;
4713#line 156
4714        __cil_tmp100 = *((int *)__cil_tmp99);
4715#line 156
4716        __cil_tmp101 = (unsigned long )tm;
4717#line 156
4718        __cil_tmp102 = __cil_tmp101 + 8;
4719#line 156
4720        __cil_tmp103 = *((int *)__cil_tmp102);
4721#line 156
4722        __cil_tmp104 = (unsigned long )tm;
4723#line 156
4724        __cil_tmp105 = __cil_tmp104 + 12;
4725#line 156
4726        __cil_tmp106 = *((int *)__cil_tmp105);
4727#line 156
4728        __cil_tmp107 = (unsigned long )tm;
4729#line 156
4730        __cil_tmp108 = __cil_tmp107 + 16;
4731#line 156
4732        __cil_tmp109 = *((int *)__cil_tmp108);
4733#line 156
4734        __cil_tmp110 = (unsigned long )tm;
4735#line 156
4736        __cil_tmp111 = __cil_tmp110 + 20;
4737#line 156
4738        __cil_tmp112 = *((int *)__cil_tmp111);
4739#line 156
4740        __cil_tmp113 = (unsigned long )tm;
4741#line 156
4742        __cil_tmp114 = __cil_tmp113 + 24;
4743#line 156
4744        __cil_tmp115 = *((int *)__cil_tmp114);
4745#line 156
4746        __dynamic_dev_dbg(& descriptor, __cil_tmp96, "%s: tm is secs=%d, mins=%d, hours=%d, mday=%d, mon=%d, year=%d, wday=%d\n",
4747                          "pcf2123_rtc_read_time", __cil_tmp97, __cil_tmp100, __cil_tmp103,
4748                          __cil_tmp106, __cil_tmp109, __cil_tmp112, __cil_tmp115);
4749        }
4750      } else {
4751
4752      }
4753#line 156
4754      goto while_break___0;
4755    }
4756    while_break___0: /* CIL Label */ ;
4757    }
4758#line 156
4759    goto while_break;
4760  }
4761  while_break: /* CIL Label */ ;
4762  }
4763  {
4764#line 165
4765  tmp___15 = rtc_valid_tm(tm);
4766  }
4767#line 165
4768  if (tmp___15 < 0) {
4769    {
4770#line 166
4771    __cil_tmp116 = (struct device  const  *)dev;
4772#line 166
4773    dev_err(__cil_tmp116, "retrieved date/time is not valid.\n");
4774    }
4775  } else {
4776
4777  }
4778#line 168
4779  return (0);
4780}
4781}
4782#line 177
4783static int pcf2123_rtc_set_time(struct device *dev , struct rtc_time *tm ) ;
4784#line 177 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
4785static struct _ddebug  __attribute__((__aligned__(8))) descriptor___0  __attribute__((__used__,
4786__section__("__verbose")))  =    {"rtc_pcf2123", "pcf2123_rtc_set_time", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c",
4787    "%s: tm is secs=%d, mins=%d, hours=%d, mday=%d, mon=%d, year=%d, wday=%d\n", 181U,
4788    1U};
4789#line 171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
4790static int pcf2123_rtc_set_time(struct device *dev , struct rtc_time *tm ) 
4791{ struct spi_device *spi ;
4792  struct spi_device *tmp___7 ;
4793  u8 txbuf[8] ;
4794  int ret ;
4795  long tmp___8 ;
4796  int tmp___9 ;
4797  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp9 ;
4798  unsigned int __cil_tmp10 ;
4799  unsigned int __cil_tmp11 ;
4800  int __cil_tmp12 ;
4801  int __cil_tmp13 ;
4802  long __cil_tmp14 ;
4803  struct device  const  *__cil_tmp15 ;
4804  int __cil_tmp16 ;
4805  unsigned long __cil_tmp17 ;
4806  unsigned long __cil_tmp18 ;
4807  int __cil_tmp19 ;
4808  unsigned long __cil_tmp20 ;
4809  unsigned long __cil_tmp21 ;
4810  int __cil_tmp22 ;
4811  unsigned long __cil_tmp23 ;
4812  unsigned long __cil_tmp24 ;
4813  int __cil_tmp25 ;
4814  unsigned long __cil_tmp26 ;
4815  unsigned long __cil_tmp27 ;
4816  int __cil_tmp28 ;
4817  unsigned long __cil_tmp29 ;
4818  unsigned long __cil_tmp30 ;
4819  int __cil_tmp31 ;
4820  unsigned long __cil_tmp32 ;
4821  unsigned long __cil_tmp33 ;
4822  int __cil_tmp34 ;
4823  unsigned long __cil_tmp35 ;
4824  unsigned long __cil_tmp36 ;
4825  int __cil_tmp37 ;
4826  unsigned long __cil_tmp38 ;
4827  unsigned long __cil_tmp39 ;
4828  unsigned long __cil_tmp40 ;
4829  unsigned long __cil_tmp41 ;
4830  u8 *__cil_tmp42 ;
4831  void const   *__cil_tmp43 ;
4832  size_t __cil_tmp44 ;
4833  unsigned long __cil_tmp45 ;
4834  unsigned long __cil_tmp46 ;
4835  int __cil_tmp47 ;
4836  int __cil_tmp48 ;
4837  unsigned long __cil_tmp49 ;
4838  unsigned long __cil_tmp50 ;
4839  int __cil_tmp51 ;
4840  int __cil_tmp52 ;
4841  unsigned int __cil_tmp53 ;
4842  unsigned long __cil_tmp54 ;
4843  unsigned long __cil_tmp55 ;
4844  unsigned long __cil_tmp56 ;
4845  unsigned long __cil_tmp57 ;
4846  int __cil_tmp58 ;
4847  int __cil_tmp59 ;
4848  unsigned int __cil_tmp60 ;
4849  unsigned long __cil_tmp61 ;
4850  unsigned long __cil_tmp62 ;
4851  unsigned long __cil_tmp63 ;
4852  unsigned long __cil_tmp64 ;
4853  int __cil_tmp65 ;
4854  int __cil_tmp66 ;
4855  unsigned int __cil_tmp67 ;
4856  unsigned long __cil_tmp68 ;
4857  unsigned long __cil_tmp69 ;
4858  unsigned long __cil_tmp70 ;
4859  unsigned long __cil_tmp71 ;
4860  int __cil_tmp72 ;
4861  int __cil_tmp73 ;
4862  unsigned int __cil_tmp74 ;
4863  unsigned long __cil_tmp75 ;
4864  unsigned long __cil_tmp76 ;
4865  unsigned long __cil_tmp77 ;
4866  unsigned long __cil_tmp78 ;
4867  int __cil_tmp79 ;
4868  int __cil_tmp80 ;
4869  unsigned long __cil_tmp81 ;
4870  unsigned long __cil_tmp82 ;
4871  unsigned long __cil_tmp83 ;
4872  unsigned long __cil_tmp84 ;
4873  int __cil_tmp85 ;
4874  int __cil_tmp86 ;
4875  int __cil_tmp87 ;
4876  unsigned int __cil_tmp88 ;
4877  unsigned long __cil_tmp89 ;
4878  unsigned long __cil_tmp90 ;
4879  int __cil_tmp91 ;
4880  unsigned long __cil_tmp92 ;
4881  unsigned long __cil_tmp93 ;
4882  unsigned long __cil_tmp94 ;
4883  unsigned long __cil_tmp95 ;
4884  int __cil_tmp96 ;
4885  unsigned long __cil_tmp97 ;
4886  unsigned long __cil_tmp98 ;
4887  unsigned int __cil_tmp99 ;
4888  unsigned long __cil_tmp100 ;
4889  unsigned long __cil_tmp101 ;
4890  u8 *__cil_tmp102 ;
4891  void const   *__cil_tmp103 ;
4892  unsigned long __cil_tmp104 ;
4893  unsigned long __cil_tmp105 ;
4894  int __cil_tmp106 ;
4895  unsigned long __cil_tmp107 ;
4896  unsigned long __cil_tmp108 ;
4897  unsigned long __cil_tmp109 ;
4898  unsigned long __cil_tmp110 ;
4899  u8 *__cil_tmp111 ;
4900  void const   *__cil_tmp112 ;
4901  size_t __cil_tmp113 ;
4902
4903  {
4904  {
4905#line 173
4906  tmp___7 = to_spi_device(dev);
4907#line 173
4908  spi = tmp___7;
4909  }
4910  {
4911#line 177
4912  while (1) {
4913    while_continue: /* CIL Label */ ;
4914    {
4915#line 177
4916    while (1) {
4917      while_continue___0: /* CIL Label */ ;
4918      {
4919#line 177
4920      __cil_tmp9 = & descriptor___0;
4921#line 177
4922      __cil_tmp10 = __cil_tmp9->flags;
4923#line 177
4924      __cil_tmp11 = __cil_tmp10 & 1U;
4925#line 177
4926      __cil_tmp12 = ! __cil_tmp11;
4927#line 177
4928      __cil_tmp13 = ! __cil_tmp12;
4929#line 177
4930      __cil_tmp14 = (long )__cil_tmp13;
4931#line 177
4932      tmp___8 = __builtin_expect(__cil_tmp14, 0L);
4933      }
4934#line 177
4935      if (tmp___8) {
4936        {
4937#line 177
4938        __cil_tmp15 = (struct device  const  *)dev;
4939#line 177
4940        __cil_tmp16 = *((int *)tm);
4941#line 177
4942        __cil_tmp17 = (unsigned long )tm;
4943#line 177
4944        __cil_tmp18 = __cil_tmp17 + 4;
4945#line 177
4946        __cil_tmp19 = *((int *)__cil_tmp18);
4947#line 177
4948        __cil_tmp20 = (unsigned long )tm;
4949#line 177
4950        __cil_tmp21 = __cil_tmp20 + 8;
4951#line 177
4952        __cil_tmp22 = *((int *)__cil_tmp21);
4953#line 177
4954        __cil_tmp23 = (unsigned long )tm;
4955#line 177
4956        __cil_tmp24 = __cil_tmp23 + 12;
4957#line 177
4958        __cil_tmp25 = *((int *)__cil_tmp24);
4959#line 177
4960        __cil_tmp26 = (unsigned long )tm;
4961#line 177
4962        __cil_tmp27 = __cil_tmp26 + 16;
4963#line 177
4964        __cil_tmp28 = *((int *)__cil_tmp27);
4965#line 177
4966        __cil_tmp29 = (unsigned long )tm;
4967#line 177
4968        __cil_tmp30 = __cil_tmp29 + 20;
4969#line 177
4970        __cil_tmp31 = *((int *)__cil_tmp30);
4971#line 177
4972        __cil_tmp32 = (unsigned long )tm;
4973#line 177
4974        __cil_tmp33 = __cil_tmp32 + 24;
4975#line 177
4976        __cil_tmp34 = *((int *)__cil_tmp33);
4977#line 177
4978        __dynamic_dev_dbg(& descriptor___0, __cil_tmp15, "%s: tm is secs=%d, mins=%d, hours=%d, mday=%d, mon=%d, year=%d, wday=%d\n",
4979                          "pcf2123_rtc_set_time", __cil_tmp16, __cil_tmp19, __cil_tmp22,
4980                          __cil_tmp25, __cil_tmp28, __cil_tmp31, __cil_tmp34);
4981        }
4982      } else {
4983
4984      }
4985#line 177
4986      goto while_break___0;
4987    }
4988    while_break___0: /* CIL Label */ ;
4989    }
4990#line 177
4991    goto while_break;
4992  }
4993  while_break: /* CIL Label */ ;
4994  }
4995  {
4996#line 184
4997  __cil_tmp35 = 0 * 1UL;
4998#line 184
4999  __cil_tmp36 = (unsigned long )(txbuf) + __cil_tmp35;
5000#line 184
5001  __cil_tmp37 = 1 << 4;
5002#line 184
5003  *((u8 *)__cil_tmp36) = (u8 )__cil_tmp37;
5004#line 185
5005  __cil_tmp38 = 1 * 1UL;
5006#line 185
5007  __cil_tmp39 = (unsigned long )(txbuf) + __cil_tmp38;
5008#line 185
5009  *((u8 *)__cil_tmp39) = (u8 )32;
5010#line 186
5011  __cil_tmp40 = 0 * 1UL;
5012#line 186
5013  __cil_tmp41 = (unsigned long )(txbuf) + __cil_tmp40;
5014#line 186
5015  __cil_tmp42 = (u8 *)__cil_tmp41;
5016#line 186
5017  __cil_tmp43 = (void const   *)__cil_tmp42;
5018#line 186
5019  __cil_tmp44 = (size_t )2;
5020#line 186
5021  ret = spi_write(spi, __cil_tmp43, __cil_tmp44);
5022  }
5023#line 187
5024  if (ret < 0) {
5025#line 188
5026    return (ret);
5027  } else {
5028
5029  }
5030  {
5031#line 189
5032  pcf2123_delay_trec();
5033#line 192
5034  __cil_tmp45 = 0 * 1UL;
5035#line 192
5036  __cil_tmp46 = (unsigned long )(txbuf) + __cil_tmp45;
5037#line 192
5038  __cil_tmp47 = 1 << 4;
5039#line 192
5040  __cil_tmp48 = __cil_tmp47 | 2;
5041#line 192
5042  *((u8 *)__cil_tmp46) = (u8 )__cil_tmp48;
5043#line 193
5044  __cil_tmp49 = 1 * 1UL;
5045#line 193
5046  __cil_tmp50 = (unsigned long )(txbuf) + __cil_tmp49;
5047#line 193
5048  __cil_tmp51 = *((int *)tm);
5049#line 193
5050  __cil_tmp52 = __cil_tmp51 & 127;
5051#line 193
5052  __cil_tmp53 = (unsigned int )__cil_tmp52;
5053#line 193
5054  *((u8 *)__cil_tmp50) = bin2bcd(__cil_tmp53);
5055#line 194
5056  __cil_tmp54 = 2 * 1UL;
5057#line 194
5058  __cil_tmp55 = (unsigned long )(txbuf) + __cil_tmp54;
5059#line 194
5060  __cil_tmp56 = (unsigned long )tm;
5061#line 194
5062  __cil_tmp57 = __cil_tmp56 + 4;
5063#line 194
5064  __cil_tmp58 = *((int *)__cil_tmp57);
5065#line 194
5066  __cil_tmp59 = __cil_tmp58 & 127;
5067#line 194
5068  __cil_tmp60 = (unsigned int )__cil_tmp59;
5069#line 194
5070  *((u8 *)__cil_tmp55) = bin2bcd(__cil_tmp60);
5071#line 195
5072  __cil_tmp61 = 3 * 1UL;
5073#line 195
5074  __cil_tmp62 = (unsigned long )(txbuf) + __cil_tmp61;
5075#line 195
5076  __cil_tmp63 = (unsigned long )tm;
5077#line 195
5078  __cil_tmp64 = __cil_tmp63 + 8;
5079#line 195
5080  __cil_tmp65 = *((int *)__cil_tmp64);
5081#line 195
5082  __cil_tmp66 = __cil_tmp65 & 63;
5083#line 195
5084  __cil_tmp67 = (unsigned int )__cil_tmp66;
5085#line 195
5086  *((u8 *)__cil_tmp62) = bin2bcd(__cil_tmp67);
5087#line 196
5088  __cil_tmp68 = 4 * 1UL;
5089#line 196
5090  __cil_tmp69 = (unsigned long )(txbuf) + __cil_tmp68;
5091#line 196
5092  __cil_tmp70 = (unsigned long )tm;
5093#line 196
5094  __cil_tmp71 = __cil_tmp70 + 12;
5095#line 196
5096  __cil_tmp72 = *((int *)__cil_tmp71);
5097#line 196
5098  __cil_tmp73 = __cil_tmp72 & 63;
5099#line 196
5100  __cil_tmp74 = (unsigned int )__cil_tmp73;
5101#line 196
5102  *((u8 *)__cil_tmp69) = bin2bcd(__cil_tmp74);
5103#line 197
5104  __cil_tmp75 = 5 * 1UL;
5105#line 197
5106  __cil_tmp76 = (unsigned long )(txbuf) + __cil_tmp75;
5107#line 197
5108  __cil_tmp77 = (unsigned long )tm;
5109#line 197
5110  __cil_tmp78 = __cil_tmp77 + 24;
5111#line 197
5112  __cil_tmp79 = *((int *)__cil_tmp78);
5113#line 197
5114  __cil_tmp80 = __cil_tmp79 & 7;
5115#line 197
5116  *((u8 *)__cil_tmp76) = (u8 )__cil_tmp80;
5117#line 198
5118  __cil_tmp81 = 6 * 1UL;
5119#line 198
5120  __cil_tmp82 = (unsigned long )(txbuf) + __cil_tmp81;
5121#line 198
5122  __cil_tmp83 = (unsigned long )tm;
5123#line 198
5124  __cil_tmp84 = __cil_tmp83 + 16;
5125#line 198
5126  __cil_tmp85 = *((int *)__cil_tmp84);
5127#line 198
5128  __cil_tmp86 = __cil_tmp85 + 1;
5129#line 198
5130  __cil_tmp87 = __cil_tmp86 & 31;
5131#line 198
5132  __cil_tmp88 = (unsigned int )__cil_tmp87;
5133#line 198
5134  *((u8 *)__cil_tmp82) = bin2bcd(__cil_tmp88);
5135  }
5136  {
5137#line 199
5138  __cil_tmp89 = (unsigned long )tm;
5139#line 199
5140  __cil_tmp90 = __cil_tmp89 + 20;
5141#line 199
5142  __cil_tmp91 = *((int *)__cil_tmp90);
5143#line 199
5144  if (__cil_tmp91 < 100) {
5145#line 199
5146    __cil_tmp92 = (unsigned long )tm;
5147#line 199
5148    __cil_tmp93 = __cil_tmp92 + 20;
5149#line 199
5150    tmp___9 = *((int *)__cil_tmp93);
5151  } else {
5152#line 199
5153    __cil_tmp94 = (unsigned long )tm;
5154#line 199
5155    __cil_tmp95 = __cil_tmp94 + 20;
5156#line 199
5157    __cil_tmp96 = *((int *)__cil_tmp95);
5158#line 199
5159    tmp___9 = __cil_tmp96 - 100;
5160  }
5161  }
5162  {
5163#line 199
5164  __cil_tmp97 = 7 * 1UL;
5165#line 199
5166  __cil_tmp98 = (unsigned long )(txbuf) + __cil_tmp97;
5167#line 199
5168  __cil_tmp99 = (unsigned int )tmp___9;
5169#line 199
5170  *((u8 *)__cil_tmp98) = bin2bcd(__cil_tmp99);
5171#line 201
5172  __cil_tmp100 = 0 * 1UL;
5173#line 201
5174  __cil_tmp101 = (unsigned long )(txbuf) + __cil_tmp100;
5175#line 201
5176  __cil_tmp102 = (u8 *)__cil_tmp101;
5177#line 201
5178  __cil_tmp103 = (void const   *)__cil_tmp102;
5179#line 201
5180  ret = spi_write(spi, __cil_tmp103, 8UL);
5181  }
5182#line 202
5183  if (ret < 0) {
5184#line 203
5185    return (ret);
5186  } else {
5187
5188  }
5189  {
5190#line 204
5191  pcf2123_delay_trec();
5192#line 207
5193  __cil_tmp104 = 0 * 1UL;
5194#line 207
5195  __cil_tmp105 = (unsigned long )(txbuf) + __cil_tmp104;
5196#line 207
5197  __cil_tmp106 = 1 << 4;
5198#line 207
5199  *((u8 *)__cil_tmp105) = (u8 )__cil_tmp106;
5200#line 208
5201  __cil_tmp107 = 1 * 1UL;
5202#line 208
5203  __cil_tmp108 = (unsigned long )(txbuf) + __cil_tmp107;
5204#line 208
5205  *((u8 *)__cil_tmp108) = (u8 )0;
5206#line 209
5207  __cil_tmp109 = 0 * 1UL;
5208#line 209
5209  __cil_tmp110 = (unsigned long )(txbuf) + __cil_tmp109;
5210#line 209
5211  __cil_tmp111 = (u8 *)__cil_tmp110;
5212#line 209
5213  __cil_tmp112 = (void const   *)__cil_tmp111;
5214#line 209
5215  __cil_tmp113 = (size_t )2;
5216#line 209
5217  ret = spi_write(spi, __cil_tmp112, __cil_tmp113);
5218  }
5219#line 210
5220  if (ret < 0) {
5221#line 211
5222    return (ret);
5223  } else {
5224
5225  }
5226  {
5227#line 212
5228  pcf2123_delay_trec();
5229  }
5230#line 214
5231  return (0);
5232}
5233}
5234#line 217 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
5235static struct rtc_class_ops  const  pcf2123_rtc_ops  = 
5236#line 217
5237     {(int (*)(struct device * ))0, (void (*)(struct device * ))0, (int (*)(struct device * ,
5238                                                                          unsigned int  ,
5239                                                                          unsigned long  ))0,
5240    & pcf2123_rtc_read_time, & pcf2123_rtc_set_time, (int (*)(struct device * , struct rtc_wkalrm * ))0,
5241    (int (*)(struct device * , struct rtc_wkalrm * ))0, (int (*)(struct device * ,
5242                                                                 struct seq_file * ))0,
5243    (int (*)(struct device * , unsigned long secs ))0, (int (*)(struct device * ,
5244                                                                int data ))0, (int (*)(struct device * ,
5245                                                                                       unsigned int enabled ))0};
5246#line 237
5247static int pcf2123_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
5248__no_instrument_function__)) ;
5249#line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
5250static struct _ddebug  __attribute__((__aligned__(8))) descriptor___1  __attribute__((__used__,
5251__section__("__verbose")))  =    {"rtc_pcf2123", "pcf2123_probe", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c",
5252    "resetting RTC (0x%02X 0x%02X)\n", 238U, 1U};
5253#line 247
5254static int pcf2123_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
5255__no_instrument_function__)) ;
5256#line 247 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
5257static struct _ddebug  __attribute__((__aligned__(8))) descriptor___2  __attribute__((__used__,
5258__section__("__verbose")))  =    {"rtc_pcf2123", "pcf2123_probe", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c",
5259    "stopping RTC (0x%02X 0x%02X)\n", 248U, 1U};
5260#line 256
5261static int pcf2123_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
5262__no_instrument_function__)) ;
5263#line 256 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
5264static struct _ddebug  __attribute__((__aligned__(8))) descriptor___3  __attribute__((__used__,
5265__section__("__verbose")))  =    {"rtc_pcf2123", "pcf2123_probe", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c",
5266    "checking for presence of RTC (0x%02X)\n", 257U, 1U};
5267#line 260
5268static int pcf2123_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
5269__no_instrument_function__)) ;
5270#line 260 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
5271static struct _ddebug  __attribute__((__aligned__(8))) descriptor___4  __attribute__((__used__,
5272__section__("__verbose")))  =    {"rtc_pcf2123", "pcf2123_probe", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c",
5273    "received data from RTC (0x%02X 0x%02X)\n", 261U, 1U};
5274#line 222
5275static int pcf2123_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
5276__no_instrument_function__)) ;
5277#line 222 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
5278static int pcf2123_probe(struct spi_device *spi ) 
5279{ struct rtc_device *rtc ;
5280  struct pcf2123_plat_data *pdata ;
5281  u8 txbuf[2] ;
5282  u8 rxbuf[2] ;
5283  int ret ;
5284  int i ;
5285  void *tmp___7 ;
5286  long tmp___8 ;
5287  long tmp___9 ;
5288  long tmp___10 ;
5289  long tmp___11 ;
5290  long tmp___12 ;
5291  long tmp___13 ;
5292  unsigned long __cil_tmp15 ;
5293  unsigned long __cil_tmp16 ;
5294  unsigned long __cil_tmp17 ;
5295  unsigned long __cil_tmp18 ;
5296  unsigned long __cil_tmp19 ;
5297  int __cil_tmp20 ;
5298  unsigned long __cil_tmp21 ;
5299  unsigned long __cil_tmp22 ;
5300  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp23 ;
5301  unsigned int __cil_tmp24 ;
5302  unsigned int __cil_tmp25 ;
5303  int __cil_tmp26 ;
5304  int __cil_tmp27 ;
5305  long __cil_tmp28 ;
5306  struct device *__cil_tmp29 ;
5307  struct device  const  *__cil_tmp30 ;
5308  unsigned long __cil_tmp31 ;
5309  unsigned long __cil_tmp32 ;
5310  u8 __cil_tmp33 ;
5311  int __cil_tmp34 ;
5312  unsigned long __cil_tmp35 ;
5313  unsigned long __cil_tmp36 ;
5314  u8 __cil_tmp37 ;
5315  int __cil_tmp38 ;
5316  unsigned long __cil_tmp39 ;
5317  unsigned long __cil_tmp40 ;
5318  u8 *__cil_tmp41 ;
5319  void const   *__cil_tmp42 ;
5320  unsigned long __cil_tmp43 ;
5321  unsigned long __cil_tmp44 ;
5322  unsigned long __cil_tmp45 ;
5323  int __cil_tmp46 ;
5324  unsigned long __cil_tmp47 ;
5325  unsigned long __cil_tmp48 ;
5326  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp49 ;
5327  unsigned int __cil_tmp50 ;
5328  unsigned int __cil_tmp51 ;
5329  int __cil_tmp52 ;
5330  int __cil_tmp53 ;
5331  long __cil_tmp54 ;
5332  struct device *__cil_tmp55 ;
5333  struct device  const  *__cil_tmp56 ;
5334  unsigned long __cil_tmp57 ;
5335  unsigned long __cil_tmp58 ;
5336  u8 __cil_tmp59 ;
5337  int __cil_tmp60 ;
5338  unsigned long __cil_tmp61 ;
5339  unsigned long __cil_tmp62 ;
5340  u8 __cil_tmp63 ;
5341  int __cil_tmp64 ;
5342  unsigned long __cil_tmp65 ;
5343  unsigned long __cil_tmp66 ;
5344  u8 *__cil_tmp67 ;
5345  void const   *__cil_tmp68 ;
5346  unsigned long __cil_tmp69 ;
5347  unsigned long __cil_tmp70 ;
5348  unsigned long __cil_tmp71 ;
5349  int __cil_tmp72 ;
5350  int __cil_tmp73 ;
5351  int __cil_tmp74 ;
5352  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp75 ;
5353  unsigned int __cil_tmp76 ;
5354  unsigned int __cil_tmp77 ;
5355  int __cil_tmp78 ;
5356  int __cil_tmp79 ;
5357  long __cil_tmp80 ;
5358  struct device *__cil_tmp81 ;
5359  struct device  const  *__cil_tmp82 ;
5360  unsigned long __cil_tmp83 ;
5361  unsigned long __cil_tmp84 ;
5362  u8 __cil_tmp85 ;
5363  int __cil_tmp86 ;
5364  unsigned long __cil_tmp87 ;
5365  unsigned long __cil_tmp88 ;
5366  u8 *__cil_tmp89 ;
5367  void const   *__cil_tmp90 ;
5368  unsigned int __cil_tmp91 ;
5369  unsigned long __cil_tmp92 ;
5370  unsigned long __cil_tmp93 ;
5371  u8 *__cil_tmp94 ;
5372  void *__cil_tmp95 ;
5373  unsigned long __cil_tmp96 ;
5374  unsigned int __cil_tmp97 ;
5375  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp98 ;
5376  unsigned int __cil_tmp99 ;
5377  unsigned int __cil_tmp100 ;
5378  int __cil_tmp101 ;
5379  int __cil_tmp102 ;
5380  long __cil_tmp103 ;
5381  struct device *__cil_tmp104 ;
5382  struct device  const  *__cil_tmp105 ;
5383  unsigned long __cil_tmp106 ;
5384  unsigned long __cil_tmp107 ;
5385  u8 __cil_tmp108 ;
5386  int __cil_tmp109 ;
5387  unsigned long __cil_tmp110 ;
5388  unsigned long __cil_tmp111 ;
5389  u8 __cil_tmp112 ;
5390  int __cil_tmp113 ;
5391  unsigned long __cil_tmp114 ;
5392  unsigned long __cil_tmp115 ;
5393  u8 __cil_tmp116 ;
5394  int __cil_tmp117 ;
5395  int __cil_tmp118 ;
5396  struct device *__cil_tmp119 ;
5397  struct device  const  *__cil_tmp120 ;
5398  struct device *__cil_tmp121 ;
5399  struct device  const  *__cil_tmp122 ;
5400  struct device *__cil_tmp123 ;
5401  struct device  const  *__cil_tmp124 ;
5402  unsigned long __cil_tmp125 ;
5403  unsigned long __cil_tmp126 ;
5404  u32 __cil_tmp127 ;
5405  u32 __cil_tmp128 ;
5406  u32 __cil_tmp129 ;
5407  unsigned long __cil_tmp130 ;
5408  unsigned long __cil_tmp131 ;
5409  int __cil_tmp132 ;
5410  unsigned long __cil_tmp133 ;
5411  unsigned long __cil_tmp134 ;
5412  unsigned long __cil_tmp135 ;
5413  unsigned long __cil_tmp136 ;
5414  u8 *__cil_tmp137 ;
5415  void const   *__cil_tmp138 ;
5416  unsigned long __cil_tmp139 ;
5417  char const   *__cil_tmp140 ;
5418  struct device *__cil_tmp141 ;
5419  void const   *__cil_tmp142 ;
5420  struct device *__cil_tmp143 ;
5421  struct device  const  *__cil_tmp144 ;
5422  void const   *__cil_tmp145 ;
5423  unsigned long __cil_tmp146 ;
5424  unsigned long __cil_tmp147 ;
5425  unsigned long __cil_tmp148 ;
5426  unsigned long __cil_tmp149 ;
5427  unsigned long __cil_tmp150 ;
5428  unsigned long __cil_tmp151 ;
5429  unsigned long __cil_tmp152 ;
5430  char *__cil_tmp153 ;
5431  unsigned long __cil_tmp154 ;
5432  unsigned long __cil_tmp155 ;
5433  unsigned long __cil_tmp156 ;
5434  unsigned long __cil_tmp157 ;
5435  unsigned long __cil_tmp158 ;
5436  unsigned long __cil_tmp159 ;
5437  unsigned long __cil_tmp160 ;
5438  unsigned long __cil_tmp161 ;
5439  unsigned long __cil_tmp162 ;
5440  unsigned long __cil_tmp163 ;
5441  unsigned long __cil_tmp164 ;
5442  unsigned long __cil_tmp165 ;
5443  unsigned long __cil_tmp166 ;
5444  unsigned long __cil_tmp167 ;
5445  unsigned long __cil_tmp168 ;
5446  unsigned long __cil_tmp169 ;
5447  unsigned long __cil_tmp170 ;
5448  unsigned long __cil_tmp171 ;
5449  char *__cil_tmp172 ;
5450  unsigned long __cil_tmp173 ;
5451  unsigned long __cil_tmp174 ;
5452  unsigned long __cil_tmp175 ;
5453  unsigned long __cil_tmp176 ;
5454  unsigned long __cil_tmp177 ;
5455  unsigned long __cil_tmp178 ;
5456  unsigned long __cil_tmp179 ;
5457  unsigned long __cil_tmp180 ;
5458  unsigned long __cil_tmp181 ;
5459  unsigned long __cil_tmp182 ;
5460  unsigned long __cil_tmp183 ;
5461  unsigned long __cil_tmp184 ;
5462  struct device *__cil_tmp185 ;
5463  unsigned long __cil_tmp186 ;
5464  unsigned long __cil_tmp187 ;
5465  unsigned long __cil_tmp188 ;
5466  unsigned long __cil_tmp189 ;
5467  struct device_attribute *__cil_tmp190 ;
5468  struct device_attribute  const  *__cil_tmp191 ;
5469  struct device *__cil_tmp192 ;
5470  struct device  const  *__cil_tmp193 ;
5471  unsigned long __cil_tmp194 ;
5472  unsigned long __cil_tmp195 ;
5473  unsigned long __cil_tmp196 ;
5474  unsigned long __cil_tmp197 ;
5475  unsigned long __cil_tmp198 ;
5476  unsigned long __cil_tmp199 ;
5477  unsigned long __cil_tmp200 ;
5478  char *__cil_tmp201 ;
5479  struct device *__cil_tmp202 ;
5480  unsigned long __cil_tmp203 ;
5481  unsigned long __cil_tmp204 ;
5482  unsigned long __cil_tmp205 ;
5483  unsigned long __cil_tmp206 ;
5484  struct device_attribute *__cil_tmp207 ;
5485  struct device_attribute  const  *__cil_tmp208 ;
5486  void const   *__cil_tmp209 ;
5487  unsigned long __cil_tmp210 ;
5488  unsigned long __cil_tmp211 ;
5489  unsigned long __cil_tmp212 ;
5490
5491  {
5492  {
5493#line 229
5494  tmp___7 = kzalloc(648UL, 208U);
5495#line 229
5496  pdata = (struct pcf2123_plat_data *)tmp___7;
5497  }
5498#line 230
5499  if (! pdata) {
5500#line 231
5501    return (-12);
5502  } else {
5503
5504  }
5505#line 232
5506  __cil_tmp15 = 0 + 184;
5507#line 232
5508  __cil_tmp16 = (unsigned long )spi;
5509#line 232
5510  __cil_tmp17 = __cil_tmp16 + __cil_tmp15;
5511#line 232
5512  *((void **)__cil_tmp17) = (void *)pdata;
5513#line 235
5514  __cil_tmp18 = 0 * 1UL;
5515#line 235
5516  __cil_tmp19 = (unsigned long )(txbuf) + __cil_tmp18;
5517#line 235
5518  __cil_tmp20 = 1 << 4;
5519#line 235
5520  *((u8 *)__cil_tmp19) = (u8 )__cil_tmp20;
5521#line 236
5522  __cil_tmp21 = 1 * 1UL;
5523#line 236
5524  __cil_tmp22 = (unsigned long )(txbuf) + __cil_tmp21;
5525#line 236
5526  *((u8 *)__cil_tmp22) = (u8 )88;
5527  {
5528#line 237
5529  while (1) {
5530    while_continue: /* CIL Label */ ;
5531    {
5532#line 237
5533    while (1) {
5534      while_continue___0: /* CIL Label */ ;
5535      {
5536#line 237
5537      __cil_tmp23 = & descriptor___1;
5538#line 237
5539      __cil_tmp24 = __cil_tmp23->flags;
5540#line 237
5541      __cil_tmp25 = __cil_tmp24 & 1U;
5542#line 237
5543      __cil_tmp26 = ! __cil_tmp25;
5544#line 237
5545      __cil_tmp27 = ! __cil_tmp26;
5546#line 237
5547      __cil_tmp28 = (long )__cil_tmp27;
5548#line 237
5549      tmp___8 = __builtin_expect(__cil_tmp28, 0L);
5550      }
5551#line 237
5552      if (tmp___8) {
5553        {
5554#line 237
5555        __cil_tmp29 = (struct device *)spi;
5556#line 237
5557        __cil_tmp30 = (struct device  const  *)__cil_tmp29;
5558#line 237
5559        __cil_tmp31 = 0 * 1UL;
5560#line 237
5561        __cil_tmp32 = (unsigned long )(txbuf) + __cil_tmp31;
5562#line 237
5563        __cil_tmp33 = *((u8 *)__cil_tmp32);
5564#line 237
5565        __cil_tmp34 = (int )__cil_tmp33;
5566#line 237
5567        __cil_tmp35 = 1 * 1UL;
5568#line 237
5569        __cil_tmp36 = (unsigned long )(txbuf) + __cil_tmp35;
5570#line 237
5571        __cil_tmp37 = *((u8 *)__cil_tmp36);
5572#line 237
5573        __cil_tmp38 = (int )__cil_tmp37;
5574#line 237
5575        __dynamic_dev_dbg(& descriptor___1, __cil_tmp30, "resetting RTC (0x%02X 0x%02X)\n",
5576                          __cil_tmp34, __cil_tmp38);
5577        }
5578      } else {
5579
5580      }
5581#line 237
5582      goto while_break___0;
5583    }
5584    while_break___0: /* CIL Label */ ;
5585    }
5586#line 237
5587    goto while_break;
5588  }
5589  while_break: /* CIL Label */ ;
5590  }
5591  {
5592#line 239
5593  __cil_tmp39 = 0 * 1UL;
5594#line 239
5595  __cil_tmp40 = (unsigned long )(txbuf) + __cil_tmp39;
5596#line 239
5597  __cil_tmp41 = (u8 *)__cil_tmp40;
5598#line 239
5599  __cil_tmp42 = (void const   *)__cil_tmp41;
5600#line 239
5601  __cil_tmp43 = 2UL * 1UL;
5602#line 239
5603  ret = spi_write(spi, __cil_tmp42, __cil_tmp43);
5604  }
5605#line 240
5606  if (ret < 0) {
5607#line 241
5608    goto kfree_exit;
5609  } else {
5610
5611  }
5612  {
5613#line 242
5614  pcf2123_delay_trec();
5615#line 245
5616  __cil_tmp44 = 0 * 1UL;
5617#line 245
5618  __cil_tmp45 = (unsigned long )(txbuf) + __cil_tmp44;
5619#line 245
5620  __cil_tmp46 = 1 << 4;
5621#line 245
5622  *((u8 *)__cil_tmp45) = (u8 )__cil_tmp46;
5623#line 246
5624  __cil_tmp47 = 1 * 1UL;
5625#line 246
5626  __cil_tmp48 = (unsigned long )(txbuf) + __cil_tmp47;
5627#line 246
5628  *((u8 *)__cil_tmp48) = (u8 )32;
5629  }
5630  {
5631#line 247
5632  while (1) {
5633    while_continue___1: /* CIL Label */ ;
5634    {
5635#line 247
5636    while (1) {
5637      while_continue___2: /* CIL Label */ ;
5638      {
5639#line 247
5640      __cil_tmp49 = & descriptor___2;
5641#line 247
5642      __cil_tmp50 = __cil_tmp49->flags;
5643#line 247
5644      __cil_tmp51 = __cil_tmp50 & 1U;
5645#line 247
5646      __cil_tmp52 = ! __cil_tmp51;
5647#line 247
5648      __cil_tmp53 = ! __cil_tmp52;
5649#line 247
5650      __cil_tmp54 = (long )__cil_tmp53;
5651#line 247
5652      tmp___9 = __builtin_expect(__cil_tmp54, 0L);
5653      }
5654#line 247
5655      if (tmp___9) {
5656        {
5657#line 247
5658        __cil_tmp55 = (struct device *)spi;
5659#line 247
5660        __cil_tmp56 = (struct device  const  *)__cil_tmp55;
5661#line 247
5662        __cil_tmp57 = 0 * 1UL;
5663#line 247
5664        __cil_tmp58 = (unsigned long )(txbuf) + __cil_tmp57;
5665#line 247
5666        __cil_tmp59 = *((u8 *)__cil_tmp58);
5667#line 247
5668        __cil_tmp60 = (int )__cil_tmp59;
5669#line 247
5670        __cil_tmp61 = 1 * 1UL;
5671#line 247
5672        __cil_tmp62 = (unsigned long )(txbuf) + __cil_tmp61;
5673#line 247
5674        __cil_tmp63 = *((u8 *)__cil_tmp62);
5675#line 247
5676        __cil_tmp64 = (int )__cil_tmp63;
5677#line 247
5678        __dynamic_dev_dbg(& descriptor___2, __cil_tmp56, "stopping RTC (0x%02X 0x%02X)\n",
5679                          __cil_tmp60, __cil_tmp64);
5680        }
5681      } else {
5682
5683      }
5684#line 247
5685      goto while_break___2;
5686    }
5687    while_break___2: /* CIL Label */ ;
5688    }
5689#line 247
5690    goto while_break___1;
5691  }
5692  while_break___1: /* CIL Label */ ;
5693  }
5694  {
5695#line 249
5696  __cil_tmp65 = 0 * 1UL;
5697#line 249
5698  __cil_tmp66 = (unsigned long )(txbuf) + __cil_tmp65;
5699#line 249
5700  __cil_tmp67 = (u8 *)__cil_tmp66;
5701#line 249
5702  __cil_tmp68 = (void const   *)__cil_tmp67;
5703#line 249
5704  __cil_tmp69 = 2UL * 1UL;
5705#line 249
5706  ret = spi_write(spi, __cil_tmp68, __cil_tmp69);
5707  }
5708#line 250
5709  if (ret < 0) {
5710#line 251
5711    goto kfree_exit;
5712  } else {
5713
5714  }
5715  {
5716#line 252
5717  pcf2123_delay_trec();
5718#line 255
5719  __cil_tmp70 = 0 * 1UL;
5720#line 255
5721  __cil_tmp71 = (unsigned long )(txbuf) + __cil_tmp70;
5722#line 255
5723  __cil_tmp72 = 1 << 4;
5724#line 255
5725  __cil_tmp73 = 1 << 7;
5726#line 255
5727  __cil_tmp74 = __cil_tmp73 | __cil_tmp72;
5728#line 255
5729  *((u8 *)__cil_tmp71) = (u8 )__cil_tmp74;
5730  }
5731  {
5732#line 256
5733  while (1) {
5734    while_continue___3: /* CIL Label */ ;
5735    {
5736#line 256
5737    while (1) {
5738      while_continue___4: /* CIL Label */ ;
5739      {
5740#line 256
5741      __cil_tmp75 = & descriptor___3;
5742#line 256
5743      __cil_tmp76 = __cil_tmp75->flags;
5744#line 256
5745      __cil_tmp77 = __cil_tmp76 & 1U;
5746#line 256
5747      __cil_tmp78 = ! __cil_tmp77;
5748#line 256
5749      __cil_tmp79 = ! __cil_tmp78;
5750#line 256
5751      __cil_tmp80 = (long )__cil_tmp79;
5752#line 256
5753      tmp___10 = __builtin_expect(__cil_tmp80, 0L);
5754      }
5755#line 256
5756      if (tmp___10) {
5757        {
5758#line 256
5759        __cil_tmp81 = (struct device *)spi;
5760#line 256
5761        __cil_tmp82 = (struct device  const  *)__cil_tmp81;
5762#line 256
5763        __cil_tmp83 = 0 * 1UL;
5764#line 256
5765        __cil_tmp84 = (unsigned long )(txbuf) + __cil_tmp83;
5766#line 256
5767        __cil_tmp85 = *((u8 *)__cil_tmp84);
5768#line 256
5769        __cil_tmp86 = (int )__cil_tmp85;
5770#line 256
5771        __dynamic_dev_dbg(& descriptor___3, __cil_tmp82, "checking for presence of RTC (0x%02X)\n",
5772                          __cil_tmp86);
5773        }
5774      } else {
5775
5776      }
5777#line 256
5778      goto while_break___4;
5779    }
5780    while_break___4: /* CIL Label */ ;
5781    }
5782#line 256
5783    goto while_break___3;
5784  }
5785  while_break___3: /* CIL Label */ ;
5786  }
5787  {
5788#line 258
5789  __cil_tmp87 = 0 * 1UL;
5790#line 258
5791  __cil_tmp88 = (unsigned long )(txbuf) + __cil_tmp87;
5792#line 258
5793  __cil_tmp89 = (u8 *)__cil_tmp88;
5794#line 258
5795  __cil_tmp90 = (void const   *)__cil_tmp89;
5796#line 258
5797  __cil_tmp91 = (unsigned int )1UL;
5798#line 258
5799  __cil_tmp92 = 0 * 1UL;
5800#line 258
5801  __cil_tmp93 = (unsigned long )(rxbuf) + __cil_tmp92;
5802#line 258
5803  __cil_tmp94 = (u8 *)__cil_tmp93;
5804#line 258
5805  __cil_tmp95 = (void *)__cil_tmp94;
5806#line 258
5807  __cil_tmp96 = 2UL * 1UL;
5808#line 258
5809  __cil_tmp97 = (unsigned int )__cil_tmp96;
5810#line 258
5811  ret = spi_write_then_read(spi, __cil_tmp90, __cil_tmp91, __cil_tmp95, __cil_tmp97);
5812  }
5813  {
5814#line 260
5815  while (1) {
5816    while_continue___5: /* CIL Label */ ;
5817    {
5818#line 260
5819    while (1) {
5820      while_continue___6: /* CIL Label */ ;
5821      {
5822#line 260
5823      __cil_tmp98 = & descriptor___4;
5824#line 260
5825      __cil_tmp99 = __cil_tmp98->flags;
5826#line 260
5827      __cil_tmp100 = __cil_tmp99 & 1U;
5828#line 260
5829      __cil_tmp101 = ! __cil_tmp100;
5830#line 260
5831      __cil_tmp102 = ! __cil_tmp101;
5832#line 260
5833      __cil_tmp103 = (long )__cil_tmp102;
5834#line 260
5835      tmp___11 = __builtin_expect(__cil_tmp103, 0L);
5836      }
5837#line 260
5838      if (tmp___11) {
5839        {
5840#line 260
5841        __cil_tmp104 = (struct device *)spi;
5842#line 260
5843        __cil_tmp105 = (struct device  const  *)__cil_tmp104;
5844#line 260
5845        __cil_tmp106 = 0 * 1UL;
5846#line 260
5847        __cil_tmp107 = (unsigned long )(rxbuf) + __cil_tmp106;
5848#line 260
5849        __cil_tmp108 = *((u8 *)__cil_tmp107);
5850#line 260
5851        __cil_tmp109 = (int )__cil_tmp108;
5852#line 260
5853        __cil_tmp110 = 1 * 1UL;
5854#line 260
5855        __cil_tmp111 = (unsigned long )(rxbuf) + __cil_tmp110;
5856#line 260
5857        __cil_tmp112 = *((u8 *)__cil_tmp111);
5858#line 260
5859        __cil_tmp113 = (int )__cil_tmp112;
5860#line 260
5861        __dynamic_dev_dbg(& descriptor___4, __cil_tmp105, "received data from RTC (0x%02X 0x%02X)\n",
5862                          __cil_tmp109, __cil_tmp113);
5863        }
5864      } else {
5865
5866      }
5867#line 260
5868      goto while_break___6;
5869    }
5870    while_break___6: /* CIL Label */ ;
5871    }
5872#line 260
5873    goto while_break___5;
5874  }
5875  while_break___5: /* CIL Label */ ;
5876  }
5877#line 262
5878  if (ret < 0) {
5879#line 263
5880    goto kfree_exit;
5881  } else {
5882
5883  }
5884  {
5885#line 264
5886  pcf2123_delay_trec();
5887  }
5888  {
5889#line 266
5890  __cil_tmp114 = 0 * 1UL;
5891#line 266
5892  __cil_tmp115 = (unsigned long )(rxbuf) + __cil_tmp114;
5893#line 266
5894  __cil_tmp116 = *((u8 *)__cil_tmp115);
5895#line 266
5896  __cil_tmp117 = (int )__cil_tmp116;
5897#line 266
5898  __cil_tmp118 = __cil_tmp117 & 32;
5899#line 266
5900  if (! __cil_tmp118) {
5901    {
5902#line 267
5903    __cil_tmp119 = (struct device *)spi;
5904#line 267
5905    __cil_tmp120 = (struct device  const  *)__cil_tmp119;
5906#line 267
5907    dev_err(__cil_tmp120, "chip not found\n");
5908    }
5909#line 268
5910    goto kfree_exit;
5911  } else {
5912
5913  }
5914  }
5915  {
5916#line 271
5917  __cil_tmp121 = (struct device *)spi;
5918#line 271
5919  __cil_tmp122 = (struct device  const  *)__cil_tmp121;
5920#line 271
5921  _dev_info(__cil_tmp122, "chip found, driver version 0.6\n");
5922#line 272
5923  __cil_tmp123 = (struct device *)spi;
5924#line 272
5925  __cil_tmp124 = (struct device  const  *)__cil_tmp123;
5926#line 272
5927  __cil_tmp125 = (unsigned long )spi;
5928#line 272
5929  __cil_tmp126 = __cil_tmp125 + 776;
5930#line 272
5931  __cil_tmp127 = *((u32 *)__cil_tmp126);
5932#line 272
5933  __cil_tmp128 = __cil_tmp127 + 500U;
5934#line 272
5935  __cil_tmp129 = __cil_tmp128 / 1000U;
5936#line 272
5937  _dev_info(__cil_tmp124, "spiclk %u KHz.\n", __cil_tmp129);
5938#line 276
5939  __cil_tmp130 = 0 * 1UL;
5940#line 276
5941  __cil_tmp131 = (unsigned long )(txbuf) + __cil_tmp130;
5942#line 276
5943  __cil_tmp132 = 1 << 4;
5944#line 276
5945  *((u8 *)__cil_tmp131) = (u8 )__cil_tmp132;
5946#line 277
5947  __cil_tmp133 = 1 * 1UL;
5948#line 277
5949  __cil_tmp134 = (unsigned long )(txbuf) + __cil_tmp133;
5950#line 277
5951  *((u8 *)__cil_tmp134) = (u8 )0;
5952#line 278
5953  __cil_tmp135 = 0 * 1UL;
5954#line 278
5955  __cil_tmp136 = (unsigned long )(txbuf) + __cil_tmp135;
5956#line 278
5957  __cil_tmp137 = (u8 *)__cil_tmp136;
5958#line 278
5959  __cil_tmp138 = (void const   *)__cil_tmp137;
5960#line 278
5961  ret = spi_write(spi, __cil_tmp138, 2UL);
5962  }
5963#line 279
5964  if (ret < 0) {
5965#line 280
5966    goto kfree_exit;
5967  } else {
5968
5969  }
5970  {
5971#line 281
5972  pcf2123_delay_trec();
5973#line 284
5974  __cil_tmp139 = (unsigned long )(& pcf2123_driver) + 48;
5975#line 284
5976  __cil_tmp140 = *((char const   **)__cil_tmp139);
5977#line 284
5978  __cil_tmp141 = (struct device *)spi;
5979#line 284
5980  rtc = rtc_device_register(__cil_tmp140, __cil_tmp141, & pcf2123_rtc_ops, & __this_module);
5981#line 287
5982  __cil_tmp142 = (void const   *)rtc;
5983#line 287
5984  tmp___13 = (long )IS_ERR(__cil_tmp142);
5985  }
5986#line 287
5987  if (tmp___13) {
5988    {
5989#line 288
5990    __cil_tmp143 = (struct device *)spi;
5991#line 288
5992    __cil_tmp144 = (struct device  const  *)__cil_tmp143;
5993#line 288
5994    dev_err(__cil_tmp144, "failed to register.\n");
5995#line 289
5996    __cil_tmp145 = (void const   *)rtc;
5997#line 289
5998    tmp___12 = (long )PTR_ERR(__cil_tmp145);
5999#line 289
6000    ret = (int )tmp___12;
6001    }
6002#line 290
6003    goto kfree_exit;
6004  } else {
6005
6006  }
6007#line 293
6008  *((struct rtc_device **)pdata) = rtc;
6009#line 295
6010  i = 0;
6011  {
6012#line 295
6013  while (1) {
6014    while_continue___7: /* CIL Label */ ;
6015#line 295
6016    if (i < 16) {
6017
6018    } else {
6019#line 295
6020      goto while_break___7;
6021    }
6022    {
6023#line 296
6024    __cil_tmp146 = 0 * 1UL;
6025#line 296
6026    __cil_tmp147 = 32 + __cil_tmp146;
6027#line 296
6028    __cil_tmp148 = i * 40UL;
6029#line 296
6030    __cil_tmp149 = __cil_tmp148 + __cil_tmp147;
6031#line 296
6032    __cil_tmp150 = 8 + __cil_tmp149;
6033#line 296
6034    __cil_tmp151 = (unsigned long )pdata;
6035#line 296
6036    __cil_tmp152 = __cil_tmp151 + __cil_tmp150;
6037#line 296
6038    __cil_tmp153 = (char *)__cil_tmp152;
6039#line 296
6040    sprintf(__cil_tmp153, "%1x", i);
6041#line 297
6042    __cil_tmp154 = 0 + 8;
6043#line 297
6044    __cil_tmp155 = 0 + __cil_tmp154;
6045#line 297
6046    __cil_tmp156 = i * 40UL;
6047#line 297
6048    __cil_tmp157 = __cil_tmp156 + __cil_tmp155;
6049#line 297
6050    __cil_tmp158 = 8 + __cil_tmp157;
6051#line 297
6052    __cil_tmp159 = (unsigned long )pdata;
6053#line 297
6054    __cil_tmp160 = __cil_tmp159 + __cil_tmp158;
6055#line 297
6056    *((umode_t *)__cil_tmp160) = (umode_t )420;
6057#line 298
6058    __cil_tmp161 = i * 40UL;
6059#line 298
6060    __cil_tmp162 = 8 + __cil_tmp161;
6061#line 298
6062    __cil_tmp163 = (unsigned long )pdata;
6063#line 298
6064    __cil_tmp164 = __cil_tmp163 + __cil_tmp162;
6065#line 298
6066    __cil_tmp165 = 0 * 1UL;
6067#line 298
6068    __cil_tmp166 = 32 + __cil_tmp165;
6069#line 298
6070    __cil_tmp167 = i * 40UL;
6071#line 298
6072    __cil_tmp168 = __cil_tmp167 + __cil_tmp166;
6073#line 298
6074    __cil_tmp169 = 8 + __cil_tmp168;
6075#line 298
6076    __cil_tmp170 = (unsigned long )pdata;
6077#line 298
6078    __cil_tmp171 = __cil_tmp170 + __cil_tmp169;
6079#line 298
6080    __cil_tmp172 = (char *)__cil_tmp171;
6081#line 298
6082    *((char const   **)__cil_tmp164) = (char const   *)__cil_tmp172;
6083#line 299
6084    __cil_tmp173 = 0 + 16;
6085#line 299
6086    __cil_tmp174 = i * 40UL;
6087#line 299
6088    __cil_tmp175 = __cil_tmp174 + __cil_tmp173;
6089#line 299
6090    __cil_tmp176 = 8 + __cil_tmp175;
6091#line 299
6092    __cil_tmp177 = (unsigned long )pdata;
6093#line 299
6094    __cil_tmp178 = __cil_tmp177 + __cil_tmp176;
6095#line 299
6096    *((ssize_t (**)(struct device *dev , struct device_attribute *attr , char *buf ))__cil_tmp178) = & pcf2123_show;
6097#line 300
6098    __cil_tmp179 = 0 + 24;
6099#line 300
6100    __cil_tmp180 = i * 40UL;
6101#line 300
6102    __cil_tmp181 = __cil_tmp180 + __cil_tmp179;
6103#line 300
6104    __cil_tmp182 = 8 + __cil_tmp181;
6105#line 300
6106    __cil_tmp183 = (unsigned long )pdata;
6107#line 300
6108    __cil_tmp184 = __cil_tmp183 + __cil_tmp182;
6109#line 300
6110    *((ssize_t (**)(struct device *dev , struct device_attribute *attr , char const   *buf ,
6111                    size_t count ))__cil_tmp184) = & pcf2123_store;
6112#line 301
6113    __cil_tmp185 = (struct device *)spi;
6114#line 301
6115    __cil_tmp186 = i * 40UL;
6116#line 301
6117    __cil_tmp187 = 8 + __cil_tmp186;
6118#line 301
6119    __cil_tmp188 = (unsigned long )pdata;
6120#line 301
6121    __cil_tmp189 = __cil_tmp188 + __cil_tmp187;
6122#line 301
6123    __cil_tmp190 = (struct device_attribute *)__cil_tmp189;
6124#line 301
6125    __cil_tmp191 = (struct device_attribute  const  *)__cil_tmp190;
6126#line 301
6127    ret = device_create_file(__cil_tmp185, __cil_tmp191);
6128    }
6129#line 302
6130    if (ret) {
6131      {
6132#line 303
6133      __cil_tmp192 = (struct device *)spi;
6134#line 303
6135      __cil_tmp193 = (struct device  const  *)__cil_tmp192;
6136#line 303
6137      __cil_tmp194 = 0 * 1UL;
6138#line 303
6139      __cil_tmp195 = 32 + __cil_tmp194;
6140#line 303
6141      __cil_tmp196 = i * 40UL;
6142#line 303
6143      __cil_tmp197 = __cil_tmp196 + __cil_tmp195;
6144#line 303
6145      __cil_tmp198 = 8 + __cil_tmp197;
6146#line 303
6147      __cil_tmp199 = (unsigned long )pdata;
6148#line 303
6149      __cil_tmp200 = __cil_tmp199 + __cil_tmp198;
6150#line 303
6151      __cil_tmp201 = (char *)__cil_tmp200;
6152#line 303
6153      dev_err(__cil_tmp193, "Unable to create sysfs %s\n", __cil_tmp201);
6154      }
6155#line 305
6156      goto sysfs_exit;
6157    } else {
6158
6159    }
6160#line 295
6161    i = i + 1;
6162  }
6163  while_break___7: /* CIL Label */ ;
6164  }
6165#line 309
6166  return (0);
6167  sysfs_exit: 
6168#line 312
6169  i = i - 1;
6170  {
6171#line 312
6172  while (1) {
6173    while_continue___8: /* CIL Label */ ;
6174#line 312
6175    if (i >= 0) {
6176
6177    } else {
6178#line 312
6179      goto while_break___8;
6180    }
6181    {
6182#line 313
6183    __cil_tmp202 = (struct device *)spi;
6184#line 313
6185    __cil_tmp203 = i * 40UL;
6186#line 313
6187    __cil_tmp204 = 8 + __cil_tmp203;
6188#line 313
6189    __cil_tmp205 = (unsigned long )pdata;
6190#line 313
6191    __cil_tmp206 = __cil_tmp205 + __cil_tmp204;
6192#line 313
6193    __cil_tmp207 = (struct device_attribute *)__cil_tmp206;
6194#line 313
6195    __cil_tmp208 = (struct device_attribute  const  *)__cil_tmp207;
6196#line 313
6197    device_remove_file(__cil_tmp202, __cil_tmp208);
6198#line 312
6199    i = i - 1;
6200    }
6201  }
6202  while_break___8: /* CIL Label */ ;
6203  }
6204  kfree_exit: 
6205  {
6206#line 316
6207  __cil_tmp209 = (void const   *)pdata;
6208#line 316
6209  kfree(__cil_tmp209);
6210#line 317
6211  __cil_tmp210 = 0 + 184;
6212#line 317
6213  __cil_tmp211 = (unsigned long )spi;
6214#line 317
6215  __cil_tmp212 = __cil_tmp211 + __cil_tmp210;
6216#line 317
6217  *((void **)__cil_tmp212) = (void *)0;
6218  }
6219#line 318
6220  return (ret);
6221}
6222}
6223#line 321
6224static int pcf2123_remove(struct spi_device *spi )  __attribute__((__section__(".devexit.text"),
6225__no_instrument_function__)) ;
6226#line 321 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6227static int pcf2123_remove(struct spi_device *spi ) 
6228{ struct pcf2123_plat_data *pdata ;
6229  int i ;
6230  struct rtc_device *rtc ;
6231  unsigned long __cil_tmp5 ;
6232  unsigned long __cil_tmp6 ;
6233  unsigned long __cil_tmp7 ;
6234  void *__cil_tmp8 ;
6235  unsigned long __cil_tmp9 ;
6236  unsigned long __cil_tmp10 ;
6237  unsigned long __cil_tmp11 ;
6238  unsigned long __cil_tmp12 ;
6239  unsigned long __cil_tmp13 ;
6240  unsigned long __cil_tmp14 ;
6241  unsigned long __cil_tmp15 ;
6242  struct device *__cil_tmp16 ;
6243  unsigned long __cil_tmp17 ;
6244  unsigned long __cil_tmp18 ;
6245  unsigned long __cil_tmp19 ;
6246  unsigned long __cil_tmp20 ;
6247  struct device_attribute *__cil_tmp21 ;
6248  struct device_attribute  const  *__cil_tmp22 ;
6249  void const   *__cil_tmp23 ;
6250
6251  {
6252#line 323
6253  __cil_tmp5 = 0 + 184;
6254#line 323
6255  __cil_tmp6 = (unsigned long )spi;
6256#line 323
6257  __cil_tmp7 = __cil_tmp6 + __cil_tmp5;
6258#line 323
6259  __cil_tmp8 = *((void **)__cil_tmp7);
6260#line 323
6261  pdata = (struct pcf2123_plat_data *)__cil_tmp8;
6262#line 326
6263  if (pdata) {
6264#line 327
6265    rtc = *((struct rtc_device **)pdata);
6266#line 329
6267    if (rtc) {
6268      {
6269#line 330
6270      rtc_device_unregister(rtc);
6271      }
6272    } else {
6273
6274    }
6275#line 331
6276    i = 0;
6277    {
6278#line 331
6279    while (1) {
6280      while_continue: /* CIL Label */ ;
6281#line 331
6282      if (i < 16) {
6283
6284      } else {
6285#line 331
6286        goto while_break;
6287      }
6288      {
6289#line 332
6290      __cil_tmp9 = 0 * 1UL;
6291#line 332
6292      __cil_tmp10 = 32 + __cil_tmp9;
6293#line 332
6294      __cil_tmp11 = i * 40UL;
6295#line 332
6296      __cil_tmp12 = __cil_tmp11 + __cil_tmp10;
6297#line 332
6298      __cil_tmp13 = 8 + __cil_tmp12;
6299#line 332
6300      __cil_tmp14 = (unsigned long )pdata;
6301#line 332
6302      __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
6303#line 332
6304      if (*((char *)__cil_tmp15)) {
6305        {
6306#line 333
6307        __cil_tmp16 = (struct device *)spi;
6308#line 333
6309        __cil_tmp17 = i * 40UL;
6310#line 333
6311        __cil_tmp18 = 8 + __cil_tmp17;
6312#line 333
6313        __cil_tmp19 = (unsigned long )pdata;
6314#line 333
6315        __cil_tmp20 = __cil_tmp19 + __cil_tmp18;
6316#line 333
6317        __cil_tmp21 = (struct device_attribute *)__cil_tmp20;
6318#line 333
6319        __cil_tmp22 = (struct device_attribute  const  *)__cil_tmp21;
6320#line 333
6321        device_remove_file(__cil_tmp16, __cil_tmp22);
6322        }
6323      } else {
6324
6325      }
6326      }
6327#line 331
6328      i = i + 1;
6329    }
6330    while_break: /* CIL Label */ ;
6331    }
6332    {
6333#line 335
6334    __cil_tmp23 = (void const   *)pdata;
6335#line 335
6336    kfree(__cil_tmp23);
6337    }
6338  } else {
6339
6340  }
6341#line 338
6342  return (0);
6343}
6344}
6345#line 341 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6346static struct spi_driver pcf2123_driver  =    {(struct spi_device_id  const  *)0, & pcf2123_probe, & pcf2123_remove, (void (*)(struct spi_device *spi ))0,
6347    (int (*)(struct spi_device *spi , pm_message_t mesg ))0, (int (*)(struct spi_device *spi ))0,
6348    {"rtc-pcf2123", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
6349     (struct of_device_id  const  *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
6350     (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
6351     (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
6352     (struct driver_private *)0}};
6353#line 350
6354static int pcf2123_driver_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
6355#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6356static int pcf2123_driver_init(void) 
6357{ int tmp___7 ;
6358
6359  {
6360  {
6361#line 350
6362  tmp___7 = spi_register_driver(& pcf2123_driver);
6363  }
6364#line 350
6365  return (tmp___7);
6366}
6367}
6368#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6369int init_module(void) 
6370{ int tmp___7 ;
6371
6372  {
6373  {
6374#line 350
6375  tmp___7 = pcf2123_driver_init();
6376  }
6377#line 350
6378  return (tmp___7);
6379}
6380}
6381#line 350
6382static void pcf2123_driver_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
6383#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6384static void pcf2123_driver_exit(void) 
6385{ 
6386
6387  {
6388  {
6389#line 350
6390  spi_unregister_driver(& pcf2123_driver);
6391  }
6392#line 350
6393  return;
6394}
6395}
6396#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6397void cleanup_module(void) 
6398{ 
6399
6400  {
6401  {
6402#line 350
6403  pcf2123_driver_exit();
6404  }
6405#line 350
6406  return;
6407}
6408}
6409#line 352 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6410static char const   __mod_author352[48]  __attribute__((__used__, __unused__, __section__(".modinfo"),
6411__aligned__(1)))  = 
6412#line 352
6413  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
6414        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'C', 
6415        (char const   )'h',      (char const   )'r',      (char const   )'i',      (char const   )'s', 
6416        (char const   )' ',      (char const   )'V',      (char const   )'e',      (char const   )'r', 
6417        (char const   )'g',      (char const   )'e',      (char const   )'s',      (char const   )' ', 
6418        (char const   )'<',      (char const   )'c',      (char const   )'h',      (char const   )'r', 
6419        (char const   )'i',      (char const   )'s',      (char const   )'v',      (char const   )'@', 
6420        (char const   )'c',      (char const   )'y',      (char const   )'b',      (char const   )'e', 
6421        (char const   )'r',      (char const   )'s',      (char const   )'w',      (char const   )'i', 
6422        (char const   )'t',      (char const   )'c',      (char const   )'h',      (char const   )'i', 
6423        (char const   )'n',      (char const   )'g',      (char const   )'.',      (char const   )'c', 
6424        (char const   )'o',      (char const   )'m',      (char const   )'>',      (char const   )'\000'};
6425#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6426static char const   __mod_description353[35]  __attribute__((__used__, __unused__,
6427__section__(".modinfo"), __aligned__(1)))  = 
6428#line 353
6429  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
6430        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
6431        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
6432        (char const   )'N',      (char const   )'X',      (char const   )'P',      (char const   )' ', 
6433        (char const   )'P',      (char const   )'C',      (char const   )'F',      (char const   )'2', 
6434        (char const   )'1',      (char const   )'2',      (char const   )'3',      (char const   )' ', 
6435        (char const   )'R',      (char const   )'T',      (char const   )'C',      (char const   )' ', 
6436        (char const   )'d',      (char const   )'r',      (char const   )'i',      (char const   )'v', 
6437        (char const   )'e',      (char const   )'r',      (char const   )'\000'};
6438#line 354 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6439static char const   __mod_license354[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
6440__aligned__(1)))  = 
6441#line 354
6442  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
6443        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
6444        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
6445#line 355 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6446static char const   __mod_version355[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
6447__aligned__(1)))  = 
6448#line 355
6449  {      (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )'s', 
6450        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
6451        (char const   )'0',      (char const   )'.',      (char const   )'6',      (char const   )'\000'};
6452#line 373
6453void ldv_check_final_state(void) ;
6454#line 376
6455extern void ldv_check_return_value(int res ) ;
6456#line 379
6457extern void ldv_initialize(void) ;
6458#line 382
6459extern int __VERIFIER_nondet_int(void) ;
6460#line 385 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6461int LDV_IN_INTERRUPT  ;
6462#line 452 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6463static int res_pcf2123_probe_5  ;
6464#line 388 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6465void main(void) 
6466{ struct device *var_group1 ;
6467  struct rtc_time *var_group2 ;
6468  struct spi_device *var_group3 ;
6469  int ldv_s_pcf2123_driver_spi_driver ;
6470  int tmp___7 ;
6471  int tmp___8 ;
6472  int __cil_tmp7 ;
6473
6474  {
6475  {
6476#line 460
6477  LDV_IN_INTERRUPT = 1;
6478#line 469
6479  ldv_initialize();
6480#line 472
6481  ldv_s_pcf2123_driver_spi_driver = 0;
6482  }
6483  {
6484#line 475
6485  while (1) {
6486    while_continue: /* CIL Label */ ;
6487    {
6488#line 475
6489    tmp___8 = __VERIFIER_nondet_int();
6490    }
6491#line 475
6492    if (tmp___8) {
6493
6494    } else {
6495      {
6496#line 475
6497      __cil_tmp7 = ldv_s_pcf2123_driver_spi_driver == 0;
6498#line 475
6499      if (! __cil_tmp7) {
6500
6501      } else {
6502#line 475
6503        goto while_break;
6504      }
6505      }
6506    }
6507    {
6508#line 479
6509    tmp___7 = __VERIFIER_nondet_int();
6510    }
6511#line 481
6512    if (tmp___7 == 0) {
6513#line 481
6514      goto case_0;
6515    } else
6516#line 511
6517    if (tmp___7 == 1) {
6518#line 511
6519      goto case_1;
6520    } else
6521#line 541
6522    if (tmp___7 == 2) {
6523#line 541
6524      goto case_2;
6525    } else {
6526      {
6527#line 574
6528      goto switch_default;
6529#line 479
6530      if (0) {
6531        case_0: /* CIL Label */ 
6532        {
6533#line 503
6534        pcf2123_rtc_read_time(var_group1, var_group2);
6535        }
6536#line 510
6537        goto switch_break;
6538        case_1: /* CIL Label */ 
6539        {
6540#line 533
6541        pcf2123_rtc_set_time(var_group1, var_group2);
6542        }
6543#line 540
6544        goto switch_break;
6545        case_2: /* CIL Label */ 
6546#line 544
6547        if (ldv_s_pcf2123_driver_spi_driver == 0) {
6548          {
6549#line 563
6550          res_pcf2123_probe_5 = pcf2123_probe(var_group3);
6551#line 564
6552          ldv_check_return_value(res_pcf2123_probe_5);
6553          }
6554#line 565
6555          if (res_pcf2123_probe_5) {
6556#line 566
6557            goto ldv_module_exit;
6558          } else {
6559
6560          }
6561#line 567
6562          ldv_s_pcf2123_driver_spi_driver = 0;
6563        } else {
6564
6565        }
6566#line 573
6567        goto switch_break;
6568        switch_default: /* CIL Label */ 
6569#line 574
6570        goto switch_break;
6571      } else {
6572        switch_break: /* CIL Label */ ;
6573      }
6574      }
6575    }
6576  }
6577  while_break: /* CIL Label */ ;
6578  }
6579  ldv_module_exit: 
6580  {
6581#line 583
6582  ldv_check_final_state();
6583  }
6584#line 586
6585  return;
6586}
6587}
6588#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6589void ldv_blast_assert(void) 
6590{ 
6591
6592  {
6593  ERROR: 
6594#line 6
6595  goto ERROR;
6596}
6597}
6598#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6599extern int __VERIFIER_nondet_int(void) ;
6600#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6601int ldv_mutex  =    1;
6602#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6603int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
6604{ int nondetermined ;
6605
6606  {
6607#line 29
6608  if (ldv_mutex == 1) {
6609
6610  } else {
6611    {
6612#line 29
6613    ldv_blast_assert();
6614    }
6615  }
6616  {
6617#line 32
6618  nondetermined = __VERIFIER_nondet_int();
6619  }
6620#line 35
6621  if (nondetermined) {
6622#line 38
6623    ldv_mutex = 2;
6624#line 40
6625    return (0);
6626  } else {
6627#line 45
6628    return (-4);
6629  }
6630}
6631}
6632#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6633int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
6634{ int nondetermined ;
6635
6636  {
6637#line 57
6638  if (ldv_mutex == 1) {
6639
6640  } else {
6641    {
6642#line 57
6643    ldv_blast_assert();
6644    }
6645  }
6646  {
6647#line 60
6648  nondetermined = __VERIFIER_nondet_int();
6649  }
6650#line 63
6651  if (nondetermined) {
6652#line 66
6653    ldv_mutex = 2;
6654#line 68
6655    return (0);
6656  } else {
6657#line 73
6658    return (-4);
6659  }
6660}
6661}
6662#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6663int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
6664{ int atomic_value_after_dec ;
6665
6666  {
6667#line 83
6668  if (ldv_mutex == 1) {
6669
6670  } else {
6671    {
6672#line 83
6673    ldv_blast_assert();
6674    }
6675  }
6676  {
6677#line 86
6678  atomic_value_after_dec = __VERIFIER_nondet_int();
6679  }
6680#line 89
6681  if (atomic_value_after_dec == 0) {
6682#line 92
6683    ldv_mutex = 2;
6684#line 94
6685    return (1);
6686  } else {
6687
6688  }
6689#line 98
6690  return (0);
6691}
6692}
6693#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6694void mutex_lock(struct mutex *lock ) 
6695{ 
6696
6697  {
6698#line 108
6699  if (ldv_mutex == 1) {
6700
6701  } else {
6702    {
6703#line 108
6704    ldv_blast_assert();
6705    }
6706  }
6707#line 110
6708  ldv_mutex = 2;
6709#line 111
6710  return;
6711}
6712}
6713#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6714int mutex_trylock(struct mutex *lock ) 
6715{ int nondetermined ;
6716
6717  {
6718#line 121
6719  if (ldv_mutex == 1) {
6720
6721  } else {
6722    {
6723#line 121
6724    ldv_blast_assert();
6725    }
6726  }
6727  {
6728#line 124
6729  nondetermined = __VERIFIER_nondet_int();
6730  }
6731#line 127
6732  if (nondetermined) {
6733#line 130
6734    ldv_mutex = 2;
6735#line 132
6736    return (1);
6737  } else {
6738#line 137
6739    return (0);
6740  }
6741}
6742}
6743#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6744void mutex_unlock(struct mutex *lock ) 
6745{ 
6746
6747  {
6748#line 147
6749  if (ldv_mutex == 2) {
6750
6751  } else {
6752    {
6753#line 147
6754    ldv_blast_assert();
6755    }
6756  }
6757#line 149
6758  ldv_mutex = 1;
6759#line 150
6760  return;
6761}
6762}
6763#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6764void ldv_check_final_state(void) 
6765{ 
6766
6767  {
6768#line 156
6769  if (ldv_mutex == 1) {
6770
6771  } else {
6772    {
6773#line 156
6774    ldv_blast_assert();
6775    }
6776  }
6777#line 157
6778  return;
6779}
6780}
6781#line 595 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6249/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-pcf2123.c.common.c"
6782long s__builtin_expect(long val , long res ) 
6783{ 
6784
6785  {
6786#line 596
6787  return (val);
6788}
6789}