Showing error 596

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-ds1390.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 4936
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 202 "include/linux/types.h"
  89typedef unsigned int gfp_t;
  90#line 203 "include/linux/types.h"
  91typedef unsigned int fmode_t;
  92#line 219 "include/linux/types.h"
  93struct __anonstruct_atomic_t_7 {
  94   int counter ;
  95};
  96#line 219 "include/linux/types.h"
  97typedef struct __anonstruct_atomic_t_7 atomic_t;
  98#line 224 "include/linux/types.h"
  99struct __anonstruct_atomic64_t_8 {
 100   long counter ;
 101};
 102#line 224 "include/linux/types.h"
 103typedef struct __anonstruct_atomic64_t_8 atomic64_t;
 104#line 229 "include/linux/types.h"
 105struct list_head {
 106   struct list_head *next ;
 107   struct list_head *prev ;
 108};
 109#line 233
 110struct hlist_node;
 111#line 233 "include/linux/types.h"
 112struct hlist_head {
 113   struct hlist_node *first ;
 114};
 115#line 237 "include/linux/types.h"
 116struct hlist_node {
 117   struct hlist_node *next ;
 118   struct hlist_node **pprev ;
 119};
 120#line 253 "include/linux/types.h"
 121struct rcu_head {
 122   struct rcu_head *next ;
 123   void (*func)(struct rcu_head *head ) ;
 124};
 125#line 146 "include/linux/init.h"
 126typedef void (*ctor_fn_t)(void);
 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 47 "include/linux/dynamic_debug.h"
 132struct device;
 133#line 47
 134struct device;
 135#line 135 "include/linux/kernel.h"
 136struct completion;
 137#line 135
 138struct completion;
 139#line 136
 140struct pt_regs;
 141#line 136
 142struct pt_regs;
 143#line 349
 144struct pid;
 145#line 349
 146struct pid;
 147#line 12 "include/linux/thread_info.h"
 148struct timespec;
 149#line 12
 150struct timespec;
 151#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 152struct page;
 153#line 18
 154struct page;
 155#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 156struct task_struct;
 157#line 20
 158struct task_struct;
 159#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 160struct task_struct;
 161#line 8
 162struct mm_struct;
 163#line 8
 164struct mm_struct;
 165#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 166struct pt_regs {
 167   unsigned long r15 ;
 168   unsigned long r14 ;
 169   unsigned long r13 ;
 170   unsigned long r12 ;
 171   unsigned long bp ;
 172   unsigned long bx ;
 173   unsigned long r11 ;
 174   unsigned long r10 ;
 175   unsigned long r9 ;
 176   unsigned long r8 ;
 177   unsigned long ax ;
 178   unsigned long cx ;
 179   unsigned long dx ;
 180   unsigned long si ;
 181   unsigned long di ;
 182   unsigned long orig_ax ;
 183   unsigned long ip ;
 184   unsigned long cs ;
 185   unsigned long flags ;
 186   unsigned long sp ;
 187   unsigned long ss ;
 188};
 189#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 190struct __anonstruct____missing_field_name_15 {
 191   unsigned int a ;
 192   unsigned int b ;
 193};
 194#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 195struct __anonstruct____missing_field_name_16 {
 196   u16 limit0 ;
 197   u16 base0 ;
 198   unsigned int base1 : 8 ;
 199   unsigned int type : 4 ;
 200   unsigned int s : 1 ;
 201   unsigned int dpl : 2 ;
 202   unsigned int p : 1 ;
 203   unsigned int limit : 4 ;
 204   unsigned int avl : 1 ;
 205   unsigned int l : 1 ;
 206   unsigned int d : 1 ;
 207   unsigned int g : 1 ;
 208   unsigned int base2 : 8 ;
 209};
 210#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 211union __anonunion____missing_field_name_14 {
 212   struct __anonstruct____missing_field_name_15 __annonCompField5 ;
 213   struct __anonstruct____missing_field_name_16 __annonCompField6 ;
 214};
 215#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 216struct desc_struct {
 217   union __anonunion____missing_field_name_14 __annonCompField7 ;
 218} __attribute__((__packed__)) ;
 219#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 220typedef unsigned long pgdval_t;
 221#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 222typedef unsigned long pgprotval_t;
 223#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 224struct pgprot {
 225   pgprotval_t pgprot ;
 226};
 227#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 228typedef struct pgprot pgprot_t;
 229#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 230struct __anonstruct_pgd_t_20 {
 231   pgdval_t pgd ;
 232};
 233#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 234typedef struct __anonstruct_pgd_t_20 pgd_t;
 235#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 236typedef struct page *pgtable_t;
 237#line 295
 238struct file;
 239#line 295
 240struct file;
 241#line 313
 242struct seq_file;
 243#line 313
 244struct seq_file;
 245#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 246struct page;
 247#line 47
 248struct thread_struct;
 249#line 47
 250struct thread_struct;
 251#line 50
 252struct mm_struct;
 253#line 51
 254struct desc_struct;
 255#line 52
 256struct task_struct;
 257#line 53
 258struct cpumask;
 259#line 53
 260struct cpumask;
 261#line 329
 262struct arch_spinlock;
 263#line 329
 264struct arch_spinlock;
 265#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 266struct task_struct;
 267#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 268struct kernel_vm86_regs {
 269   struct pt_regs pt ;
 270   unsigned short es ;
 271   unsigned short __esh ;
 272   unsigned short ds ;
 273   unsigned short __dsh ;
 274   unsigned short fs ;
 275   unsigned short __fsh ;
 276   unsigned short gs ;
 277   unsigned short __gsh ;
 278};
 279#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 280union __anonunion____missing_field_name_24 {
 281   struct pt_regs *regs ;
 282   struct kernel_vm86_regs *vm86 ;
 283};
 284#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 285struct math_emu_info {
 286   long ___orig_eip ;
 287   union __anonunion____missing_field_name_24 __annonCompField8 ;
 288};
 289#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 290struct task_struct;
 291#line 10 "include/asm-generic/bug.h"
 292struct bug_entry {
 293   int bug_addr_disp ;
 294   int file_disp ;
 295   unsigned short line ;
 296   unsigned short flags ;
 297};
 298#line 12 "include/linux/bug.h"
 299struct pt_regs;
 300#line 14 "include/linux/cpumask.h"
 301struct cpumask {
 302   unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 303};
 304#line 14 "include/linux/cpumask.h"
 305typedef struct cpumask cpumask_t;
 306#line 637 "include/linux/cpumask.h"
 307typedef struct cpumask *cpumask_var_t;
 308#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 309struct static_key;
 310#line 234
 311struct static_key;
 312#line 11 "include/linux/personality.h"
 313struct pt_regs;
 314#line 153 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 315struct seq_operations;
 316#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 317struct i387_fsave_struct {
 318   u32 cwd ;
 319   u32 swd ;
 320   u32 twd ;
 321   u32 fip ;
 322   u32 fcs ;
 323   u32 foo ;
 324   u32 fos ;
 325   u32 st_space[20] ;
 326   u32 status ;
 327};
 328#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 329struct __anonstruct____missing_field_name_31 {
 330   u64 rip ;
 331   u64 rdp ;
 332};
 333#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 334struct __anonstruct____missing_field_name_32 {
 335   u32 fip ;
 336   u32 fcs ;
 337   u32 foo ;
 338   u32 fos ;
 339};
 340#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 341union __anonunion____missing_field_name_30 {
 342   struct __anonstruct____missing_field_name_31 __annonCompField12 ;
 343   struct __anonstruct____missing_field_name_32 __annonCompField13 ;
 344};
 345#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 346union __anonunion____missing_field_name_33 {
 347   u32 padding1[12] ;
 348   u32 sw_reserved[12] ;
 349};
 350#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 351struct i387_fxsave_struct {
 352   u16 cwd ;
 353   u16 swd ;
 354   u16 twd ;
 355   u16 fop ;
 356   union __anonunion____missing_field_name_30 __annonCompField14 ;
 357   u32 mxcsr ;
 358   u32 mxcsr_mask ;
 359   u32 st_space[32] ;
 360   u32 xmm_space[64] ;
 361   u32 padding[12] ;
 362   union __anonunion____missing_field_name_33 __annonCompField15 ;
 363} __attribute__((__aligned__(16))) ;
 364#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 365struct i387_soft_struct {
 366   u32 cwd ;
 367   u32 swd ;
 368   u32 twd ;
 369   u32 fip ;
 370   u32 fcs ;
 371   u32 foo ;
 372   u32 fos ;
 373   u32 st_space[20] ;
 374   u8 ftop ;
 375   u8 changed ;
 376   u8 lookahead ;
 377   u8 no_update ;
 378   u8 rm ;
 379   u8 alimit ;
 380   struct math_emu_info *info ;
 381   u32 entry_eip ;
 382};
 383#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 384struct ymmh_struct {
 385   u32 ymmh_space[64] ;
 386};
 387#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 388struct xsave_hdr_struct {
 389   u64 xstate_bv ;
 390   u64 reserved1[2] ;
 391   u64 reserved2[5] ;
 392} __attribute__((__packed__)) ;
 393#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 394struct xsave_struct {
 395   struct i387_fxsave_struct i387 ;
 396   struct xsave_hdr_struct xsave_hdr ;
 397   struct ymmh_struct ymmh ;
 398} __attribute__((__packed__, __aligned__(64))) ;
 399#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 400union thread_xstate {
 401   struct i387_fsave_struct fsave ;
 402   struct i387_fxsave_struct fxsave ;
 403   struct i387_soft_struct soft ;
 404   struct xsave_struct xsave ;
 405};
 406#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 407struct fpu {
 408   unsigned int last_cpu ;
 409   unsigned int has_fpu ;
 410   union thread_xstate *state ;
 411};
 412#line 433
 413struct kmem_cache;
 414#line 435
 415struct perf_event;
 416#line 435
 417struct perf_event;
 418#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 419struct thread_struct {
 420   struct desc_struct tls_array[3] ;
 421   unsigned long sp0 ;
 422   unsigned long sp ;
 423   unsigned long usersp ;
 424   unsigned short es ;
 425   unsigned short ds ;
 426   unsigned short fsindex ;
 427   unsigned short gsindex ;
 428   unsigned long fs ;
 429   unsigned long gs ;
 430   struct perf_event *ptrace_bps[4] ;
 431   unsigned long debugreg6 ;
 432   unsigned long ptrace_dr7 ;
 433   unsigned long cr2 ;
 434   unsigned long trap_nr ;
 435   unsigned long error_code ;
 436   struct fpu fpu ;
 437   unsigned long *io_bitmap_ptr ;
 438   unsigned long iopl ;
 439   unsigned int io_bitmap_max ;
 440};
 441#line 23 "include/asm-generic/atomic-long.h"
 442typedef atomic64_t atomic_long_t;
 443#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 444typedef u16 __ticket_t;
 445#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 446typedef u32 __ticketpair_t;
 447#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 448struct __raw_tickets {
 449   __ticket_t head ;
 450   __ticket_t tail ;
 451};
 452#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 453union __anonunion____missing_field_name_36 {
 454   __ticketpair_t head_tail ;
 455   struct __raw_tickets tickets ;
 456};
 457#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 458struct arch_spinlock {
 459   union __anonunion____missing_field_name_36 __annonCompField17 ;
 460};
 461#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 462typedef struct arch_spinlock arch_spinlock_t;
 463#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 464struct __anonstruct____missing_field_name_38 {
 465   u32 read ;
 466   s32 write ;
 467};
 468#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 469union __anonunion_arch_rwlock_t_37 {
 470   s64 lock ;
 471   struct __anonstruct____missing_field_name_38 __annonCompField18 ;
 472};
 473#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 474typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
 475#line 12 "include/linux/lockdep.h"
 476struct task_struct;
 477#line 391 "include/linux/lockdep.h"
 478struct lock_class_key {
 479
 480};
 481#line 20 "include/linux/spinlock_types.h"
 482struct raw_spinlock {
 483   arch_spinlock_t raw_lock ;
 484   unsigned int magic ;
 485   unsigned int owner_cpu ;
 486   void *owner ;
 487};
 488#line 20 "include/linux/spinlock_types.h"
 489typedef struct raw_spinlock raw_spinlock_t;
 490#line 64 "include/linux/spinlock_types.h"
 491union __anonunion____missing_field_name_39 {
 492   struct raw_spinlock rlock ;
 493};
 494#line 64 "include/linux/spinlock_types.h"
 495struct spinlock {
 496   union __anonunion____missing_field_name_39 __annonCompField19 ;
 497};
 498#line 64 "include/linux/spinlock_types.h"
 499typedef struct spinlock spinlock_t;
 500#line 11 "include/linux/rwlock_types.h"
 501struct __anonstruct_rwlock_t_40 {
 502   arch_rwlock_t raw_lock ;
 503   unsigned int magic ;
 504   unsigned int owner_cpu ;
 505   void *owner ;
 506};
 507#line 11 "include/linux/rwlock_types.h"
 508typedef struct __anonstruct_rwlock_t_40 rwlock_t;
 509#line 119 "include/linux/seqlock.h"
 510struct seqcount {
 511   unsigned int sequence ;
 512};
 513#line 119 "include/linux/seqlock.h"
 514typedef struct seqcount seqcount_t;
 515#line 14 "include/linux/time.h"
 516struct timespec {
 517   __kernel_time_t tv_sec ;
 518   long tv_nsec ;
 519};
 520#line 62 "include/linux/stat.h"
 521struct kstat {
 522   u64 ino ;
 523   dev_t dev ;
 524   umode_t mode ;
 525   unsigned int nlink ;
 526   uid_t uid ;
 527   gid_t gid ;
 528   dev_t rdev ;
 529   loff_t size ;
 530   struct timespec atime ;
 531   struct timespec mtime ;
 532   struct timespec ctime ;
 533   unsigned long blksize ;
 534   unsigned long long blocks ;
 535};
 536#line 49 "include/linux/wait.h"
 537struct __wait_queue_head {
 538   spinlock_t lock ;
 539   struct list_head task_list ;
 540};
 541#line 53 "include/linux/wait.h"
 542typedef struct __wait_queue_head wait_queue_head_t;
 543#line 55
 544struct task_struct;
 545#line 98 "include/linux/nodemask.h"
 546struct __anonstruct_nodemask_t_42 {
 547   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 548};
 549#line 98 "include/linux/nodemask.h"
 550typedef struct __anonstruct_nodemask_t_42 nodemask_t;
 551#line 60 "include/linux/pageblock-flags.h"
 552struct page;
 553#line 48 "include/linux/mutex.h"
 554struct mutex {
 555   atomic_t count ;
 556   spinlock_t wait_lock ;
 557   struct list_head wait_list ;
 558   struct task_struct *owner ;
 559   char const   *name ;
 560   void *magic ;
 561};
 562#line 69 "include/linux/mutex.h"
 563struct mutex_waiter {
 564   struct list_head list ;
 565   struct task_struct *task ;
 566   void *magic ;
 567};
 568#line 19 "include/linux/rwsem.h"
 569struct rw_semaphore;
 570#line 19
 571struct rw_semaphore;
 572#line 25 "include/linux/rwsem.h"
 573struct rw_semaphore {
 574   long count ;
 575   raw_spinlock_t wait_lock ;
 576   struct list_head wait_list ;
 577};
 578#line 25 "include/linux/completion.h"
 579struct completion {
 580   unsigned int done ;
 581   wait_queue_head_t wait ;
 582};
 583#line 9 "include/linux/memory_hotplug.h"
 584struct page;
 585#line 202 "include/linux/ioport.h"
 586struct device;
 587#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 588struct device;
 589#line 46 "include/linux/ktime.h"
 590union ktime {
 591   s64 tv64 ;
 592};
 593#line 59 "include/linux/ktime.h"
 594typedef union ktime ktime_t;
 595#line 10 "include/linux/timer.h"
 596struct tvec_base;
 597#line 10
 598struct tvec_base;
 599#line 12 "include/linux/timer.h"
 600struct timer_list {
 601   struct list_head entry ;
 602   unsigned long expires ;
 603   struct tvec_base *base ;
 604   void (*function)(unsigned long  ) ;
 605   unsigned long data ;
 606   int slack ;
 607   int start_pid ;
 608   void *start_site ;
 609   char start_comm[16] ;
 610};
 611#line 289
 612struct hrtimer;
 613#line 289
 614struct hrtimer;
 615#line 290
 616enum hrtimer_restart;
 617#line 17 "include/linux/workqueue.h"
 618struct work_struct;
 619#line 17
 620struct work_struct;
 621#line 79 "include/linux/workqueue.h"
 622struct work_struct {
 623   atomic_long_t data ;
 624   struct list_head entry ;
 625   void (*func)(struct work_struct *work ) ;
 626};
 627#line 92 "include/linux/workqueue.h"
 628struct delayed_work {
 629   struct work_struct work ;
 630   struct timer_list timer ;
 631};
 632#line 42 "include/linux/pm.h"
 633struct device;
 634#line 50 "include/linux/pm.h"
 635struct pm_message {
 636   int event ;
 637};
 638#line 50 "include/linux/pm.h"
 639typedef struct pm_message pm_message_t;
 640#line 264 "include/linux/pm.h"
 641struct dev_pm_ops {
 642   int (*prepare)(struct device *dev ) ;
 643   void (*complete)(struct device *dev ) ;
 644   int (*suspend)(struct device *dev ) ;
 645   int (*resume)(struct device *dev ) ;
 646   int (*freeze)(struct device *dev ) ;
 647   int (*thaw)(struct device *dev ) ;
 648   int (*poweroff)(struct device *dev ) ;
 649   int (*restore)(struct device *dev ) ;
 650   int (*suspend_late)(struct device *dev ) ;
 651   int (*resume_early)(struct device *dev ) ;
 652   int (*freeze_late)(struct device *dev ) ;
 653   int (*thaw_early)(struct device *dev ) ;
 654   int (*poweroff_late)(struct device *dev ) ;
 655   int (*restore_early)(struct device *dev ) ;
 656   int (*suspend_noirq)(struct device *dev ) ;
 657   int (*resume_noirq)(struct device *dev ) ;
 658   int (*freeze_noirq)(struct device *dev ) ;
 659   int (*thaw_noirq)(struct device *dev ) ;
 660   int (*poweroff_noirq)(struct device *dev ) ;
 661   int (*restore_noirq)(struct device *dev ) ;
 662   int (*runtime_suspend)(struct device *dev ) ;
 663   int (*runtime_resume)(struct device *dev ) ;
 664   int (*runtime_idle)(struct device *dev ) ;
 665};
 666#line 458
 667enum rpm_status {
 668    RPM_ACTIVE = 0,
 669    RPM_RESUMING = 1,
 670    RPM_SUSPENDED = 2,
 671    RPM_SUSPENDING = 3
 672} ;
 673#line 480
 674enum rpm_request {
 675    RPM_REQ_NONE = 0,
 676    RPM_REQ_IDLE = 1,
 677    RPM_REQ_SUSPEND = 2,
 678    RPM_REQ_AUTOSUSPEND = 3,
 679    RPM_REQ_RESUME = 4
 680} ;
 681#line 488
 682struct wakeup_source;
 683#line 488
 684struct wakeup_source;
 685#line 495 "include/linux/pm.h"
 686struct pm_subsys_data {
 687   spinlock_t lock ;
 688   unsigned int refcount ;
 689};
 690#line 506
 691struct dev_pm_qos_request;
 692#line 506
 693struct pm_qos_constraints;
 694#line 506 "include/linux/pm.h"
 695struct dev_pm_info {
 696   pm_message_t power_state ;
 697   unsigned int can_wakeup : 1 ;
 698   unsigned int async_suspend : 1 ;
 699   bool is_prepared : 1 ;
 700   bool is_suspended : 1 ;
 701   bool ignore_children : 1 ;
 702   spinlock_t lock ;
 703   struct list_head entry ;
 704   struct completion completion ;
 705   struct wakeup_source *wakeup ;
 706   bool wakeup_path : 1 ;
 707   struct timer_list suspend_timer ;
 708   unsigned long timer_expires ;
 709   struct work_struct work ;
 710   wait_queue_head_t wait_queue ;
 711   atomic_t usage_count ;
 712   atomic_t child_count ;
 713   unsigned int disable_depth : 3 ;
 714   unsigned int idle_notification : 1 ;
 715   unsigned int request_pending : 1 ;
 716   unsigned int deferred_resume : 1 ;
 717   unsigned int run_wake : 1 ;
 718   unsigned int runtime_auto : 1 ;
 719   unsigned int no_callbacks : 1 ;
 720   unsigned int irq_safe : 1 ;
 721   unsigned int use_autosuspend : 1 ;
 722   unsigned int timer_autosuspends : 1 ;
 723   enum rpm_request request ;
 724   enum rpm_status runtime_status ;
 725   int runtime_error ;
 726   int autosuspend_delay ;
 727   unsigned long last_busy ;
 728   unsigned long active_jiffies ;
 729   unsigned long suspended_jiffies ;
 730   unsigned long accounting_timestamp ;
 731   ktime_t suspend_time ;
 732   s64 max_time_suspended_ns ;
 733   struct dev_pm_qos_request *pq_req ;
 734   struct pm_subsys_data *subsys_data ;
 735   struct pm_qos_constraints *constraints ;
 736};
 737#line 564 "include/linux/pm.h"
 738struct dev_pm_domain {
 739   struct dev_pm_ops ops ;
 740};
 741#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 742struct __anonstruct_mm_context_t_112 {
 743   void *ldt ;
 744   int size ;
 745   unsigned short ia32_compat ;
 746   struct mutex lock ;
 747   void *vdso ;
 748};
 749#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 750typedef struct __anonstruct_mm_context_t_112 mm_context_t;
 751#line 8 "include/linux/vmalloc.h"
 752struct vm_area_struct;
 753#line 8
 754struct vm_area_struct;
 755#line 994 "include/linux/mmzone.h"
 756struct page;
 757#line 10 "include/linux/gfp.h"
 758struct vm_area_struct;
 759#line 29 "include/linux/sysctl.h"
 760struct completion;
 761#line 100 "include/linux/rbtree.h"
 762struct rb_node {
 763   unsigned long rb_parent_color ;
 764   struct rb_node *rb_right ;
 765   struct rb_node *rb_left ;
 766} __attribute__((__aligned__(sizeof(long )))) ;
 767#line 110 "include/linux/rbtree.h"
 768struct rb_root {
 769   struct rb_node *rb_node ;
 770};
 771#line 939 "include/linux/sysctl.h"
 772struct nsproxy;
 773#line 939
 774struct nsproxy;
 775#line 48 "include/linux/kmod.h"
 776struct cred;
 777#line 48
 778struct cred;
 779#line 49
 780struct file;
 781#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 782struct task_struct;
 783#line 18 "include/linux/elf.h"
 784typedef __u64 Elf64_Addr;
 785#line 19 "include/linux/elf.h"
 786typedef __u16 Elf64_Half;
 787#line 23 "include/linux/elf.h"
 788typedef __u32 Elf64_Word;
 789#line 24 "include/linux/elf.h"
 790typedef __u64 Elf64_Xword;
 791#line 194 "include/linux/elf.h"
 792struct elf64_sym {
 793   Elf64_Word st_name ;
 794   unsigned char st_info ;
 795   unsigned char st_other ;
 796   Elf64_Half st_shndx ;
 797   Elf64_Addr st_value ;
 798   Elf64_Xword st_size ;
 799};
 800#line 194 "include/linux/elf.h"
 801typedef struct elf64_sym Elf64_Sym;
 802#line 438
 803struct file;
 804#line 20 "include/linux/kobject_ns.h"
 805struct sock;
 806#line 20
 807struct sock;
 808#line 21
 809struct kobject;
 810#line 21
 811struct kobject;
 812#line 27
 813enum kobj_ns_type {
 814    KOBJ_NS_TYPE_NONE = 0,
 815    KOBJ_NS_TYPE_NET = 1,
 816    KOBJ_NS_TYPES = 2
 817} ;
 818#line 40 "include/linux/kobject_ns.h"
 819struct kobj_ns_type_operations {
 820   enum kobj_ns_type type ;
 821   void *(*grab_current_ns)(void) ;
 822   void const   *(*netlink_ns)(struct sock *sk ) ;
 823   void const   *(*initial_ns)(void) ;
 824   void (*drop_ns)(void * ) ;
 825};
 826#line 22 "include/linux/sysfs.h"
 827struct kobject;
 828#line 23
 829struct module;
 830#line 24
 831enum kobj_ns_type;
 832#line 26 "include/linux/sysfs.h"
 833struct attribute {
 834   char const   *name ;
 835   umode_t mode ;
 836};
 837#line 56 "include/linux/sysfs.h"
 838struct attribute_group {
 839   char const   *name ;
 840   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 841   struct attribute **attrs ;
 842};
 843#line 85
 844struct file;
 845#line 86
 846struct vm_area_struct;
 847#line 88 "include/linux/sysfs.h"
 848struct bin_attribute {
 849   struct attribute attr ;
 850   size_t size ;
 851   void *private ;
 852   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 853                   loff_t  , size_t  ) ;
 854   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 855                    loff_t  , size_t  ) ;
 856   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 857};
 858#line 112 "include/linux/sysfs.h"
 859struct sysfs_ops {
 860   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 861   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 862   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 863};
 864#line 118
 865struct sysfs_dirent;
 866#line 118
 867struct sysfs_dirent;
 868#line 22 "include/linux/kref.h"
 869struct kref {
 870   atomic_t refcount ;
 871};
 872#line 60 "include/linux/kobject.h"
 873struct kset;
 874#line 60
 875struct kobj_type;
 876#line 60 "include/linux/kobject.h"
 877struct kobject {
 878   char const   *name ;
 879   struct list_head entry ;
 880   struct kobject *parent ;
 881   struct kset *kset ;
 882   struct kobj_type *ktype ;
 883   struct sysfs_dirent *sd ;
 884   struct kref kref ;
 885   unsigned int state_initialized : 1 ;
 886   unsigned int state_in_sysfs : 1 ;
 887   unsigned int state_add_uevent_sent : 1 ;
 888   unsigned int state_remove_uevent_sent : 1 ;
 889   unsigned int uevent_suppress : 1 ;
 890};
 891#line 108 "include/linux/kobject.h"
 892struct kobj_type {
 893   void (*release)(struct kobject *kobj ) ;
 894   struct sysfs_ops  const  *sysfs_ops ;
 895   struct attribute **default_attrs ;
 896   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 897   void const   *(*namespace)(struct kobject *kobj ) ;
 898};
 899#line 116 "include/linux/kobject.h"
 900struct kobj_uevent_env {
 901   char *envp[32] ;
 902   int envp_idx ;
 903   char buf[2048] ;
 904   int buflen ;
 905};
 906#line 123 "include/linux/kobject.h"
 907struct kset_uevent_ops {
 908   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 909   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 910   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 911};
 912#line 140
 913struct sock;
 914#line 159 "include/linux/kobject.h"
 915struct kset {
 916   struct list_head list ;
 917   spinlock_t list_lock ;
 918   struct kobject kobj ;
 919   struct kset_uevent_ops  const  *uevent_ops ;
 920};
 921#line 39 "include/linux/moduleparam.h"
 922struct kernel_param;
 923#line 39
 924struct kernel_param;
 925#line 41 "include/linux/moduleparam.h"
 926struct kernel_param_ops {
 927   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 928   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 929   void (*free)(void *arg ) ;
 930};
 931#line 50
 932struct kparam_string;
 933#line 50
 934struct kparam_array;
 935#line 50 "include/linux/moduleparam.h"
 936union __anonunion____missing_field_name_199 {
 937   void *arg ;
 938   struct kparam_string  const  *str ;
 939   struct kparam_array  const  *arr ;
 940};
 941#line 50 "include/linux/moduleparam.h"
 942struct kernel_param {
 943   char const   *name ;
 944   struct kernel_param_ops  const  *ops ;
 945   u16 perm ;
 946   s16 level ;
 947   union __anonunion____missing_field_name_199 __annonCompField32 ;
 948};
 949#line 63 "include/linux/moduleparam.h"
 950struct kparam_string {
 951   unsigned int maxlen ;
 952   char *string ;
 953};
 954#line 69 "include/linux/moduleparam.h"
 955struct kparam_array {
 956   unsigned int max ;
 957   unsigned int elemsize ;
 958   unsigned int *num ;
 959   struct kernel_param_ops  const  *ops ;
 960   void *elem ;
 961};
 962#line 445
 963struct module;
 964#line 80 "include/linux/jump_label.h"
 965struct module;
 966#line 143 "include/linux/jump_label.h"
 967struct static_key {
 968   atomic_t enabled ;
 969};
 970#line 22 "include/linux/tracepoint.h"
 971struct module;
 972#line 23
 973struct tracepoint;
 974#line 23
 975struct tracepoint;
 976#line 25 "include/linux/tracepoint.h"
 977struct tracepoint_func {
 978   void *func ;
 979   void *data ;
 980};
 981#line 30 "include/linux/tracepoint.h"
 982struct tracepoint {
 983   char const   *name ;
 984   struct static_key key ;
 985   void (*regfunc)(void) ;
 986   void (*unregfunc)(void) ;
 987   struct tracepoint_func *funcs ;
 988};
 989#line 19 "include/linux/export.h"
 990struct kernel_symbol {
 991   unsigned long value ;
 992   char const   *name ;
 993};
 994#line 8 "include/asm-generic/module.h"
 995struct mod_arch_specific {
 996
 997};
 998#line 35 "include/linux/module.h"
 999struct module;
