Showing error 1200

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