1000#line 37
1001struct module_param_attrs;
1002#line 37 "include/linux/module.h"
1003struct module_kobject {
1004   struct kobject kobj ;
1005   struct module *mod ;
1006   struct kobject *drivers_dir ;
1007   struct module_param_attrs *mp ;
1008};
1009#line 44 "include/linux/module.h"
1010struct module_attribute {
1011   struct attribute attr ;
1012   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
1013   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
1014                    size_t count ) ;
1015   void (*setup)(struct module * , char const   * ) ;
1016   int (*test)(struct module * ) ;
1017   void (*free)(struct module * ) ;
1018};
1019#line 71
1020struct exception_table_entry;
1021#line 71
1022struct exception_table_entry;
1023#line 199
1024enum module_state {
1025    MODULE_STATE_LIVE = 0,
1026    MODULE_STATE_COMING = 1,
1027    MODULE_STATE_GOING = 2
1028} ;
1029#line 215 "include/linux/module.h"
1030struct module_ref {
1031   unsigned long incs ;
1032   unsigned long decs ;
1033} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1034#line 220
1035struct module_sect_attrs;
1036#line 220
1037struct module_notes_attrs;
1038#line 220
1039struct ftrace_event_call;
1040#line 220 "include/linux/module.h"
1041struct module {
1042   enum module_state state ;
1043   struct list_head list ;
1044   char name[64UL - sizeof(unsigned long )] ;
1045   struct module_kobject mkobj ;
1046   struct module_attribute *modinfo_attrs ;
1047   char const   *version ;
1048   char const   *srcversion ;
1049   struct kobject *holders_dir ;
1050   struct kernel_symbol  const  *syms ;
1051   unsigned long const   *crcs ;
1052   unsigned int num_syms ;
1053   struct kernel_param *kp ;
1054   unsigned int num_kp ;
1055   unsigned int num_gpl_syms ;
1056   struct kernel_symbol  const  *gpl_syms ;
1057   unsigned long const   *gpl_crcs ;
1058   struct kernel_symbol  const  *unused_syms ;
1059   unsigned long const   *unused_crcs ;
1060   unsigned int num_unused_syms ;
1061   unsigned int num_unused_gpl_syms ;
1062   struct kernel_symbol  const  *unused_gpl_syms ;
1063   unsigned long const   *unused_gpl_crcs ;
1064   struct kernel_symbol  const  *gpl_future_syms ;
1065   unsigned long const   *gpl_future_crcs ;
1066   unsigned int num_gpl_future_syms ;
1067   unsigned int num_exentries ;
1068   struct exception_table_entry *extable ;
1069   int (*init)(void) ;
1070   void *module_init ;
1071   void *module_core ;
1072   unsigned int init_size ;
1073   unsigned int core_size ;
1074   unsigned int init_text_size ;
1075   unsigned int core_text_size ;
1076   unsigned int init_ro_size ;
1077   unsigned int core_ro_size ;
1078   struct mod_arch_specific arch ;
1079   unsigned int taints ;
1080   unsigned int num_bugs ;
1081   struct list_head bug_list ;
1082   struct bug_entry *bug_table ;
1083   Elf64_Sym *symtab ;
1084   Elf64_Sym *core_symtab ;
1085   unsigned int num_symtab ;
1086   unsigned int core_num_syms ;
1087   char *strtab ;
1088   char *core_strtab ;
1089   struct module_sect_attrs *sect_attrs ;
1090   struct module_notes_attrs *notes_attrs ;
1091   char *args ;
1092   void *percpu ;
1093   unsigned int percpu_size ;
1094   unsigned int num_tracepoints ;
1095   struct tracepoint * const  *tracepoints_ptrs ;
1096   unsigned int num_trace_bprintk_fmt ;
1097   char const   **trace_bprintk_fmt_start ;
1098   struct ftrace_event_call **trace_events ;
1099   unsigned int num_trace_events ;
1100   struct list_head source_list ;
1101   struct list_head target_list ;
1102   struct task_struct *waiter ;
1103   void (*exit)(void) ;
1104   struct module_ref *refptr ;
1105   ctor_fn_t *ctors ;
1106   unsigned int num_ctors ;
1107};
1108#line 19 "include/linux/klist.h"
1109struct klist_node;
1110#line 19
1111struct klist_node;
1112#line 39 "include/linux/klist.h"
1113struct klist_node {
1114   void *n_klist ;
1115   struct list_head n_node ;
1116   struct kref n_ref ;
1117};
1118#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1119struct dma_map_ops;
1120#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1121struct dev_archdata {
1122   void *acpi_handle ;
1123   struct dma_map_ops *dma_ops ;
1124   void *iommu ;
1125};
1126#line 28 "include/linux/device.h"
1127struct device;
1128#line 29
1129struct device_private;
1130#line 29
1131struct device_private;
1132#line 30
1133struct device_driver;
1134#line 30
1135struct device_driver;
1136#line 31
1137struct driver_private;
1138#line 31
1139struct driver_private;
1140#line 32
1141struct module;
1142#line 33
1143struct class;
1144#line 33
1145struct class;
1146#line 34
1147struct subsys_private;
1148#line 34
1149struct subsys_private;
1150#line 35
1151struct bus_type;
1152#line 35
1153struct bus_type;
1154#line 36
1155struct device_node;
1156#line 36
1157struct device_node;
1158#line 37
1159struct iommu_ops;
1160#line 37
1161struct iommu_ops;
1162#line 39 "include/linux/device.h"
1163struct bus_attribute {
1164   struct attribute attr ;
1165   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
1166   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
1167};
1168#line 89
1169struct device_attribute;
1170#line 89
1171struct driver_attribute;
1172#line 89 "include/linux/device.h"
1173struct bus_type {
1174   char const   *name ;
1175   char const   *dev_name ;
1176   struct device *dev_root ;
1177   struct bus_attribute *bus_attrs ;
1178   struct device_attribute *dev_attrs ;
1179   struct driver_attribute *drv_attrs ;
1180   int (*match)(struct device *dev , struct device_driver *drv ) ;
1181   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1182   int (*probe)(struct device *dev ) ;
1183   int (*remove)(struct device *dev ) ;
1184   void (*shutdown)(struct device *dev ) ;
1185   int (*suspend)(struct device *dev , pm_message_t state ) ;
1186   int (*resume)(struct device *dev ) ;
1187   struct dev_pm_ops  const  *pm ;
1188   struct iommu_ops *iommu_ops ;
1189   struct subsys_private *p ;
1190};
1191#line 127
1192struct device_type;
1193#line 214
1194struct of_device_id;
1195#line 214 "include/linux/device.h"
1196struct device_driver {
1197   char const   *name ;
1198   struct bus_type *bus ;
1199   struct module *owner ;
1200   char const   *mod_name ;
1201   bool suppress_bind_attrs ;
1202   struct of_device_id  const  *of_match_table ;
1203   int (*probe)(struct device *dev ) ;
1204   int (*remove)(struct device *dev ) ;
1205   void (*shutdown)(struct device *dev ) ;
1206   int (*suspend)(struct device *dev , pm_message_t state ) ;
1207   int (*resume)(struct device *dev ) ;
1208   struct attribute_group  const  **groups ;
1209   struct dev_pm_ops  const  *pm ;
1210   struct driver_private *p ;
1211};
1212#line 249 "include/linux/device.h"
1213struct driver_attribute {
1214   struct attribute attr ;
1215   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1216   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
1217};
1218#line 330
1219struct class_attribute;
1220#line 330 "include/linux/device.h"
1221struct class {
1222   char const   *name ;
1223   struct module *owner ;
1224   struct class_attribute *class_attrs ;
1225   struct device_attribute *dev_attrs ;
1226   struct bin_attribute *dev_bin_attrs ;
1227   struct kobject *dev_kobj ;
1228   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1229   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1230   void (*class_release)(struct class *class ) ;
1231   void (*dev_release)(struct device *dev ) ;
1232   int (*suspend)(struct device *dev , pm_message_t state ) ;
1233   int (*resume)(struct device *dev ) ;
1234   struct kobj_ns_type_operations  const  *ns_type ;
1235   void const   *(*namespace)(struct device *dev ) ;
1236   struct dev_pm_ops  const  *pm ;
1237   struct subsys_private *p ;
1238};
1239#line 397 "include/linux/device.h"
1240struct class_attribute {
1241   struct attribute attr ;
1242   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1243   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
1244                    size_t count ) ;
1245   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
1246};
1247#line 465 "include/linux/device.h"
1248struct device_type {
1249   char const   *name ;
1250   struct attribute_group  const  **groups ;
1251   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1252   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1253   void (*release)(struct device *dev ) ;
1254   struct dev_pm_ops  const  *pm ;
1255};
1256#line 476 "include/linux/device.h"
1257struct device_attribute {
1258   struct attribute attr ;
1259   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1260   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
1261                    size_t count ) ;
1262};
1263#line 559 "include/linux/device.h"
1264struct device_dma_parameters {
1265   unsigned int max_segment_size ;
1266   unsigned long segment_boundary_mask ;
1267};
1268#line 627
1269struct dma_coherent_mem;
1270#line 627 "include/linux/device.h"
1271struct device {
1272   struct device *parent ;
1273   struct device_private *p ;
1274   struct kobject kobj ;
1275   char const   *init_name ;
1276   struct device_type  const  *type ;
1277   struct mutex mutex ;
1278   struct bus_type *bus ;
1279   struct device_driver *driver ;
1280   void *platform_data ;
1281   struct dev_pm_info power ;
1282   struct dev_pm_domain *pm_domain ;
1283   int numa_node ;
1284   u64 *dma_mask ;
1285   u64 coherent_dma_mask ;
1286   struct device_dma_parameters *dma_parms ;
1287   struct list_head dma_pools ;
1288   struct dma_coherent_mem *dma_mem ;
1289   struct dev_archdata archdata ;
1290   struct device_node *of_node ;
1291   dev_t devt ;
1292   u32 id ;
1293   spinlock_t devres_lock ;
1294   struct list_head devres_head ;
1295   struct klist_node knode_class ;
1296   struct class *class ;
1297   struct attribute_group  const  **groups ;
1298   void (*release)(struct device *dev ) ;
1299};
1300#line 43 "include/linux/pm_wakeup.h"
1301struct wakeup_source {
1302   char const   *name ;
1303   struct list_head entry ;
1304   spinlock_t lock ;
1305   struct timer_list timer ;
1306   unsigned long timer_expires ;
1307   ktime_t total_time ;
1308   ktime_t max_time ;
1309   ktime_t last_time ;
1310   unsigned long event_count ;
1311   unsigned long active_count ;
1312   unsigned long relax_count ;
1313   unsigned long hit_count ;
1314   unsigned int active : 1 ;
1315};
1316#line 12 "include/linux/mod_devicetable.h"
1317typedef unsigned long kernel_ulong_t;
1318#line 219 "include/linux/mod_devicetable.h"
1319struct of_device_id {
1320   char name[32] ;
1321   char type[32] ;
1322   char compatible[128] ;
1323   void *data ;
1324};
1325#line 442 "include/linux/mod_devicetable.h"
1326struct spi_device_id {
1327   char name[32] ;
1328   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
1329};
1330#line 20 "include/linux/rtc.h"
1331struct rtc_time {
1332   int tm_sec ;
1333   int tm_min ;
1334   int tm_hour ;
1335   int tm_mday ;
1336   int tm_mon ;
1337   int tm_year ;
1338   int tm_wday ;
1339   int tm_yday ;
1340   int tm_isdst ;
1341};
1342#line 36 "include/linux/rtc.h"
1343struct rtc_wkalrm {
1344   unsigned char enabled ;
1345   unsigned char pending ;
1346   struct rtc_time time ;
1347};
1348#line 31 "include/linux/irq.h"
1349struct seq_file;
1350#line 32
1351struct module;
1352#line 14 "include/linux/irqdesc.h"
1353struct module;
1354#line 17 "include/linux/profile.h"
1355struct pt_regs;
1356#line 65
1357struct task_struct;
1358#line 66
1359struct mm_struct;
1360#line 88
1361struct pt_regs;
1362#line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess.h"
1363struct exception_table_entry {
1364   unsigned long insn ;
1365   unsigned long fixup ;
1366};
1367#line 132 "include/linux/hardirq.h"
1368struct task_struct;
1369#line 8 "include/linux/timerqueue.h"
1370struct timerqueue_node {
1371   struct rb_node node ;
1372   ktime_t expires ;
1373};
1374#line 13 "include/linux/timerqueue.h"
1375struct timerqueue_head {
1376   struct rb_root head ;
1377   struct timerqueue_node *next ;
1378};
1379#line 27 "include/linux/hrtimer.h"
1380struct hrtimer_clock_base;
1381#line 27
1382struct hrtimer_clock_base;
1383#line 28
1384struct hrtimer_cpu_base;
1385#line 28
1386struct hrtimer_cpu_base;
1387#line 44
1388enum hrtimer_restart {
1389    HRTIMER_NORESTART = 0,
1390    HRTIMER_RESTART = 1
1391} ;
1392#line 108 "include/linux/hrtimer.h"
1393struct hrtimer {
1394   struct timerqueue_node node ;
1395   ktime_t _softexpires ;
1396   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1397   struct hrtimer_clock_base *base ;
1398   unsigned long state ;
1399   int start_pid ;
1400   void *start_site ;
1401   char start_comm[16] ;
1402};
1403#line 145 "include/linux/hrtimer.h"
1404struct hrtimer_clock_base {
1405   struct hrtimer_cpu_base *cpu_base ;
1406   int index ;
1407   clockid_t clockid ;
1408   struct timerqueue_head active ;
1409   ktime_t resolution ;
1410   ktime_t (*get_time)(void) ;
1411   ktime_t softirq_time ;
1412   ktime_t offset ;
1413};
1414#line 178 "include/linux/hrtimer.h"
1415struct hrtimer_cpu_base {
1416   raw_spinlock_t lock ;
1417   unsigned long active_bases ;
1418   ktime_t expires_next ;
1419   int hres_active ;
1420   int hang_detected ;
1421   unsigned long nr_events ;
1422   unsigned long nr_retries ;
1423   unsigned long nr_hangs ;
1424   ktime_t max_hang_time ;
1425   struct hrtimer_clock_base clock_base[3] ;
1426};
1427#line 187 "include/linux/interrupt.h"
1428struct device;
1429#line 695
1430struct seq_file;
1431#line 11 "include/linux/seq_file.h"
1432struct seq_operations;
1433#line 12
1434struct file;
1435#line 13
1436struct path;
1437#line 13
1438struct path;
1439#line 14
1440struct inode;
1441#line 14
1442struct inode;
1443#line 15
1444struct dentry;
1445#line 15
1446struct dentry;
1447#line 17 "include/linux/seq_file.h"
1448struct seq_file {
1449   char *buf ;
1450   size_t size ;
1451   size_t from ;
1452   size_t count ;
1453   loff_t index ;
1454   loff_t read_pos ;
1455   u64 version ;
1456   struct mutex lock ;
1457   struct seq_operations  const  *op ;
1458   int poll_event ;
1459   void *private ;
1460};
1461#line 31 "include/linux/seq_file.h"
1462struct seq_operations {
1463   void *(*start)(struct seq_file *m , loff_t *pos ) ;
1464   void (*stop)(struct seq_file *m , void *v ) ;
1465   void *(*next)(struct seq_file *m , void *v , loff_t *pos ) ;
1466   int (*show)(struct seq_file *m , void *v ) ;
1467};
1468#line 8 "include/linux/cdev.h"
1469struct file_operations;
1470#line 8
1471struct file_operations;
1472#line 9
1473struct inode;
1474#line 10
1475struct module;
1476#line 12 "include/linux/cdev.h"
1477struct cdev {
1478   struct kobject kobj ;
1479   struct module *owner ;
1480   struct file_operations  const  *ops ;
1481   struct list_head list ;
1482   dev_t dev ;
1483   unsigned int count ;
1484};
1485#line 33
1486struct backing_dev_info;
1487#line 15 "include/linux/blk_types.h"
1488struct page;
1489#line 16
1490struct block_device;
1491#line 16
1492struct block_device;
1493#line 33 "include/linux/list_bl.h"
1494struct hlist_bl_node;
1495#line 33 "include/linux/list_bl.h"
1496struct hlist_bl_head {
1497   struct hlist_bl_node *first ;
1498};
1499#line 37 "include/linux/list_bl.h"
1500struct hlist_bl_node {
1501   struct hlist_bl_node *next ;
1502   struct hlist_bl_node **pprev ;
1503};
1504#line 13 "include/linux/dcache.h"
1505struct nameidata;
1506#line 13
1507struct nameidata;
1508#line 14
1509struct path;
1510#line 15
1511struct vfsmount;
1512#line 15
1513struct vfsmount;
1514#line 35 "include/linux/dcache.h"
1515struct qstr {
1516   unsigned int hash ;
1517   unsigned int len ;
1518   unsigned char const   *name ;
1519};
1520#line 88
1521struct dentry_operations;
1522#line 88
1523struct super_block;
1524#line 88 "include/linux/dcache.h"
1525union __anonunion_d_u_210 {
1526   struct list_head d_child ;
1527   struct rcu_head d_rcu ;
1528};
1529#line 88 "include/linux/dcache.h"
1530struct dentry {
1531   unsigned int d_flags ;
1532   seqcount_t d_seq ;
1533   struct hlist_bl_node d_hash ;
1534   struct dentry *d_parent ;
1535   struct qstr d_name ;
1536   struct inode *d_inode ;
1537   unsigned char d_iname[32] ;
1538   unsigned int d_count ;
1539   spinlock_t d_lock ;
1540   struct dentry_operations  const  *d_op ;
1541   struct super_block *d_sb ;
1542   unsigned long d_time ;
1543   void *d_fsdata ;
1544   struct list_head d_lru ;
1545   union __anonunion_d_u_210 d_u ;
1546   struct list_head d_subdirs ;
1547   struct list_head d_alias ;
1548};
1549#line 131 "include/linux/dcache.h"
1550struct dentry_operations {
1551   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1552   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
1553   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
1554                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
1555   int (*d_delete)(struct dentry  const  * ) ;
1556   void (*d_release)(struct dentry * ) ;
1557   void (*d_prune)(struct dentry * ) ;
1558   void (*d_iput)(struct dentry * , struct inode * ) ;
1559   char *(*d_dname)(struct dentry * , char * , int  ) ;
1560   struct vfsmount *(*d_automount)(struct path * ) ;
1561   int (*d_manage)(struct dentry * , bool  ) ;
1562} __attribute__((__aligned__((1) <<  (6) ))) ;
1563#line 4 "include/linux/path.h"
1564struct dentry;
1565#line 5
1566struct vfsmount;
1567#line 7 "include/linux/path.h"
1568struct path {
1569   struct vfsmount *mnt ;
1570   struct dentry *dentry ;
1571};
1572#line 64 "include/linux/radix-tree.h"
1573struct radix_tree_node;
1574#line 64 "include/linux/radix-tree.h"
1575struct radix_tree_root {
1576   unsigned int height ;
1577   gfp_t gfp_mask ;
1578   struct radix_tree_node *rnode ;
1579};
1580#line 14 "include/linux/prio_tree.h"
1581struct prio_tree_node;
1582#line 14 "include/linux/prio_tree.h"
1583struct raw_prio_tree_node {
1584   struct prio_tree_node *left ;
1585   struct prio_tree_node *right ;
1586   struct prio_tree_node *parent ;
1587};
1588#line 20 "include/linux/prio_tree.h"
1589struct prio_tree_node {
1590   struct prio_tree_node *left ;
1591   struct prio_tree_node *right ;
1592   struct prio_tree_node *parent ;
1593   unsigned long start ;
1594   unsigned long last ;
1595};
1596#line 28 "include/linux/prio_tree.h"
1597struct prio_tree_root {
1598   struct prio_tree_node *prio_tree_node ;
1599   unsigned short index_bits ;
1600   unsigned short raw ;
1601};
1602#line 6 "include/linux/pid.h"
1603enum pid_type {
1604    PIDTYPE_PID = 0,
1605    PIDTYPE_PGID = 1,
1606    PIDTYPE_SID = 2,
1607    PIDTYPE_MAX = 3
1608} ;
1609#line 50
1610struct pid_namespace;
1611#line 50 "include/linux/pid.h"
1612struct upid {
1613   int nr ;
1614   struct pid_namespace *ns ;
1615   struct hlist_node pid_chain ;
1616};
1617#line 57 "include/linux/pid.h"
1618struct pid {
1619   atomic_t count ;
1620   unsigned int level ;
1621   struct hlist_head tasks[3] ;
1622   struct rcu_head rcu ;
1623   struct upid numbers[1] ;
1624};
1625#line 69 "include/linux/pid.h"
1626struct pid_link {
1627   struct hlist_node node ;
1628   struct pid *pid ;
1629};
1630#line 100
1631struct pid_namespace;
1632#line 18 "include/linux/capability.h"
1633struct task_struct;
1634#line 94 "include/linux/capability.h"
1635struct kernel_cap_struct {
1636   __u32 cap[2] ;
1637};
1638#line 94 "include/linux/capability.h"
1639typedef struct kernel_cap_struct kernel_cap_t;
1640#line 377
1641struct dentry;
1642#line 378
1643struct user_namespace;
1644#line 378
1645struct user_namespace;
1646#line 16 "include/linux/fiemap.h"
1647struct fiemap_extent {
1648   __u64 fe_logical ;
1649   __u64 fe_physical ;
1650   __u64 fe_length ;
1651   __u64 fe_reserved64[2] ;
1652   __u32 fe_flags ;
1653   __u32 fe_reserved[3] ;
1654};
1655#line 8 "include/linux/shrinker.h"
1656struct shrink_control {
1657   gfp_t gfp_mask ;
1658   unsigned long nr_to_scan ;
1659};
1660#line 31 "include/linux/shrinker.h"
1661struct shrinker {
1662   int (*shrink)(struct shrinker * , struct shrink_control *sc ) ;
1663   int seeks ;
1664   long batch ;
1665   struct list_head list ;
1666   atomic_long_t nr_in_batch ;
1667};
1668#line 10 "include/linux/migrate_mode.h"
1669enum migrate_mode {
1670    MIGRATE_ASYNC = 0,
1671    MIGRATE_SYNC_LIGHT = 1,
1672    MIGRATE_SYNC = 2
1673} ;
1674#line 408 "include/linux/fs.h"
1675struct export_operations;
1676#line 408
1677struct export_operations;
1678#line 410
1679struct iovec;
1680#line 410
1681struct iovec;
1682#line 411
1683struct nameidata;
1684#line 412
1685struct kiocb;
1686#line 412
1687struct kiocb;
1688#line 413
1689struct kobject;
1690#line 414
1691struct pipe_inode_info;
1692#line 414
1693struct pipe_inode_info;
1694#line 415
1695struct poll_table_struct;
1696#line 415
1697struct poll_table_struct;
1698#line 416
1699struct kstatfs;
1700#line 416
1701struct kstatfs;
1702#line 417
1703struct vm_area_struct;
1704#line 418
1705struct vfsmount;
1706#line 419
1707struct cred;
1708#line 469 "include/linux/fs.h"
1709struct iattr {
1710   unsigned int ia_valid ;
1711   umode_t ia_mode ;
1712   uid_t ia_uid ;
1713   gid_t ia_gid ;
1714   loff_t ia_size ;
1715   struct timespec ia_atime ;
1716   struct timespec ia_mtime ;
1717   struct timespec ia_ctime ;
1718   struct file *ia_file ;
1719};
1720#line 129 "include/linux/quota.h"
1721struct if_dqinfo {
1722   __u64 dqi_bgrace ;
1723   __u64 dqi_igrace ;
1724   __u32 dqi_flags ;
1725   __u32 dqi_valid ;
1726};
1727#line 50 "include/linux/dqblk_xfs.h"
1728struct fs_disk_quota {
1729   __s8 d_version ;
1730   __s8 d_flags ;
1731   __u16 d_fieldmask ;
1732   __u32 d_id ;
1733   __u64 d_blk_hardlimit ;
1734   __u64 d_blk_softlimit ;
1735   __u64 d_ino_hardlimit ;
1736   __u64 d_ino_softlimit ;
1737   __u64 d_bcount ;
1738   __u64 d_icount ;
1739   __s32 d_itimer ;
1740   __s32 d_btimer ;
1741   __u16 d_iwarns ;
1742   __u16 d_bwarns ;
1743   __s32 d_padding2 ;
1744   __u64 d_rtb_hardlimit ;
1745   __u64 d_rtb_softlimit ;
1746   __u64 d_rtbcount ;
1747   __s32 d_rtbtimer ;
1748   __u16 d_rtbwarns ;
1749   __s16 d_padding3 ;
1750   char d_padding4[8] ;
1751};
1752#line 146 "include/linux/dqblk_xfs.h"
1753struct fs_qfilestat {
1754   __u64 qfs_ino ;
1755   __u64 qfs_nblks ;
1756   __u32 qfs_nextents ;
1757};
1758#line 146 "include/linux/dqblk_xfs.h"
1759typedef struct fs_qfilestat fs_qfilestat_t;
1760#line 152 "include/linux/dqblk_xfs.h"
1761struct fs_quota_stat {
1762   __s8 qs_version ;
1763   __u16 qs_flags ;
1764   __s8 qs_pad ;
1765   fs_qfilestat_t qs_uquota ;
1766   fs_qfilestat_t qs_gquota ;
1767   __u32 qs_incoredqs ;
1768   __s32 qs_btimelimit ;
1769   __s32 qs_itimelimit ;
1770   __s32 qs_rtbtimelimit ;
1771   __u16 qs_bwarnlimit ;
1772   __u16 qs_iwarnlimit ;
1773};
1774#line 17 "include/linux/dqblk_qtree.h"
1775struct dquot;
1776#line 17
1777struct dquot;
1778#line 185 "include/linux/quota.h"
1779typedef __kernel_uid32_t qid_t;
1780#line 186 "include/linux/quota.h"
1781typedef long long qsize_t;
1782#line 200 "include/linux/quota.h"
1783struct mem_dqblk {
1784   qsize_t dqb_bhardlimit ;
1785   qsize_t dqb_bsoftlimit ;
1786   qsize_t dqb_curspace ;
1787   qsize_t dqb_rsvspace ;
1788   qsize_t dqb_ihardlimit ;
1789   qsize_t dqb_isoftlimit ;
1790   qsize_t dqb_curinodes ;
1791   time_t dqb_btime ;
1792   time_t dqb_itime ;
1793};
1794#line 215
1795struct quota_format_type;
1796#line 215
1797struct quota_format_type;
1798#line 217 "include/linux/quota.h"
1799struct mem_dqinfo {
1800   struct quota_format_type *dqi_format ;
1801   int dqi_fmt_id ;
1802   struct list_head dqi_dirty_list ;
1803   unsigned long dqi_flags ;
1804   unsigned int dqi_bgrace ;
1805   unsigned int dqi_igrace ;
1806   qsize_t dqi_maxblimit ;
1807   qsize_t dqi_maxilimit ;
1808   void *dqi_priv ;
1809};
1810#line 230
1811struct super_block;
1812#line 288 "include/linux/quota.h"
1813struct dquot {
1814   struct hlist_node dq_hash ;
1815   struct list_head dq_inuse ;
1816   struct list_head dq_free ;
1817   struct list_head dq_dirty ;
1818   struct mutex dq_lock ;
1819   atomic_t dq_count ;
1820   wait_queue_head_t dq_wait_unused ;
1821   struct super_block *dq_sb ;
1822   unsigned int dq_id ;
1823   loff_t dq_off ;
1824   unsigned long dq_flags ;
1825   short dq_type ;
1826   struct mem_dqblk dq_dqb ;
1827};
1828#line 305 "include/linux/quota.h"
1829struct quota_format_ops {
1830   int (*check_quota_file)(struct super_block *sb , int type ) ;
1831   int (*read_file_info)(struct super_block *sb , int type ) ;
1832   int (*write_file_info)(struct super_block *sb , int type ) ;
1833   int (*free_file_info)(struct super_block *sb , int type ) ;
1834   int (*read_dqblk)(struct dquot *dquot ) ;
1835   int (*commit_dqblk)(struct dquot *dquot ) ;
1836   int (*release_dqblk)(struct dquot *dquot ) ;
1837};
1838#line 316 "include/linux/quota.h"
1839struct dquot_operations {
1840   int (*write_dquot)(struct dquot * ) ;
1841   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
1842   void (*destroy_dquot)(struct dquot * ) ;
1843   int (*acquire_dquot)(struct dquot * ) ;
1844   int (*release_dquot)(struct dquot * ) ;
1845   int (*mark_dirty)(struct dquot * ) ;
1846   int (*write_info)(struct super_block * , int  ) ;
1847   qsize_t *(*get_reserved_space)(struct inode * ) ;
1848};
1849#line 329
1850struct path;
1851#line 332 "include/linux/quota.h"
1852struct quotactl_ops {
1853   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
1854   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
1855   int (*quota_off)(struct super_block * , int  ) ;
1856   int (*quota_sync)(struct super_block * , int  , int  ) ;
1857   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1858   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1859   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1860   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1861   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1862   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
1863};
1864#line 345 "include/linux/quota.h"
1865struct quota_format_type {
1866   int qf_fmt_id ;
1867   struct quota_format_ops  const  *qf_ops ;
1868   struct module *qf_owner ;
1869   struct quota_format_type *qf_next ;
1870};
1871#line 399 "include/linux/quota.h"
1872struct quota_info {
1873   unsigned int flags ;
1874   struct mutex dqio_mutex ;
1875   struct mutex dqonoff_mutex ;
1876   struct rw_semaphore dqptr_sem ;
1877   struct inode *files[2] ;
1878   struct mem_dqinfo info[2] ;
1879   struct quota_format_ops  const  *ops[2] ;
1880};
1881#line 532 "include/linux/fs.h"
1882struct page;
1883#line 533
1884struct address_space;
1885#line 533
1886struct address_space;
1887#line 534
1888struct writeback_control;
1889#line 534
1890struct writeback_control;
1891#line 577 "include/linux/fs.h"
1892union __anonunion_arg_218 {
1893   char *buf ;
1894   void *data ;
1895};
1896#line 577 "include/linux/fs.h"
1897struct __anonstruct_read_descriptor_t_217 {
1898   size_t written ;
1899   size_t count ;
1900   union __anonunion_arg_218 arg ;
1901   int error ;
1902};
1903#line 577 "include/linux/fs.h"
1904typedef struct __anonstruct_read_descriptor_t_217 read_descriptor_t;
1905#line 590 "include/linux/fs.h"
1906struct address_space_operations {
1907   int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
1908   int (*readpage)(struct file * , struct page * ) ;
1909   int (*writepages)(struct address_space * , struct writeback_control * ) ;
1910   int (*set_page_dirty)(struct page *page ) ;
1911   int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
1912                    unsigned int nr_pages ) ;
1913   int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
1914                      unsigned int len , unsigned int flags , struct page **pagep ,
1915                      void **fsdata ) ;
1916   int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
1917                    unsigned int copied , struct page *page , void *fsdata ) ;
1918   sector_t (*bmap)(struct address_space * , sector_t  ) ;
1919   void (*invalidatepage)(struct page * , unsigned long  ) ;
1920   int (*releasepage)(struct page * , gfp_t  ) ;
1921   void (*freepage)(struct page * ) ;
1922   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  *iov , loff_t offset ,
1923                        unsigned long nr_segs ) ;
1924   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
1925   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
1926   int (*launder_page)(struct page * ) ;
1927   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
1928   int (*error_remove_page)(struct address_space * , struct page * ) ;
1929};
1930#line 645
1931struct backing_dev_info;
1932#line 646 "include/linux/fs.h"
1933struct address_space {
1934   struct inode *host ;
1935   struct radix_tree_root page_tree ;
1936   spinlock_t tree_lock ;
1937   unsigned int i_mmap_writable ;
1938   struct prio_tree_root i_mmap ;
1939   struct list_head i_mmap_nonlinear ;
1940   struct mutex i_mmap_mutex ;
1941   unsigned long nrpages ;
1942   unsigned long writeback_index ;
1943   struct address_space_operations  const  *a_ops ;
1944   unsigned long flags ;
1945   struct backing_dev_info *backing_dev_info ;
1946   spinlock_t private_lock ;
1947   struct list_head private_list ;
1948   struct address_space *assoc_mapping ;
1949} __attribute__((__aligned__(sizeof(long )))) ;
1950#line 669
1951struct request_queue;
1952#line 669
1953struct request_queue;
1954#line 671
1955struct hd_struct;
1956#line 671
1957struct gendisk;
1958#line 671 "include/linux/fs.h"
1959struct block_device {
1960   dev_t bd_dev ;
1961   int bd_openers ;
1962   struct inode *bd_inode ;
1963   struct super_block *bd_super ;
1964   struct mutex bd_mutex ;
1965   struct list_head bd_inodes ;
1966   void *bd_claiming ;
1967   void *bd_holder ;
1968   int bd_holders ;
1969   bool bd_write_holder ;
1970   struct list_head bd_holder_disks ;
1971   struct block_device *bd_contains ;
1972   unsigned int bd_block_size ;
1973   struct hd_struct *bd_part ;
1974   unsigned int bd_part_count ;
1975   int bd_invalidated ;
1976   struct gendisk *bd_disk ;
1977   struct request_queue *bd_queue ;
1978   struct list_head bd_list ;
1979   unsigned long bd_private ;
1980   int bd_fsfreeze_count ;
1981   struct mutex bd_fsfreeze_mutex ;
1982};
1983#line 749
1984struct posix_acl;
1985#line 749
1986struct posix_acl;
1987#line 761
1988struct inode_operations;
1989#line 761 "include/linux/fs.h"
1990union __anonunion____missing_field_name_219 {
1991   unsigned int const   i_nlink ;
1992   unsigned int __i_nlink ;
1993};
1994#line 761 "include/linux/fs.h"
1995union __anonunion____missing_field_name_220 {
1996   struct list_head i_dentry ;
1997   struct rcu_head i_rcu ;
1998};
1999#line 761
2000struct file_lock;
2001#line 761 "include/linux/fs.h"
2002union __anonunion____missing_field_name_221 {
2003   struct pipe_inode_info *i_pipe ;
2004   struct block_device *i_bdev ;
2005   struct cdev *i_cdev ;
2006};
2007#line 761 "include/linux/fs.h"
2008struct inode {
2009   umode_t i_mode ;
2010   unsigned short i_opflags ;
2011   uid_t i_uid ;
2012   gid_t i_gid ;
2013   unsigned int i_flags ;
2014   struct posix_acl *i_acl ;
2015   struct posix_acl *i_default_acl ;
2016   struct inode_operations  const  *i_op ;
2017   struct super_block *i_sb ;
2018   struct address_space *i_mapping ;
2019   void *i_security ;
2020   unsigned long i_ino ;
2021   union __anonunion____missing_field_name_219 __annonCompField33 ;
2022   dev_t i_rdev ;
2023   struct timespec i_atime ;
2024   struct timespec i_mtime ;
2025   struct timespec i_ctime ;
2026   spinlock_t i_lock ;
2027   unsigned short i_bytes ;
2028   blkcnt_t i_blocks ;
2029   loff_t i_size ;
2030   unsigned long i_state ;
2031   struct mutex i_mutex ;
2032   unsigned long dirtied_when ;
2033   struct hlist_node i_hash ;
2034   struct list_head i_wb_list ;
2035   struct list_head i_lru ;
2036   struct list_head i_sb_list ;
2037   union __anonunion____missing_field_name_220 __annonCompField34 ;
2038   atomic_t i_count ;
2039   unsigned int i_blkbits ;
2040   u64 i_version ;
2041   atomic_t i_dio_count ;
2042   atomic_t i_writecount ;
2043   struct file_operations  const  *i_fop ;
2044   struct file_lock *i_flock ;
2045   struct address_space i_data ;
2046   struct dquot *i_dquot[2] ;
2047   struct list_head i_devices ;
2048   union __anonunion____missing_field_name_221 __annonCompField35 ;
2049   __u32 i_generation ;
2050   __u32 i_fsnotify_mask ;
2051   struct hlist_head i_fsnotify_marks ;
2052   atomic_t i_readcount ;
2053   void *i_private ;
2054};
2055#line 942 "include/linux/fs.h"
2056struct fown_struct {
2057   rwlock_t lock ;
2058   struct pid *pid ;
2059   enum pid_type pid_type ;
2060   uid_t uid ;
2061   uid_t euid ;
2062   int signum ;
2063};
2064#line 953 "include/linux/fs.h"
2065struct file_ra_state {
2066   unsigned long start ;
2067   unsigned int size ;
2068   unsigned int async_size ;
2069   unsigned int ra_pages ;
2070   unsigned int mmap_miss ;
2071   loff_t prev_pos ;
2072};
2073#line 976 "include/linux/fs.h"
2074union __anonunion_f_u_222 {
2075   struct list_head fu_list ;
2076   struct rcu_head fu_rcuhead ;
2077};
2078#line 976 "include/linux/fs.h"
2079struct file {
2080   union __anonunion_f_u_222 f_u ;
2081   struct path f_path ;
2082   struct file_operations  const  *f_op ;
2083   spinlock_t f_lock ;
2084   int f_sb_list_cpu ;
2085   atomic_long_t f_count ;
2086   unsigned int f_flags ;
2087   fmode_t f_mode ;
2088   loff_t f_pos ;
2089   struct fown_struct f_owner ;
2090   struct cred  const  *f_cred ;
2091   struct file_ra_state f_ra ;
2092   u64 f_version ;
2093   void *f_security ;
2094   void *private_data ;
2095   struct list_head f_ep_links ;
2096   struct list_head f_tfile_llink ;
2097   struct address_space *f_mapping ;
2098   unsigned long f_mnt_write_state ;
2099};
2100#line 1111
2101struct files_struct;
2102#line 1111 "include/linux/fs.h"
2103typedef struct files_struct *fl_owner_t;
2104#line 1113 "include/linux/fs.h"
2105struct file_lock_operations {
2106   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
2107   void (*fl_release_private)(struct file_lock * ) ;
2108};
2109#line 1118 "include/linux/fs.h"
2110struct lock_manager_operations {
2111   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
2112   void (*lm_notify)(struct file_lock * ) ;
2113   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
2114   void (*lm_release_private)(struct file_lock * ) ;
2115   void (*lm_break)(struct file_lock * ) ;
2116   int (*lm_change)(struct file_lock ** , int  ) ;
2117};
2118#line 4 "include/linux/nfs_fs_i.h"
2119struct nlm_lockowner;
2120#line 4
2121struct nlm_lockowner;
2122#line 9 "include/linux/nfs_fs_i.h"
2123struct nfs_lock_info {
2124   u32 state ;
2125   struct nlm_lockowner *owner ;
2126   struct list_head list ;
2127};
2128#line 15
2129struct nfs4_lock_state;
2130#line 15
2131struct nfs4_lock_state;
2132#line 16 "include/linux/nfs_fs_i.h"
2133struct nfs4_lock_info {
2134   struct nfs4_lock_state *owner ;
2135};
2136#line 1138 "include/linux/fs.h"
2137struct fasync_struct;
2138#line 1138 "include/linux/fs.h"
2139struct __anonstruct_afs_224 {
2140   struct list_head link ;
2141   int state ;
2142};
2143#line 1138 "include/linux/fs.h"
2144union __anonunion_fl_u_223 {
2145   struct nfs_lock_info nfs_fl ;
2146   struct nfs4_lock_info nfs4_fl ;
2147   struct __anonstruct_afs_224 afs ;
2148};
2149#line 1138 "include/linux/fs.h"
2150struct file_lock {
2151   struct file_lock *fl_next ;
2152   struct list_head fl_link ;
2153   struct list_head fl_block ;
2154   fl_owner_t fl_owner ;
2155   unsigned int fl_flags ;
2156   unsigned char fl_type ;
2157   unsigned int fl_pid ;
2158   struct pid *fl_nspid ;
2159   wait_queue_head_t fl_wait ;
2160   struct file *fl_file ;
2161   loff_t fl_start ;
2162   loff_t fl_end ;
2163   struct fasync_struct *fl_fasync ;
2164   unsigned long fl_break_time ;
2165   unsigned long fl_downgrade_time ;
2166   struct file_lock_operations  const  *fl_ops ;
2167   struct lock_manager_operations  const  *fl_lmops ;
2168   union __anonunion_fl_u_223 fl_u ;
2169};
2170#line 1378 "include/linux/fs.h"
2171struct fasync_struct {
2172   spinlock_t fa_lock ;
2173   int magic ;
2174   int fa_fd ;
2175   struct fasync_struct *fa_next ;
2176   struct file *fa_file ;
2177   struct rcu_head fa_rcu ;
2178};
2179#line 1418
2180struct file_system_type;
2181#line 1418
2182struct super_operations;
2183#line 1418
2184struct xattr_handler;
2185#line 1418
2186struct mtd_info;
2187#line 1418 "include/linux/fs.h"
2188struct super_block {
2189   struct list_head s_list ;
2190   dev_t s_dev ;
2191   unsigned char s_dirt ;
2192   unsigned char s_blocksize_bits ;
2193   unsigned long s_blocksize ;
2194   loff_t s_maxbytes ;
2195   struct file_system_type *s_type ;
2196   struct super_operations  const  *s_op ;
2197   struct dquot_operations  const  *dq_op ;
2198   struct quotactl_ops  const  *s_qcop ;
2199   struct export_operations  const  *s_export_op ;
2200   unsigned long s_flags ;
2201   unsigned long s_magic ;
2202   struct dentry *s_root ;
2203   struct rw_semaphore s_umount ;
2204   struct mutex s_lock ;
2205   int s_count ;
2206   atomic_t s_active ;
2207   void *s_security ;
2208   struct xattr_handler  const  **s_xattr ;
2209   struct list_head s_inodes ;
2210   struct hlist_bl_head s_anon ;
2211   struct list_head *s_files ;
2212   struct list_head s_mounts ;
2213   struct list_head s_dentry_lru ;
2214   int s_nr_dentry_unused ;
2215   spinlock_t s_inode_lru_lock  __attribute__((__aligned__((1) <<  (6) ))) ;
2216   struct list_head s_inode_lru ;
2217   int s_nr_inodes_unused ;
2218   struct block_device *s_bdev ;
2219   struct backing_dev_info *s_bdi ;
2220   struct mtd_info *s_mtd ;
2221   struct hlist_node s_instances ;
2222   struct quota_info s_dquot ;
2223   int s_frozen ;
2224   wait_queue_head_t s_wait_unfrozen ;
2225   char s_id[32] ;
2226   u8 s_uuid[16] ;
2227   void *s_fs_info ;
2228   unsigned int s_max_links ;
2229   fmode_t s_mode ;
2230   u32 s_time_gran ;
2231   struct mutex s_vfs_rename_mutex ;
2232   char *s_subtype ;
2233   char *s_options ;
2234   struct dentry_operations  const  *s_d_op ;
2235   int cleancache_poolid ;
2236   struct shrinker s_shrink ;
2237   atomic_long_t s_remove_count ;
2238   int s_readonly_remount ;
2239};
2240#line 1567 "include/linux/fs.h"
2241struct fiemap_extent_info {
2242   unsigned int fi_flags ;
2243   unsigned int fi_extents_mapped ;
2244   unsigned int fi_extents_max ;
2245   struct fiemap_extent *fi_extents_start ;
2246};
2247#line 1609 "include/linux/fs.h"
2248struct file_operations {
2249   struct module *owner ;
2250   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
2251   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
2252   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
2253   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
2254                       loff_t  ) ;
2255   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
2256                        loff_t  ) ;
2257   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
2258                                                   loff_t  , u64  , unsigned int  ) ) ;
2259   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
2260   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
2261   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
2262   int (*mmap)(struct file * , struct vm_area_struct * ) ;
2263   int (*open)(struct inode * , struct file * ) ;
2264   int (*flush)(struct file * , fl_owner_t id ) ;
2265   int (*release)(struct inode * , struct file * ) ;
2266   int (*fsync)(struct file * , loff_t  , loff_t  , int datasync ) ;
2267   int (*aio_fsync)(struct kiocb * , int datasync ) ;
2268   int (*fasync)(int  , struct file * , int  ) ;
2269   int (*lock)(struct file * , int  , struct file_lock * ) ;
2270   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
2271                       int  ) ;
2272   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
2273                                      unsigned long  , unsigned long  ) ;
2274   int (*check_flags)(int  ) ;
2275   int (*flock)(struct file * , int  , struct file_lock * ) ;
2276   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
2277                           unsigned int  ) ;
2278   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
2279                          unsigned int  ) ;
2280   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
2281   long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
2282};
2283#line 1639 "include/linux/fs.h"
2284struct inode_operations {
2285   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
2286   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
2287   int (*permission)(struct inode * , int  ) ;
2288   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
2289   int (*readlink)(struct dentry * , char * , int  ) ;
2290   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
2291   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
2292   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
2293   int (*unlink)(struct inode * , struct dentry * ) ;
2294   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
2295   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
2296   int (*rmdir)(struct inode * , struct dentry * ) ;
2297   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
2298   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
2299   void (*truncate)(struct inode * ) ;
2300   int (*setattr)(struct dentry * , struct iattr * ) ;
2301   int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
2302   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
2303   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
2304   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
2305   int (*removexattr)(struct dentry * , char const   * ) ;
2306   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
2307   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
2308} __attribute__((__aligned__((1) <<  (6) ))) ;
2309#line 1669
2310struct seq_file;
2311#line 1684 "include/linux/fs.h"
2312struct super_operations {
2313   struct inode *(*alloc_inode)(struct super_block *sb ) ;
2314   void (*destroy_inode)(struct inode * ) ;
2315   void (*dirty_inode)(struct inode * , int flags ) ;
2316   int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
2317   int (*drop_inode)(struct inode * ) ;
2318   void (*evict_inode)(struct inode * ) ;
2319   void (*put_super)(struct super_block * ) ;
2320   void (*write_super)(struct super_block * ) ;
2321   int (*sync_fs)(struct super_block *sb , int wait ) ;
2322   int (*freeze_fs)(struct super_block * ) ;
2323   int (*unfreeze_fs)(struct super_block * ) ;
2324   int (*statfs)(struct dentry * , struct kstatfs * ) ;
2325   int (*remount_fs)(struct super_block * , int * , char * ) ;
2326   void (*umount_begin)(struct super_block * ) ;
2327   int (*show_options)(struct seq_file * , struct dentry * ) ;
2328   int (*show_devname)(struct seq_file * , struct dentry * ) ;
2329   int (*show_path)(struct seq_file * , struct dentry * ) ;
2330   int (*show_stats)(struct seq_file * , struct dentry * ) ;
2331   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
2332   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
2333                          loff_t  ) ;
2334   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
2335   int (*nr_cached_objects)(struct super_block * ) ;
2336   void (*free_cached_objects)(struct super_block * , int  ) ;
2337};
2338#line 1835 "include/linux/fs.h"
2339struct file_system_type {
2340   char const   *name ;
2341   int fs_flags ;
2342   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
2343   void (*kill_sb)(struct super_block * ) ;
2344   struct module *owner ;
2345   struct file_system_type *next ;
2346   struct hlist_head fs_supers ;
2347   struct lock_class_key s_lock_key ;
2348   struct lock_class_key s_umount_key ;
2349   struct lock_class_key s_vfs_rename_key ;
2350   struct lock_class_key i_lock_key ;
2351   struct lock_class_key i_mutex_key ;
2352   struct lock_class_key i_mutex_dir_key ;
2353};
2354#line 28 "include/linux/poll.h"
2355struct poll_table_struct;
2356#line 39 "include/linux/poll.h"
2357struct poll_table_struct {
2358   void (*_qproc)(struct file * , wait_queue_head_t * , struct poll_table_struct * ) ;
2359   unsigned long _key ;
2360};
2361#line 143 "include/linux/rtc.h"
2362struct rtc_class_ops {
2363   int (*open)(struct device * ) ;
2364   void (*release)(struct device * ) ;
2365   int (*ioctl)(struct device * , unsigned int  , unsigned long  ) ;
2366   int (*read_time)(struct device * , struct rtc_time * ) ;
2367   int (*set_time)(struct device * , struct rtc_time * ) ;
2368   int (*read_alarm)(struct device * , struct rtc_wkalrm * ) ;
2369   int (*set_alarm)(struct device * , struct rtc_wkalrm * ) ;
2370   int (*proc)(struct device * , struct seq_file * ) ;
2371   int (*set_mmss)(struct device * , unsigned long secs ) ;
2372   int (*read_callback)(struct device * , int data ) ;
2373   int (*alarm_irq_enable)(struct device * , unsigned int enabled ) ;
2374};
2375#line 158 "include/linux/rtc.h"
2376struct rtc_task {
2377   void (*func)(void *private_data ) ;
2378   void *private_data ;
2379};
2380#line 164 "include/linux/rtc.h"
2381struct rtc_timer {
2382   struct rtc_task task ;
2383   struct timerqueue_node node ;
2384   ktime_t period ;
2385   int enabled ;
2386};
2387#line 175 "include/linux/rtc.h"
2388struct rtc_device {
2389   struct device dev ;
2390   struct module *owner ;
2391   int id ;
2392   char name[20] ;
2393   struct rtc_class_ops  const  *ops ;
2394   struct mutex ops_lock ;
2395   struct cdev char_dev ;
2396   unsigned long flags ;
2397   unsigned long irq_data ;
2398   spinlock_t irq_lock ;
2399   wait_queue_head_t irq_queue ;
2400   struct fasync_struct *async_queue ;
2401   struct rtc_task *irq_task ;
2402   spinlock_t irq_task_lock ;
2403   int irq_freq ;
2404   int max_user_freq ;
2405   struct timerqueue_head timerqueue ;
2406   struct rtc_timer aie_timer ;
2407   struct rtc_timer uie_rtctimer ;
2408   struct hrtimer pie_timer ;
2409   int pie_enabled ;
2410   struct work_struct irqwork ;
2411   int uie_unsupported ;
2412   struct work_struct uie_task ;
2413   struct timer_list uie_timer ;
2414   unsigned int oldsecs ;
2415   unsigned int uie_irq_active : 1 ;
2416   unsigned int stop_uie_polling : 1 ;
2417   unsigned int uie_task_active : 1 ;
2418   unsigned int uie_timer_active : 1 ;
2419};
2420#line 46 "include/linux/slub_def.h"
2421struct kmem_cache_cpu {
2422   void **freelist ;
2423   unsigned long tid ;
2424   struct page *page ;
2425   struct page *partial ;
2426   int node ;
2427   unsigned int stat[26] ;
2428};
2429#line 57 "include/linux/slub_def.h"
2430struct kmem_cache_node {
2431   spinlock_t list_lock ;
2432   unsigned long nr_partial ;
2433   struct list_head partial ;
2434   atomic_long_t nr_slabs ;
2435   atomic_long_t total_objects ;
2436   struct list_head full ;
2437};
2438#line 73 "include/linux/slub_def.h"
2439struct kmem_cache_order_objects {
2440   unsigned long x ;
2441};
2442#line 80 "include/linux/slub_def.h"
2443struct kmem_cache {
2444   struct kmem_cache_cpu *cpu_slab ;
2445   unsigned long flags ;
2446   unsigned long min_partial ;
2447   int size ;
2448   int objsize ;
2449   int offset ;
2450   int cpu_partial ;
2451   struct kmem_cache_order_objects oo ;
2452   struct kmem_cache_order_objects max ;
2453   struct kmem_cache_order_objects min ;
2454   gfp_t allocflags ;
2455   int refcount ;
2456   void (*ctor)(void * ) ;
2457   int inuse ;
2458   int align ;
2459   int reserved ;
2460   char const   *name ;
2461   struct list_head list ;
2462   struct kobject kobj ;
2463   int remote_node_defrag_ratio ;
2464   struct kmem_cache_node *node[1 << 10] ;
2465};
2466#line 23 "include/linux/mm_types.h"
2467struct address_space;
2468#line 40 "include/linux/mm_types.h"
2469union __anonunion____missing_field_name_229 {
2470   unsigned long index ;
2471   void *freelist ;
2472};
2473#line 40 "include/linux/mm_types.h"
2474struct __anonstruct____missing_field_name_233 {
2475   unsigned int inuse : 16 ;
2476   unsigned int objects : 15 ;
2477   unsigned int frozen : 1 ;
2478};
2479#line 40 "include/linux/mm_types.h"
2480union __anonunion____missing_field_name_232 {
2481   atomic_t _mapcount ;
2482   struct __anonstruct____missing_field_name_233 __annonCompField37 ;
2483};
2484#line 40 "include/linux/mm_types.h"
2485struct __anonstruct____missing_field_name_231 {
2486   union __anonunion____missing_field_name_232 __annonCompField38 ;
2487   atomic_t _count ;
2488};
2489#line 40 "include/linux/mm_types.h"
2490union __anonunion____missing_field_name_230 {
2491   unsigned long counters ;
2492   struct __anonstruct____missing_field_name_231 __annonCompField39 ;
2493};
2494#line 40 "include/linux/mm_types.h"
2495struct __anonstruct____missing_field_name_228 {
2496   union __anonunion____missing_field_name_229 __annonCompField36 ;
2497   union __anonunion____missing_field_name_230 __annonCompField40 ;
2498};
2499#line 40 "include/linux/mm_types.h"
2500struct __anonstruct____missing_field_name_235 {
2501   struct page *next ;
2502   int pages ;
2503   int pobjects ;
2504};
2505#line 40 "include/linux/mm_types.h"
2506union __anonunion____missing_field_name_234 {
2507   struct list_head lru ;
2508   struct __anonstruct____missing_field_name_235 __annonCompField42 ;
2509};
2510#line 40 "include/linux/mm_types.h"
2511union __anonunion____missing_field_name_236 {
2512   unsigned long private ;
2513   struct kmem_cache *slab ;
2514   struct page *first_page ;
2515};
2516#line 40 "include/linux/mm_types.h"
2517struct page {
2518   unsigned long flags ;
2519   struct address_space *mapping ;
2520   struct __anonstruct____missing_field_name_228 __annonCompField41 ;
2521   union __anonunion____missing_field_name_234 __annonCompField43 ;
2522   union __anonunion____missing_field_name_236 __annonCompField44 ;
2523   unsigned long debug_flags ;
2524} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
2525#line 200 "include/linux/mm_types.h"
2526struct __anonstruct_vm_set_238 {
2527   struct list_head list ;
2528   void *parent ;
2529   struct vm_area_struct *head ;
2530};
2531#line 200 "include/linux/mm_types.h"
2532union __anonunion_shared_237 {
2533   struct __anonstruct_vm_set_238 vm_set ;
2534   struct raw_prio_tree_node prio_tree_node ;
2535};
2536#line 200
2537struct anon_vma;
2538#line 200
2539struct vm_operations_struct;
2540#line 200
2541struct mempolicy;
2542#line 200 "include/linux/mm_types.h"
2543struct vm_area_struct {
2544   struct mm_struct *vm_mm ;
2545   unsigned long vm_start ;
2546   unsigned long vm_end ;
2547   struct vm_area_struct *vm_next ;
2548   struct vm_area_struct *vm_prev ;
2549   pgprot_t vm_page_prot ;
2550   unsigned long vm_flags ;
2551   struct rb_node vm_rb ;
2552   union __anonunion_shared_237 shared ;
2553   struct list_head anon_vma_chain ;
2554   struct anon_vma *anon_vma ;
2555   struct vm_operations_struct  const  *vm_ops ;
2556   unsigned long vm_pgoff ;
2557   struct file *vm_file ;
2558   void *vm_private_data ;
2559   struct mempolicy *vm_policy ;
2560};
2561#line 257 "include/linux/mm_types.h"
2562struct core_thread {
2563   struct task_struct *task ;
2564   struct core_thread *next ;
2565};
2566#line 262 "include/linux/mm_types.h"
2567struct core_state {
2568   atomic_t nr_threads ;
2569   struct core_thread dumper ;
2570   struct completion startup ;
2571};
2572#line 284 "include/linux/mm_types.h"
2573struct mm_rss_stat {
2574   atomic_long_t count[3] ;
2575};
2576#line 288
2577struct linux_binfmt;
2578#line 288
2579struct mmu_notifier_mm;
2580#line 288 "include/linux/mm_types.h"
2581struct mm_struct {
2582   struct vm_area_struct *mmap ;
2583   struct rb_root mm_rb ;
2584   struct vm_area_struct *mmap_cache ;
2585   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
2586                                      unsigned long pgoff , unsigned long flags ) ;
2587   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
2588   unsigned long mmap_base ;
2589   unsigned long task_size ;
2590   unsigned long cached_hole_size ;
2591   unsigned long free_area_cache ;
2592   pgd_t *pgd ;
2593   atomic_t mm_users ;
2594   atomic_t mm_count ;
2595   int map_count ;
2596   spinlock_t page_table_lock ;
2597   struct rw_semaphore mmap_sem ;
2598   struct list_head mmlist ;
2599   unsigned long hiwater_rss ;
2600   unsigned long hiwater_vm ;
2601   unsigned long total_vm ;
2602   unsigned long locked_vm ;
2603   unsigned long pinned_vm ;
2604   unsigned long shared_vm ;
2605   unsigned long exec_vm ;
2606   unsigned long stack_vm ;
2607   unsigned long reserved_vm ;
2608   unsigned long def_flags ;
2609   unsigned long nr_ptes ;
2610   unsigned long start_code ;
2611   unsigned long end_code ;
2612   unsigned long start_data ;
2613   unsigned long end_data ;
2614   unsigned long start_brk ;
2615   unsigned long brk ;
2616   unsigned long start_stack ;
2617   unsigned long arg_start ;
2618   unsigned long arg_end ;
2619   unsigned long env_start ;
2620   unsigned long env_end ;
2621   unsigned long saved_auxv[44] ;
2622   struct mm_rss_stat rss_stat ;
2623   struct linux_binfmt *binfmt ;
2624   cpumask_var_t cpu_vm_mask_var ;
2625   mm_context_t context ;
2626   unsigned int faultstamp ;
2627   unsigned int token_priority ;
2628   unsigned int last_interval ;
2629   unsigned long flags ;
2630   struct core_state *core_state ;
2631   spinlock_t ioctx_lock ;
2632   struct hlist_head ioctx_list ;
2633   struct task_struct *owner ;
2634   struct file *exe_file ;
2635   unsigned long num_exe_file_vmas ;
2636   struct mmu_notifier_mm *mmu_notifier_mm ;
2637   pgtable_t pmd_huge_pte ;
2638   struct cpumask cpumask_allocation ;
2639};
2640#line 7 "include/asm-generic/cputime.h"
2641typedef unsigned long cputime_t;
2642#line 84 "include/linux/sem.h"
2643struct task_struct;
2644#line 101
2645struct sem_undo_list;
2646#line 101 "include/linux/sem.h"
2647struct sysv_sem {
2648   struct sem_undo_list *undo_list ;
2649};
2650#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2651struct siginfo;
2652#line 10
2653struct siginfo;
2654#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2655struct __anonstruct_sigset_t_240 {
2656   unsigned long sig[1] ;
2657};
2658#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2659typedef struct __anonstruct_sigset_t_240 sigset_t;
2660#line 17 "include/asm-generic/signal-defs.h"
2661typedef void __signalfn_t(int  );
2662#line 18 "include/asm-generic/signal-defs.h"
2663typedef __signalfn_t *__sighandler_t;
2664#line 20 "include/asm-generic/signal-defs.h"
2665typedef void __restorefn_t(void);
2666#line 21 "include/asm-generic/signal-defs.h"
2667typedef __restorefn_t *__sigrestore_t;
2668#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2669struct sigaction {
2670   __sighandler_t sa_handler ;
2671   unsigned long sa_flags ;
2672   __sigrestore_t sa_restorer ;
2673   sigset_t sa_mask ;
2674};
2675#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
2676struct k_sigaction {
2677   struct sigaction sa ;
2678};
2679#line 7 "include/asm-generic/siginfo.h"
2680union sigval {
2681   int sival_int ;
2682   void *sival_ptr ;
2683};
2684#line 7 "include/asm-generic/siginfo.h"
2685typedef union sigval sigval_t;
2686#line 48 "include/asm-generic/siginfo.h"
2687struct __anonstruct__kill_242 {
2688   __kernel_pid_t _pid ;
2689   __kernel_uid32_t _uid ;
2690};
2691#line 48 "include/asm-generic/siginfo.h"
2692struct __anonstruct__timer_243 {
2693   __kernel_timer_t _tid ;
2694   int _overrun ;
2695   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
2696   sigval_t _sigval ;
2697   int _sys_private ;
2698};
2699#line 48 "include/asm-generic/siginfo.h"
2700struct __anonstruct__rt_244 {
2701   __kernel_pid_t _pid ;
2702   __kernel_uid32_t _uid ;
2703   sigval_t _sigval ;
2704};
2705#line 48 "include/asm-generic/siginfo.h"
2706struct __anonstruct__sigchld_245 {
2707   __kernel_pid_t _pid ;
2708   __kernel_uid32_t _uid ;
2709   int _status ;
2710   __kernel_clock_t _utime ;
2711   __kernel_clock_t _stime ;
2712};
2713#line 48 "include/asm-generic/siginfo.h"
2714struct __anonstruct__sigfault_246 {
2715   void *_addr ;
2716   short _addr_lsb ;
2717};
2718#line 48 "include/asm-generic/siginfo.h"
2719struct __anonstruct__sigpoll_247 {
2720   long _band ;
2721   int _fd ;
2722};
2723#line 48 "include/asm-generic/siginfo.h"
2724union __anonunion__sifields_241 {
2725   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
2726   struct __anonstruct__kill_242 _kill ;
2727   struct __anonstruct__timer_243 _timer ;
2728   struct __anonstruct__rt_244 _rt ;
2729   struct __anonstruct__sigchld_245 _sigchld ;
2730   struct __anonstruct__sigfault_246 _sigfault ;
2731   struct __anonstruct__sigpoll_247 _sigpoll ;
2732};
2733#line 48 "include/asm-generic/siginfo.h"
2734struct siginfo {
2735   int si_signo ;
2736   int si_errno ;
2737   int si_code ;
2738   union __anonunion__sifields_241 _sifields ;
2739};
2740#line 48 "include/asm-generic/siginfo.h"
2741typedef struct siginfo siginfo_t;
2742#line 288
2743struct siginfo;
2744#line 10 "include/linux/signal.h"
2745struct task_struct;
2746#line 18
2747struct user_struct;
2748#line 28 "include/linux/signal.h"
2749struct sigpending {
2750   struct list_head list ;
2751   sigset_t signal ;
2752};
2753#line 239
2754struct timespec;
2755#line 240
2756struct pt_regs;
2757#line 10 "include/linux/seccomp.h"
2758struct __anonstruct_seccomp_t_250 {
2759   int mode ;
2760};
2761#line 10 "include/linux/seccomp.h"
2762typedef struct __anonstruct_seccomp_t_250 seccomp_t;
2763#line 81 "include/linux/plist.h"
2764struct plist_head {
2765   struct list_head node_list ;
2766};
2767#line 85 "include/linux/plist.h"
2768struct plist_node {
2769   int prio ;
2770   struct list_head prio_list ;
2771   struct list_head node_list ;
2772};
2773#line 40 "include/linux/rtmutex.h"
2774struct rt_mutex_waiter;
2775#line 40
2776struct rt_mutex_waiter;
2777#line 42 "include/linux/resource.h"
2778struct rlimit {
2779   unsigned long rlim_cur ;
2780   unsigned long rlim_max ;
2781};
2782#line 81
2783struct task_struct;
2784#line 11 "include/linux/task_io_accounting.h"
2785struct task_io_accounting {
2786   u64 rchar ;
2787   u64 wchar ;
2788   u64 syscr ;
2789   u64 syscw ;
2790   u64 read_bytes ;
2791   u64 write_bytes ;
2792   u64 cancelled_write_bytes ;
2793};
2794#line 13 "include/linux/latencytop.h"
2795struct task_struct;
2796#line 20 "include/linux/latencytop.h"
2797struct latency_record {
2798   unsigned long backtrace[12] ;
2799   unsigned int count ;
2800   unsigned long time ;
2801   unsigned long max ;
2802};
2803#line 29 "include/linux/key.h"
2804typedef int32_t key_serial_t;
2805#line 32 "include/linux/key.h"
2806typedef uint32_t key_perm_t;
2807#line 34
2808struct key;
2809#line 34
2810struct key;
2811#line 74
2812struct seq_file;
2813#line 75
2814struct user_struct;
2815#line 76
2816struct signal_struct;
2817#line 76
2818struct signal_struct;
2819#line 77
2820struct cred;
2821#line 79
2822struct key_type;
2823#line 79
2824struct key_type;
2825#line 81
2826struct keyring_list;
2827#line 81
2828struct keyring_list;
2829#line 124
2830struct key_user;
2831#line 124 "include/linux/key.h"
2832union __anonunion____missing_field_name_251 {
2833   time_t expiry ;
2834   time_t revoked_at ;
2835};
2836#line 124 "include/linux/key.h"
2837union __anonunion_type_data_252 {
2838   struct list_head link ;
2839   unsigned long x[2] ;
2840   void *p[2] ;
2841   int reject_error ;
2842};
2843#line 124 "include/linux/key.h"
2844union __anonunion_payload_253 {
2845   unsigned long value ;
2846   void *rcudata ;
2847   void *data ;
2848   struct keyring_list *subscriptions ;
2849};
2850#line 124 "include/linux/key.h"
2851struct key {
2852   atomic_t usage ;
2853   key_serial_t serial ;
2854   struct rb_node serial_node ;
2855   struct key_type *type ;
2856   struct rw_semaphore sem ;
2857   struct key_user *user ;
2858   void *security ;
2859   union __anonunion____missing_field_name_251 __annonCompField45 ;
2860   uid_t uid ;
2861   gid_t gid ;
2862   key_perm_t perm ;
2863   unsigned short quotalen ;
2864   unsigned short datalen ;
2865   unsigned long flags ;
2866   char *description ;
2867   union __anonunion_type_data_252 type_data ;
2868   union __anonunion_payload_253 payload ;
2869};
2870#line 18 "include/linux/selinux.h"
2871struct audit_context;
2872#line 18
2873struct audit_context;
2874#line 21 "include/linux/cred.h"
2875struct user_struct;
2876#line 22
2877struct cred;
2878#line 23
2879struct inode;
2880#line 31 "include/linux/cred.h"
2881struct group_info {
2882   atomic_t usage ;
2883   int ngroups ;
2884   int nblocks ;
2885   gid_t small_block[32] ;
2886   gid_t *blocks[0] ;
2887};
2888#line 83 "include/linux/cred.h"
2889struct thread_group_cred {
2890   atomic_t usage ;
2891   pid_t tgid ;
2892   spinlock_t lock ;
2893   struct key *session_keyring ;
2894   struct key *process_keyring ;
2895   struct rcu_head rcu ;
2896};
2897#line 116 "include/linux/cred.h"
2898struct cred {
2899   atomic_t usage ;
2900   atomic_t subscribers ;
2901   void *put_addr ;
2902   unsigned int magic ;
2903   uid_t uid ;
2904   gid_t gid ;
2905   uid_t suid ;
2906   gid_t sgid ;
2907   uid_t euid ;
2908   gid_t egid ;
2909   uid_t fsuid ;
2910   gid_t fsgid ;
2911   unsigned int securebits ;
2912   kernel_cap_t cap_inheritable ;
2913   kernel_cap_t cap_permitted ;
2914   kernel_cap_t cap_effective ;
2915   kernel_cap_t cap_bset ;
2916   unsigned char jit_keyring ;
2917   struct key *thread_keyring ;
2918   struct key *request_key_auth ;
2919   struct thread_group_cred *tgcred ;
2920   void *security ;
2921   struct user_struct *user ;
2922   struct user_namespace *user_ns ;
2923   struct group_info *group_info ;
2924   struct rcu_head rcu ;
2925};
2926#line 61 "include/linux/llist.h"
2927struct llist_node;
2928#line 65 "include/linux/llist.h"
2929struct llist_node {
2930   struct llist_node *next ;
2931};
2932#line 97 "include/linux/sched.h"
2933struct futex_pi_state;
2934#line 97
2935struct futex_pi_state;
2936#line 98
2937struct robust_list_head;
2938#line 98
2939struct robust_list_head;
2940#line 99
2941struct bio_list;
2942#line 99
2943struct bio_list;
2944#line 100
2945struct fs_struct;
2946#line 100
2947struct fs_struct;
2948#line 101
2949struct perf_event_context;
2950#line 101
2951struct perf_event_context;
2952#line 102
2953struct blk_plug;
2954#line 102
2955struct blk_plug;
2956#line 150
2957struct seq_file;
2958#line 151
2959struct cfs_rq;
2960#line 151
2961struct cfs_rq;
2962#line 259
2963struct task_struct;
2964#line 366
2965struct nsproxy;
2966#line 367
2967struct user_namespace;
2968#line 58 "include/linux/aio_abi.h"
2969struct io_event {
2970   __u64 data ;
2971   __u64 obj ;
2972   __s64 res ;
2973   __s64 res2 ;
2974};
2975#line 16 "include/linux/uio.h"
2976struct iovec {
2977   void *iov_base ;
2978   __kernel_size_t iov_len ;
2979};
2980#line 15 "include/linux/aio.h"
2981struct kioctx;
2982#line 15
2983struct kioctx;
2984#line 87 "include/linux/aio.h"
2985union __anonunion_ki_obj_255 {
2986   void *user ;
2987   struct task_struct *tsk ;
2988};
2989#line 87
2990struct eventfd_ctx;
2991#line 87 "include/linux/aio.h"
2992struct kiocb {
2993   struct list_head ki_run_list ;
2994   unsigned long ki_flags ;
2995   int ki_users ;
2996   unsigned int ki_key ;
2997   struct file *ki_filp ;
2998   struct kioctx *ki_ctx ;
2999   int (*ki_cancel)(struct kiocb * , struct io_event * ) ;
3000   ssize_t (*ki_retry)(struct kiocb * ) ;
3001   void (*ki_dtor)(struct kiocb * ) ;
3002   union __anonunion_ki_obj_255 ki_obj ;
3003   __u64 ki_user_data ;
3004   loff_t ki_pos ;
3005   void *private ;
3006   unsigned short ki_opcode ;
3007   size_t ki_nbytes ;
3008   char *ki_buf ;
3009   size_t ki_left ;
3010   struct iovec ki_inline_vec ;
3011   struct iovec *ki_iovec ;
3012   unsigned long ki_nr_segs ;
3013   unsigned long ki_cur_seg ;
3014   struct list_head ki_list ;
3015   struct list_head ki_batch ;
3016   struct eventfd_ctx *ki_eventfd ;
3017};
3018#line 166 "include/linux/aio.h"
3019struct aio_ring_info {
3020   unsigned long mmap_base ;
3021   unsigned long mmap_size ;
3022   struct page **ring_pages ;
3023   spinlock_t ring_lock ;
3024   long nr_pages ;
3025   unsigned int nr ;
3026   unsigned int tail ;
3027   struct page *internal_pages[8] ;
3028};
3029#line 179 "include/linux/aio.h"
3030struct kioctx {
3031   atomic_t users ;
3032   int dead ;
3033   struct mm_struct *mm ;
3034   unsigned long user_id ;
3035   struct hlist_node list ;
3036   wait_queue_head_t wait ;
3037   spinlock_t ctx_lock ;
3038   int reqs_active ;
3039   struct list_head active_reqs ;
3040   struct list_head run_list ;
3041   unsigned int max_reqs ;
3042   struct aio_ring_info ring_info ;
3043   struct delayed_work wq ;
3044   struct rcu_head rcu_head ;
3045};
3046#line 214
3047struct mm_struct;
3048#line 443 "include/linux/sched.h"
3049struct sighand_struct {
3050   atomic_t count ;
3051   struct k_sigaction action[64] ;
3052   spinlock_t siglock ;
3053   wait_queue_head_t signalfd_wqh ;
3054};
3055#line 450 "include/linux/sched.h"
3056struct pacct_struct {
3057   int ac_flag ;
3058   long ac_exitcode ;
3059   unsigned long ac_mem ;
3060   cputime_t ac_utime ;
3061   cputime_t ac_stime ;
3062   unsigned long ac_minflt ;
3063   unsigned long ac_majflt ;
3064};
3065#line 458 "include/linux/sched.h"
3066struct cpu_itimer {
3067   cputime_t expires ;
3068   cputime_t incr ;
3069   u32 error ;
3070   u32 incr_error ;
3071};
3072#line 476 "include/linux/sched.h"
3073struct task_cputime {
3074   cputime_t utime ;
3075   cputime_t stime ;
3076   unsigned long long sum_exec_runtime ;
3077};
3078#line 512 "include/linux/sched.h"
3079struct thread_group_cputimer {
3080   struct task_cputime cputime ;
3081   int running ;
3082   raw_spinlock_t lock ;
3083};
3084#line 519
3085struct autogroup;
3086#line 519
3087struct autogroup;
3088#line 528
3089struct tty_struct;
3090#line 528
3091struct taskstats;
3092#line 528
3093struct tty_audit_buf;
3094#line 528 "include/linux/sched.h"
3095struct signal_struct {
3096   atomic_t sigcnt ;
3097   atomic_t live ;
3098   int nr_threads ;
3099   wait_queue_head_t wait_chldexit ;
3100   struct task_struct *curr_target ;
3101   struct sigpending shared_pending ;
3102   int group_exit_code ;
3103   int notify_count ;
3104   struct task_struct *group_exit_task ;
3105   int group_stop_count ;
3106   unsigned int flags ;
3107   unsigned int is_child_subreaper : 1 ;
3108   unsigned int has_child_subreaper : 1 ;
3109   struct list_head posix_timers ;
3110   struct hrtimer real_timer ;
3111   struct pid *leader_pid ;
3112   ktime_t it_real_incr ;
3113   struct cpu_itimer it[2] ;
3114   struct thread_group_cputimer cputimer ;
3115   struct task_cputime cputime_expires ;
3116   struct list_head cpu_timers[3] ;
3117   struct pid *tty_old_pgrp ;
3118   int leader ;
3119   struct tty_struct *tty ;
3120   struct autogroup *autogroup ;
3121   cputime_t utime ;
3122   cputime_t stime ;
3123   cputime_t cutime ;
3124   cputime_t cstime ;
3125   cputime_t gtime ;
3126   cputime_t cgtime ;
3127   cputime_t prev_utime ;
3128   cputime_t prev_stime ;
3129   unsigned long nvcsw ;
3130   unsigned long nivcsw ;
3131   unsigned long cnvcsw ;
3132   unsigned long cnivcsw ;
3133   unsigned long min_flt ;
3134   unsigned long maj_flt ;
3135   unsigned long cmin_flt ;
3136   unsigned long cmaj_flt ;
3137   unsigned long inblock ;
3138   unsigned long oublock ;
3139   unsigned long cinblock ;
3140   unsigned long coublock ;
3141   unsigned long maxrss ;
3142   unsigned long cmaxrss ;
3143   struct task_io_accounting ioac ;
3144   unsigned long long sum_sched_runtime ;
3145   struct rlimit rlim[16] ;
3146   struct pacct_struct pacct ;
3147   struct taskstats *stats ;
3148   unsigned int audit_tty ;
3149   struct tty_audit_buf *tty_audit_buf ;
3150   struct rw_semaphore group_rwsem ;
3151   int oom_adj ;
3152   int oom_score_adj ;
3153   int oom_score_adj_min ;
3154   struct mutex cred_guard_mutex ;
3155};
3156#line 703 "include/linux/sched.h"
3157struct user_struct {
3158   atomic_t __count ;
3159   atomic_t processes ;
3160   atomic_t files ;
3161   atomic_t sigpending ;
3162   atomic_t inotify_watches ;
3163   atomic_t inotify_devs ;
3164   atomic_t fanotify_listeners ;
3165   atomic_long_t epoll_watches ;
3166   unsigned long mq_bytes ;
3167   unsigned long locked_shm ;
3168   struct key *uid_keyring ;
3169   struct key *session_keyring ;
3170   struct hlist_node uidhash_node ;
3171   uid_t uid ;
3172   struct user_namespace *user_ns ;
3173   atomic_long_t locked_vm ;
3174};
3175#line 747
3176struct backing_dev_info;
3177#line 748
3178struct reclaim_state;
3179#line 748
3180struct reclaim_state;
3181#line 751 "include/linux/sched.h"
3182struct sched_info {
3183   unsigned long pcount ;
3184   unsigned long long run_delay ;
3185   unsigned long long last_arrival ;
3186   unsigned long long last_queued ;
3187};
3188#line 763 "include/linux/sched.h"
3189struct task_delay_info {
3190   spinlock_t lock ;
3191   unsigned int flags ;
3192   struct timespec blkio_start ;
3193   struct timespec blkio_end ;
3194   u64 blkio_delay ;
3195   u64 swapin_delay ;
3196   u32 blkio_count ;
3197   u32 swapin_count ;
3198   struct timespec freepages_start ;
3199   struct timespec freepages_end ;
3200   u64 freepages_delay ;
3201   u32 freepages_count ;
3202};
3203#line 1088
3204struct io_context;
3205#line 1088
3206struct io_context;
3207#line 1097
3208struct audit_context;
3209#line 1098
3210struct mempolicy;
3211#line 1099
3212struct pipe_inode_info;
3213#line 1102
3214struct rq;
3215#line 1102
3216struct rq;
3217#line 1122 "include/linux/sched.h"
3218struct sched_class {
3219   struct sched_class  const  *next ;
3220   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
3221   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
3222   void (*yield_task)(struct rq *rq ) ;
3223   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
3224   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
3225   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
3226   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
3227   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
3228   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
3229   void (*post_schedule)(struct rq *this_rq ) ;
3230   void (*task_waking)(struct task_struct *task ) ;
3231   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
3232   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
3233   void (*rq_online)(struct rq *rq ) ;
3234   void (*rq_offline)(struct rq *rq ) ;
3235   void (*set_curr_task)(struct rq *rq ) ;
3236   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
3237   void (*task_fork)(struct task_struct *p ) ;
3238   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
3239   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
3240   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
3241   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
3242   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
3243};
3244#line 1167 "include/linux/sched.h"
3245struct load_weight {
3246   unsigned long weight ;
3247   unsigned long inv_weight ;
3248};
3249#line 1172 "include/linux/sched.h"
3250struct sched_statistics {
3251   u64 wait_start ;
3252   u64 wait_max ;
3253   u64 wait_count ;
3254   u64 wait_sum ;
3255   u64 iowait_count ;
3256   u64 iowait_sum ;
3257   u64 sleep_start ;
3258   u64 sleep_max ;
3259   s64 sum_sleep_runtime ;
3260   u64 block_start ;
3261   u64 block_max ;
3262   u64 exec_max ;
3263   u64 slice_max ;
3264   u64 nr_migrations_cold ;
3265   u64 nr_failed_migrations_affine ;
3266   u64 nr_failed_migrations_running ;
3267   u64 nr_failed_migrations_hot ;
3268   u64 nr_forced_migrations ;
3269   u64 nr_wakeups ;
3270   u64 nr_wakeups_sync ;
3271   u64 nr_wakeups_migrate ;
3272   u64 nr_wakeups_local ;
3273   u64 nr_wakeups_remote ;
3274   u64 nr_wakeups_affine ;
3275   u64 nr_wakeups_affine_attempts ;
3276   u64 nr_wakeups_passive ;
3277   u64 nr_wakeups_idle ;
3278};
3279#line 1207 "include/linux/sched.h"
3280struct sched_entity {
3281   struct load_weight load ;
3282   struct rb_node run_node ;
3283   struct list_head group_node ;
3284   unsigned int on_rq ;
3285   u64 exec_start ;
3286   u64 sum_exec_runtime ;
3287   u64 vruntime ;
3288   u64 prev_sum_exec_runtime ;
3289   u64 nr_migrations ;
3290   struct sched_statistics statistics ;
3291   struct sched_entity *parent ;
3292   struct cfs_rq *cfs_rq ;
3293   struct cfs_rq *my_q ;
3294};
3295#line 1233
3296struct rt_rq;
3297#line 1233 "include/linux/sched.h"
3298struct sched_rt_entity {
3299   struct list_head run_list ;
3300   unsigned long timeout ;
3301   unsigned int time_slice ;
3302   int nr_cpus_allowed ;
3303   struct sched_rt_entity *back ;
3304   struct sched_rt_entity *parent ;
3305   struct rt_rq *rt_rq ;
3306   struct rt_rq *my_q ;
3307};
3308#line 1264
3309struct css_set;
3310#line 1264
3311struct compat_robust_list_head;
3312#line 1264
3313struct mem_cgroup;
3314#line 1264 "include/linux/sched.h"
3315struct memcg_batch_info {
3316   int do_batch ;
3317   struct mem_cgroup *memcg ;
3318   unsigned long nr_pages ;
3319   unsigned long memsw_nr_pages ;
3320};
3321#line 1264 "include/linux/sched.h"
3322struct task_struct {
3323   long volatile   state ;
3324   void *stack ;
3325   atomic_t usage ;
3326   unsigned int flags ;
3327   unsigned int ptrace ;
3328   struct llist_node wake_entry ;
3329   int on_cpu ;
3330   int on_rq ;
3331   int prio ;
3332   int static_prio ;
3333   int normal_prio ;
3334   unsigned int rt_priority ;
3335   struct sched_class  const  *sched_class ;
3336   struct sched_entity se ;
3337   struct sched_rt_entity rt ;
3338   struct hlist_head preempt_notifiers ;
3339   unsigned char fpu_counter ;
3340   unsigned int policy ;
3341   cpumask_t cpus_allowed ;
3342   struct sched_info sched_info ;
3343   struct list_head tasks ;
3344   struct plist_node pushable_tasks ;
3345   struct mm_struct *mm ;
3346   struct mm_struct *active_mm ;
3347   unsigned int brk_randomized : 1 ;
3348   int exit_state ;
3349   int exit_code ;
3350   int exit_signal ;
3351   int pdeath_signal ;
3352   unsigned int jobctl ;
3353   unsigned int personality ;
3354   unsigned int did_exec : 1 ;
3355   unsigned int in_execve : 1 ;
3356   unsigned int in_iowait : 1 ;
3357   unsigned int sched_reset_on_fork : 1 ;
3358   unsigned int sched_contributes_to_load : 1 ;
3359   unsigned int irq_thread : 1 ;
3360   pid_t pid ;
3361   pid_t tgid ;
3362   unsigned long stack_canary ;
3363   struct task_struct *real_parent ;
3364   struct task_struct *parent ;
3365   struct list_head children ;
3366   struct list_head sibling ;
3367   struct task_struct *group_leader ;
3368   struct list_head ptraced ;
3369   struct list_head ptrace_entry ;
3370   struct pid_link pids[3] ;
3371   struct list_head thread_group ;
3372   struct completion *vfork_done ;
3373   int *set_child_tid ;
3374   int *clear_child_tid ;
3375   cputime_t utime ;
3376   cputime_t stime ;
3377   cputime_t utimescaled ;
3378   cputime_t stimescaled ;
3379   cputime_t gtime ;
3380   cputime_t prev_utime ;
3381   cputime_t prev_stime ;
3382   unsigned long nvcsw ;
3383   unsigned long nivcsw ;
3384   struct timespec start_time ;
3385   struct timespec real_start_time ;
3386   unsigned long min_flt ;
3387   unsigned long maj_flt ;
3388   struct task_cputime cputime_expires ;
3389   struct list_head cpu_timers[3] ;
3390   struct cred  const  *real_cred ;
3391   struct cred  const  *cred ;
3392   struct cred *replacement_session_keyring ;
3393   char comm[16] ;
3394   int link_count ;
3395   int total_link_count ;
3396   struct sysv_sem sysvsem ;
3397   unsigned long last_switch_count ;
3398   struct thread_struct thread ;
3399   struct fs_struct *fs ;
3400   struct files_struct *files ;
3401   struct nsproxy *nsproxy ;
3402   struct signal_struct *signal ;
3403   struct sighand_struct *sighand ;
3404   sigset_t blocked ;
3405   sigset_t real_blocked ;
3406   sigset_t saved_sigmask ;
3407   struct sigpending pending ;
3408   unsigned long sas_ss_sp ;
3409   size_t sas_ss_size ;
3410   int (*notifier)(void *priv ) ;
3411   void *notifier_data ;
3412   sigset_t *notifier_mask ;
3413   struct audit_context *audit_context ;
3414   uid_t loginuid ;
3415   unsigned int sessionid ;
3416   seccomp_t seccomp ;
3417   u32 parent_exec_id ;
3418   u32 self_exec_id ;
3419   spinlock_t alloc_lock ;
3420   raw_spinlock_t pi_lock ;
3421   struct plist_head pi_waiters ;
3422   struct rt_mutex_waiter *pi_blocked_on ;
3423   struct mutex_waiter *blocked_on ;
3424   unsigned int irq_events ;
3425   unsigned long hardirq_enable_ip ;
3426   unsigned long hardirq_disable_ip ;
3427   unsigned int hardirq_enable_event ;
3428   unsigned int hardirq_disable_event ;
3429   int hardirqs_enabled ;
3430   int hardirq_context ;
3431   unsigned long softirq_disable_ip ;
3432   unsigned long softirq_enable_ip ;
3433   unsigned int softirq_disable_event ;
3434   unsigned int softirq_enable_event ;
3435   int softirqs_enabled ;
3436   int softirq_context ;
3437   void *journal_info ;
3438   struct bio_list *bio_list ;
3439   struct blk_plug *plug ;
3440   struct reclaim_state *reclaim_state ;
3441   struct backing_dev_info *backing_dev_info ;
3442   struct io_context *io_context ;
3443   unsigned long ptrace_message ;
3444   siginfo_t *last_siginfo ;
3445   struct task_io_accounting ioac ;
3446   u64 acct_rss_mem1 ;
3447   u64 acct_vm_mem1 ;
3448   cputime_t acct_timexpd ;
3449   nodemask_t mems_allowed ;
3450   seqcount_t mems_allowed_seq ;
3451   int cpuset_mem_spread_rotor ;
3452   int cpuset_slab_spread_rotor ;
3453   struct css_set *cgroups ;
3454   struct list_head cg_list ;
3455   struct robust_list_head *robust_list ;
3456   struct compat_robust_list_head *compat_robust_list ;
3457   struct list_head pi_state_list ;
3458   struct futex_pi_state *pi_state_cache ;
3459   struct perf_event_context *perf_event_ctxp[2] ;
3460   struct mutex perf_event_mutex ;
3461   struct list_head perf_event_list ;
3462   struct mempolicy *mempolicy ;
3463   short il_next ;
3464   short pref_node_fork ;
3465   struct rcu_head rcu ;
3466   struct pipe_inode_info *splice_pipe ;
3467   struct task_delay_info *delays ;
3468   int make_it_fail ;
3469   int nr_dirtied ;
3470   int nr_dirtied_pause ;
3471   unsigned long dirty_paused_when ;
3472   int latency_record_count ;
3473   struct latency_record latency_record[32] ;
3474   unsigned long timer_slack_ns ;
3475   unsigned long default_timer_slack_ns ;
3476   struct list_head *scm_work_list ;
3477   unsigned long trace ;
3478   unsigned long trace_recursion ;
3479   struct memcg_batch_info memcg_batch ;
3480   atomic_t ptrace_bp_refcnt ;
3481};
3482#line 1681
3483struct pid_namespace;
3484#line 55 "include/linux/kthread.h"
3485struct kthread_work;
3486#line 55
3487struct kthread_work;
3488#line 58 "include/linux/kthread.h"
3489struct kthread_worker {
3490   spinlock_t lock ;
3491   struct list_head work_list ;
3492   struct task_struct *task ;
3493};
3494#line 64 "include/linux/kthread.h"
3495struct kthread_work {
3496   struct list_head node ;
3497   void (*func)(struct kthread_work *work ) ;
3498   wait_queue_head_t done ;
3499   atomic_t flushing ;
3500   int queue_seq ;
3501   int done_seq ;
3502};
3503#line 70 "include/linux/spi/spi.h"
3504struct spi_master;
3505#line 70 "include/linux/spi/spi.h"
3506struct spi_device {
3507   struct device dev ;
3508   struct spi_master *master ;
3509   u32 max_speed_hz ;
3510   u8 chip_select ;
3511   u8 mode ;
3512   u8 bits_per_word ;
3513   int irq ;
3514   void *controller_state ;
3515   void *controller_data ;
3516   char modalias[32] ;
3517};
3518#line 145
3519struct spi_message;
3520#line 145
3521struct spi_message;
3522#line 176 "include/linux/spi/spi.h"
3523struct spi_driver {
3524   struct spi_device_id  const  *id_table ;
3525   int (*probe)(struct spi_device *spi ) ;
3526   int (*remove)(struct spi_device *spi ) ;
3527   void (*shutdown)(struct spi_device *spi ) ;
3528   int (*suspend)(struct spi_device *spi , pm_message_t mesg ) ;
3529   int (*resume)(struct spi_device *spi ) ;
3530   struct device_driver driver ;
3531};
3532#line 272 "include/linux/spi/spi.h"
3533struct spi_master {
3534   struct device dev ;
3535   struct list_head list ;
3536   s16 bus_num ;
3537   u16 num_chipselect ;
3538   u16 dma_alignment ;
3539   u16 mode_bits ;
3540   u16 flags ;
3541   spinlock_t bus_lock_spinlock ;
3542   struct mutex bus_lock_mutex ;
3543   bool bus_lock_flag ;
3544   int (*setup)(struct spi_device *spi ) ;
3545   int (*transfer)(struct spi_device *spi , struct spi_message *mesg ) ;
3546   void (*cleanup)(struct spi_device *spi ) ;
3547   bool queued ;
3548   struct kthread_worker kworker ;
3549   struct task_struct *kworker_task ;
3550   struct kthread_work pump_messages ;
3551   spinlock_t queue_lock ;
3552   struct list_head queue ;
3553   struct spi_message *cur_msg ;
3554   bool busy ;
3555   bool running ;
3556   bool rt ;
3557   int (*prepare_transfer_hardware)(struct spi_master *master ) ;
3558   int (*transfer_one_message)(struct spi_master *master , struct spi_message *mesg ) ;
3559   int (*unprepare_transfer_hardware)(struct spi_master *master ) ;
3560};
3561#line 541 "include/linux/spi/spi.h"
3562struct spi_message {
3563   struct list_head transfers ;
3564   struct spi_device *spi ;
3565   unsigned int is_dma_mapped : 1 ;
3566   void (*complete)(void *context ) ;
3567   void *context ;
3568   unsigned int actual_length ;
3569   int status ;
3570   struct list_head queue ;
3571   void *state ;
3572};
3573#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
3574struct ds1390 {
3575   struct rtc_device *rtc ;
3576   u8 txrx_buf[9] ;
3577};
3578#line 1 "<compiler builtins>"
3579long __builtin_expect(long val , long res ) ;
3580#line 27 "include/linux/err.h"
3581__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
3582#line 27 "include/linux/err.h"
3583__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr ) 
3584{ 
3585
3586  {
3587#line 29
3588  return ((long )ptr);
3589}
3590}
3591#line 32
3592__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
3593#line 32 "include/linux/err.h"
3594__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr ) 
3595{ long tmp ;
3596  unsigned long __cil_tmp3 ;
3597  int __cil_tmp4 ;
3598  int __cil_tmp5 ;
3599  int __cil_tmp6 ;
3600  long __cil_tmp7 ;
3601
3602  {
3603  {
3604#line 34
3605  __cil_tmp3 = (unsigned long )ptr;
3606#line 34
3607  __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
3608#line 34
3609  __cil_tmp5 = ! __cil_tmp4;
3610#line 34
3611  __cil_tmp6 = ! __cil_tmp5;
3612#line 34
3613  __cil_tmp7 = (long )__cil_tmp6;
3614#line 34
3615  tmp = __builtin_expect(__cil_tmp7, 0L);
3616  }
3617#line 34
3618  return (tmp);
3619}
3620}
3621#line 152 "include/linux/mutex.h"
3622void mutex_lock(struct mutex *lock ) ;
3623#line 153
3624int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
3625#line 154
3626int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
3627#line 168
3628int mutex_trylock(struct mutex *lock ) ;
3629#line 169
3630void mutex_unlock(struct mutex *lock ) ;
3631#line 170
3632int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
3633#line 26 "include/linux/export.h"
3634extern struct module __this_module ;
3635#line 67 "include/linux/module.h"
3636int init_module(void) ;
3637#line 68
3638void cleanup_module(void) ;
3639#line 239 "include/linux/device.h"
3640extern void driver_unregister(struct device_driver *drv ) ;
3641#line 792
3642extern void *dev_get_drvdata(struct device  const  *dev ) ;
3643#line 793
3644extern int dev_set_drvdata(struct device *dev , void *data ) ;
3645#line 891
3646extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
3647                                              , ...) ;
3648#line 110 "include/linux/rtc.h"
3649extern int rtc_valid_tm(struct rtc_time *tm ) ;
3650#line 221
3651extern struct rtc_device *rtc_device_register(char const   *name , struct device *dev ,
3652                                              struct rtc_class_ops  const  *ops ,
3653                                              struct module *owner ) ;
3654#line 225
3655extern void rtc_device_unregister(struct rtc_device *rtc ) ;
3656#line 161 "include/linux/slab.h"
3657extern void kfree(void const   * ) ;
3658#line 221 "include/linux/slub_def.h"
3659extern void *__kmalloc(size_t size , gfp_t flags ) ;
3660#line 268
3661__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
3662                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
3663#line 268 "include/linux/slub_def.h"
3664__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
3665                                                                    gfp_t flags ) 
3666{ void *tmp___2 ;
3667
3668  {
3669  {
3670#line 283
3671  tmp___2 = __kmalloc(size, flags);
3672  }
3673#line 283
3674  return (tmp___2);
3675}
3676}
3677#line 349 "include/linux/slab.h"
3678__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
3679#line 349 "include/linux/slab.h"
3680__inline static void *kzalloc(size_t size , gfp_t flags ) 
3681{ void *tmp ;
3682  unsigned int __cil_tmp4 ;
3683
3684  {
3685  {
3686#line 351
3687  __cil_tmp4 = flags | 32768U;
3688#line 351
3689  tmp = kmalloc(size, __cil_tmp4);
3690  }
3691#line 351
3692  return (tmp);
3693}
3694}
3695#line 105 "include/linux/spi/spi.h"
3696__inline static struct spi_device *to_spi_device(struct device *dev )  __attribute__((__no_instrument_function__)) ;
3697#line 105 "include/linux/spi/spi.h"
3698__inline static struct spi_device *to_spi_device(struct device *dev ) 
3699{ struct device  const  *__mptr ;
3700  struct spi_device *tmp___7 ;
3701  struct spi_device *__cil_tmp4 ;
3702  struct device *__cil_tmp5 ;
3703  unsigned int __cil_tmp6 ;
3704  char *__cil_tmp7 ;
3705  char *__cil_tmp8 ;
3706  void *__cil_tmp9 ;
3707
3708  {
3709#line 107
3710  if (dev) {
3711#line 107
3712    __mptr = (struct device  const  *)dev;
3713#line 107
3714    __cil_tmp4 = (struct spi_device *)0;
3715#line 107
3716    __cil_tmp5 = (struct device *)__cil_tmp4;
3717#line 107
3718    __cil_tmp6 = (unsigned int )__cil_tmp5;
3719#line 107
3720    __cil_tmp7 = (char *)__mptr;
3721#line 107
3722    __cil_tmp8 = __cil_tmp7 - __cil_tmp6;
3723#line 107
3724    tmp___7 = (struct spi_device *)__cil_tmp8;
3725  } else {
3726#line 107
3727    __cil_tmp9 = (void *)0;
3728#line 107
3729    tmp___7 = (struct spi_device *)__cil_tmp9;
3730  }
3731#line 107
3732  return (tmp___7);
3733}
3734}
3735#line 140
3736__inline static void *spi_get_drvdata(struct spi_device *spi )  __attribute__((__no_instrument_function__)) ;
3737#line 140 "include/linux/spi/spi.h"
3738__inline static void *spi_get_drvdata(struct spi_device *spi ) 
3739{ void *tmp___7 ;
3740  struct device *__cil_tmp3 ;
3741  struct device  const  *__cil_tmp4 ;
3742
3743  {
3744  {
3745#line 142
3746  __cil_tmp3 = (struct device *)spi;
3747#line 142
3748  __cil_tmp4 = (struct device  const  *)__cil_tmp3;
3749#line 142
3750  tmp___7 = dev_get_drvdata(__cil_tmp4);
3751  }
3752#line 142
3753  return (tmp___7);
3754}
3755}
3756#line 191
3757extern int spi_register_driver(struct spi_driver *sdrv ) ;
3758#line 198
3759__inline static void spi_unregister_driver(struct spi_driver *sdrv )  __attribute__((__no_instrument_function__)) ;
3760#line 198 "include/linux/spi/spi.h"
3761__inline static void spi_unregister_driver(struct spi_driver *sdrv ) 
3762{ unsigned long __cil_tmp2 ;
3763  unsigned long __cil_tmp3 ;
3764  struct device_driver *__cil_tmp4 ;
3765
3766  {
3767#line 200
3768  if (sdrv) {
3769    {
3770#line 201
3771    __cil_tmp2 = (unsigned long )sdrv;
3772#line 201
3773    __cil_tmp3 = __cil_tmp2 + 48;
3774#line 201
3775    __cil_tmp4 = (struct device_driver *)__cil_tmp3;
3776#line 201
3777    driver_unregister(__cil_tmp4);
3778    }
3779  } else {
3780
3781  }
3782#line 202
3783  return;
3784}
3785}
3786#line 618
3787extern int spi_setup(struct spi_device *spi ) ;
3788#line 684
3789extern int spi_write_then_read(struct spi_device *spi , void const   *txbuf , unsigned int n_tx ,
3790                               void *rxbuf , unsigned int n_rx ) ;
3791#line 6 "include/linux/bcd.h"
3792extern unsigned int bcd2bin(unsigned char val )  __attribute__((__const__)) ;
3793#line 7
3794extern unsigned char bin2bcd(unsigned int val )  __attribute__((__const__)) ;
3795#line 49 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
3796static int ds1390_get_reg(struct device *dev , unsigned char address , unsigned char *data ) 
3797{ struct spi_device *spi ;
3798  struct spi_device *tmp___7 ;
3799  struct ds1390 *chip ;
3800  void *tmp___8 ;
3801  int status ;
3802  struct device  const  *__cil_tmp9 ;
3803  unsigned long __cil_tmp10 ;
3804  unsigned long __cil_tmp11 ;
3805  unsigned long __cil_tmp12 ;
3806  unsigned long __cil_tmp13 ;
3807  int __cil_tmp14 ;
3808  int __cil_tmp15 ;
3809  unsigned long __cil_tmp16 ;
3810  unsigned long __cil_tmp17 ;
3811  unsigned long __cil_tmp18 ;
3812  unsigned long __cil_tmp19 ;
3813  u8 *__cil_tmp20 ;
3814  void const   *__cil_tmp21 ;
3815  unsigned long __cil_tmp22 ;
3816  unsigned long __cil_tmp23 ;
3817  unsigned long __cil_tmp24 ;
3818  unsigned long __cil_tmp25 ;
3819  u8 *__cil_tmp26 ;
3820  void *__cil_tmp27 ;
3821  unsigned long __cil_tmp28 ;
3822  unsigned long __cil_tmp29 ;
3823  unsigned long __cil_tmp30 ;
3824  unsigned long __cil_tmp31 ;
3825
3826  {
3827  {
3828#line 52
3829  tmp___7 = to_spi_device(dev);
3830#line 52
3831  spi = tmp___7;
3832#line 53
3833  __cil_tmp9 = (struct device  const  *)dev;
3834#line 53
3835  tmp___8 = dev_get_drvdata(__cil_tmp9);
3836#line 53
3837  chip = (struct ds1390 *)tmp___8;
3838  }
3839#line 56
3840  if (! data) {
3841#line 57
3842    return (-22);
3843  } else {
3844
3845  }
3846  {
3847#line 60
3848  __cil_tmp10 = 0 * 1UL;
3849#line 60
3850  __cil_tmp11 = 8 + __cil_tmp10;
3851#line 60
3852  __cil_tmp12 = (unsigned long )chip;
3853#line 60
3854  __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
3855#line 60
3856  __cil_tmp14 = (int )address;
3857#line 60
3858  __cil_tmp15 = __cil_tmp14 & 127;
3859#line 60
3860  *((u8 *)__cil_tmp13) = (u8 )__cil_tmp15;
3861#line 62
3862  __cil_tmp16 = 0 * 1UL;
3863#line 62
3864  __cil_tmp17 = 8 + __cil_tmp16;
3865#line 62
3866  __cil_tmp18 = (unsigned long )chip;
3867#line 62
3868  __cil_tmp19 = __cil_tmp18 + __cil_tmp17;
3869#line 62
3870  __cil_tmp20 = (u8 *)__cil_tmp19;
3871#line 62
3872  __cil_tmp21 = (void const   *)__cil_tmp20;
3873#line 62
3874  __cil_tmp22 = 0 * 1UL;
3875#line 62
3876  __cil_tmp23 = 8 + __cil_tmp22;
3877#line 62
3878  __cil_tmp24 = (unsigned long )chip;
3879#line 62
3880  __cil_tmp25 = __cil_tmp24 + __cil_tmp23;
3881#line 62
3882  __cil_tmp26 = (u8 *)__cil_tmp25;
3883#line 62
3884  __cil_tmp27 = (void *)__cil_tmp26;
3885#line 62
3886  status = spi_write_then_read(spi, __cil_tmp21, 1U, __cil_tmp27, 1U);
3887  }
3888#line 63
3889  if (status != 0) {
3890#line 64
3891    return (status);
3892  } else {
3893
3894  }
3895#line 66
3896  __cil_tmp28 = 1 * 1UL;
3897#line 66
3898  __cil_tmp29 = 8 + __cil_tmp28;
3899#line 66
3900  __cil_tmp30 = (unsigned long )chip;
3901#line 66
3902  __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
3903#line 66
3904  *data = *((u8 *)__cil_tmp31);
3905#line 68
3906  return (0);
3907}
3908}
3909#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
3910static int ds1390_read_time(struct device *dev , struct rtc_time *dt ) 
3911{ struct spi_device *spi ;
3912  struct spi_device *tmp___7 ;
3913  struct ds1390 *chip ;
3914  void *tmp___8 ;
3915  int status ;
3916  unsigned int tmp___9 ;
3917  unsigned int tmp___10 ;
3918  unsigned int tmp___11 ;
3919  unsigned int tmp___12 ;
3920  unsigned int tmp___13 ;
3921  unsigned int tmp___14 ;
3922  unsigned int tmp___15 ;
3923  int tmp___16 ;
3924  int tmp___17 ;
3925  struct device  const  *__cil_tmp17 ;
3926  unsigned long __cil_tmp18 ;
3927  unsigned long __cil_tmp19 ;
3928  unsigned long __cil_tmp20 ;
3929  unsigned long __cil_tmp21 ;
3930  unsigned long __cil_tmp22 ;
3931  unsigned long __cil_tmp23 ;
3932  unsigned long __cil_tmp24 ;
3933  unsigned long __cil_tmp25 ;
3934  u8 *__cil_tmp26 ;
3935  void const   *__cil_tmp27 ;
3936  unsigned long __cil_tmp28 ;
3937  unsigned long __cil_tmp29 ;
3938  unsigned long __cil_tmp30 ;
3939  unsigned long __cil_tmp31 ;
3940  u8 *__cil_tmp32 ;
3941  void *__cil_tmp33 ;
3942  unsigned long __cil_tmp34 ;
3943  unsigned long __cil_tmp35 ;
3944  unsigned long __cil_tmp36 ;
3945  unsigned long __cil_tmp37 ;
3946  u8 __cil_tmp38 ;
3947  unsigned long __cil_tmp39 ;
3948  unsigned long __cil_tmp40 ;
3949  unsigned long __cil_tmp41 ;
3950  unsigned long __cil_tmp42 ;
3951  u8 __cil_tmp43 ;
3952  unsigned long __cil_tmp44 ;
3953  unsigned long __cil_tmp45 ;
3954  unsigned long __cil_tmp46 ;
3955  unsigned long __cil_tmp47 ;
3956  unsigned long __cil_tmp48 ;
3957  unsigned long __cil_tmp49 ;
3958  u8 __cil_tmp50 ;
3959  unsigned long __cil_tmp51 ;
3960  unsigned long __cil_tmp52 ;
3961  unsigned long __cil_tmp53 ;
3962  unsigned long __cil_tmp54 ;
3963  unsigned long __cil_tmp55 ;
3964  unsigned long __cil_tmp56 ;
3965  u8 __cil_tmp57 ;
3966  unsigned long __cil_tmp58 ;
3967  unsigned long __cil_tmp59 ;
3968  unsigned long __cil_tmp60 ;
3969  unsigned long __cil_tmp61 ;
3970  unsigned long __cil_tmp62 ;
3971  unsigned long __cil_tmp63 ;
3972  u8 __cil_tmp64 ;
3973  unsigned long __cil_tmp65 ;
3974  unsigned long __cil_tmp66 ;
3975  unsigned long __cil_tmp67 ;
3976  unsigned long __cil_tmp68 ;
3977  unsigned long __cil_tmp69 ;
3978  unsigned long __cil_tmp70 ;
3979  u8 __cil_tmp71 ;
3980  int __cil_tmp72 ;
3981  int __cil_tmp73 ;
3982  unsigned char __cil_tmp74 ;
3983  unsigned long __cil_tmp75 ;
3984  unsigned long __cil_tmp76 ;
3985  unsigned int __cil_tmp77 ;
3986  unsigned long __cil_tmp78 ;
3987  unsigned long __cil_tmp79 ;
3988  unsigned long __cil_tmp80 ;
3989  unsigned long __cil_tmp81 ;
3990  u8 __cil_tmp82 ;
3991  unsigned long __cil_tmp83 ;
3992  unsigned long __cil_tmp84 ;
3993  unsigned long __cil_tmp85 ;
3994  unsigned long __cil_tmp86 ;
3995  u8 __cil_tmp87 ;
3996  int __cil_tmp88 ;
3997  unsigned long __cil_tmp89 ;
3998  unsigned long __cil_tmp90 ;
3999  unsigned int __cil_tmp91 ;
4000  unsigned int __cil_tmp92 ;
4001
4002  {
4003  {
4004#line 73
4005  tmp___7 = to_spi_device(dev);
4006#line 73
4007  spi = tmp___7;
4008#line 74
4009  __cil_tmp17 = (struct device  const  *)dev;
4010#line 74
4011  tmp___8 = dev_get_drvdata(__cil_tmp17);
4012#line 74
4013  chip = (struct ds1390 *)tmp___8;
4014#line 78
4015  __cil_tmp18 = 0 * 1UL;
4016#line 78
4017  __cil_tmp19 = 8 + __cil_tmp18;
4018#line 78
4019  __cil_tmp20 = (unsigned long )chip;
4020#line 78
4021  __cil_tmp21 = __cil_tmp20 + __cil_tmp19;
4022#line 78
4023  *((u8 *)__cil_tmp21) = (u8 )1;
4024#line 81
4025  __cil_tmp22 = 0 * 1UL;
4026#line 81
4027  __cil_tmp23 = 8 + __cil_tmp22;
4028#line 81
4029  __cil_tmp24 = (unsigned long )chip;
4030#line 81
4031  __cil_tmp25 = __cil_tmp24 + __cil_tmp23;
4032#line 81
4033  __cil_tmp26 = (u8 *)__cil_tmp25;
4034#line 81
4035  __cil_tmp27 = (void const   *)__cil_tmp26;
4036#line 81
4037  __cil_tmp28 = 0 * 1UL;
4038#line 81
4039  __cil_tmp29 = 8 + __cil_tmp28;
4040#line 81
4041  __cil_tmp30 = (unsigned long )chip;
4042#line 81
4043  __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
4044#line 81
4045  __cil_tmp32 = (u8 *)__cil_tmp31;
4046#line 81
4047  __cil_tmp33 = (void *)__cil_tmp32;
4048#line 81
4049  status = spi_write_then_read(spi, __cil_tmp27, 1U, __cil_tmp33, 8U);
4050  }
4051#line 82
4052  if (status != 0) {
4053#line 83
4054    return (status);
4055  } else {
4056
4057  }
4058  {
4059#line 87
4060  __cil_tmp34 = 0 * 1UL;
4061#line 87
4062  __cil_tmp35 = 8 + __cil_tmp34;
4063#line 87
4064  __cil_tmp36 = (unsigned long )chip;
4065#line 87
4066  __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
4067#line 87
4068  __cil_tmp38 = *((u8 *)__cil_tmp37);
4069#line 87
4070  tmp___9 = bcd2bin(__cil_tmp38);
4071#line 87
4072  *((int *)dt) = (int )tmp___9;
4073#line 88
4074  __cil_tmp39 = 1 * 1UL;
4075#line 88
4076  __cil_tmp40 = 8 + __cil_tmp39;
4077#line 88
4078  __cil_tmp41 = (unsigned long )chip;
4079#line 88
4080  __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
4081#line 88
4082  __cil_tmp43 = *((u8 *)__cil_tmp42);
4083#line 88
4084  tmp___10 = bcd2bin(__cil_tmp43);
4085#line 88
4086  __cil_tmp44 = (unsigned long )dt;
4087#line 88
4088  __cil_tmp45 = __cil_tmp44 + 4;
4089#line 88
4090  *((int *)__cil_tmp45) = (int )tmp___10;
4091#line 89
4092  __cil_tmp46 = 2 * 1UL;
4093#line 89
4094  __cil_tmp47 = 8 + __cil_tmp46;
4095#line 89
4096  __cil_tmp48 = (unsigned long )chip;
4097#line 89
4098  __cil_tmp49 = __cil_tmp48 + __cil_tmp47;
4099#line 89
4100  __cil_tmp50 = *((u8 *)__cil_tmp49);
4101#line 89
4102  tmp___11 = bcd2bin(__cil_tmp50);
4103#line 89
4104  __cil_tmp51 = (unsigned long )dt;
4105#line 89
4106  __cil_tmp52 = __cil_tmp51 + 8;
4107#line 89
4108  *((int *)__cil_tmp52) = (int )tmp___11;
4109#line 90
4110  __cil_tmp53 = 3 * 1UL;
4111#line 90
4112  __cil_tmp54 = 8 + __cil_tmp53;
4113#line 90
4114  __cil_tmp55 = (unsigned long )chip;
4115#line 90
4116  __cil_tmp56 = __cil_tmp55 + __cil_tmp54;
4117#line 90
4118  __cil_tmp57 = *((u8 *)__cil_tmp56);
4119#line 90
4120  tmp___12 = bcd2bin(__cil_tmp57);
4121#line 90
4122  __cil_tmp58 = (unsigned long )dt;
4123#line 90
4124  __cil_tmp59 = __cil_tmp58 + 24;
4125#line 90
4126  *((int *)__cil_tmp59) = (int )tmp___12;
4127#line 91
4128  __cil_tmp60 = 4 * 1UL;
4129#line 91
4130  __cil_tmp61 = 8 + __cil_tmp60;
4131#line 91
4132  __cil_tmp62 = (unsigned long )chip;
4133#line 91
4134  __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
4135#line 91
4136  __cil_tmp64 = *((u8 *)__cil_tmp63);
4137#line 91
4138  tmp___13 = bcd2bin(__cil_tmp64);
4139#line 91
4140  __cil_tmp65 = (unsigned long )dt;
4141#line 91
4142  __cil_tmp66 = __cil_tmp65 + 12;
4143#line 91
4144  *((int *)__cil_tmp66) = (int )tmp___13;
4145#line 93
4146  __cil_tmp67 = 5 * 1UL;
4147#line 93
4148  __cil_tmp68 = 8 + __cil_tmp67;
4149#line 93
4150  __cil_tmp69 = (unsigned long )chip;
4151#line 93
4152  __cil_tmp70 = __cil_tmp69 + __cil_tmp68;
4153#line 93
4154  __cil_tmp71 = *((u8 *)__cil_tmp70);
4155#line 93
4156  __cil_tmp72 = (int )__cil_tmp71;
4157#line 93
4158  __cil_tmp73 = __cil_tmp72 & 127;
4159#line 93
4160  __cil_tmp74 = (unsigned char )__cil_tmp73;
4161#line 93
4162  tmp___14 = bcd2bin(__cil_tmp74);
4163#line 93
4164  __cil_tmp75 = (unsigned long )dt;
4165#line 93
4166  __cil_tmp76 = __cil_tmp75 + 16;
4167#line 93
4168  __cil_tmp77 = tmp___14 - 1U;
4169#line 93
4170  *((int *)__cil_tmp76) = (int )__cil_tmp77;
4171#line 95
4172  __cil_tmp78 = 6 * 1UL;
4173#line 95
4174  __cil_tmp79 = 8 + __cil_tmp78;
4175#line 95
4176  __cil_tmp80 = (unsigned long )chip;
4177#line 95
4178  __cil_tmp81 = __cil_tmp80 + __cil_tmp79;
4179#line 95
4180  __cil_tmp82 = *((u8 *)__cil_tmp81);
4181#line 95
4182  tmp___15 = bcd2bin(__cil_tmp82);
4183  }
4184  {
4185#line 95
4186  __cil_tmp83 = 5 * 1UL;
4187#line 95
4188  __cil_tmp84 = 8 + __cil_tmp83;
4189#line 95
4190  __cil_tmp85 = (unsigned long )chip;
4191#line 95
4192  __cil_tmp86 = __cil_tmp85 + __cil_tmp84;
4193#line 95
4194  __cil_tmp87 = *((u8 *)__cil_tmp86);
4195#line 95
4196  __cil_tmp88 = (int )__cil_tmp87;
4197#line 95
4198  if (__cil_tmp88 & 128) {
4199#line 95
4200    tmp___16 = 100;
4201  } else {
4202#line 95
4203    tmp___16 = 0;
4204  }
4205  }
4206  {
4207#line 95
4208  __cil_tmp89 = (unsigned long )dt;
4209#line 95
4210  __cil_tmp90 = __cil_tmp89 + 20;
4211#line 95
4212  __cil_tmp91 = (unsigned int )tmp___16;
4213#line 95
4214  __cil_tmp92 = tmp___15 + __cil_tmp91;
4215#line 95
4216  *((int *)__cil_tmp90) = (int )__cil_tmp92;
4217#line 97
4218  tmp___17 = rtc_valid_tm(dt);
4219  }
4220#line 97
4221  return (tmp___17);
4222}
4223}
4224#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4225static int ds1390_set_time(struct device *dev , struct rtc_time *dt ) 
4226{ struct spi_device *spi ;
4227  struct spi_device *tmp___7 ;
4228  struct ds1390 *chip ;
4229  void *tmp___8 ;
4230  unsigned char tmp___9 ;
4231  int tmp___10 ;
4232  int tmp___11 ;
4233  struct device  const  *__cil_tmp10 ;
4234  unsigned long __cil_tmp11 ;
4235  unsigned long __cil_tmp12 ;
4236  unsigned long __cil_tmp13 ;
4237  unsigned long __cil_tmp14 ;
4238  unsigned long __cil_tmp15 ;
4239  unsigned long __cil_tmp16 ;
4240  unsigned long __cil_tmp17 ;
4241  unsigned long __cil_tmp18 ;
4242  int __cil_tmp19 ;
4243  unsigned int __cil_tmp20 ;
4244  unsigned long __cil_tmp21 ;
4245  unsigned long __cil_tmp22 ;
4246  unsigned long __cil_tmp23 ;
4247  unsigned long __cil_tmp24 ;
4248  unsigned long __cil_tmp25 ;
4249  unsigned long __cil_tmp26 ;
4250  int __cil_tmp27 ;
4251  unsigned int __cil_tmp28 ;
4252  unsigned long __cil_tmp29 ;
4253  unsigned long __cil_tmp30 ;
4254  unsigned long __cil_tmp31 ;
4255  unsigned long __cil_tmp32 ;
4256  unsigned long __cil_tmp33 ;
4257  unsigned long __cil_tmp34 ;
4258  int __cil_tmp35 ;
4259  unsigned int __cil_tmp36 ;
4260  unsigned long __cil_tmp37 ;
4261  unsigned long __cil_tmp38 ;
4262  unsigned long __cil_tmp39 ;
4263  unsigned long __cil_tmp40 ;
4264  unsigned long __cil_tmp41 ;
4265  unsigned long __cil_tmp42 ;
4266  int __cil_tmp43 ;
4267  unsigned int __cil_tmp44 ;
4268  unsigned long __cil_tmp45 ;
4269  unsigned long __cil_tmp46 ;
4270  unsigned long __cil_tmp47 ;
4271  unsigned long __cil_tmp48 ;
4272  unsigned long __cil_tmp49 ;
4273  unsigned long __cil_tmp50 ;
4274  int __cil_tmp51 ;
4275  unsigned int __cil_tmp52 ;
4276  unsigned long __cil_tmp53 ;
4277  unsigned long __cil_tmp54 ;
4278  int __cil_tmp55 ;
4279  int __cil_tmp56 ;
4280  unsigned int __cil_tmp57 ;
4281  unsigned long __cil_tmp58 ;
4282  unsigned long __cil_tmp59 ;
4283  int __cil_tmp60 ;
4284  unsigned long __cil_tmp61 ;
4285  unsigned long __cil_tmp62 ;
4286  unsigned long __cil_tmp63 ;
4287  unsigned long __cil_tmp64 ;
4288  int __cil_tmp65 ;
4289  int __cil_tmp66 ;
4290  unsigned long __cil_tmp67 ;
4291  unsigned long __cil_tmp68 ;
4292  unsigned long __cil_tmp69 ;
4293  unsigned long __cil_tmp70 ;
4294  unsigned long __cil_tmp71 ;
4295  unsigned long __cil_tmp72 ;
4296  int __cil_tmp73 ;
4297  int __cil_tmp74 ;
4298  unsigned int __cil_tmp75 ;
4299  unsigned long __cil_tmp76 ;
4300  unsigned long __cil_tmp77 ;
4301  unsigned long __cil_tmp78 ;
4302  unsigned long __cil_tmp79 ;
4303  u8 *__cil_tmp80 ;
4304  void const   *__cil_tmp81 ;
4305  void *__cil_tmp82 ;
4306
4307  {
4308  {
4309#line 102
4310  tmp___7 = to_spi_device(dev);
4311#line 102
4312  spi = tmp___7;
4313#line 103
4314  __cil_tmp10 = (struct device  const  *)dev;
4315#line 103
4316  tmp___8 = dev_get_drvdata(__cil_tmp10);
4317#line 103
4318  chip = (struct ds1390 *)tmp___8;
4319#line 106
4320  __cil_tmp11 = 0 * 1UL;
4321#line 106
4322  __cil_tmp12 = 8 + __cil_tmp11;
4323#line 106
4324  __cil_tmp13 = (unsigned long )chip;
4325#line 106
4326  __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
4327#line 106
4328  *((u8 *)__cil_tmp14) = (u8 )129;
4329#line 107
4330  __cil_tmp15 = 1 * 1UL;
4331#line 107
4332  __cil_tmp16 = 8 + __cil_tmp15;
4333#line 107
4334  __cil_tmp17 = (unsigned long )chip;
4335#line 107
4336  __cil_tmp18 = __cil_tmp17 + __cil_tmp16;
4337#line 107
4338  __cil_tmp19 = *((int *)dt);
4339#line 107
4340  __cil_tmp20 = (unsigned int )__cil_tmp19;
4341#line 107
4342  *((u8 *)__cil_tmp18) = bin2bcd(__cil_tmp20);
4343#line 108
4344  __cil_tmp21 = 2 * 1UL;
4345#line 108
4346  __cil_tmp22 = 8 + __cil_tmp21;
4347#line 108
4348  __cil_tmp23 = (unsigned long )chip;
4349#line 108
4350  __cil_tmp24 = __cil_tmp23 + __cil_tmp22;
4351#line 108
4352  __cil_tmp25 = (unsigned long )dt;
4353#line 108
4354  __cil_tmp26 = __cil_tmp25 + 4;
4355#line 108
4356  __cil_tmp27 = *((int *)__cil_tmp26);
4357#line 108
4358  __cil_tmp28 = (unsigned int )__cil_tmp27;
4359#line 108
4360  *((u8 *)__cil_tmp24) = bin2bcd(__cil_tmp28);
4361#line 109
4362  __cil_tmp29 = 3 * 1UL;
4363#line 109
4364  __cil_tmp30 = 8 + __cil_tmp29;
4365#line 109
4366  __cil_tmp31 = (unsigned long )chip;
4367#line 109
4368  __cil_tmp32 = __cil_tmp31 + __cil_tmp30;
4369#line 109
4370  __cil_tmp33 = (unsigned long )dt;
4371#line 109
4372  __cil_tmp34 = __cil_tmp33 + 8;
4373#line 109
4374  __cil_tmp35 = *((int *)__cil_tmp34);
4375#line 109
4376  __cil_tmp36 = (unsigned int )__cil_tmp35;
4377#line 109
4378  *((u8 *)__cil_tmp32) = bin2bcd(__cil_tmp36);
4379#line 110
4380  __cil_tmp37 = 4 * 1UL;
4381#line 110
4382  __cil_tmp38 = 8 + __cil_tmp37;
4383#line 110
4384  __cil_tmp39 = (unsigned long )chip;
4385#line 110
4386  __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
4387#line 110
4388  __cil_tmp41 = (unsigned long )dt;
4389#line 110
4390  __cil_tmp42 = __cil_tmp41 + 24;
4391#line 110
4392  __cil_tmp43 = *((int *)__cil_tmp42);
4393#line 110
4394  __cil_tmp44 = (unsigned int )__cil_tmp43;
4395#line 110
4396  *((u8 *)__cil_tmp40) = bin2bcd(__cil_tmp44);
4397#line 111
4398  __cil_tmp45 = 5 * 1UL;
4399#line 111
4400  __cil_tmp46 = 8 + __cil_tmp45;
4401#line 111
4402  __cil_tmp47 = (unsigned long )chip;
4403#line 111
4404  __cil_tmp48 = __cil_tmp47 + __cil_tmp46;
4405#line 111
4406  __cil_tmp49 = (unsigned long )dt;
4407#line 111
4408  __cil_tmp50 = __cil_tmp49 + 12;
4409#line 111
4410  __cil_tmp51 = *((int *)__cil_tmp50);
4411#line 111
4412  __cil_tmp52 = (unsigned int )__cil_tmp51;
4413#line 111
4414  *((u8 *)__cil_tmp48) = bin2bcd(__cil_tmp52);
4415#line 112
4416  __cil_tmp53 = (unsigned long )dt;
4417#line 112
4418  __cil_tmp54 = __cil_tmp53 + 16;
4419#line 112
4420  __cil_tmp55 = *((int *)__cil_tmp54);
4421#line 112
4422  __cil_tmp56 = __cil_tmp55 + 1;
4423#line 112
4424  __cil_tmp57 = (unsigned int )__cil_tmp56;
4425#line 112
4426  tmp___9 = bin2bcd(__cil_tmp57);
4427  }
4428  {
4429#line 112
4430  __cil_tmp58 = (unsigned long )dt;
4431#line 112
4432  __cil_tmp59 = __cil_tmp58 + 20;
4433#line 112
4434  __cil_tmp60 = *((int *)__cil_tmp59);
4435#line 112
4436  if (__cil_tmp60 > 99) {
4437#line 112
4438    tmp___10 = 128;
4439  } else {
4440#line 112
4441    tmp___10 = 0;
4442  }
4443  }
4444  {
4445#line 112
4446  __cil_tmp61 = 6 * 1UL;
4447#line 112
4448  __cil_tmp62 = 8 + __cil_tmp61;
4449#line 112
4450  __cil_tmp63 = (unsigned long )chip;
4451#line 112
4452  __cil_tmp64 = __cil_tmp63 + __cil_tmp62;
4453#line 112
4454  __cil_tmp65 = (int )tmp___9;
4455#line 112
4456  __cil_tmp66 = __cil_tmp65 | tmp___10;
4457#line 112
4458  *((u8 *)__cil_tmp64) = (u8 )__cil_tmp66;
4459#line 114
4460  __cil_tmp67 = 7 * 1UL;
4461#line 114
4462  __cil_tmp68 = 8 + __cil_tmp67;
4463#line 114
4464  __cil_tmp69 = (unsigned long )chip;
4465#line 114
4466  __cil_tmp70 = __cil_tmp69 + __cil_tmp68;
4467#line 114
4468  __cil_tmp71 = (unsigned long )dt;
4469#line 114
4470  __cil_tmp72 = __cil_tmp71 + 20;
4471#line 114
4472  __cil_tmp73 = *((int *)__cil_tmp72);
4473#line 114
4474  __cil_tmp74 = __cil_tmp73 % 100;
4475#line 114
4476  __cil_tmp75 = (unsigned int )__cil_tmp74;
4477#line 114
4478  *((u8 *)__cil_tmp70) = bin2bcd(__cil_tmp75);
4479#line 117
4480  __cil_tmp76 = 0 * 1UL;
4481#line 117
4482  __cil_tmp77 = 8 + __cil_tmp76;
4483#line 117
4484  __cil_tmp78 = (unsigned long )chip;
4485#line 117
4486  __cil_tmp79 = __cil_tmp78 + __cil_tmp77;
4487#line 117
4488  __cil_tmp80 = (u8 *)__cil_tmp79;
4489#line 117
4490  __cil_tmp81 = (void const   *)__cil_tmp80;
4491#line 117
4492  __cil_tmp82 = (void *)0;
4493#line 117
4494  tmp___11 = spi_write_then_read(spi, __cil_tmp81, 8U, __cil_tmp82, 0U);
4495  }
4496#line 117
4497  return (tmp___11);
4498}
4499}
4500#line 120 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4501static struct rtc_class_ops  const  ds1390_rtc_ops  = 
4502#line 120
4503     {(int (*)(struct device * ))0, (void (*)(struct device * ))0, (int (*)(struct device * ,
4504                                                                          unsigned int  ,
4505                                                                          unsigned long  ))0,
4506    & ds1390_read_time, & ds1390_set_time, (int (*)(struct device * , struct rtc_wkalrm * ))0,
4507    (int (*)(struct device * , struct rtc_wkalrm * ))0, (int (*)(struct device * ,
4508                                                                 struct seq_file * ))0,
4509    (int (*)(struct device * , unsigned long secs ))0, (int (*)(struct device * ,
4510                                                                int data ))0, (int (*)(struct device * ,
4511                                                                                       unsigned int enabled ))0};
4512#line 125
4513static int ds1390_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
4514__no_instrument_function__)) ;
4515#line 125 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4516static int ds1390_probe(struct spi_device *spi ) 
4517{ unsigned char tmp___7 ;
4518  struct ds1390 *chip ;
4519  int res ;
4520  void *tmp___8 ;
4521  long tmp___9 ;
4522  long tmp___10 ;
4523  unsigned long __cil_tmp8 ;
4524  unsigned long __cil_tmp9 ;
4525  unsigned long __cil_tmp10 ;
4526  unsigned long __cil_tmp11 ;
4527  struct device *__cil_tmp12 ;
4528  struct device  const  *__cil_tmp13 ;
4529  struct device *__cil_tmp14 ;
4530  void *__cil_tmp15 ;
4531  struct device *__cil_tmp16 ;
4532  struct device *__cil_tmp17 ;
4533  struct device  const  *__cil_tmp18 ;
4534  void const   *__cil_tmp19 ;
4535  struct device *__cil_tmp20 ;
4536  struct rtc_device *__cil_tmp21 ;
4537  void const   *__cil_tmp22 ;
4538  struct device *__cil_tmp23 ;
4539  struct device  const  *__cil_tmp24 ;
4540  struct rtc_device *__cil_tmp25 ;
4541  void const   *__cil_tmp26 ;
4542  void const   *__cil_tmp27 ;
4543
4544  {
4545  {
4546#line 131
4547  __cil_tmp8 = (unsigned long )spi;
4548#line 131
4549  __cil_tmp9 = __cil_tmp8 + 781;
4550#line 131
4551  *((u8 *)__cil_tmp9) = (u8 )3;
4552#line 132
4553  __cil_tmp10 = (unsigned long )spi;
4554#line 132
4555  __cil_tmp11 = __cil_tmp10 + 782;
4556#line 132
4557  *((u8 *)__cil_tmp11) = (u8 )8;
4558#line 133
4559  spi_setup(spi);
4560#line 135
4561  tmp___8 = kzalloc(24UL, 208U);
4562#line 135
4563  chip = (struct ds1390 *)tmp___8;
4564  }
4565#line 136
4566  if (! chip) {
4567    {
4568#line 137
4569    __cil_tmp12 = (struct device *)spi;
4570#line 137
4571    __cil_tmp13 = (struct device  const  *)__cil_tmp12;
4572#line 137
4573    dev_err(__cil_tmp13, "unable to allocate device memory\n");
4574    }
4575#line 138
4576    return (-12);
4577  } else {
4578
4579  }
4580  {
4581#line 140
4582  __cil_tmp14 = (struct device *)spi;
4583#line 140
4584  __cil_tmp15 = (void *)chip;
4585#line 140
4586  dev_set_drvdata(__cil_tmp14, __cil_tmp15);
4587#line 142
4588  __cil_tmp16 = (struct device *)spi;
4589#line 142
4590  res = ds1390_get_reg(__cil_tmp16, (unsigned char)1, & tmp___7);
4591  }
4592#line 143
4593  if (res != 0) {
4594    {
4595#line 144
4596    __cil_tmp17 = (struct device *)spi;
4597#line 144
4598    __cil_tmp18 = (struct device  const  *)__cil_tmp17;
4599#line 144
4600    dev_err(__cil_tmp18, "unable to read device\n");
4601#line 145
4602    __cil_tmp19 = (void const   *)chip;
4603#line 145
4604    kfree(__cil_tmp19);
4605    }
4606#line 146
4607    return (res);
4608  } else {
4609
4610  }
4611  {
4612#line 149
4613  __cil_tmp20 = (struct device *)spi;
4614#line 149
4615  *((struct rtc_device **)chip) = rtc_device_register("ds1390", __cil_tmp20, & ds1390_rtc_ops,
4616                                                      & __this_module);
4617#line 151
4618  __cil_tmp21 = *((struct rtc_device **)chip);
4619#line 151
4620  __cil_tmp22 = (void const   *)__cil_tmp21;
4621#line 151
4622  tmp___10 = (long )IS_ERR(__cil_tmp22);
4623  }
4624#line 151
4625  if (tmp___10) {
4626    {
4627#line 152
4628    __cil_tmp23 = (struct device *)spi;
4629#line 152
4630    __cil_tmp24 = (struct device  const  *)__cil_tmp23;
4631#line 152
4632    dev_err(__cil_tmp24, "unable to register device\n");
4633#line 153
4634    __cil_tmp25 = *((struct rtc_device **)chip);
4635#line 153
4636    __cil_tmp26 = (void const   *)__cil_tmp25;
4637#line 153
4638    tmp___9 = (long )PTR_ERR(__cil_tmp26);
4639#line 153
4640    res = (int )tmp___9;
4641#line 154
4642    __cil_tmp27 = (void const   *)chip;
4643#line 154
4644    kfree(__cil_tmp27);
4645    }
4646  } else {
4647
4648  }
4649#line 157
4650  return (res);
4651}
4652}
4653#line 160
4654static int ds1390_remove(struct spi_device *spi )  __attribute__((__section__(".devexit.text"),
4655__no_instrument_function__)) ;
4656#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4657static int ds1390_remove(struct spi_device *spi ) 
4658{ struct ds1390 *chip ;
4659  void *tmp___7 ;
4660  struct rtc_device *__cil_tmp4 ;
4661  void const   *__cil_tmp5 ;
4662
4663  {
4664  {
4665#line 162
4666  tmp___7 = spi_get_drvdata(spi);
4667#line 162
4668  chip = (struct ds1390 *)tmp___7;
4669#line 164
4670  __cil_tmp4 = *((struct rtc_device **)chip);
4671#line 164
4672  rtc_device_unregister(__cil_tmp4);
4673#line 165
4674  __cil_tmp5 = (void const   *)chip;
4675#line 165
4676  kfree(__cil_tmp5);
4677  }
4678#line 167
4679  return (0);
4680}
4681}
4682#line 170 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4683static struct spi_driver ds1390_driver  =    {(struct spi_device_id  const  *)0, & ds1390_probe, & ds1390_remove, (void (*)(struct spi_device *spi ))0,
4684    (int (*)(struct spi_device *spi , pm_message_t mesg ))0, (int (*)(struct spi_device *spi ))0,
4685    {"rtc-ds1390", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
4686     (struct of_device_id  const  *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
4687     (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
4688     (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
4689     (struct driver_private *)0}};
4690#line 179
4691static int ds1390_driver_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
4692#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4693static int ds1390_driver_init(void) 
4694{ int tmp___7 ;
4695
4696  {
4697  {
4698#line 179
4699  tmp___7 = spi_register_driver(& ds1390_driver);
4700  }
4701#line 179
4702  return (tmp___7);
4703}
4704}
4705#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4706int init_module(void) 
4707{ int tmp___7 ;
4708
4709  {
4710  {
4711#line 179
4712  tmp___7 = ds1390_driver_init();
4713  }
4714#line 179
4715  return (tmp___7);
4716}
4717}
4718#line 179
4719static void ds1390_driver_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
4720#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4721static void ds1390_driver_exit(void) 
4722{ 
4723
4724  {
4725  {
4726#line 179
4727  spi_unregister_driver(& ds1390_driver);
4728  }
4729#line 179
4730  return;
4731}
4732}
4733#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4734void cleanup_module(void) 
4735{ 
4736
4737  {
4738  {
4739#line 179
4740  ds1390_driver_exit();
4741  }
4742#line 179
4743  return;
4744}
4745}
4746#line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4747static char const   __mod_description181[53]  __attribute__((__used__, __unused__,
4748__section__(".modinfo"), __aligned__(1)))  = 
4749#line 181
4750  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
4751        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
4752        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
4753        (char const   )'D',      (char const   )'a',      (char const   )'l',      (char const   )'l', 
4754        (char const   )'a',      (char const   )'s',      (char const   )'/',      (char const   )'M', 
4755        (char const   )'a',      (char const   )'x',      (char const   )'i',      (char const   )'m', 
4756        (char const   )' ',      (char const   )'D',      (char const   )'S',      (char const   )'1', 
4757        (char const   )'3',      (char const   )'9',      (char const   )'0',      (char const   )'/', 
4758        (char const   )'9',      (char const   )'3',      (char const   )'/',      (char const   )'9', 
4759        (char const   )'4',      (char const   )' ',      (char const   )'S',      (char const   )'P', 
4760        (char const   )'I',      (char const   )' ',      (char const   )'R',      (char const   )'T', 
4761        (char const   )'C',      (char const   )' ',      (char const   )'d',      (char const   )'r', 
4762        (char const   )'i',      (char const   )'v',      (char const   )'e',      (char const   )'r', 
4763        (char const   )'\000'};
4764#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4765static char const   __mod_author182[38]  __attribute__((__used__, __unused__, __section__(".modinfo"),
4766__aligned__(1)))  = 
4767#line 182
4768  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
4769        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'M', 
4770        (char const   )'a',      (char const   )'r',      (char const   )'k',      (char const   )' ', 
4771        (char const   )'J',      (char const   )'a',      (char const   )'c',      (char const   )'k', 
4772        (char const   )'s',      (char const   )'o',      (char const   )'n',      (char const   )' ', 
4773        (char const   )'<',      (char const   )'m',      (char const   )'p',      (char const   )'f', 
4774        (char const   )'j',      (char const   )'@',      (char const   )'m',      (char const   )'i', 
4775        (char const   )'m',      (char const   )'c',      (char const   )'.',      (char const   )'c', 
4776        (char const   )'o',      (char const   )'.',      (char const   )'u',      (char const   )'k', 
4777        (char const   )'>',      (char const   )'\000'};
4778#line 183 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4779static char const   __mod_license183[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
4780__aligned__(1)))  = 
4781#line 183
4782  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
4783        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
4784        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
4785#line 184 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4786static char const   __mod_alias184[21]  __attribute__((__used__, __unused__, __section__(".modinfo"),
4787__aligned__(1)))  = 
4788#line 184
4789  {      (char const   )'a',      (char const   )'l',      (char const   )'i',      (char const   )'a', 
4790        (char const   )'s',      (char const   )'=',      (char const   )'s',      (char const   )'p', 
4791        (char const   )'i',      (char const   )':',      (char const   )'r',      (char const   )'t', 
4792        (char const   )'c',      (char const   )'-',      (char const   )'d',      (char const   )'s', 
4793        (char const   )'1',      (char const   )'3',      (char const   )'9',      (char const   )'0', 
4794        (char const   )'\000'};
4795#line 202
4796void ldv_check_final_state(void) ;
4797#line 205
4798extern void ldv_check_return_value(int res ) ;
4799#line 208
4800extern void ldv_initialize(void) ;
4801#line 211
4802extern int __VERIFIER_nondet_int(void) ;
4803#line 214 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4804int LDV_IN_INTERRUPT  ;
4805#line 290 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4806static int res_ds1390_probe_3  ;
4807#line 217 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
4808void main(void) 
4809{ struct device *var_group1 ;
4810  struct rtc_time *var_group2 ;
4811  struct spi_device *var_group3 ;
4812  int ldv_s_ds1390_driver_spi_driver ;
4813  int tmp___7 ;
4814  int tmp___8 ;
4815  int __cil_tmp7 ;
4816
4817  {
4818  {
4819#line 298
4820  LDV_IN_INTERRUPT = 1;
4821#line 307
4822  ldv_initialize();
4823#line 310
4824  ldv_s_ds1390_driver_spi_driver = 0;
4825  }
4826  {
4827#line 313
4828  while (1) {
4829    while_continue: /* CIL Label */ ;
4830    {
4831#line 313
4832    tmp___8 = __VERIFIER_nondet_int();
4833    }
4834#line 313
4835    if (tmp___8) {
4836
4837    } else {
4838      {
4839#line 313
4840      __cil_tmp7 = ldv_s_ds1390_driver_spi_driver == 0;
4841#line 313
4842      if (! __cil_tmp7) {
4843
4844      } else {
4845#line 313
4846        goto while_break;
4847      }
4848      }
4849    }
4850    {
4851#line 317
4852    tmp___7 = __VERIFIER_nondet_int();
4853    }
4854#line 319
4855    if (tmp___7 == 0) {
4856#line 319
4857      goto case_0;
4858    } else
4859#line 352
4860    if (tmp___7 == 1) {
4861#line 352
4862      goto case_1;
4863    } else
4864#line 385
4865    if (tmp___7 == 2) {
4866#line 385
4867      goto case_2;
4868    } else {
4869      {
4870#line 421
4871      goto switch_default;
4872#line 317
4873      if (0) {
4874        case_0: /* CIL Label */ 
4875        {
4876#line 344
4877        ds1390_read_time(var_group1, var_group2);
4878        }
4879#line 351
4880        goto switch_break;
4881        case_1: /* CIL Label */ 
4882        {
4883#line 377
4884        ds1390_set_time(var_group1, var_group2);
4885        }
4886#line 384
4887        goto switch_break;
4888        case_2: /* CIL Label */ 
4889#line 388
4890        if (ldv_s_ds1390_driver_spi_driver == 0) {
4891          {
4892#line 410
4893          res_ds1390_probe_3 = ds1390_probe(var_group3);
4894#line 411
4895          ldv_check_return_value(res_ds1390_probe_3);
4896          }
4897#line 412
4898          if (res_ds1390_probe_3) {
4899#line 413
4900            goto ldv_module_exit;
4901          } else {
4902
4903          }
4904#line 414
4905          ldv_s_ds1390_driver_spi_driver = 0;
4906        } else {
4907
4908        }
4909#line 420
4910        goto switch_break;
4911        switch_default: /* CIL Label */ 
4912#line 421
4913        goto switch_break;
4914      } else {
4915        switch_break: /* CIL Label */ ;
4916      }
4917      }
4918    }
4919  }
4920  while_break: /* CIL Label */ ;
4921  }
4922  ldv_module_exit: 
4923  {
4924#line 430
4925  ldv_check_final_state();
4926  }
4927#line 433
4928  return;
4929}
4930}
4931#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4932void ldv_blast_assert(void) 
4933{ 
4934
4935  {
4936  ERROR: 
4937#line 6
4938  goto ERROR;
4939}
4940}
4941#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4942extern int __VERIFIER_nondet_int(void) ;
4943#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4944int ldv_mutex  =    1;
4945#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4946int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
4947{ int nondetermined ;
4948
4949  {
4950#line 29
4951  if (ldv_mutex == 1) {
4952
4953  } else {
4954    {
4955#line 29
4956    ldv_blast_assert();
4957    }
4958  }
4959  {
4960#line 32
4961  nondetermined = __VERIFIER_nondet_int();
4962  }
4963#line 35
4964  if (nondetermined) {
4965#line 38
4966    ldv_mutex = 2;
4967#line 40
4968    return (0);
4969  } else {
4970#line 45
4971    return (-4);
4972  }
4973}
4974}
4975#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4976int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
4977{ int nondetermined ;
4978
4979  {
4980#line 57
4981  if (ldv_mutex == 1) {
4982
4983  } else {
4984    {
4985#line 57
4986    ldv_blast_assert();
4987    }
4988  }
4989  {
4990#line 60
4991  nondetermined = __VERIFIER_nondet_int();
4992  }
4993#line 63
4994  if (nondetermined) {
4995#line 66
4996    ldv_mutex = 2;
4997#line 68
4998    return (0);
4999  } else {
5000#line 73
5001    return (-4);
5002  }
5003}
5004}
5005#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5006int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
5007{ int atomic_value_after_dec ;
5008
5009  {
5010#line 83
5011  if (ldv_mutex == 1) {
5012
5013  } else {
5014    {
5015#line 83
5016    ldv_blast_assert();
5017    }
5018  }
5019  {
5020#line 86
5021  atomic_value_after_dec = __VERIFIER_nondet_int();
5022  }
5023#line 89
5024  if (atomic_value_after_dec == 0) {
5025#line 92
5026    ldv_mutex = 2;
5027#line 94
5028    return (1);
5029  } else {
5030
5031  }
5032#line 98
5033  return (0);
5034}
5035}
5036#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5037void mutex_lock(struct mutex *lock ) 
5038{ 
5039
5040  {
5041#line 108
5042  if (ldv_mutex == 1) {
5043
5044  } else {
5045    {
5046#line 108
5047    ldv_blast_assert();
5048    }
5049  }
5050#line 110
5051  ldv_mutex = 2;
5052#line 111
5053  return;
5054}
5055}
5056#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5057int mutex_trylock(struct mutex *lock ) 
5058{ int nondetermined ;
5059
5060  {
5061#line 121
5062  if (ldv_mutex == 1) {
5063
5064  } else {
5065    {
5066#line 121
5067    ldv_blast_assert();
5068    }
5069  }
5070  {
5071#line 124
5072  nondetermined = __VERIFIER_nondet_int();
5073  }
5074#line 127
5075  if (nondetermined) {
5076#line 130
5077    ldv_mutex = 2;
5078#line 132
5079    return (1);
5080  } else {
5081#line 137
5082    return (0);
5083  }
5084}
5085}
5086#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5087void mutex_unlock(struct mutex *lock ) 
5088{ 
5089
5090  {
5091#line 147
5092  if (ldv_mutex == 2) {
5093
5094  } else {
5095    {
5096#line 147
5097    ldv_blast_assert();
5098    }
5099  }
5100#line 149
5101  ldv_mutex = 1;
5102#line 150
5103  return;
5104}
5105}
5106#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5107void ldv_check_final_state(void) 
5108{ 
5109
5110  {
5111#line 156
5112  if (ldv_mutex == 1) {
5113
5114  } else {
5115    {
5116#line 156
5117    ldv_blast_assert();
5118    }
5119  }
5120#line 157
5121  return;
5122}
5123}
5124#line 442 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6227/dscv_tempdir/dscv/ri/32_1/drivers/rtc/rtc-ds1390.c.common.c"
5125long s__builtin_expect(long val , long res ) 
5126{ 
5127
5128  {
5129#line 443
5130  return (val);
5131}
5132}