Showing error 232

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--hwmon--max1111.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3696
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 20 "include/asm-generic/int-ll64.h"
   5typedef unsigned char __u8;
   6#line 23 "include/asm-generic/int-ll64.h"
   7typedef unsigned short __u16;
   8#line 25 "include/asm-generic/int-ll64.h"
   9typedef int __s32;
  10#line 26 "include/asm-generic/int-ll64.h"
  11typedef unsigned int __u32;
  12#line 30 "include/asm-generic/int-ll64.h"
  13typedef unsigned long long __u64;
  14#line 43 "include/asm-generic/int-ll64.h"
  15typedef unsigned char u8;
  16#line 45 "include/asm-generic/int-ll64.h"
  17typedef short s16;
  18#line 46 "include/asm-generic/int-ll64.h"
  19typedef unsigned short u16;
  20#line 49 "include/asm-generic/int-ll64.h"
  21typedef unsigned int u32;
  22#line 51 "include/asm-generic/int-ll64.h"
  23typedef long long s64;
  24#line 52 "include/asm-generic/int-ll64.h"
  25typedef unsigned long long u64;
  26#line 14 "include/asm-generic/posix_types.h"
  27typedef long __kernel_long_t;
  28#line 15 "include/asm-generic/posix_types.h"
  29typedef unsigned long __kernel_ulong_t;
  30#line 31 "include/asm-generic/posix_types.h"
  31typedef int __kernel_pid_t;
  32#line 52 "include/asm-generic/posix_types.h"
  33typedef unsigned int __kernel_uid32_t;
  34#line 53 "include/asm-generic/posix_types.h"
  35typedef unsigned int __kernel_gid32_t;
  36#line 75 "include/asm-generic/posix_types.h"
  37typedef __kernel_ulong_t __kernel_size_t;
  38#line 76 "include/asm-generic/posix_types.h"
  39typedef __kernel_long_t __kernel_ssize_t;
  40#line 91 "include/asm-generic/posix_types.h"
  41typedef long long __kernel_loff_t;
  42#line 92 "include/asm-generic/posix_types.h"
  43typedef __kernel_long_t __kernel_time_t;
  44#line 93 "include/asm-generic/posix_types.h"
  45typedef __kernel_long_t __kernel_clock_t;
  46#line 94 "include/asm-generic/posix_types.h"
  47typedef int __kernel_timer_t;
  48#line 95 "include/asm-generic/posix_types.h"
  49typedef int __kernel_clockid_t;
  50#line 21 "include/linux/types.h"
  51typedef __u32 __kernel_dev_t;
  52#line 24 "include/linux/types.h"
  53typedef __kernel_dev_t dev_t;
  54#line 27 "include/linux/types.h"
  55typedef unsigned short umode_t;
  56#line 30 "include/linux/types.h"
  57typedef __kernel_pid_t pid_t;
  58#line 35 "include/linux/types.h"
  59typedef __kernel_clockid_t clockid_t;
  60#line 38 "include/linux/types.h"
  61typedef _Bool bool;
  62#line 40 "include/linux/types.h"
  63typedef __kernel_uid32_t uid_t;
  64#line 41 "include/linux/types.h"
  65typedef __kernel_gid32_t gid_t;
  66#line 54 "include/linux/types.h"
  67typedef __kernel_loff_t loff_t;
  68#line 63 "include/linux/types.h"
  69typedef __kernel_size_t size_t;
  70#line 68 "include/linux/types.h"
  71typedef __kernel_ssize_t ssize_t;
  72#line 78 "include/linux/types.h"
  73typedef __kernel_time_t time_t;
  74#line 111 "include/linux/types.h"
  75typedef __s32 int32_t;
  76#line 115 "include/linux/types.h"
  77typedef __u8 uint8_t;
  78#line 117 "include/linux/types.h"
  79typedef __u32 uint32_t;
  80#line 155 "include/linux/types.h"
  81typedef u64 dma_addr_t;
  82#line 202 "include/linux/types.h"
  83typedef unsigned int gfp_t;
  84#line 219 "include/linux/types.h"
  85struct __anonstruct_atomic_t_7 {
  86   int counter ;
  87};
  88#line 219 "include/linux/types.h"
  89typedef struct __anonstruct_atomic_t_7 atomic_t;
  90#line 224 "include/linux/types.h"
  91struct __anonstruct_atomic64_t_8 {
  92   long counter ;
  93};
  94#line 224 "include/linux/types.h"
  95typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  96#line 229 "include/linux/types.h"
  97struct list_head {
  98   struct list_head *next ;
  99   struct list_head *prev ;
 100};
 101#line 233
 102struct hlist_node;
 103#line 233 "include/linux/types.h"
 104struct hlist_head {
 105   struct hlist_node *first ;
 106};
 107#line 237 "include/linux/types.h"
 108struct hlist_node {
 109   struct hlist_node *next ;
 110   struct hlist_node **pprev ;
 111};
 112#line 253 "include/linux/types.h"
 113struct rcu_head {
 114   struct rcu_head *next ;
 115   void (*func)(struct rcu_head *head ) ;
 116};
 117#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 118struct module;
 119#line 56
 120struct module;
 121#line 146 "include/linux/init.h"
 122typedef void (*ctor_fn_t)(void);
 123#line 47 "include/linux/dynamic_debug.h"
 124struct device;
 125#line 47
 126struct device;
 127#line 135 "include/linux/kernel.h"
 128struct completion;
 129#line 135
 130struct completion;
 131#line 136
 132struct pt_regs;
 133#line 136
 134struct pt_regs;
 135#line 349
 136struct pid;
 137#line 349
 138struct pid;
 139#line 12 "include/linux/thread_info.h"
 140struct timespec;
 141#line 12
 142struct timespec;
 143#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 144struct page;
 145#line 18
 146struct page;
 147#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 148struct task_struct;
 149#line 20
 150struct task_struct;
 151#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 152struct task_struct;
 153#line 8
 154struct mm_struct;
 155#line 8
 156struct mm_struct;
 157#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 158struct pt_regs {
 159   unsigned long r15 ;
 160   unsigned long r14 ;
 161   unsigned long r13 ;
 162   unsigned long r12 ;
 163   unsigned long bp ;
 164   unsigned long bx ;
 165   unsigned long r11 ;
 166   unsigned long r10 ;
 167   unsigned long r9 ;
 168   unsigned long r8 ;
 169   unsigned long ax ;
 170   unsigned long cx ;
 171   unsigned long dx ;
 172   unsigned long si ;
 173   unsigned long di ;
 174   unsigned long orig_ax ;
 175   unsigned long ip ;
 176   unsigned long cs ;
 177   unsigned long flags ;
 178   unsigned long sp ;
 179   unsigned long ss ;
 180};
 181#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 182struct __anonstruct____missing_field_name_15 {
 183   unsigned int a ;
 184   unsigned int b ;
 185};
 186#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 187struct __anonstruct____missing_field_name_16 {
 188   u16 limit0 ;
 189   u16 base0 ;
 190   unsigned int base1 : 8 ;
 191   unsigned int type : 4 ;
 192   unsigned int s : 1 ;
 193   unsigned int dpl : 2 ;
 194   unsigned int p : 1 ;
 195   unsigned int limit : 4 ;
 196   unsigned int avl : 1 ;
 197   unsigned int l : 1 ;
 198   unsigned int d : 1 ;
 199   unsigned int g : 1 ;
 200   unsigned int base2 : 8 ;
 201};
 202#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 203union __anonunion____missing_field_name_14 {
 204   struct __anonstruct____missing_field_name_15 __annonCompField5 ;
 205   struct __anonstruct____missing_field_name_16 __annonCompField6 ;
 206};
 207#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 208struct desc_struct {
 209   union __anonunion____missing_field_name_14 __annonCompField7 ;
 210} __attribute__((__packed__)) ;
 211#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 212typedef unsigned long pgdval_t;
 213#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 214typedef unsigned long pgprotval_t;
 215#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 216struct pgprot {
 217   pgprotval_t pgprot ;
 218};
 219#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 220typedef struct pgprot pgprot_t;
 221#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 222struct __anonstruct_pgd_t_20 {
 223   pgdval_t pgd ;
 224};
 225#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 226typedef struct __anonstruct_pgd_t_20 pgd_t;
 227#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 228typedef struct page *pgtable_t;
 229#line 295
 230struct file;
 231#line 295
 232struct file;
 233#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 234struct page;
 235#line 47
 236struct thread_struct;
 237#line 47
 238struct thread_struct;
 239#line 50
 240struct mm_struct;
 241#line 51
 242struct desc_struct;
 243#line 52
 244struct task_struct;
 245#line 53
 246struct cpumask;
 247#line 53
 248struct cpumask;
 249#line 329
 250struct arch_spinlock;
 251#line 329
 252struct arch_spinlock;
 253#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 254struct task_struct;
 255#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.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 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 268union __anonunion____missing_field_name_24 {
 269   struct pt_regs *regs ;
 270   struct kernel_vm86_regs *vm86 ;
 271};
 272#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 273struct math_emu_info {
 274   long ___orig_eip ;
 275   union __anonunion____missing_field_name_24 __annonCompField8 ;
 276};
 277#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 278struct task_struct;
 279#line 10 "include/asm-generic/bug.h"
 280struct bug_entry {
 281   int bug_addr_disp ;
 282   int file_disp ;
 283   unsigned short line ;
 284   unsigned short flags ;
 285};
 286#line 12 "include/linux/bug.h"
 287struct pt_regs;
 288#line 14 "include/linux/cpumask.h"
 289struct cpumask {
 290   unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 291};
 292#line 14 "include/linux/cpumask.h"
 293typedef struct cpumask cpumask_t;
 294#line 637 "include/linux/cpumask.h"
 295typedef struct cpumask *cpumask_var_t;
 296#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 297struct static_key;
 298#line 234
 299struct static_key;
 300#line 11 "include/linux/personality.h"
 301struct pt_regs;
 302#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 303struct i387_fsave_struct {
 304   u32 cwd ;
 305   u32 swd ;
 306   u32 twd ;
 307   u32 fip ;
 308   u32 fcs ;
 309   u32 foo ;
 310   u32 fos ;
 311   u32 st_space[20] ;
 312   u32 status ;
 313};
 314#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 315struct __anonstruct____missing_field_name_31 {
 316   u64 rip ;
 317   u64 rdp ;
 318};
 319#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 320struct __anonstruct____missing_field_name_32 {
 321   u32 fip ;
 322   u32 fcs ;
 323   u32 foo ;
 324   u32 fos ;
 325};
 326#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 327union __anonunion____missing_field_name_30 {
 328   struct __anonstruct____missing_field_name_31 __annonCompField12 ;
 329   struct __anonstruct____missing_field_name_32 __annonCompField13 ;
 330};
 331#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 332union __anonunion____missing_field_name_33 {
 333   u32 padding1[12] ;
 334   u32 sw_reserved[12] ;
 335};
 336#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 337struct i387_fxsave_struct {
 338   u16 cwd ;
 339   u16 swd ;
 340   u16 twd ;
 341   u16 fop ;
 342   union __anonunion____missing_field_name_30 __annonCompField14 ;
 343   u32 mxcsr ;
 344   u32 mxcsr_mask ;
 345   u32 st_space[32] ;
 346   u32 xmm_space[64] ;
 347   u32 padding[12] ;
 348   union __anonunion____missing_field_name_33 __annonCompField15 ;
 349} __attribute__((__aligned__(16))) ;
 350#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 351struct i387_soft_struct {
 352   u32 cwd ;
 353   u32 swd ;
 354   u32 twd ;
 355   u32 fip ;
 356   u32 fcs ;
 357   u32 foo ;
 358   u32 fos ;
 359   u32 st_space[20] ;
 360   u8 ftop ;
 361   u8 changed ;
 362   u8 lookahead ;
 363   u8 no_update ;
 364   u8 rm ;
 365   u8 alimit ;
 366   struct math_emu_info *info ;
 367   u32 entry_eip ;
 368};
 369#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 370struct ymmh_struct {
 371   u32 ymmh_space[64] ;
 372};
 373#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 374struct xsave_hdr_struct {
 375   u64 xstate_bv ;
 376   u64 reserved1[2] ;
 377   u64 reserved2[5] ;
 378} __attribute__((__packed__)) ;
 379#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 380struct xsave_struct {
 381   struct i387_fxsave_struct i387 ;
 382   struct xsave_hdr_struct xsave_hdr ;
 383   struct ymmh_struct ymmh ;
 384} __attribute__((__packed__, __aligned__(64))) ;
 385#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 386union thread_xstate {
 387   struct i387_fsave_struct fsave ;
 388   struct i387_fxsave_struct fxsave ;
 389   struct i387_soft_struct soft ;
 390   struct xsave_struct xsave ;
 391};
 392#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 393struct fpu {
 394   unsigned int last_cpu ;
 395   unsigned int has_fpu ;
 396   union thread_xstate *state ;
 397};
 398#line 433
 399struct kmem_cache;
 400#line 435
 401struct perf_event;
 402#line 435
 403struct perf_event;
 404#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 405struct thread_struct {
 406   struct desc_struct tls_array[3] ;
 407   unsigned long sp0 ;
 408   unsigned long sp ;
 409   unsigned long usersp ;
 410   unsigned short es ;
 411   unsigned short ds ;
 412   unsigned short fsindex ;
 413   unsigned short gsindex ;
 414   unsigned long fs ;
 415   unsigned long gs ;
 416   struct perf_event *ptrace_bps[4] ;
 417   unsigned long debugreg6 ;
 418   unsigned long ptrace_dr7 ;
 419   unsigned long cr2 ;
 420   unsigned long trap_nr ;
 421   unsigned long error_code ;
 422   struct fpu fpu ;
 423   unsigned long *io_bitmap_ptr ;
 424   unsigned long iopl ;
 425   unsigned int io_bitmap_max ;
 426};
 427#line 23 "include/asm-generic/atomic-long.h"
 428typedef atomic64_t atomic_long_t;
 429#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 430typedef u16 __ticket_t;
 431#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 432typedef u32 __ticketpair_t;
 433#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 434struct __raw_tickets {
 435   __ticket_t head ;
 436   __ticket_t tail ;
 437};
 438#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 439union __anonunion____missing_field_name_36 {
 440   __ticketpair_t head_tail ;
 441   struct __raw_tickets tickets ;
 442};
 443#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 444struct arch_spinlock {
 445   union __anonunion____missing_field_name_36 __annonCompField17 ;
 446};
 447#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 448typedef struct arch_spinlock arch_spinlock_t;
 449#line 12 "include/linux/lockdep.h"
 450struct task_struct;
 451#line 391 "include/linux/lockdep.h"
 452struct lock_class_key {
 453
 454};
 455#line 20 "include/linux/spinlock_types.h"
 456struct raw_spinlock {
 457   arch_spinlock_t raw_lock ;
 458   unsigned int magic ;
 459   unsigned int owner_cpu ;
 460   void *owner ;
 461};
 462#line 20 "include/linux/spinlock_types.h"
 463typedef struct raw_spinlock raw_spinlock_t;
 464#line 64 "include/linux/spinlock_types.h"
 465union __anonunion____missing_field_name_39 {
 466   struct raw_spinlock rlock ;
 467};
 468#line 64 "include/linux/spinlock_types.h"
 469struct spinlock {
 470   union __anonunion____missing_field_name_39 __annonCompField19 ;
 471};
 472#line 64 "include/linux/spinlock_types.h"
 473typedef struct spinlock spinlock_t;
 474#line 119 "include/linux/seqlock.h"
 475struct seqcount {
 476   unsigned int sequence ;
 477};
 478#line 119 "include/linux/seqlock.h"
 479typedef struct seqcount seqcount_t;
 480#line 14 "include/linux/time.h"
 481struct timespec {
 482   __kernel_time_t tv_sec ;
 483   long tv_nsec ;
 484};
 485#line 49 "include/linux/wait.h"
 486struct __wait_queue_head {
 487   spinlock_t lock ;
 488   struct list_head task_list ;
 489};
 490#line 53 "include/linux/wait.h"
 491typedef struct __wait_queue_head wait_queue_head_t;
 492#line 55
 493struct task_struct;
 494#line 98 "include/linux/nodemask.h"
 495struct __anonstruct_nodemask_t_42 {
 496   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 497};
 498#line 98 "include/linux/nodemask.h"
 499typedef struct __anonstruct_nodemask_t_42 nodemask_t;
 500#line 60 "include/linux/pageblock-flags.h"
 501struct page;
 502#line 48 "include/linux/mutex.h"
 503struct mutex {
 504   atomic_t count ;
 505   spinlock_t wait_lock ;
 506   struct list_head wait_list ;
 507   struct task_struct *owner ;
 508   char const   *name ;
 509   void *magic ;
 510};
 511#line 69 "include/linux/mutex.h"
 512struct mutex_waiter {
 513   struct list_head list ;
 514   struct task_struct *task ;
 515   void *magic ;
 516};
 517#line 19 "include/linux/rwsem.h"
 518struct rw_semaphore;
 519#line 19
 520struct rw_semaphore;
 521#line 25 "include/linux/rwsem.h"
 522struct rw_semaphore {
 523   long count ;
 524   raw_spinlock_t wait_lock ;
 525   struct list_head wait_list ;
 526};
 527#line 25 "include/linux/completion.h"
 528struct completion {
 529   unsigned int done ;
 530   wait_queue_head_t wait ;
 531};
 532#line 9 "include/linux/memory_hotplug.h"
 533struct page;
 534#line 202 "include/linux/ioport.h"
 535struct device;
 536#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 537struct device;
 538#line 46 "include/linux/ktime.h"
 539union ktime {
 540   s64 tv64 ;
 541};
 542#line 59 "include/linux/ktime.h"
 543typedef union ktime ktime_t;
 544#line 10 "include/linux/timer.h"
 545struct tvec_base;
 546#line 10
 547struct tvec_base;
 548#line 12 "include/linux/timer.h"
 549struct timer_list {
 550   struct list_head entry ;
 551   unsigned long expires ;
 552   struct tvec_base *base ;
 553   void (*function)(unsigned long  ) ;
 554   unsigned long data ;
 555   int slack ;
 556   int start_pid ;
 557   void *start_site ;
 558   char start_comm[16] ;
 559};
 560#line 289
 561struct hrtimer;
 562#line 289
 563struct hrtimer;
 564#line 290
 565enum hrtimer_restart;
 566#line 17 "include/linux/workqueue.h"
 567struct work_struct;
 568#line 17
 569struct work_struct;
 570#line 79 "include/linux/workqueue.h"
 571struct work_struct {
 572   atomic_long_t data ;
 573   struct list_head entry ;
 574   void (*func)(struct work_struct *work ) ;
 575};
 576#line 42 "include/linux/pm.h"
 577struct device;
 578#line 50 "include/linux/pm.h"
 579struct pm_message {
 580   int event ;
 581};
 582#line 50 "include/linux/pm.h"
 583typedef struct pm_message pm_message_t;
 584#line 264 "include/linux/pm.h"
 585struct dev_pm_ops {
 586   int (*prepare)(struct device *dev ) ;
 587   void (*complete)(struct device *dev ) ;
 588   int (*suspend)(struct device *dev ) ;
 589   int (*resume)(struct device *dev ) ;
 590   int (*freeze)(struct device *dev ) ;
 591   int (*thaw)(struct device *dev ) ;
 592   int (*poweroff)(struct device *dev ) ;
 593   int (*restore)(struct device *dev ) ;
 594   int (*suspend_late)(struct device *dev ) ;
 595   int (*resume_early)(struct device *dev ) ;
 596   int (*freeze_late)(struct device *dev ) ;
 597   int (*thaw_early)(struct device *dev ) ;
 598   int (*poweroff_late)(struct device *dev ) ;
 599   int (*restore_early)(struct device *dev ) ;
 600   int (*suspend_noirq)(struct device *dev ) ;
 601   int (*resume_noirq)(struct device *dev ) ;
 602   int (*freeze_noirq)(struct device *dev ) ;
 603   int (*thaw_noirq)(struct device *dev ) ;
 604   int (*poweroff_noirq)(struct device *dev ) ;
 605   int (*restore_noirq)(struct device *dev ) ;
 606   int (*runtime_suspend)(struct device *dev ) ;
 607   int (*runtime_resume)(struct device *dev ) ;
 608   int (*runtime_idle)(struct device *dev ) ;
 609};
 610#line 458
 611enum rpm_status {
 612    RPM_ACTIVE = 0,
 613    RPM_RESUMING = 1,
 614    RPM_SUSPENDED = 2,
 615    RPM_SUSPENDING = 3
 616} ;
 617#line 480
 618enum rpm_request {
 619    RPM_REQ_NONE = 0,
 620    RPM_REQ_IDLE = 1,
 621    RPM_REQ_SUSPEND = 2,
 622    RPM_REQ_AUTOSUSPEND = 3,
 623    RPM_REQ_RESUME = 4
 624} ;
 625#line 488
 626struct wakeup_source;
 627#line 488
 628struct wakeup_source;
 629#line 495 "include/linux/pm.h"
 630struct pm_subsys_data {
 631   spinlock_t lock ;
 632   unsigned int refcount ;
 633};
 634#line 506
 635struct dev_pm_qos_request;
 636#line 506
 637struct pm_qos_constraints;
 638#line 506 "include/linux/pm.h"
 639struct dev_pm_info {
 640   pm_message_t power_state ;
 641   unsigned int can_wakeup : 1 ;
 642   unsigned int async_suspend : 1 ;
 643   bool is_prepared : 1 ;
 644   bool is_suspended : 1 ;
 645   bool ignore_children : 1 ;
 646   spinlock_t lock ;
 647   struct list_head entry ;
 648   struct completion completion ;
 649   struct wakeup_source *wakeup ;
 650   bool wakeup_path : 1 ;
 651   struct timer_list suspend_timer ;
 652   unsigned long timer_expires ;
 653   struct work_struct work ;
 654   wait_queue_head_t wait_queue ;
 655   atomic_t usage_count ;
 656   atomic_t child_count ;
 657   unsigned int disable_depth : 3 ;
 658   unsigned int idle_notification : 1 ;
 659   unsigned int request_pending : 1 ;
 660   unsigned int deferred_resume : 1 ;
 661   unsigned int run_wake : 1 ;
 662   unsigned int runtime_auto : 1 ;
 663   unsigned int no_callbacks : 1 ;
 664   unsigned int irq_safe : 1 ;
 665   unsigned int use_autosuspend : 1 ;
 666   unsigned int timer_autosuspends : 1 ;
 667   enum rpm_request request ;
 668   enum rpm_status runtime_status ;
 669   int runtime_error ;
 670   int autosuspend_delay ;
 671   unsigned long last_busy ;
 672   unsigned long active_jiffies ;
 673   unsigned long suspended_jiffies ;
 674   unsigned long accounting_timestamp ;
 675   ktime_t suspend_time ;
 676   s64 max_time_suspended_ns ;
 677   struct dev_pm_qos_request *pq_req ;
 678   struct pm_subsys_data *subsys_data ;
 679   struct pm_qos_constraints *constraints ;
 680};
 681#line 564 "include/linux/pm.h"
 682struct dev_pm_domain {
 683   struct dev_pm_ops ops ;
 684};
 685#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 686struct __anonstruct_mm_context_t_112 {
 687   void *ldt ;
 688   int size ;
 689   unsigned short ia32_compat ;
 690   struct mutex lock ;
 691   void *vdso ;
 692};
 693#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 694typedef struct __anonstruct_mm_context_t_112 mm_context_t;
 695#line 8 "include/linux/vmalloc.h"
 696struct vm_area_struct;
 697#line 8
 698struct vm_area_struct;
 699#line 994 "include/linux/mmzone.h"
 700struct page;
 701#line 10 "include/linux/gfp.h"
 702struct vm_area_struct;
 703#line 29 "include/linux/sysctl.h"
 704struct completion;
 705#line 100 "include/linux/rbtree.h"
 706struct rb_node {
 707   unsigned long rb_parent_color ;
 708   struct rb_node *rb_right ;
 709   struct rb_node *rb_left ;
 710} __attribute__((__aligned__(sizeof(long )))) ;
 711#line 110 "include/linux/rbtree.h"
 712struct rb_root {
 713   struct rb_node *rb_node ;
 714};
 715#line 939 "include/linux/sysctl.h"
 716struct nsproxy;
 717#line 939
 718struct nsproxy;
 719#line 48 "include/linux/kmod.h"
 720struct cred;
 721#line 48
 722struct cred;
 723#line 49
 724struct file;
 725#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 726struct task_struct;
 727#line 18 "include/linux/elf.h"
 728typedef __u64 Elf64_Addr;
 729#line 19 "include/linux/elf.h"
 730typedef __u16 Elf64_Half;
 731#line 23 "include/linux/elf.h"
 732typedef __u32 Elf64_Word;
 733#line 24 "include/linux/elf.h"
 734typedef __u64 Elf64_Xword;
 735#line 194 "include/linux/elf.h"
 736struct elf64_sym {
 737   Elf64_Word st_name ;
 738   unsigned char st_info ;
 739   unsigned char st_other ;
 740   Elf64_Half st_shndx ;
 741   Elf64_Addr st_value ;
 742   Elf64_Xword st_size ;
 743};
 744#line 194 "include/linux/elf.h"
 745typedef struct elf64_sym Elf64_Sym;
 746#line 438
 747struct file;
 748#line 20 "include/linux/kobject_ns.h"
 749struct sock;
 750#line 20
 751struct sock;
 752#line 21
 753struct kobject;
 754#line 21
 755struct kobject;
 756#line 27
 757enum kobj_ns_type {
 758    KOBJ_NS_TYPE_NONE = 0,
 759    KOBJ_NS_TYPE_NET = 1,
 760    KOBJ_NS_TYPES = 2
 761} ;
 762#line 40 "include/linux/kobject_ns.h"
 763struct kobj_ns_type_operations {
 764   enum kobj_ns_type type ;
 765   void *(*grab_current_ns)(void) ;
 766   void const   *(*netlink_ns)(struct sock *sk ) ;
 767   void const   *(*initial_ns)(void) ;
 768   void (*drop_ns)(void * ) ;
 769};
 770#line 22 "include/linux/sysfs.h"
 771struct kobject;
 772#line 23
 773struct module;
 774#line 24
 775enum kobj_ns_type;
 776#line 26 "include/linux/sysfs.h"
 777struct attribute {
 778   char const   *name ;
 779   umode_t mode ;
 780};
 781#line 56 "include/linux/sysfs.h"
 782struct attribute_group {
 783   char const   *name ;
 784   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 785   struct attribute **attrs ;
 786};
 787#line 85
 788struct file;
 789#line 86
 790struct vm_area_struct;
 791#line 88 "include/linux/sysfs.h"
 792struct bin_attribute {
 793   struct attribute attr ;
 794   size_t size ;
 795   void *private ;
 796   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 797                   loff_t  , size_t  ) ;
 798   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 799                    loff_t  , size_t  ) ;
 800   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 801};
 802#line 112 "include/linux/sysfs.h"
 803struct sysfs_ops {
 804   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 805   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 806   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 807};
 808#line 118
 809struct sysfs_dirent;
 810#line 118
 811struct sysfs_dirent;
 812#line 22 "include/linux/kref.h"
 813struct kref {
 814   atomic_t refcount ;
 815};
 816#line 60 "include/linux/kobject.h"
 817struct kset;
 818#line 60
 819struct kobj_type;
 820#line 60 "include/linux/kobject.h"
 821struct kobject {
 822   char const   *name ;
 823   struct list_head entry ;
 824   struct kobject *parent ;
 825   struct kset *kset ;
 826   struct kobj_type *ktype ;
 827   struct sysfs_dirent *sd ;
 828   struct kref kref ;
 829   unsigned int state_initialized : 1 ;
 830   unsigned int state_in_sysfs : 1 ;
 831   unsigned int state_add_uevent_sent : 1 ;
 832   unsigned int state_remove_uevent_sent : 1 ;
 833   unsigned int uevent_suppress : 1 ;
 834};
 835#line 108 "include/linux/kobject.h"
 836struct kobj_type {
 837   void (*release)(struct kobject *kobj ) ;
 838   struct sysfs_ops  const  *sysfs_ops ;
 839   struct attribute **default_attrs ;
 840   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 841   void const   *(*namespace)(struct kobject *kobj ) ;
 842};
 843#line 116 "include/linux/kobject.h"
 844struct kobj_uevent_env {
 845   char *envp[32] ;
 846   int envp_idx ;
 847   char buf[2048] ;
 848   int buflen ;
 849};
 850#line 123 "include/linux/kobject.h"
 851struct kset_uevent_ops {
 852   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 853   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 854   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 855};
 856#line 140
 857struct sock;
 858#line 159 "include/linux/kobject.h"
 859struct kset {
 860   struct list_head list ;
 861   spinlock_t list_lock ;
 862   struct kobject kobj ;
 863   struct kset_uevent_ops  const  *uevent_ops ;
 864};
 865#line 39 "include/linux/moduleparam.h"
 866struct kernel_param;
 867#line 39
 868struct kernel_param;
 869#line 41 "include/linux/moduleparam.h"
 870struct kernel_param_ops {
 871   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 872   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 873   void (*free)(void *arg ) ;
 874};
 875#line 50
 876struct kparam_string;
 877#line 50
 878struct kparam_array;
 879#line 50 "include/linux/moduleparam.h"
 880union __anonunion____missing_field_name_199 {
 881   void *arg ;
 882   struct kparam_string  const  *str ;
 883   struct kparam_array  const  *arr ;
 884};
 885#line 50 "include/linux/moduleparam.h"
 886struct kernel_param {
 887   char const   *name ;
 888   struct kernel_param_ops  const  *ops ;
 889   u16 perm ;
 890   s16 level ;
 891   union __anonunion____missing_field_name_199 __annonCompField32 ;
 892};
 893#line 63 "include/linux/moduleparam.h"
 894struct kparam_string {
 895   unsigned int maxlen ;
 896   char *string ;
 897};
 898#line 69 "include/linux/moduleparam.h"
 899struct kparam_array {
 900   unsigned int max ;
 901   unsigned int elemsize ;
 902   unsigned int *num ;
 903   struct kernel_param_ops  const  *ops ;
 904   void *elem ;
 905};
 906#line 445
 907struct module;
 908#line 80 "include/linux/jump_label.h"
 909struct module;
 910#line 143 "include/linux/jump_label.h"
 911struct static_key {
 912   atomic_t enabled ;
 913};
 914#line 22 "include/linux/tracepoint.h"
 915struct module;
 916#line 23
 917struct tracepoint;
 918#line 23
 919struct tracepoint;
 920#line 25 "include/linux/tracepoint.h"
 921struct tracepoint_func {
 922   void *func ;
 923   void *data ;
 924};
 925#line 30 "include/linux/tracepoint.h"
 926struct tracepoint {
 927   char const   *name ;
 928   struct static_key key ;
 929   void (*regfunc)(void) ;
 930   void (*unregfunc)(void) ;
 931   struct tracepoint_func *funcs ;
 932};
 933#line 19 "include/linux/export.h"
 934struct kernel_symbol {
 935   unsigned long value ;
 936   char const   *name ;
 937};
 938#line 8 "include/asm-generic/module.h"
 939struct mod_arch_specific {
 940
 941};
 942#line 35 "include/linux/module.h"
 943struct module;
 944#line 37
 945struct module_param_attrs;
 946#line 37 "include/linux/module.h"
 947struct module_kobject {
 948   struct kobject kobj ;
 949   struct module *mod ;
 950   struct kobject *drivers_dir ;
 951   struct module_param_attrs *mp ;
 952};
 953#line 44 "include/linux/module.h"
 954struct module_attribute {
 955   struct attribute attr ;
 956   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 957   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 958                    size_t count ) ;
 959   void (*setup)(struct module * , char const   * ) ;
 960   int (*test)(struct module * ) ;
 961   void (*free)(struct module * ) ;
 962};
 963#line 71
 964struct exception_table_entry;
 965#line 71
 966struct exception_table_entry;
 967#line 199
 968enum module_state {
 969    MODULE_STATE_LIVE = 0,
 970    MODULE_STATE_COMING = 1,
 971    MODULE_STATE_GOING = 2
 972} ;
 973#line 215 "include/linux/module.h"
 974struct module_ref {
 975   unsigned long incs ;
 976   unsigned long decs ;
 977} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 978#line 220
 979struct module_sect_attrs;
 980#line 220
 981struct module_notes_attrs;
 982#line 220
 983struct ftrace_event_call;
 984#line 220 "include/linux/module.h"
 985struct module {
 986   enum module_state state ;
 987   struct list_head list ;
 988   char name[64UL - sizeof(unsigned long )] ;
 989   struct module_kobject mkobj ;
 990   struct module_attribute *modinfo_attrs ;
 991   char const   *version ;
 992   char const   *srcversion ;
 993   struct kobject *holders_dir ;
 994   struct kernel_symbol  const  *syms ;
 995   unsigned long const   *crcs ;
 996   unsigned int num_syms ;
 997   struct kernel_param *kp ;
 998   unsigned int num_kp ;
 999   unsigned int num_gpl_syms ;
1000   struct kernel_symbol  const  *gpl_syms ;
1001   unsigned long const   *gpl_crcs ;
1002   struct kernel_symbol  const  *unused_syms ;
1003   unsigned long const   *unused_crcs ;
1004   unsigned int num_unused_syms ;
1005   unsigned int num_unused_gpl_syms ;
1006   struct kernel_symbol  const  *unused_gpl_syms ;
1007   unsigned long const   *unused_gpl_crcs ;
1008   struct kernel_symbol  const  *gpl_future_syms ;
1009   unsigned long const   *gpl_future_crcs ;
1010   unsigned int num_gpl_future_syms ;
1011   unsigned int num_exentries ;
1012   struct exception_table_entry *extable ;
1013   int (*init)(void) ;
1014   void *module_init ;
1015   void *module_core ;
1016   unsigned int init_size ;
1017   unsigned int core_size ;
1018   unsigned int init_text_size ;
1019   unsigned int core_text_size ;
1020   unsigned int init_ro_size ;
1021   unsigned int core_ro_size ;
1022   struct mod_arch_specific arch ;
1023   unsigned int taints ;
1024   unsigned int num_bugs ;
1025   struct list_head bug_list ;
1026   struct bug_entry *bug_table ;
1027   Elf64_Sym *symtab ;
1028   Elf64_Sym *core_symtab ;
1029   unsigned int num_symtab ;
1030   unsigned int core_num_syms ;
1031   char *strtab ;
1032   char *core_strtab ;
1033   struct module_sect_attrs *sect_attrs ;
1034   struct module_notes_attrs *notes_attrs ;
1035   char *args ;
1036   void *percpu ;
1037   unsigned int percpu_size ;
1038   unsigned int num_tracepoints ;
1039   struct tracepoint * const  *tracepoints_ptrs ;
1040   unsigned int num_trace_bprintk_fmt ;
1041   char const   **trace_bprintk_fmt_start ;
1042   struct ftrace_event_call **trace_events ;
1043   unsigned int num_trace_events ;
1044   struct list_head source_list ;
1045   struct list_head target_list ;
1046   struct task_struct *waiter ;
1047   void (*exit)(void) ;
1048   struct module_ref *refptr ;
1049   ctor_fn_t *ctors ;
1050   unsigned int num_ctors ;
1051};
1052#line 17 "include/linux/hwmon.h"
1053struct device;
1054#line 19 "include/linux/klist.h"
1055struct klist_node;
1056#line 19
1057struct klist_node;
1058#line 39 "include/linux/klist.h"
1059struct klist_node {
1060   void *n_klist ;
1061   struct list_head n_node ;
1062   struct kref n_ref ;
1063};
1064#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1065struct dma_map_ops;
1066#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1067struct dev_archdata {
1068   void *acpi_handle ;
1069   struct dma_map_ops *dma_ops ;
1070   void *iommu ;
1071};
1072#line 28 "include/linux/device.h"
1073struct device;
1074#line 29
1075struct device_private;
1076#line 29
1077struct device_private;
1078#line 30
1079struct device_driver;
1080#line 30
1081struct device_driver;
1082#line 31
1083struct driver_private;
1084#line 31
1085struct driver_private;
1086#line 32
1087struct module;
1088#line 33
1089struct class;
1090#line 33
1091struct class;
1092#line 34
1093struct subsys_private;
1094#line 34
1095struct subsys_private;
1096#line 35
1097struct bus_type;
1098#line 35
1099struct bus_type;
1100#line 36
1101struct device_node;
1102#line 36
1103struct device_node;
1104#line 37
1105struct iommu_ops;
1106#line 37
1107struct iommu_ops;
1108#line 39 "include/linux/device.h"
1109struct bus_attribute {
1110   struct attribute attr ;
1111   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
1112   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
1113};
1114#line 89
1115struct device_attribute;
1116#line 89
1117struct driver_attribute;
1118#line 89 "include/linux/device.h"
1119struct bus_type {
1120   char const   *name ;
1121   char const   *dev_name ;
1122   struct device *dev_root ;
1123   struct bus_attribute *bus_attrs ;
1124   struct device_attribute *dev_attrs ;
1125   struct driver_attribute *drv_attrs ;
1126   int (*match)(struct device *dev , struct device_driver *drv ) ;
1127   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1128   int (*probe)(struct device *dev ) ;
1129   int (*remove)(struct device *dev ) ;
1130   void (*shutdown)(struct device *dev ) ;
1131   int (*suspend)(struct device *dev , pm_message_t state ) ;
1132   int (*resume)(struct device *dev ) ;
1133   struct dev_pm_ops  const  *pm ;
1134   struct iommu_ops *iommu_ops ;
1135   struct subsys_private *p ;
1136};
1137#line 127
1138struct device_type;
1139#line 214
1140struct of_device_id;
1141#line 214 "include/linux/device.h"
1142struct device_driver {
1143   char const   *name ;
1144   struct bus_type *bus ;
1145   struct module *owner ;
1146   char const   *mod_name ;
1147   bool suppress_bind_attrs ;
1148   struct of_device_id  const  *of_match_table ;
1149   int (*probe)(struct device *dev ) ;
1150   int (*remove)(struct device *dev ) ;
1151   void (*shutdown)(struct device *dev ) ;
1152   int (*suspend)(struct device *dev , pm_message_t state ) ;
1153   int (*resume)(struct device *dev ) ;
1154   struct attribute_group  const  **groups ;
1155   struct dev_pm_ops  const  *pm ;
1156   struct driver_private *p ;
1157};
1158#line 249 "include/linux/device.h"
1159struct driver_attribute {
1160   struct attribute attr ;
1161   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1162   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
1163};
1164#line 330
1165struct class_attribute;
1166#line 330 "include/linux/device.h"
1167struct class {
1168   char const   *name ;
1169   struct module *owner ;
1170   struct class_attribute *class_attrs ;
1171   struct device_attribute *dev_attrs ;
1172   struct bin_attribute *dev_bin_attrs ;
1173   struct kobject *dev_kobj ;
1174   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1175   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1176   void (*class_release)(struct class *class ) ;
1177   void (*dev_release)(struct device *dev ) ;
1178   int (*suspend)(struct device *dev , pm_message_t state ) ;
1179   int (*resume)(struct device *dev ) ;
1180   struct kobj_ns_type_operations  const  *ns_type ;
1181   void const   *(*namespace)(struct device *dev ) ;
1182   struct dev_pm_ops  const  *pm ;
1183   struct subsys_private *p ;
1184};
1185#line 397 "include/linux/device.h"
1186struct class_attribute {
1187   struct attribute attr ;
1188   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1189   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
1190                    size_t count ) ;
1191   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
1192};
1193#line 465 "include/linux/device.h"
1194struct device_type {
1195   char const   *name ;
1196   struct attribute_group  const  **groups ;
1197   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1198   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1199   void (*release)(struct device *dev ) ;
1200   struct dev_pm_ops  const  *pm ;
1201};
1202#line 476 "include/linux/device.h"
1203struct device_attribute {
1204   struct attribute attr ;
1205   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1206   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
1207                    size_t count ) ;
1208};
1209#line 559 "include/linux/device.h"
1210struct device_dma_parameters {
1211   unsigned int max_segment_size ;
1212   unsigned long segment_boundary_mask ;
1213};
1214#line 627
1215struct dma_coherent_mem;
1216#line 627 "include/linux/device.h"
1217struct device {
1218   struct device *parent ;
1219   struct device_private *p ;
1220   struct kobject kobj ;
1221   char const   *init_name ;
1222   struct device_type  const  *type ;
1223   struct mutex mutex ;
1224   struct bus_type *bus ;
1225   struct device_driver *driver ;
1226   void *platform_data ;
1227   struct dev_pm_info power ;
1228   struct dev_pm_domain *pm_domain ;
1229   int numa_node ;
1230   u64 *dma_mask ;
1231   u64 coherent_dma_mask ;
1232   struct device_dma_parameters *dma_parms ;
1233   struct list_head dma_pools ;
1234   struct dma_coherent_mem *dma_mem ;
1235   struct dev_archdata archdata ;
1236   struct device_node *of_node ;
1237   dev_t devt ;
1238   u32 id ;
1239   spinlock_t devres_lock ;
1240   struct list_head devres_head ;
1241   struct klist_node knode_class ;
1242   struct class *class ;
1243   struct attribute_group  const  **groups ;
1244   void (*release)(struct device *dev ) ;
1245};
1246#line 43 "include/linux/pm_wakeup.h"
1247struct wakeup_source {
1248   char const   *name ;
1249   struct list_head entry ;
1250   spinlock_t lock ;
1251   struct timer_list timer ;
1252   unsigned long timer_expires ;
1253   ktime_t total_time ;
1254   ktime_t max_time ;
1255   ktime_t last_time ;
1256   unsigned long event_count ;
1257   unsigned long active_count ;
1258   unsigned long relax_count ;
1259   unsigned long hit_count ;
1260   unsigned int active : 1 ;
1261};
1262#line 25 "include/linux/hwmon-sysfs.h"
1263struct sensor_device_attribute {
1264   struct device_attribute dev_attr ;
1265   int index ;
1266};
1267#line 12 "include/linux/mod_devicetable.h"
1268typedef unsigned long kernel_ulong_t;
1269#line 219 "include/linux/mod_devicetable.h"
1270struct of_device_id {
1271   char name[32] ;
1272   char type[32] ;
1273   char compatible[128] ;
1274   void *data ;
1275};
1276#line 442 "include/linux/mod_devicetable.h"
1277struct spi_device_id {
1278   char name[32] ;
1279   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
1280};
1281#line 46 "include/linux/slub_def.h"
1282struct kmem_cache_cpu {
1283   void **freelist ;
1284   unsigned long tid ;
1285   struct page *page ;
1286   struct page *partial ;
1287   int node ;
1288   unsigned int stat[26] ;
1289};
1290#line 57 "include/linux/slub_def.h"
1291struct kmem_cache_node {
1292   spinlock_t list_lock ;
1293   unsigned long nr_partial ;
1294   struct list_head partial ;
1295   atomic_long_t nr_slabs ;
1296   atomic_long_t total_objects ;
1297   struct list_head full ;
1298};
1299#line 73 "include/linux/slub_def.h"
1300struct kmem_cache_order_objects {
1301   unsigned long x ;
1302};
1303#line 80 "include/linux/slub_def.h"
1304struct kmem_cache {
1305   struct kmem_cache_cpu *cpu_slab ;
1306   unsigned long flags ;
1307   unsigned long min_partial ;
1308   int size ;
1309   int objsize ;
1310   int offset ;
1311   int cpu_partial ;
1312   struct kmem_cache_order_objects oo ;
1313   struct kmem_cache_order_objects max ;
1314   struct kmem_cache_order_objects min ;
1315   gfp_t allocflags ;
1316   int refcount ;
1317   void (*ctor)(void * ) ;
1318   int inuse ;
1319   int align ;
1320   int reserved ;
1321   char const   *name ;
1322   struct list_head list ;
1323   struct kobject kobj ;
1324   int remote_node_defrag_ratio ;
1325   struct kmem_cache_node *node[1 << 10] ;
1326};
1327#line 18 "include/linux/capability.h"
1328struct task_struct;
1329#line 94 "include/linux/capability.h"
1330struct kernel_cap_struct {
1331   __u32 cap[2] ;
1332};
1333#line 94 "include/linux/capability.h"
1334typedef struct kernel_cap_struct kernel_cap_t;
1335#line 378
1336struct user_namespace;
1337#line 378
1338struct user_namespace;
1339#line 14 "include/linux/prio_tree.h"
1340struct prio_tree_node;
1341#line 14 "include/linux/prio_tree.h"
1342struct raw_prio_tree_node {
1343   struct prio_tree_node *left ;
1344   struct prio_tree_node *right ;
1345   struct prio_tree_node *parent ;
1346};
1347#line 20 "include/linux/prio_tree.h"
1348struct prio_tree_node {
1349   struct prio_tree_node *left ;
1350   struct prio_tree_node *right ;
1351   struct prio_tree_node *parent ;
1352   unsigned long start ;
1353   unsigned long last ;
1354};
1355#line 23 "include/linux/mm_types.h"
1356struct address_space;
1357#line 23
1358struct address_space;
1359#line 40 "include/linux/mm_types.h"
1360union __anonunion____missing_field_name_204 {
1361   unsigned long index ;
1362   void *freelist ;
1363};
1364#line 40 "include/linux/mm_types.h"
1365struct __anonstruct____missing_field_name_208 {
1366   unsigned int inuse : 16 ;
1367   unsigned int objects : 15 ;
1368   unsigned int frozen : 1 ;
1369};
1370#line 40 "include/linux/mm_types.h"
1371union __anonunion____missing_field_name_207 {
1372   atomic_t _mapcount ;
1373   struct __anonstruct____missing_field_name_208 __annonCompField34 ;
1374};
1375#line 40 "include/linux/mm_types.h"
1376struct __anonstruct____missing_field_name_206 {
1377   union __anonunion____missing_field_name_207 __annonCompField35 ;
1378   atomic_t _count ;
1379};
1380#line 40 "include/linux/mm_types.h"
1381union __anonunion____missing_field_name_205 {
1382   unsigned long counters ;
1383   struct __anonstruct____missing_field_name_206 __annonCompField36 ;
1384};
1385#line 40 "include/linux/mm_types.h"
1386struct __anonstruct____missing_field_name_203 {
1387   union __anonunion____missing_field_name_204 __annonCompField33 ;
1388   union __anonunion____missing_field_name_205 __annonCompField37 ;
1389};
1390#line 40 "include/linux/mm_types.h"
1391struct __anonstruct____missing_field_name_210 {
1392   struct page *next ;
1393   int pages ;
1394   int pobjects ;
1395};
1396#line 40 "include/linux/mm_types.h"
1397union __anonunion____missing_field_name_209 {
1398   struct list_head lru ;
1399   struct __anonstruct____missing_field_name_210 __annonCompField39 ;
1400};
1401#line 40 "include/linux/mm_types.h"
1402union __anonunion____missing_field_name_211 {
1403   unsigned long private ;
1404   struct kmem_cache *slab ;
1405   struct page *first_page ;
1406};
1407#line 40 "include/linux/mm_types.h"
1408struct page {
1409   unsigned long flags ;
1410   struct address_space *mapping ;
1411   struct __anonstruct____missing_field_name_203 __annonCompField38 ;
1412   union __anonunion____missing_field_name_209 __annonCompField40 ;
1413   union __anonunion____missing_field_name_211 __annonCompField41 ;
1414   unsigned long debug_flags ;
1415} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1416#line 200 "include/linux/mm_types.h"
1417struct __anonstruct_vm_set_213 {
1418   struct list_head list ;
1419   void *parent ;
1420   struct vm_area_struct *head ;
1421};
1422#line 200 "include/linux/mm_types.h"
1423union __anonunion_shared_212 {
1424   struct __anonstruct_vm_set_213 vm_set ;
1425   struct raw_prio_tree_node prio_tree_node ;
1426};
1427#line 200
1428struct anon_vma;
1429#line 200
1430struct vm_operations_struct;
1431#line 200
1432struct mempolicy;
1433#line 200 "include/linux/mm_types.h"
1434struct vm_area_struct {
1435   struct mm_struct *vm_mm ;
1436   unsigned long vm_start ;
1437   unsigned long vm_end ;
1438   struct vm_area_struct *vm_next ;
1439   struct vm_area_struct *vm_prev ;
1440   pgprot_t vm_page_prot ;
1441   unsigned long vm_flags ;
1442   struct rb_node vm_rb ;
1443   union __anonunion_shared_212 shared ;
1444   struct list_head anon_vma_chain ;
1445   struct anon_vma *anon_vma ;
1446   struct vm_operations_struct  const  *vm_ops ;
1447   unsigned long vm_pgoff ;
1448   struct file *vm_file ;
1449   void *vm_private_data ;
1450   struct mempolicy *vm_policy ;
1451};
1452#line 257 "include/linux/mm_types.h"
1453struct core_thread {
1454   struct task_struct *task ;
1455   struct core_thread *next ;
1456};
1457#line 262 "include/linux/mm_types.h"
1458struct core_state {
1459   atomic_t nr_threads ;
1460   struct core_thread dumper ;
1461   struct completion startup ;
1462};
1463#line 284 "include/linux/mm_types.h"
1464struct mm_rss_stat {
1465   atomic_long_t count[3] ;
1466};
1467#line 288
1468struct linux_binfmt;
1469#line 288
1470struct mmu_notifier_mm;
1471#line 288 "include/linux/mm_types.h"
1472struct mm_struct {
1473   struct vm_area_struct *mmap ;
1474   struct rb_root mm_rb ;
1475   struct vm_area_struct *mmap_cache ;
1476   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
1477                                      unsigned long pgoff , unsigned long flags ) ;
1478   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
1479   unsigned long mmap_base ;
1480   unsigned long task_size ;
1481   unsigned long cached_hole_size ;
1482   unsigned long free_area_cache ;
1483   pgd_t *pgd ;
1484   atomic_t mm_users ;
1485   atomic_t mm_count ;
1486   int map_count ;
1487   spinlock_t page_table_lock ;
1488   struct rw_semaphore mmap_sem ;
1489   struct list_head mmlist ;
1490   unsigned long hiwater_rss ;
1491   unsigned long hiwater_vm ;
1492   unsigned long total_vm ;
1493   unsigned long locked_vm ;
1494   unsigned long pinned_vm ;
1495   unsigned long shared_vm ;
1496   unsigned long exec_vm ;
1497   unsigned long stack_vm ;
1498   unsigned long reserved_vm ;
1499   unsigned long def_flags ;
1500   unsigned long nr_ptes ;
1501   unsigned long start_code ;
1502   unsigned long end_code ;
1503   unsigned long start_data ;
1504   unsigned long end_data ;
1505   unsigned long start_brk ;
1506   unsigned long brk ;
1507   unsigned long start_stack ;
1508   unsigned long arg_start ;
1509   unsigned long arg_end ;
1510   unsigned long env_start ;
1511   unsigned long env_end ;
1512   unsigned long saved_auxv[44] ;
1513   struct mm_rss_stat rss_stat ;
1514   struct linux_binfmt *binfmt ;
1515   cpumask_var_t cpu_vm_mask_var ;
1516   mm_context_t context ;
1517   unsigned int faultstamp ;
1518   unsigned int token_priority ;
1519   unsigned int last_interval ;
1520   unsigned long flags ;
1521   struct core_state *core_state ;
1522   spinlock_t ioctx_lock ;
1523   struct hlist_head ioctx_list ;
1524   struct task_struct *owner ;
1525   struct file *exe_file ;
1526   unsigned long num_exe_file_vmas ;
1527   struct mmu_notifier_mm *mmu_notifier_mm ;
1528   pgtable_t pmd_huge_pte ;
1529   struct cpumask cpumask_allocation ;
1530};
1531#line 7 "include/asm-generic/cputime.h"
1532typedef unsigned long cputime_t;
1533#line 84 "include/linux/sem.h"
1534struct task_struct;
1535#line 101
1536struct sem_undo_list;
1537#line 101 "include/linux/sem.h"
1538struct sysv_sem {
1539   struct sem_undo_list *undo_list ;
1540};
1541#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1542struct siginfo;
1543#line 10
1544struct siginfo;
1545#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1546struct __anonstruct_sigset_t_215 {
1547   unsigned long sig[1] ;
1548};
1549#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1550typedef struct __anonstruct_sigset_t_215 sigset_t;
1551#line 17 "include/asm-generic/signal-defs.h"
1552typedef void __signalfn_t(int  );
1553#line 18 "include/asm-generic/signal-defs.h"
1554typedef __signalfn_t *__sighandler_t;
1555#line 20 "include/asm-generic/signal-defs.h"
1556typedef void __restorefn_t(void);
1557#line 21 "include/asm-generic/signal-defs.h"
1558typedef __restorefn_t *__sigrestore_t;
1559#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1560struct sigaction {
1561   __sighandler_t sa_handler ;
1562   unsigned long sa_flags ;
1563   __sigrestore_t sa_restorer ;
1564   sigset_t sa_mask ;
1565};
1566#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1567struct k_sigaction {
1568   struct sigaction sa ;
1569};
1570#line 7 "include/asm-generic/siginfo.h"
1571union sigval {
1572   int sival_int ;
1573   void *sival_ptr ;
1574};
1575#line 7 "include/asm-generic/siginfo.h"
1576typedef union sigval sigval_t;
1577#line 48 "include/asm-generic/siginfo.h"
1578struct __anonstruct__kill_217 {
1579   __kernel_pid_t _pid ;
1580   __kernel_uid32_t _uid ;
1581};
1582#line 48 "include/asm-generic/siginfo.h"
1583struct __anonstruct__timer_218 {
1584   __kernel_timer_t _tid ;
1585   int _overrun ;
1586   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
1587   sigval_t _sigval ;
1588   int _sys_private ;
1589};
1590#line 48 "include/asm-generic/siginfo.h"
1591struct __anonstruct__rt_219 {
1592   __kernel_pid_t _pid ;
1593   __kernel_uid32_t _uid ;
1594   sigval_t _sigval ;
1595};
1596#line 48 "include/asm-generic/siginfo.h"
1597struct __anonstruct__sigchld_220 {
1598   __kernel_pid_t _pid ;
1599   __kernel_uid32_t _uid ;
1600   int _status ;
1601   __kernel_clock_t _utime ;
1602   __kernel_clock_t _stime ;
1603};
1604#line 48 "include/asm-generic/siginfo.h"
1605struct __anonstruct__sigfault_221 {
1606   void *_addr ;
1607   short _addr_lsb ;
1608};
1609#line 48 "include/asm-generic/siginfo.h"
1610struct __anonstruct__sigpoll_222 {
1611   long _band ;
1612   int _fd ;
1613};
1614#line 48 "include/asm-generic/siginfo.h"
1615union __anonunion__sifields_216 {
1616   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
1617   struct __anonstruct__kill_217 _kill ;
1618   struct __anonstruct__timer_218 _timer ;
1619   struct __anonstruct__rt_219 _rt ;
1620   struct __anonstruct__sigchld_220 _sigchld ;
1621   struct __anonstruct__sigfault_221 _sigfault ;
1622   struct __anonstruct__sigpoll_222 _sigpoll ;
1623};
1624#line 48 "include/asm-generic/siginfo.h"
1625struct siginfo {
1626   int si_signo ;
1627   int si_errno ;
1628   int si_code ;
1629   union __anonunion__sifields_216 _sifields ;
1630};
1631#line 48 "include/asm-generic/siginfo.h"
1632typedef struct siginfo siginfo_t;
1633#line 288
1634struct siginfo;
1635#line 10 "include/linux/signal.h"
1636struct task_struct;
1637#line 18
1638struct user_struct;
1639#line 28 "include/linux/signal.h"
1640struct sigpending {
1641   struct list_head list ;
1642   sigset_t signal ;
1643};
1644#line 239
1645struct timespec;
1646#line 240
1647struct pt_regs;
1648#line 50 "include/linux/pid.h"
1649struct pid_namespace;
1650#line 50 "include/linux/pid.h"
1651struct upid {
1652   int nr ;
1653   struct pid_namespace *ns ;
1654   struct hlist_node pid_chain ;
1655};
1656#line 57 "include/linux/pid.h"
1657struct pid {
1658   atomic_t count ;
1659   unsigned int level ;
1660   struct hlist_head tasks[3] ;
1661   struct rcu_head rcu ;
1662   struct upid numbers[1] ;
1663};
1664#line 69 "include/linux/pid.h"
1665struct pid_link {
1666   struct hlist_node node ;
1667   struct pid *pid ;
1668};
1669#line 100
1670struct pid_namespace;
1671#line 10 "include/linux/seccomp.h"
1672struct __anonstruct_seccomp_t_225 {
1673   int mode ;
1674};
1675#line 10 "include/linux/seccomp.h"
1676typedef struct __anonstruct_seccomp_t_225 seccomp_t;
1677#line 81 "include/linux/plist.h"
1678struct plist_head {
1679   struct list_head node_list ;
1680};
1681#line 85 "include/linux/plist.h"
1682struct plist_node {
1683   int prio ;
1684   struct list_head prio_list ;
1685   struct list_head node_list ;
1686};
1687#line 40 "include/linux/rtmutex.h"
1688struct rt_mutex_waiter;
1689#line 40
1690struct rt_mutex_waiter;
1691#line 42 "include/linux/resource.h"
1692struct rlimit {
1693   unsigned long rlim_cur ;
1694   unsigned long rlim_max ;
1695};
1696#line 81
1697struct task_struct;
1698#line 8 "include/linux/timerqueue.h"
1699struct timerqueue_node {
1700   struct rb_node node ;
1701   ktime_t expires ;
1702};
1703#line 13 "include/linux/timerqueue.h"
1704struct timerqueue_head {
1705   struct rb_root head ;
1706   struct timerqueue_node *next ;
1707};
1708#line 27 "include/linux/hrtimer.h"
1709struct hrtimer_clock_base;
1710#line 27
1711struct hrtimer_clock_base;
1712#line 28
1713struct hrtimer_cpu_base;
1714#line 28
1715struct hrtimer_cpu_base;
1716#line 44
1717enum hrtimer_restart {
1718    HRTIMER_NORESTART = 0,
1719    HRTIMER_RESTART = 1
1720} ;
1721#line 108 "include/linux/hrtimer.h"
1722struct hrtimer {
1723   struct timerqueue_node node ;
1724   ktime_t _softexpires ;
1725   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1726   struct hrtimer_clock_base *base ;
1727   unsigned long state ;
1728   int start_pid ;
1729   void *start_site ;
1730   char start_comm[16] ;
1731};
1732#line 145 "include/linux/hrtimer.h"
1733struct hrtimer_clock_base {
1734   struct hrtimer_cpu_base *cpu_base ;
1735   int index ;
1736   clockid_t clockid ;
1737   struct timerqueue_head active ;
1738   ktime_t resolution ;
1739   ktime_t (*get_time)(void) ;
1740   ktime_t softirq_time ;
1741   ktime_t offset ;
1742};
1743#line 178 "include/linux/hrtimer.h"
1744struct hrtimer_cpu_base {
1745   raw_spinlock_t lock ;
1746   unsigned long active_bases ;
1747   ktime_t expires_next ;
1748   int hres_active ;
1749   int hang_detected ;
1750   unsigned long nr_events ;
1751   unsigned long nr_retries ;
1752   unsigned long nr_hangs ;
1753   ktime_t max_hang_time ;
1754   struct hrtimer_clock_base clock_base[3] ;
1755};
1756#line 11 "include/linux/task_io_accounting.h"
1757struct task_io_accounting {
1758   u64 rchar ;
1759   u64 wchar ;
1760   u64 syscr ;
1761   u64 syscw ;
1762   u64 read_bytes ;
1763   u64 write_bytes ;
1764   u64 cancelled_write_bytes ;
1765};
1766#line 13 "include/linux/latencytop.h"
1767struct task_struct;
1768#line 20 "include/linux/latencytop.h"
1769struct latency_record {
1770   unsigned long backtrace[12] ;
1771   unsigned int count ;
1772   unsigned long time ;
1773   unsigned long max ;
1774};
1775#line 29 "include/linux/key.h"
1776typedef int32_t key_serial_t;
1777#line 32 "include/linux/key.h"
1778typedef uint32_t key_perm_t;
1779#line 34
1780struct key;
1781#line 34
1782struct key;
1783#line 75
1784struct user_struct;
1785#line 76
1786struct signal_struct;
1787#line 76
1788struct signal_struct;
1789#line 77
1790struct cred;
1791#line 79
1792struct key_type;
1793#line 79
1794struct key_type;
1795#line 81
1796struct keyring_list;
1797#line 81
1798struct keyring_list;
1799#line 124
1800struct key_user;
1801#line 124 "include/linux/key.h"
1802union __anonunion____missing_field_name_226 {
1803   time_t expiry ;
1804   time_t revoked_at ;
1805};
1806#line 124 "include/linux/key.h"
1807union __anonunion_type_data_227 {
1808   struct list_head link ;
1809   unsigned long x[2] ;
1810   void *p[2] ;
1811   int reject_error ;
1812};
1813#line 124 "include/linux/key.h"
1814union __anonunion_payload_228 {
1815   unsigned long value ;
1816   void *rcudata ;
1817   void *data ;
1818   struct keyring_list *subscriptions ;
1819};
1820#line 124 "include/linux/key.h"
1821struct key {
1822   atomic_t usage ;
1823   key_serial_t serial ;
1824   struct rb_node serial_node ;
1825   struct key_type *type ;
1826   struct rw_semaphore sem ;
1827   struct key_user *user ;
1828   void *security ;
1829   union __anonunion____missing_field_name_226 __annonCompField42 ;
1830   uid_t uid ;
1831   gid_t gid ;
1832   key_perm_t perm ;
1833   unsigned short quotalen ;
1834   unsigned short datalen ;
1835   unsigned long flags ;
1836   char *description ;
1837   union __anonunion_type_data_227 type_data ;
1838   union __anonunion_payload_228 payload ;
1839};
1840#line 18 "include/linux/selinux.h"
1841struct audit_context;
1842#line 18
1843struct audit_context;
1844#line 21 "include/linux/cred.h"
1845struct user_struct;
1846#line 22
1847struct cred;
1848#line 31 "include/linux/cred.h"
1849struct group_info {
1850   atomic_t usage ;
1851   int ngroups ;
1852   int nblocks ;
1853   gid_t small_block[32] ;
1854   gid_t *blocks[0] ;
1855};
1856#line 83 "include/linux/cred.h"
1857struct thread_group_cred {
1858   atomic_t usage ;
1859   pid_t tgid ;
1860   spinlock_t lock ;
1861   struct key *session_keyring ;
1862   struct key *process_keyring ;
1863   struct rcu_head rcu ;
1864};
1865#line 116 "include/linux/cred.h"
1866struct cred {
1867   atomic_t usage ;
1868   atomic_t subscribers ;
1869   void *put_addr ;
1870   unsigned int magic ;
1871   uid_t uid ;
1872   gid_t gid ;
1873   uid_t suid ;
1874   gid_t sgid ;
1875   uid_t euid ;
1876   gid_t egid ;
1877   uid_t fsuid ;
1878   gid_t fsgid ;
1879   unsigned int securebits ;
1880   kernel_cap_t cap_inheritable ;
1881   kernel_cap_t cap_permitted ;
1882   kernel_cap_t cap_effective ;
1883   kernel_cap_t cap_bset ;
1884   unsigned char jit_keyring ;
1885   struct key *thread_keyring ;
1886   struct key *request_key_auth ;
1887   struct thread_group_cred *tgcred ;
1888   void *security ;
1889   struct user_struct *user ;
1890   struct user_namespace *user_ns ;
1891   struct group_info *group_info ;
1892   struct rcu_head rcu ;
1893};
1894#line 61 "include/linux/llist.h"
1895struct llist_node;
1896#line 65 "include/linux/llist.h"
1897struct llist_node {
1898   struct llist_node *next ;
1899};
1900#line 97 "include/linux/sched.h"
1901struct futex_pi_state;
1902#line 97
1903struct futex_pi_state;
1904#line 98
1905struct robust_list_head;
1906#line 98
1907struct robust_list_head;
1908#line 99
1909struct bio_list;
1910#line 99
1911struct bio_list;
1912#line 100
1913struct fs_struct;
1914#line 100
1915struct fs_struct;
1916#line 101
1917struct perf_event_context;
1918#line 101
1919struct perf_event_context;
1920#line 102
1921struct blk_plug;
1922#line 102
1923struct blk_plug;
1924#line 151
1925struct cfs_rq;
1926#line 151
1927struct cfs_rq;
1928#line 259
1929struct task_struct;
1930#line 366
1931struct nsproxy;
1932#line 367
1933struct user_namespace;
1934#line 214 "include/linux/aio.h"
1935struct mm_struct;
1936#line 443 "include/linux/sched.h"
1937struct sighand_struct {
1938   atomic_t count ;
1939   struct k_sigaction action[64] ;
1940   spinlock_t siglock ;
1941   wait_queue_head_t signalfd_wqh ;
1942};
1943#line 450 "include/linux/sched.h"
1944struct pacct_struct {
1945   int ac_flag ;
1946   long ac_exitcode ;
1947   unsigned long ac_mem ;
1948   cputime_t ac_utime ;
1949   cputime_t ac_stime ;
1950   unsigned long ac_minflt ;
1951   unsigned long ac_majflt ;
1952};
1953#line 458 "include/linux/sched.h"
1954struct cpu_itimer {
1955   cputime_t expires ;
1956   cputime_t incr ;
1957   u32 error ;
1958   u32 incr_error ;
1959};
1960#line 476 "include/linux/sched.h"
1961struct task_cputime {
1962   cputime_t utime ;
1963   cputime_t stime ;
1964   unsigned long long sum_exec_runtime ;
1965};
1966#line 512 "include/linux/sched.h"
1967struct thread_group_cputimer {
1968   struct task_cputime cputime ;
1969   int running ;
1970   raw_spinlock_t lock ;
1971};
1972#line 519
1973struct autogroup;
1974#line 519
1975struct autogroup;
1976#line 528
1977struct tty_struct;
1978#line 528
1979struct taskstats;
1980#line 528
1981struct tty_audit_buf;
1982#line 528 "include/linux/sched.h"
1983struct signal_struct {
1984   atomic_t sigcnt ;
1985   atomic_t live ;
1986   int nr_threads ;
1987   wait_queue_head_t wait_chldexit ;
1988   struct task_struct *curr_target ;
1989   struct sigpending shared_pending ;
1990   int group_exit_code ;
1991   int notify_count ;
1992   struct task_struct *group_exit_task ;
1993   int group_stop_count ;
1994   unsigned int flags ;
1995   unsigned int is_child_subreaper : 1 ;
1996   unsigned int has_child_subreaper : 1 ;
1997   struct list_head posix_timers ;
1998   struct hrtimer real_timer ;
1999   struct pid *leader_pid ;
2000   ktime_t it_real_incr ;
2001   struct cpu_itimer it[2] ;
2002   struct thread_group_cputimer cputimer ;
2003   struct task_cputime cputime_expires ;
2004   struct list_head cpu_timers[3] ;
2005   struct pid *tty_old_pgrp ;
2006   int leader ;
2007   struct tty_struct *tty ;
2008   struct autogroup *autogroup ;
2009   cputime_t utime ;
2010   cputime_t stime ;
2011   cputime_t cutime ;
2012   cputime_t cstime ;
2013   cputime_t gtime ;
2014   cputime_t cgtime ;
2015   cputime_t prev_utime ;
2016   cputime_t prev_stime ;
2017   unsigned long nvcsw ;
2018   unsigned long nivcsw ;
2019   unsigned long cnvcsw ;
2020   unsigned long cnivcsw ;
2021   unsigned long min_flt ;
2022   unsigned long maj_flt ;
2023   unsigned long cmin_flt ;
2024   unsigned long cmaj_flt ;
2025   unsigned long inblock ;
2026   unsigned long oublock ;
2027   unsigned long cinblock ;
2028   unsigned long coublock ;
2029   unsigned long maxrss ;
2030   unsigned long cmaxrss ;
2031   struct task_io_accounting ioac ;
2032   unsigned long long sum_sched_runtime ;
2033   struct rlimit rlim[16] ;
2034   struct pacct_struct pacct ;
2035   struct taskstats *stats ;
2036   unsigned int audit_tty ;
2037   struct tty_audit_buf *tty_audit_buf ;
2038   struct rw_semaphore group_rwsem ;
2039   int oom_adj ;
2040   int oom_score_adj ;
2041   int oom_score_adj_min ;
2042   struct mutex cred_guard_mutex ;
2043};
2044#line 703 "include/linux/sched.h"
2045struct user_struct {
2046   atomic_t __count ;
2047   atomic_t processes ;
2048   atomic_t files ;
2049   atomic_t sigpending ;
2050   atomic_t inotify_watches ;
2051   atomic_t inotify_devs ;
2052   atomic_t fanotify_listeners ;
2053   atomic_long_t epoll_watches ;
2054   unsigned long mq_bytes ;
2055   unsigned long locked_shm ;
2056   struct key *uid_keyring ;
2057   struct key *session_keyring ;
2058   struct hlist_node uidhash_node ;
2059   uid_t uid ;
2060   struct user_namespace *user_ns ;
2061   atomic_long_t locked_vm ;
2062};
2063#line 747
2064struct backing_dev_info;
2065#line 747
2066struct backing_dev_info;
2067#line 748
2068struct reclaim_state;
2069#line 748
2070struct reclaim_state;
2071#line 751 "include/linux/sched.h"
2072struct sched_info {
2073   unsigned long pcount ;
2074   unsigned long long run_delay ;
2075   unsigned long long last_arrival ;
2076   unsigned long long last_queued ;
2077};
2078#line 763 "include/linux/sched.h"
2079struct task_delay_info {
2080   spinlock_t lock ;
2081   unsigned int flags ;
2082   struct timespec blkio_start ;
2083   struct timespec blkio_end ;
2084   u64 blkio_delay ;
2085   u64 swapin_delay ;
2086   u32 blkio_count ;
2087   u32 swapin_count ;
2088   struct timespec freepages_start ;
2089   struct timespec freepages_end ;
2090   u64 freepages_delay ;
2091   u32 freepages_count ;
2092};
2093#line 1088
2094struct io_context;
2095#line 1088
2096struct io_context;
2097#line 1097
2098struct audit_context;
2099#line 1098
2100struct mempolicy;
2101#line 1099
2102struct pipe_inode_info;
2103#line 1099
2104struct pipe_inode_info;
2105#line 1102
2106struct rq;
2107#line 1102
2108struct rq;
2109#line 1122 "include/linux/sched.h"
2110struct sched_class {
2111   struct sched_class  const  *next ;
2112   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2113   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2114   void (*yield_task)(struct rq *rq ) ;
2115   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
2116   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
2117   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
2118   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
2119   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
2120   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
2121   void (*post_schedule)(struct rq *this_rq ) ;
2122   void (*task_waking)(struct task_struct *task ) ;
2123   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
2124   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
2125   void (*rq_online)(struct rq *rq ) ;
2126   void (*rq_offline)(struct rq *rq ) ;
2127   void (*set_curr_task)(struct rq *rq ) ;
2128   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
2129   void (*task_fork)(struct task_struct *p ) ;
2130   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
2131   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
2132   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
2133   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
2134   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
2135};
2136#line 1167 "include/linux/sched.h"
2137struct load_weight {
2138   unsigned long weight ;
2139   unsigned long inv_weight ;
2140};
2141#line 1172 "include/linux/sched.h"
2142struct sched_statistics {
2143   u64 wait_start ;
2144   u64 wait_max ;
2145   u64 wait_count ;
2146   u64 wait_sum ;
2147   u64 iowait_count ;
2148   u64 iowait_sum ;
2149   u64 sleep_start ;
2150   u64 sleep_max ;
2151   s64 sum_sleep_runtime ;
2152   u64 block_start ;
2153   u64 block_max ;
2154   u64 exec_max ;
2155   u64 slice_max ;
2156   u64 nr_migrations_cold ;
2157   u64 nr_failed_migrations_affine ;
2158   u64 nr_failed_migrations_running ;
2159   u64 nr_failed_migrations_hot ;
2160   u64 nr_forced_migrations ;
2161   u64 nr_wakeups ;
2162   u64 nr_wakeups_sync ;
2163   u64 nr_wakeups_migrate ;
2164   u64 nr_wakeups_local ;
2165   u64 nr_wakeups_remote ;
2166   u64 nr_wakeups_affine ;
2167   u64 nr_wakeups_affine_attempts ;
2168   u64 nr_wakeups_passive ;
2169   u64 nr_wakeups_idle ;
2170};
2171#line 1207 "include/linux/sched.h"
2172struct sched_entity {
2173   struct load_weight load ;
2174   struct rb_node run_node ;
2175   struct list_head group_node ;
2176   unsigned int on_rq ;
2177   u64 exec_start ;
2178   u64 sum_exec_runtime ;
2179   u64 vruntime ;
2180   u64 prev_sum_exec_runtime ;
2181   u64 nr_migrations ;
2182   struct sched_statistics statistics ;
2183   struct sched_entity *parent ;
2184   struct cfs_rq *cfs_rq ;
2185   struct cfs_rq *my_q ;
2186};
2187#line 1233
2188struct rt_rq;
2189#line 1233 "include/linux/sched.h"
2190struct sched_rt_entity {
2191   struct list_head run_list ;
2192   unsigned long timeout ;
2193   unsigned int time_slice ;
2194   int nr_cpus_allowed ;
2195   struct sched_rt_entity *back ;
2196   struct sched_rt_entity *parent ;
2197   struct rt_rq *rt_rq ;
2198   struct rt_rq *my_q ;
2199};
2200#line 1264
2201struct files_struct;
2202#line 1264
2203struct css_set;
2204#line 1264
2205struct compat_robust_list_head;
2206#line 1264
2207struct mem_cgroup;
2208#line 1264 "include/linux/sched.h"
2209struct memcg_batch_info {
2210   int do_batch ;
2211   struct mem_cgroup *memcg ;
2212   unsigned long nr_pages ;
2213   unsigned long memsw_nr_pages ;
2214};
2215#line 1264 "include/linux/sched.h"
2216struct task_struct {
2217   long volatile   state ;
2218   void *stack ;
2219   atomic_t usage ;
2220   unsigned int flags ;
2221   unsigned int ptrace ;
2222   struct llist_node wake_entry ;
2223   int on_cpu ;
2224   int on_rq ;
2225   int prio ;
2226   int static_prio ;
2227   int normal_prio ;
2228   unsigned int rt_priority ;
2229   struct sched_class  const  *sched_class ;
2230   struct sched_entity se ;
2231   struct sched_rt_entity rt ;
2232   struct hlist_head preempt_notifiers ;
2233   unsigned char fpu_counter ;
2234   unsigned int policy ;
2235   cpumask_t cpus_allowed ;
2236   struct sched_info sched_info ;
2237   struct list_head tasks ;
2238   struct plist_node pushable_tasks ;
2239   struct mm_struct *mm ;
2240   struct mm_struct *active_mm ;
2241   unsigned int brk_randomized : 1 ;
2242   int exit_state ;
2243   int exit_code ;
2244   int exit_signal ;
2245   int pdeath_signal ;
2246   unsigned int jobctl ;
2247   unsigned int personality ;
2248   unsigned int did_exec : 1 ;
2249   unsigned int in_execve : 1 ;
2250   unsigned int in_iowait : 1 ;
2251   unsigned int sched_reset_on_fork : 1 ;
2252   unsigned int sched_contributes_to_load : 1 ;
2253   unsigned int irq_thread : 1 ;
2254   pid_t pid ;
2255   pid_t tgid ;
2256   unsigned long stack_canary ;
2257   struct task_struct *real_parent ;
2258   struct task_struct *parent ;
2259   struct list_head children ;
2260   struct list_head sibling ;
2261   struct task_struct *group_leader ;
2262   struct list_head ptraced ;
2263   struct list_head ptrace_entry ;
2264   struct pid_link pids[3] ;
2265   struct list_head thread_group ;
2266   struct completion *vfork_done ;
2267   int *set_child_tid ;
2268   int *clear_child_tid ;
2269   cputime_t utime ;
2270   cputime_t stime ;
2271   cputime_t utimescaled ;
2272   cputime_t stimescaled ;
2273   cputime_t gtime ;
2274   cputime_t prev_utime ;
2275   cputime_t prev_stime ;
2276   unsigned long nvcsw ;
2277   unsigned long nivcsw ;
2278   struct timespec start_time ;
2279   struct timespec real_start_time ;
2280   unsigned long min_flt ;
2281   unsigned long maj_flt ;
2282   struct task_cputime cputime_expires ;
2283   struct list_head cpu_timers[3] ;
2284   struct cred  const  *real_cred ;
2285   struct cred  const  *cred ;
2286   struct cred *replacement_session_keyring ;
2287   char comm[16] ;
2288   int link_count ;
2289   int total_link_count ;
2290   struct sysv_sem sysvsem ;
2291   unsigned long last_switch_count ;
2292   struct thread_struct thread ;
2293   struct fs_struct *fs ;
2294   struct files_struct *files ;
2295   struct nsproxy *nsproxy ;
2296   struct signal_struct *signal ;
2297   struct sighand_struct *sighand ;
2298   sigset_t blocked ;
2299   sigset_t real_blocked ;
2300   sigset_t saved_sigmask ;
2301   struct sigpending pending ;
2302   unsigned long sas_ss_sp ;
2303   size_t sas_ss_size ;
2304   int (*notifier)(void *priv ) ;
2305   void *notifier_data ;
2306   sigset_t *notifier_mask ;
2307   struct audit_context *audit_context ;
2308   uid_t loginuid ;
2309   unsigned int sessionid ;
2310   seccomp_t seccomp ;
2311   u32 parent_exec_id ;
2312   u32 self_exec_id ;
2313   spinlock_t alloc_lock ;
2314   raw_spinlock_t pi_lock ;
2315   struct plist_head pi_waiters ;
2316   struct rt_mutex_waiter *pi_blocked_on ;
2317   struct mutex_waiter *blocked_on ;
2318   unsigned int irq_events ;
2319   unsigned long hardirq_enable_ip ;
2320   unsigned long hardirq_disable_ip ;
2321   unsigned int hardirq_enable_event ;
2322   unsigned int hardirq_disable_event ;
2323   int hardirqs_enabled ;
2324   int hardirq_context ;
2325   unsigned long softirq_disable_ip ;
2326   unsigned long softirq_enable_ip ;
2327   unsigned int softirq_disable_event ;
2328   unsigned int softirq_enable_event ;
2329   int softirqs_enabled ;
2330   int softirq_context ;
2331   void *journal_info ;
2332   struct bio_list *bio_list ;
2333   struct blk_plug *plug ;
2334   struct reclaim_state *reclaim_state ;
2335   struct backing_dev_info *backing_dev_info ;
2336   struct io_context *io_context ;
2337   unsigned long ptrace_message ;
2338   siginfo_t *last_siginfo ;
2339   struct task_io_accounting ioac ;
2340   u64 acct_rss_mem1 ;
2341   u64 acct_vm_mem1 ;
2342   cputime_t acct_timexpd ;
2343   nodemask_t mems_allowed ;
2344   seqcount_t mems_allowed_seq ;
2345   int cpuset_mem_spread_rotor ;
2346   int cpuset_slab_spread_rotor ;
2347   struct css_set *cgroups ;
2348   struct list_head cg_list ;
2349   struct robust_list_head *robust_list ;
2350   struct compat_robust_list_head *compat_robust_list ;
2351   struct list_head pi_state_list ;
2352   struct futex_pi_state *pi_state_cache ;
2353   struct perf_event_context *perf_event_ctxp[2] ;
2354   struct mutex perf_event_mutex ;
2355   struct list_head perf_event_list ;
2356   struct mempolicy *mempolicy ;
2357   short il_next ;
2358   short pref_node_fork ;
2359   struct rcu_head rcu ;
2360   struct pipe_inode_info *splice_pipe ;
2361   struct task_delay_info *delays ;
2362   int make_it_fail ;
2363   int nr_dirtied ;
2364   int nr_dirtied_pause ;
2365   unsigned long dirty_paused_when ;
2366   int latency_record_count ;
2367   struct latency_record latency_record[32] ;
2368   unsigned long timer_slack_ns ;
2369   unsigned long default_timer_slack_ns ;
2370   struct list_head *scm_work_list ;
2371   unsigned long trace ;
2372   unsigned long trace_recursion ;
2373   struct memcg_batch_info memcg_batch ;
2374   atomic_t ptrace_bp_refcnt ;
2375};
2376#line 1681
2377struct pid_namespace;
2378#line 55 "include/linux/kthread.h"
2379struct kthread_work;
2380#line 55
2381struct kthread_work;
2382#line 58 "include/linux/kthread.h"
2383struct kthread_worker {
2384   spinlock_t lock ;
2385   struct list_head work_list ;
2386   struct task_struct *task ;
2387};
2388#line 64 "include/linux/kthread.h"
2389struct kthread_work {
2390   struct list_head node ;
2391   void (*func)(struct kthread_work *work ) ;
2392   wait_queue_head_t done ;
2393   atomic_t flushing ;
2394   int queue_seq ;
2395   int done_seq ;
2396};
2397#line 70 "include/linux/spi/spi.h"
2398struct spi_master;
2399#line 70 "include/linux/spi/spi.h"
2400struct spi_device {
2401   struct device dev ;
2402   struct spi_master *master ;
2403   u32 max_speed_hz ;
2404   u8 chip_select ;
2405   u8 mode ;
2406   u8 bits_per_word ;
2407   int irq ;
2408   void *controller_state ;
2409   void *controller_data ;
2410   char modalias[32] ;
2411};
2412#line 145
2413struct spi_message;
2414#line 145
2415struct spi_message;
2416#line 176 "include/linux/spi/spi.h"
2417struct spi_driver {
2418   struct spi_device_id  const  *id_table ;
2419   int (*probe)(struct spi_device *spi ) ;
2420   int (*remove)(struct spi_device *spi ) ;
2421   void (*shutdown)(struct spi_device *spi ) ;
2422   int (*suspend)(struct spi_device *spi , pm_message_t mesg ) ;
2423   int (*resume)(struct spi_device *spi ) ;
2424   struct device_driver driver ;
2425};
2426#line 272 "include/linux/spi/spi.h"
2427struct spi_master {
2428   struct device dev ;
2429   struct list_head list ;
2430   s16 bus_num ;
2431   u16 num_chipselect ;
2432   u16 dma_alignment ;
2433   u16 mode_bits ;
2434   u16 flags ;
2435   spinlock_t bus_lock_spinlock ;
2436   struct mutex bus_lock_mutex ;
2437   bool bus_lock_flag ;
2438   int (*setup)(struct spi_device *spi ) ;
2439   int (*transfer)(struct spi_device *spi , struct spi_message *mesg ) ;
2440   void (*cleanup)(struct spi_device *spi ) ;
2441   bool queued ;
2442   struct kthread_worker kworker ;
2443   struct task_struct *kworker_task ;
2444   struct kthread_work pump_messages ;
2445   spinlock_t queue_lock ;
2446   struct list_head queue ;
2447   struct spi_message *cur_msg ;
2448   bool busy ;
2449   bool running ;
2450   bool rt ;
2451   int (*prepare_transfer_hardware)(struct spi_master *master ) ;
2452   int (*transfer_one_message)(struct spi_master *master , struct spi_message *mesg ) ;
2453   int (*unprepare_transfer_hardware)(struct spi_master *master ) ;
2454};
2455#line 492 "include/linux/spi/spi.h"
2456struct spi_transfer {
2457   void const   *tx_buf ;
2458   void *rx_buf ;
2459   unsigned int len ;
2460   dma_addr_t tx_dma ;
2461   dma_addr_t rx_dma ;
2462   unsigned int cs_change : 1 ;
2463   u8 bits_per_word ;
2464   u16 delay_usecs ;
2465   u32 speed_hz ;
2466   struct list_head transfer_list ;
2467};
2468#line 541 "include/linux/spi/spi.h"
2469struct spi_message {
2470   struct list_head transfers ;
2471   struct spi_device *spi ;
2472   unsigned int is_dma_mapped : 1 ;
2473   void (*complete)(void *context ) ;
2474   void *context ;
2475   unsigned int actual_length ;
2476   int status ;
2477   struct list_head queue ;
2478   void *state ;
2479};
2480#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
2481struct max1111_data {
2482   struct spi_device *spi ;
2483   struct device *hwmon_dev ;
2484   struct spi_message msg ;
2485   struct spi_transfer xfer[2] ;
2486   uint8_t tx_buf[1] ;
2487   uint8_t rx_buf[2] ;
2488   struct mutex drvdata_lock ;
2489};
2490#line 1 "<compiler builtins>"
2491long __builtin_expect(long val , long res ) ;
2492#line 24 "include/linux/list.h"
2493__inline static void INIT_LIST_HEAD(struct list_head *list )  __attribute__((__no_instrument_function__)) ;
2494#line 24 "include/linux/list.h"
2495__inline static void INIT_LIST_HEAD(struct list_head *list ) 
2496{ unsigned long __cil_tmp2 ;
2497  unsigned long __cil_tmp3 ;
2498
2499  {
2500#line 26
2501  *((struct list_head **)list) = list;
2502#line 27
2503  __cil_tmp2 = (unsigned long )list;
2504#line 27
2505  __cil_tmp3 = __cil_tmp2 + 8;
2506#line 27
2507  *((struct list_head **)__cil_tmp3) = list;
2508#line 28
2509  return;
2510}
2511}
2512#line 47
2513extern void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next ) ;
2514#line 74
2515__inline static void list_add_tail(struct list_head *new , struct list_head *head )  __attribute__((__no_instrument_function__)) ;
2516#line 74 "include/linux/list.h"
2517__inline static void list_add_tail(struct list_head *new , struct list_head *head ) 
2518{ unsigned long __cil_tmp3 ;
2519  unsigned long __cil_tmp4 ;
2520  struct list_head *__cil_tmp5 ;
2521
2522  {
2523  {
2524#line 76
2525  __cil_tmp3 = (unsigned long )head;
2526#line 76
2527  __cil_tmp4 = __cil_tmp3 + 8;
2528#line 76
2529  __cil_tmp5 = *((struct list_head **)__cil_tmp4);
2530#line 76
2531  __list_add(new, __cil_tmp5, head);
2532  }
2533#line 77
2534  return;
2535}
2536}
2537#line 320 "include/linux/kernel.h"
2538extern int ( /* format attribute */  sprintf)(char *buf , char const   *fmt  , ...) ;
2539#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
2540extern void *memset(void *s , int c , size_t n ) ;
2541#line 27 "include/linux/err.h"
2542__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
2543#line 27 "include/linux/err.h"
2544__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr ) 
2545{ 
2546
2547  {
2548#line 29
2549  return ((long )ptr);
2550}
2551}
2552#line 32
2553__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
2554#line 32 "include/linux/err.h"
2555__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr ) 
2556{ long tmp ;
2557  unsigned long __cil_tmp3 ;
2558  int __cil_tmp4 ;
2559  int __cil_tmp5 ;
2560  int __cil_tmp6 ;
2561  long __cil_tmp7 ;
2562
2563  {
2564  {
2565#line 34
2566  __cil_tmp3 = (unsigned long )ptr;
2567#line 34
2568  __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
2569#line 34
2570  __cil_tmp5 = ! __cil_tmp4;
2571#line 34
2572  __cil_tmp6 = ! __cil_tmp5;
2573#line 34
2574  __cil_tmp7 = (long )__cil_tmp6;
2575#line 34
2576  tmp = __builtin_expect(__cil_tmp7, 0L);
2577  }
2578#line 34
2579  return (tmp);
2580}
2581}
2582#line 21 "include/linux/mutex-debug.h"
2583extern void mutex_destroy(struct mutex *lock ) ;
2584#line 115 "include/linux/mutex.h"
2585extern void __mutex_init(struct mutex *lock , char const   *name , struct lock_class_key *key ) ;
2586#line 152
2587void mutex_lock(struct mutex *lock ) ;
2588#line 153
2589int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2590#line 154
2591int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2592#line 168
2593int mutex_trylock(struct mutex *lock ) ;
2594#line 169
2595void mutex_unlock(struct mutex *lock ) ;
2596#line 170
2597int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2598#line 158 "include/linux/sysfs.h"
2599extern int __attribute__((__warn_unused_result__))  sysfs_create_group(struct kobject *kobj ,
2600                                                                       struct attribute_group  const  *grp ) ;
2601#line 162
2602extern void sysfs_remove_group(struct kobject *kobj , struct attribute_group  const  *grp ) ;
2603#line 26 "include/linux/export.h"
2604extern struct module __this_module ;
2605#line 67 "include/linux/module.h"
2606int init_module(void) ;
2607#line 68
2608void cleanup_module(void) ;
2609#line 19 "include/linux/hwmon.h"
2610extern struct device *hwmon_device_register(struct device *dev ) ;
2611#line 21
2612extern void hwmon_device_unregister(struct device *dev ) ;
2613#line 239 "include/linux/device.h"
2614extern void driver_unregister(struct device_driver *drv ) ;
2615#line 792
2616extern void *dev_get_drvdata(struct device  const  *dev ) ;
2617#line 793
2618extern int dev_set_drvdata(struct device *dev , void *data ) ;
2619#line 891
2620extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
2621                                              , ...) ;
2622#line 161 "include/linux/slab.h"
2623extern void kfree(void const   * ) ;
2624#line 221 "include/linux/slub_def.h"
2625extern void *__kmalloc(size_t size , gfp_t flags ) ;
2626#line 268
2627__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2628                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2629#line 268 "include/linux/slub_def.h"
2630__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2631                                                                    gfp_t flags ) 
2632{ void *tmp___2 ;
2633
2634  {
2635  {
2636#line 283
2637  tmp___2 = __kmalloc(size, flags);
2638  }
2639#line 283
2640  return (tmp___2);
2641}
2642}
2643#line 349 "include/linux/slab.h"
2644__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2645#line 349 "include/linux/slab.h"
2646__inline static void *kzalloc(size_t size , gfp_t flags ) 
2647{ void *tmp ;
2648  unsigned int __cil_tmp4 ;
2649
2650  {
2651  {
2652#line 351
2653  __cil_tmp4 = flags | 32768U;
2654#line 351
2655  tmp = kmalloc(size, __cil_tmp4);
2656  }
2657#line 351
2658  return (tmp);
2659}
2660}
2661#line 135 "include/linux/spi/spi.h"
2662__inline static void spi_set_drvdata(struct spi_device *spi , void *data )  __attribute__((__no_instrument_function__)) ;
2663#line 135 "include/linux/spi/spi.h"
2664__inline static void spi_set_drvdata(struct spi_device *spi , void *data ) 
2665{ struct device *__cil_tmp3 ;
2666
2667  {
2668  {
2669#line 137
2670  __cil_tmp3 = (struct device *)spi;
2671#line 137
2672  dev_set_drvdata(__cil_tmp3, data);
2673  }
2674#line 138
2675  return;
2676}
2677}
2678#line 140
2679__inline static void *spi_get_drvdata(struct spi_device *spi )  __attribute__((__no_instrument_function__)) ;
2680#line 140 "include/linux/spi/spi.h"
2681__inline static void *spi_get_drvdata(struct spi_device *spi ) 
2682{ void *tmp___7 ;
2683  struct device *__cil_tmp3 ;
2684  struct device  const  *__cil_tmp4 ;
2685
2686  {
2687  {
2688#line 142
2689  __cil_tmp3 = (struct device *)spi;
2690#line 142
2691  __cil_tmp4 = (struct device  const  *)__cil_tmp3;
2692#line 142
2693  tmp___7 = dev_get_drvdata(__cil_tmp4);
2694  }
2695#line 142
2696  return (tmp___7);
2697}
2698}
2699#line 191
2700extern int spi_register_driver(struct spi_driver *sdrv ) ;
2701#line 198
2702__inline static void spi_unregister_driver(struct spi_driver *sdrv )  __attribute__((__no_instrument_function__)) ;
2703#line 198 "include/linux/spi/spi.h"
2704__inline static void spi_unregister_driver(struct spi_driver *sdrv ) 
2705{ unsigned long __cil_tmp2 ;
2706  unsigned long __cil_tmp3 ;
2707  struct device_driver *__cil_tmp4 ;
2708
2709  {
2710#line 200
2711  if (sdrv) {
2712    {
2713#line 201
2714    __cil_tmp2 = (unsigned long )sdrv;
2715#line 201
2716    __cil_tmp3 = __cil_tmp2 + 48;
2717#line 201
2718    __cil_tmp4 = (struct device_driver *)__cil_tmp3;
2719#line 201
2720    driver_unregister(__cil_tmp4);
2721    }
2722  } else {
2723
2724  }
2725#line 202
2726  return;
2727}
2728}
2729#line 573
2730__inline static void spi_message_init(struct spi_message *m )  __attribute__((__no_instrument_function__)) ;
2731#line 573 "include/linux/spi/spi.h"
2732__inline static void spi_message_init(struct spi_message *m ) 
2733{ void *__cil_tmp2 ;
2734  struct list_head *__cil_tmp3 ;
2735
2736  {
2737  {
2738#line 575
2739  __cil_tmp2 = (void *)m;
2740#line 575
2741  memset(__cil_tmp2, 0, 80UL);
2742#line 576
2743  __cil_tmp3 = (struct list_head *)m;
2744#line 576
2745  INIT_LIST_HEAD(__cil_tmp3);
2746  }
2747#line 577
2748  return;
2749}
2750}
2751#line 579
2752__inline static void spi_message_add_tail(struct spi_transfer *t , struct spi_message *m )  __attribute__((__no_instrument_function__)) ;
2753#line 579 "include/linux/spi/spi.h"
2754__inline static void spi_message_add_tail(struct spi_transfer *t , struct spi_message *m ) 
2755{ unsigned long __cil_tmp3 ;
2756  unsigned long __cil_tmp4 ;
2757  struct list_head *__cil_tmp5 ;
2758  struct list_head *__cil_tmp6 ;
2759
2760  {
2761  {
2762#line 582
2763  __cil_tmp3 = (unsigned long )t;
2764#line 582
2765  __cil_tmp4 = __cil_tmp3 + 48;
2766#line 582
2767  __cil_tmp5 = (struct list_head *)__cil_tmp4;
2768#line 582
2769  __cil_tmp6 = (struct list_head *)m;
2770#line 582
2771  list_add_tail(__cil_tmp5, __cil_tmp6);
2772  }
2773#line 583
2774  return;
2775}
2776}
2777#line 618
2778extern int spi_setup(struct spi_device *spi ) ;
2779#line 630
2780extern int spi_sync(struct spi_device *spi , struct spi_message *message ) ;
2781#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
2782static int max1111_read(struct device *dev , int channel ) 
2783{ struct max1111_data *data ;
2784  void *tmp___7 ;
2785  uint8_t v1 ;
2786  uint8_t v2 ;
2787  int err ;
2788  struct device  const  *__cil_tmp8 ;
2789  unsigned long __cil_tmp9 ;
2790  unsigned long __cil_tmp10 ;
2791  struct mutex *__cil_tmp11 ;
2792  unsigned long __cil_tmp12 ;
2793  unsigned long __cil_tmp13 ;
2794  unsigned long __cil_tmp14 ;
2795  unsigned long __cil_tmp15 ;
2796  unsigned int __cil_tmp16 ;
2797  unsigned int __cil_tmp17 ;
2798  unsigned int __cil_tmp18 ;
2799  unsigned int __cil_tmp19 ;
2800  int __cil_tmp20 ;
2801  unsigned int __cil_tmp21 ;
2802  unsigned int __cil_tmp22 ;
2803  unsigned int __cil_tmp23 ;
2804  unsigned int __cil_tmp24 ;
2805  unsigned int __cil_tmp25 ;
2806  unsigned int __cil_tmp26 ;
2807  struct spi_device *__cil_tmp27 ;
2808  unsigned long __cil_tmp28 ;
2809  unsigned long __cil_tmp29 ;
2810  struct spi_message *__cil_tmp30 ;
2811  struct device  const  *__cil_tmp31 ;
2812  unsigned long __cil_tmp32 ;
2813  unsigned long __cil_tmp33 ;
2814  struct mutex *__cil_tmp34 ;
2815  unsigned long __cil_tmp35 ;
2816  unsigned long __cil_tmp36 ;
2817  unsigned long __cil_tmp37 ;
2818  unsigned long __cil_tmp38 ;
2819  unsigned long __cil_tmp39 ;
2820  unsigned long __cil_tmp40 ;
2821  unsigned long __cil_tmp41 ;
2822  unsigned long __cil_tmp42 ;
2823  unsigned long __cil_tmp43 ;
2824  unsigned long __cil_tmp44 ;
2825  struct mutex *__cil_tmp45 ;
2826  int __cil_tmp46 ;
2827  int __cil_tmp47 ;
2828  int __cil_tmp48 ;
2829  int __cil_tmp49 ;
2830  int __cil_tmp50 ;
2831  int __cil_tmp51 ;
2832
2833  {
2834  {
2835#line 50
2836  __cil_tmp8 = (struct device  const  *)dev;
2837#line 50
2838  tmp___7 = dev_get_drvdata(__cil_tmp8);
2839#line 50
2840  data = (struct max1111_data *)tmp___7;
2841#line 55
2842  __cil_tmp9 = (unsigned long )data;
2843#line 55
2844  __cil_tmp10 = __cil_tmp9 + 232;
2845#line 55
2846  __cil_tmp11 = (struct mutex *)__cil_tmp10;
2847#line 55
2848  mutex_lock(__cil_tmp11);
2849#line 57
2850  __cil_tmp12 = 0 * 1UL;
2851#line 57
2852  __cil_tmp13 = 224 + __cil_tmp12;
2853#line 57
2854  __cil_tmp14 = (unsigned long )data;
2855#line 57
2856  __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
2857#line 57
2858  __cil_tmp16 = 1U << 7;
2859#line 57
2860  __cil_tmp17 = 1U << 3;
2861#line 57
2862  __cil_tmp18 = 1U << 2;
2863#line 57
2864  __cil_tmp19 = 1U << 1;
2865#line 57
2866  __cil_tmp20 = channel << 5;
2867#line 57
2868  __cil_tmp21 = (unsigned int )__cil_tmp20;
2869#line 57
2870  __cil_tmp22 = __cil_tmp21 | 1U;
2871#line 57
2872  __cil_tmp23 = __cil_tmp22 | __cil_tmp19;
2873#line 57
2874  __cil_tmp24 = __cil_tmp23 | __cil_tmp18;
2875#line 57
2876  __cil_tmp25 = __cil_tmp24 | __cil_tmp17;
2877#line 57
2878  __cil_tmp26 = __cil_tmp25 | __cil_tmp16;
2879#line 57
2880  *((uint8_t *)__cil_tmp15) = (uint8_t )__cil_tmp26;
2881#line 61
2882  __cil_tmp27 = *((struct spi_device **)data);
2883#line 61
2884  __cil_tmp28 = (unsigned long )data;
2885#line 61
2886  __cil_tmp29 = __cil_tmp28 + 16;
2887#line 61
2888  __cil_tmp30 = (struct spi_message *)__cil_tmp29;
2889#line 61
2890  err = spi_sync(__cil_tmp27, __cil_tmp30);
2891  }
2892#line 62
2893  if (err < 0) {
2894    {
2895#line 63
2896    __cil_tmp31 = (struct device  const  *)dev;
2897#line 63
2898    dev_err(__cil_tmp31, "spi_sync failed with %d\n", err);
2899#line 64
2900    __cil_tmp32 = (unsigned long )data;
2901#line 64
2902    __cil_tmp33 = __cil_tmp32 + 232;
2903#line 64
2904    __cil_tmp34 = (struct mutex *)__cil_tmp33;
2905#line 64
2906    mutex_unlock(__cil_tmp34);
2907    }
2908#line 65
2909    return (err);
2910  } else {
2911
2912  }
2913  {
2914#line 68
2915  __cil_tmp35 = 0 * 1UL;
2916#line 68
2917  __cil_tmp36 = 225 + __cil_tmp35;
2918#line 68
2919  __cil_tmp37 = (unsigned long )data;
2920#line 68
2921  __cil_tmp38 = __cil_tmp37 + __cil_tmp36;
2922#line 68
2923  v1 = *((uint8_t *)__cil_tmp38);
2924#line 69
2925  __cil_tmp39 = 1 * 1UL;
2926#line 69
2927  __cil_tmp40 = 225 + __cil_tmp39;
2928#line 69
2929  __cil_tmp41 = (unsigned long )data;
2930#line 69
2931  __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
2932#line 69
2933  v2 = *((uint8_t *)__cil_tmp42);
2934#line 71
2935  __cil_tmp43 = (unsigned long )data;
2936#line 71
2937  __cil_tmp44 = __cil_tmp43 + 232;
2938#line 71
2939  __cil_tmp45 = (struct mutex *)__cil_tmp44;
2940#line 71
2941  mutex_unlock(__cil_tmp45);
2942  }
2943  {
2944#line 73
2945  __cil_tmp46 = (int )v1;
2946#line 73
2947  if (__cil_tmp46 & 192) {
2948#line 74
2949    return (-22);
2950  } else {
2951    {
2952#line 73
2953    __cil_tmp47 = (int )v2;
2954#line 73
2955    if (__cil_tmp47 & 63) {
2956#line 74
2957      return (-22);
2958    } else {
2959
2960    }
2961    }
2962  }
2963  }
2964  {
2965#line 76
2966  __cil_tmp48 = (int )v2;
2967#line 76
2968  __cil_tmp49 = __cil_tmp48 >> 6;
2969#line 76
2970  __cil_tmp50 = (int )v1;
2971#line 76
2972  __cil_tmp51 = __cil_tmp50 << 2;
2973#line 76
2974  return (__cil_tmp51 | __cil_tmp49);
2975  }
2976}
2977}
2978#line 94 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
2979static ssize_t show_name(struct device *dev , struct device_attribute *attr , char *buf ) 
2980{ int tmp___7 ;
2981
2982  {
2983  {
2984#line 97
2985  tmp___7 = sprintf(buf, "max1111\n");
2986  }
2987#line 97
2988  return ((ssize_t )tmp___7);
2989}
2990}
2991#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
2992static ssize_t show_adc(struct device *dev , struct device_attribute *attr , char *buf ) 
2993{ int channel ;
2994  struct device_attribute  const  *__mptr ;
2995  int ret ;
2996  int tmp___7 ;
2997  struct sensor_device_attribute *__cil_tmp8 ;
2998  struct device_attribute *__cil_tmp9 ;
2999  unsigned int __cil_tmp10 ;
3000  char *__cil_tmp11 ;
3001  char *__cil_tmp12 ;
3002  struct sensor_device_attribute *__cil_tmp13 ;
3003  unsigned long __cil_tmp14 ;
3004  unsigned long __cil_tmp15 ;
3005  int __cil_tmp16 ;
3006
3007  {
3008  {
3009#line 103
3010  __mptr = (struct device_attribute  const  *)attr;
3011#line 103
3012  __cil_tmp8 = (struct sensor_device_attribute *)0;
3013#line 103
3014  __cil_tmp9 = (struct device_attribute *)__cil_tmp8;
3015#line 103
3016  __cil_tmp10 = (unsigned int )__cil_tmp9;
3017#line 103
3018  __cil_tmp11 = (char *)__mptr;
3019#line 103
3020  __cil_tmp12 = __cil_tmp11 - __cil_tmp10;
3021#line 103
3022  __cil_tmp13 = (struct sensor_device_attribute *)__cil_tmp12;
3023#line 103
3024  __cil_tmp14 = (unsigned long )__cil_tmp13;
3025#line 103
3026  __cil_tmp15 = __cil_tmp14 + 32;
3027#line 103
3028  channel = *((int *)__cil_tmp15);
3029#line 106
3030  ret = max1111_read(dev, channel);
3031  }
3032#line 107
3033  if (ret < 0) {
3034#line 108
3035    return ((ssize_t )ret);
3036  } else {
3037
3038  }
3039  {
3040#line 114
3041  __cil_tmp16 = ret * 8;
3042#line 114
3043  tmp___7 = sprintf(buf, "%d\n", __cil_tmp16);
3044  }
3045#line 114
3046  return ((ssize_t )tmp___7);
3047}
3048}
3049#line 120 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3050static struct device_attribute dev_attr_name  =    {{"name", (umode_t )292}, & show_name, (ssize_t (*)(struct device *dev , struct device_attribute *attr ,
3051                                                       char const   *buf , size_t count ))((void *)0)};
3052#line 121 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3053static struct sensor_device_attribute sensor_dev_attr_in0_input  =    {{{"in0_input", (umode_t )292}, & show_adc, (ssize_t (*)(struct device *dev , struct device_attribute *attr ,
3054                                                            char const   *buf , size_t count ))((void *)0)},
3055    0};
3056#line 122 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3057static struct sensor_device_attribute sensor_dev_attr_in1_input  =    {{{"in1_input", (umode_t )292}, & show_adc, (ssize_t (*)(struct device *dev , struct device_attribute *attr ,
3058                                                            char const   *buf , size_t count ))((void *)0)},
3059    1};
3060#line 123 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3061static struct sensor_device_attribute sensor_dev_attr_in2_input  =    {{{"in2_input", (umode_t )292}, & show_adc, (ssize_t (*)(struct device *dev , struct device_attribute *attr ,
3062                                                            char const   *buf , size_t count ))((void *)0)},
3063    2};
3064#line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3065static struct sensor_device_attribute sensor_dev_attr_in3_input  =    {{{"in3_input", (umode_t )292}, & show_adc, (ssize_t (*)(struct device *dev , struct device_attribute *attr ,
3066                                                            char const   *buf , size_t count ))((void *)0)},
3067    3};
3068#line 126 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3069static struct attribute *max1111_attributes[6]  = {      & dev_attr_name.attr,      & sensor_dev_attr_in0_input.dev_attr.attr,      & sensor_dev_attr_in1_input.dev_attr.attr,      & sensor_dev_attr_in2_input.dev_attr.attr, 
3070        & sensor_dev_attr_in3_input.dev_attr.attr,      (struct attribute *)((void *)0)};
3071#line 135 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3072static struct attribute_group  const  max1111_attr_group  =    {(char const   *)0, (umode_t (*)(struct kobject * , struct attribute * , int  ))0,
3073    max1111_attributes};
3074#line 139
3075static int setup_transfer(struct max1111_data *data )  __attribute__((__section__(".devinit.text"),
3076__no_instrument_function__)) ;
3077#line 139 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3078static int setup_transfer(struct max1111_data *data ) 
3079{ struct spi_message *m ;
3080  struct spi_transfer *x ;
3081  unsigned long __cil_tmp4 ;
3082  unsigned long __cil_tmp5 ;
3083  unsigned long __cil_tmp6 ;
3084  unsigned long __cil_tmp7 ;
3085  unsigned long __cil_tmp8 ;
3086  unsigned long __cil_tmp9 ;
3087  unsigned long __cil_tmp10 ;
3088  unsigned long __cil_tmp11 ;
3089  unsigned long __cil_tmp12 ;
3090  unsigned long __cil_tmp13 ;
3091  uint8_t *__cil_tmp14 ;
3092  unsigned long __cil_tmp15 ;
3093  unsigned long __cil_tmp16 ;
3094  unsigned long __cil_tmp17 ;
3095  unsigned long __cil_tmp18 ;
3096  unsigned long __cil_tmp19 ;
3097  unsigned long __cil_tmp20 ;
3098  unsigned long __cil_tmp21 ;
3099  unsigned long __cil_tmp22 ;
3100  uint8_t *__cil_tmp23 ;
3101  unsigned long __cil_tmp24 ;
3102  unsigned long __cil_tmp25 ;
3103
3104  {
3105  {
3106#line 144
3107  __cil_tmp4 = (unsigned long )data;
3108#line 144
3109  __cil_tmp5 = __cil_tmp4 + 16;
3110#line 144
3111  m = (struct spi_message *)__cil_tmp5;
3112#line 145
3113  __cil_tmp6 = 0 * 64UL;
3114#line 145
3115  __cil_tmp7 = 96 + __cil_tmp6;
3116#line 145
3117  __cil_tmp8 = (unsigned long )data;
3118#line 145
3119  __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
3120#line 145
3121  x = (struct spi_transfer *)__cil_tmp9;
3122#line 147
3123  spi_message_init(m);
3124#line 149
3125  __cil_tmp10 = 0 * 1UL;
3126#line 149
3127  __cil_tmp11 = 224 + __cil_tmp10;
3128#line 149
3129  __cil_tmp12 = (unsigned long )data;
3130#line 149
3131  __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
3132#line 149
3133  __cil_tmp14 = (uint8_t *)__cil_tmp13;
3134#line 149
3135  *((void const   **)x) = (void const   *)__cil_tmp14;
3136#line 150
3137  __cil_tmp15 = (unsigned long )x;
3138#line 150
3139  __cil_tmp16 = __cil_tmp15 + 16;
3140#line 150
3141  *((unsigned int *)__cil_tmp16) = 1U;
3142#line 151
3143  spi_message_add_tail(x, m);
3144#line 153
3145  x = x + 1;
3146#line 154
3147  __cil_tmp17 = (unsigned long )x;
3148#line 154
3149  __cil_tmp18 = __cil_tmp17 + 8;
3150#line 154
3151  __cil_tmp19 = 0 * 1UL;
3152#line 154
3153  __cil_tmp20 = 225 + __cil_tmp19;
3154#line 154
3155  __cil_tmp21 = (unsigned long )data;
3156#line 154
3157  __cil_tmp22 = __cil_tmp21 + __cil_tmp20;
3158#line 154
3159  __cil_tmp23 = (uint8_t *)__cil_tmp22;
3160#line 154
3161  *((void **)__cil_tmp18) = (void *)__cil_tmp23;
3162#line 155
3163  __cil_tmp24 = (unsigned long )x;
3164#line 155
3165  __cil_tmp25 = __cil_tmp24 + 16;
3166#line 155
3167  *((unsigned int *)__cil_tmp25) = 2U;
3168#line 156
3169  spi_message_add_tail(x, m);
3170  }
3171#line 158
3172  return (0);
3173}
3174}
3175#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3176static struct lock_class_key __key___3  ;
3177#line 161
3178static int max1111_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
3179__no_instrument_function__)) ;
3180#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3181static int max1111_probe(struct spi_device *spi ) 
3182{ struct max1111_data *data ;
3183  int err ;
3184  void *tmp___7 ;
3185  long tmp___8 ;
3186  long tmp___9 ;
3187  unsigned long __cil_tmp7 ;
3188  unsigned long __cil_tmp8 ;
3189  unsigned long __cil_tmp9 ;
3190  unsigned long __cil_tmp10 ;
3191  void *__cil_tmp11 ;
3192  unsigned long __cil_tmp12 ;
3193  unsigned long __cil_tmp13 ;
3194  struct device *__cil_tmp14 ;
3195  struct device  const  *__cil_tmp15 ;
3196  unsigned long __cil_tmp16 ;
3197  unsigned long __cil_tmp17 ;
3198  struct mutex *__cil_tmp18 ;
3199  void *__cil_tmp19 ;
3200  unsigned long __cil_tmp20 ;
3201  unsigned long __cil_tmp21 ;
3202  unsigned long __cil_tmp22 ;
3203  struct kobject *__cil_tmp23 ;
3204  struct device *__cil_tmp24 ;
3205  struct device  const  *__cil_tmp25 ;
3206  unsigned long __cil_tmp26 ;
3207  unsigned long __cil_tmp27 ;
3208  struct device *__cil_tmp28 ;
3209  unsigned long __cil_tmp29 ;
3210  unsigned long __cil_tmp30 ;
3211  struct device *__cil_tmp31 ;
3212  void const   *__cil_tmp32 ;
3213  struct device *__cil_tmp33 ;
3214  struct device  const  *__cil_tmp34 ;
3215  unsigned long __cil_tmp35 ;
3216  unsigned long __cil_tmp36 ;
3217  struct device *__cil_tmp37 ;
3218  void const   *__cil_tmp38 ;
3219  unsigned long __cil_tmp39 ;
3220  unsigned long __cil_tmp40 ;
3221  unsigned long __cil_tmp41 ;
3222  struct kobject *__cil_tmp42 ;
3223  void const   *__cil_tmp43 ;
3224
3225  {
3226  {
3227#line 166
3228  __cil_tmp7 = (unsigned long )spi;
3229#line 166
3230  __cil_tmp8 = __cil_tmp7 + 782;
3231#line 166
3232  *((u8 *)__cil_tmp8) = (u8 )8;
3233#line 167
3234  __cil_tmp9 = (unsigned long )spi;
3235#line 167
3236  __cil_tmp10 = __cil_tmp9 + 781;
3237#line 167
3238  *((u8 *)__cil_tmp10) = (u8 )0;
3239#line 168
3240  err = spi_setup(spi);
3241  }
3242#line 169
3243  if (err < 0) {
3244#line 170
3245    return (err);
3246  } else {
3247
3248  }
3249  {
3250#line 172
3251  tmp___7 = kzalloc(304UL, 208U);
3252#line 172
3253  data = (struct max1111_data *)tmp___7;
3254  }
3255  {
3256#line 173
3257  __cil_tmp11 = (void *)0;
3258#line 173
3259  __cil_tmp12 = (unsigned long )__cil_tmp11;
3260#line 173
3261  __cil_tmp13 = (unsigned long )data;
3262#line 173
3263  if (__cil_tmp13 == __cil_tmp12) {
3264    {
3265#line 174
3266    __cil_tmp14 = (struct device *)spi;
3267#line 174
3268    __cil_tmp15 = (struct device  const  *)__cil_tmp14;
3269#line 174
3270    dev_err(__cil_tmp15, "failed to allocate memory\n");
3271    }
3272#line 175
3273    return (-12);
3274  } else {
3275
3276  }
3277  }
3278  {
3279#line 178
3280  err = setup_transfer(data);
3281  }
3282#line 179
3283  if (err) {
3284#line 180
3285    goto err_free_data;
3286  } else {
3287
3288  }
3289  {
3290#line 182
3291  while (1) {
3292    while_continue: /* CIL Label */ ;
3293    {
3294#line 182
3295    __cil_tmp16 = (unsigned long )data;
3296#line 182
3297    __cil_tmp17 = __cil_tmp16 + 232;
3298#line 182
3299    __cil_tmp18 = (struct mutex *)__cil_tmp17;
3300#line 182
3301    __mutex_init(__cil_tmp18, "&data->drvdata_lock", & __key___3);
3302    }
3303#line 182
3304    goto while_break;
3305  }
3306  while_break: /* CIL Label */ ;
3307  }
3308  {
3309#line 184
3310  *((struct spi_device **)data) = spi;
3311#line 185
3312  __cil_tmp19 = (void *)data;
3313#line 185
3314  spi_set_drvdata(spi, __cil_tmp19);
3315#line 187
3316  __cil_tmp20 = 0 + 16;
3317#line 187
3318  __cil_tmp21 = (unsigned long )spi;
3319#line 187
3320  __cil_tmp22 = __cil_tmp21 + __cil_tmp20;
3321#line 187
3322  __cil_tmp23 = (struct kobject *)__cil_tmp22;
3323#line 187
3324  err = (int )sysfs_create_group(__cil_tmp23, & max1111_attr_group);
3325  }
3326#line 188
3327  if (err) {
3328    {
3329#line 189
3330    __cil_tmp24 = (struct device *)spi;
3331#line 189
3332    __cil_tmp25 = (struct device  const  *)__cil_tmp24;
3333#line 189
3334    dev_err(__cil_tmp25, "failed to create attribute group\n");
3335    }
3336#line 190
3337    goto err_free_data;
3338  } else {
3339
3340  }
3341  {
3342#line 193
3343  __cil_tmp26 = (unsigned long )data;
3344#line 193
3345  __cil_tmp27 = __cil_tmp26 + 8;
3346#line 193
3347  __cil_tmp28 = (struct device *)spi;
3348#line 193
3349  *((struct device **)__cil_tmp27) = hwmon_device_register(__cil_tmp28);
3350#line 194
3351  __cil_tmp29 = (unsigned long )data;
3352#line 194
3353  __cil_tmp30 = __cil_tmp29 + 8;
3354#line 194
3355  __cil_tmp31 = *((struct device **)__cil_tmp30);
3356#line 194
3357  __cil_tmp32 = (void const   *)__cil_tmp31;
3358#line 194
3359  tmp___9 = (long )IS_ERR(__cil_tmp32);
3360  }
3361#line 194
3362  if (tmp___9) {
3363    {
3364#line 195
3365    __cil_tmp33 = (struct device *)spi;
3366#line 195
3367    __cil_tmp34 = (struct device  const  *)__cil_tmp33;
3368#line 195
3369    dev_err(__cil_tmp34, "failed to create hwmon device\n");
3370#line 196
3371    __cil_tmp35 = (unsigned long )data;
3372#line 196
3373    __cil_tmp36 = __cil_tmp35 + 8;
3374#line 196
3375    __cil_tmp37 = *((struct device **)__cil_tmp36);
3376#line 196
3377    __cil_tmp38 = (void const   *)__cil_tmp37;
3378#line 196
3379    tmp___8 = (long )PTR_ERR(__cil_tmp38);
3380#line 196
3381    err = (int )tmp___8;
3382    }
3383#line 197
3384    goto err_remove;
3385  } else {
3386
3387  }
3388#line 203
3389  return (0);
3390  err_remove: 
3391  {
3392#line 206
3393  __cil_tmp39 = 0 + 16;
3394#line 206
3395  __cil_tmp40 = (unsigned long )spi;
3396#line 206
3397  __cil_tmp41 = __cil_tmp40 + __cil_tmp39;
3398#line 206
3399  __cil_tmp42 = (struct kobject *)__cil_tmp41;
3400#line 206
3401  sysfs_remove_group(__cil_tmp42, & max1111_attr_group);
3402  }
3403  err_free_data: 
3404  {
3405#line 208
3406  __cil_tmp43 = (void const   *)data;
3407#line 208
3408  kfree(__cil_tmp43);
3409  }
3410#line 209
3411  return (err);
3412}
3413}
3414#line 212
3415static int max1111_remove(struct spi_device *spi )  __attribute__((__section__(".devexit.text"),
3416__no_instrument_function__)) ;
3417#line 212 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3418static int max1111_remove(struct spi_device *spi ) 
3419{ struct max1111_data *data ;
3420  void *tmp___7 ;
3421  unsigned long __cil_tmp4 ;
3422  unsigned long __cil_tmp5 ;
3423  struct device *__cil_tmp6 ;
3424  unsigned long __cil_tmp7 ;
3425  unsigned long __cil_tmp8 ;
3426  unsigned long __cil_tmp9 ;
3427  struct kobject *__cil_tmp10 ;
3428  unsigned long __cil_tmp11 ;
3429  unsigned long __cil_tmp12 ;
3430  struct mutex *__cil_tmp13 ;
3431  void const   *__cil_tmp14 ;
3432
3433  {
3434  {
3435#line 214
3436  tmp___7 = spi_get_drvdata(spi);
3437#line 214
3438  data = (struct max1111_data *)tmp___7;
3439#line 216
3440  __cil_tmp4 = (unsigned long )data;
3441#line 216
3442  __cil_tmp5 = __cil_tmp4 + 8;
3443#line 216
3444  __cil_tmp6 = *((struct device **)__cil_tmp5);
3445#line 216
3446  hwmon_device_unregister(__cil_tmp6);
3447#line 217
3448  __cil_tmp7 = 0 + 16;
3449#line 217
3450  __cil_tmp8 = (unsigned long )spi;
3451#line 217
3452  __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
3453#line 217
3454  __cil_tmp10 = (struct kobject *)__cil_tmp9;
3455#line 217
3456  sysfs_remove_group(__cil_tmp10, & max1111_attr_group);
3457#line 218
3458  __cil_tmp11 = (unsigned long )data;
3459#line 218
3460  __cil_tmp12 = __cil_tmp11 + 232;
3461#line 218
3462  __cil_tmp13 = (struct mutex *)__cil_tmp12;
3463#line 218
3464  mutex_destroy(__cil_tmp13);
3465#line 219
3466  __cil_tmp14 = (void const   *)data;
3467#line 219
3468  kfree(__cil_tmp14);
3469  }
3470#line 220
3471  return (0);
3472}
3473}
3474#line 223 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3475static struct spi_driver max1111_driver  =    {(struct spi_device_id  const  *)0, & max1111_probe, & max1111_remove, (void (*)(struct spi_device *spi ))0,
3476    (int (*)(struct spi_device *spi , pm_message_t mesg ))0, (int (*)(struct spi_device *spi ))0,
3477    {"max1111", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
3478     (struct of_device_id  const  *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3479     (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
3480     (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
3481     (struct driver_private *)0}};
3482#line 232
3483static int max1111_driver_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
3484#line 232 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3485static int max1111_driver_init(void) 
3486{ int tmp___7 ;
3487
3488  {
3489  {
3490#line 232
3491  tmp___7 = spi_register_driver(& max1111_driver);
3492  }
3493#line 232
3494  return (tmp___7);
3495}
3496}
3497#line 232 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3498int init_module(void) 
3499{ int tmp___7 ;
3500
3501  {
3502  {
3503#line 232
3504  tmp___7 = max1111_driver_init();
3505  }
3506#line 232
3507  return (tmp___7);
3508}
3509}
3510#line 232
3511static void max1111_driver_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
3512#line 232 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3513static void max1111_driver_exit(void) 
3514{ 
3515
3516  {
3517  {
3518#line 232
3519  spi_unregister_driver(& max1111_driver);
3520  }
3521#line 232
3522  return;
3523}
3524}
3525#line 232 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3526void cleanup_module(void) 
3527{ 
3528
3529  {
3530  {
3531#line 232
3532  max1111_driver_exit();
3533  }
3534#line 232
3535  return;
3536}
3537}
3538#line 234 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3539static char const   __mod_author234[41]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3540__aligned__(1)))  = 
3541#line 234
3542  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
3543        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'E', 
3544        (char const   )'r',      (char const   )'i',      (char const   )'c',      (char const   )' ', 
3545        (char const   )'M',      (char const   )'i',      (char const   )'a',      (char const   )'o', 
3546        (char const   )' ',      (char const   )'<',      (char const   )'e',      (char const   )'r', 
3547        (char const   )'i',      (char const   )'c',      (char const   )'.',      (char const   )'m', 
3548        (char const   )'i',      (char const   )'a',      (char const   )'o',      (char const   )'@', 
3549        (char const   )'m',      (char const   )'a',      (char const   )'r',      (char const   )'v', 
3550        (char const   )'e',      (char const   )'l',      (char const   )'l',      (char const   )'.', 
3551        (char const   )'c',      (char const   )'o',      (char const   )'m',      (char const   )'>', 
3552        (char const   )'\000'};
3553#line 235 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3554static char const   __mod_description235[31]  __attribute__((__used__, __unused__,
3555__section__(".modinfo"), __aligned__(1)))  = 
3556#line 235
3557  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
3558        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
3559        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
3560        (char const   )'M',      (char const   )'A',      (char const   )'X',      (char const   )'1', 
3561        (char const   )'1',      (char const   )'1',      (char const   )'1',      (char const   )' ', 
3562        (char const   )'A',      (char const   )'D',      (char const   )'C',      (char const   )' ', 
3563        (char const   )'D',      (char const   )'r',      (char const   )'i',      (char const   )'v', 
3564        (char const   )'e',      (char const   )'r',      (char const   )'\000'};
3565#line 236 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3566static char const   __mod_license236[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3567__aligned__(1)))  = 
3568#line 236
3569  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
3570        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
3571        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
3572#line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3573static char const   __mod_alias237[18]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3574__aligned__(1)))  = 
3575#line 237
3576  {      (char const   )'a',      (char const   )'l',      (char const   )'i',      (char const   )'a', 
3577        (char const   )'s',      (char const   )'=',      (char const   )'s',      (char const   )'p', 
3578        (char const   )'i',      (char const   )':',      (char const   )'m',      (char const   )'a', 
3579        (char const   )'x',      (char const   )'1',      (char const   )'1',      (char const   )'1', 
3580        (char const   )'1',      (char const   )'\000'};
3581#line 255
3582void ldv_check_final_state(void) ;
3583#line 258
3584extern void ldv_check_return_value(int res ) ;
3585#line 261
3586extern void ldv_initialize(void) ;
3587#line 264
3588extern int __VERIFIER_nondet_int(void) ;
3589#line 267 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3590int LDV_IN_INTERRUPT  ;
3591#line 295 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3592static int res_max1111_probe_5  ;
3593#line 270 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3594void main(void) 
3595{ struct spi_device *var_group1 ;
3596  int ldv_s_max1111_driver_spi_driver ;
3597  int tmp___7 ;
3598  int tmp___8 ;
3599  int __cil_tmp5 ;
3600
3601  {
3602  {
3603#line 303
3604  LDV_IN_INTERRUPT = 1;
3605#line 312
3606  ldv_initialize();
3607#line 313
3608  ldv_s_max1111_driver_spi_driver = 0;
3609  }
3610  {
3611#line 316
3612  while (1) {
3613    while_continue: /* CIL Label */ ;
3614    {
3615#line 316
3616    tmp___8 = __VERIFIER_nondet_int();
3617    }
3618#line 316
3619    if (tmp___8) {
3620
3621    } else {
3622      {
3623#line 316
3624      __cil_tmp5 = ldv_s_max1111_driver_spi_driver == 0;
3625#line 316
3626      if (! __cil_tmp5) {
3627
3628      } else {
3629#line 316
3630        goto while_break;
3631      }
3632      }
3633    }
3634    {
3635#line 320
3636    tmp___7 = __VERIFIER_nondet_int();
3637    }
3638#line 322
3639    if (tmp___7 == 0) {
3640#line 322
3641      goto case_0;
3642    } else {
3643      {
3644#line 354
3645      goto switch_default;
3646#line 320
3647      if (0) {
3648        case_0: /* CIL Label */ 
3649#line 325
3650        if (ldv_s_max1111_driver_spi_driver == 0) {
3651          {
3652#line 343
3653          res_max1111_probe_5 = max1111_probe(var_group1);
3654#line 344
3655          ldv_check_return_value(res_max1111_probe_5);
3656          }
3657#line 345
3658          if (res_max1111_probe_5) {
3659#line 346
3660            goto ldv_module_exit;
3661          } else {
3662
3663          }
3664#line 347
3665          ldv_s_max1111_driver_spi_driver = 0;
3666        } else {
3667
3668        }
3669#line 353
3670        goto switch_break;
3671        switch_default: /* CIL Label */ 
3672#line 354
3673        goto switch_break;
3674      } else {
3675        switch_break: /* CIL Label */ ;
3676      }
3677      }
3678    }
3679  }
3680  while_break: /* CIL Label */ ;
3681  }
3682  ldv_module_exit: 
3683  {
3684#line 363
3685  ldv_check_final_state();
3686  }
3687#line 366
3688  return;
3689}
3690}
3691#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3692void ldv_blast_assert(void) 
3693{ 
3694
3695  {
3696  ERROR: 
3697#line 6
3698  goto ERROR;
3699}
3700}
3701#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3702extern int __VERIFIER_nondet_int(void) ;
3703#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3704int ldv_mutex  =    1;
3705#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3706int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
3707{ int nondetermined ;
3708
3709  {
3710#line 29
3711  if (ldv_mutex == 1) {
3712
3713  } else {
3714    {
3715#line 29
3716    ldv_blast_assert();
3717    }
3718  }
3719  {
3720#line 32
3721  nondetermined = __VERIFIER_nondet_int();
3722  }
3723#line 35
3724  if (nondetermined) {
3725#line 38
3726    ldv_mutex = 2;
3727#line 40
3728    return (0);
3729  } else {
3730#line 45
3731    return (-4);
3732  }
3733}
3734}
3735#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3736int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
3737{ int nondetermined ;
3738
3739  {
3740#line 57
3741  if (ldv_mutex == 1) {
3742
3743  } else {
3744    {
3745#line 57
3746    ldv_blast_assert();
3747    }
3748  }
3749  {
3750#line 60
3751  nondetermined = __VERIFIER_nondet_int();
3752  }
3753#line 63
3754  if (nondetermined) {
3755#line 66
3756    ldv_mutex = 2;
3757#line 68
3758    return (0);
3759  } else {
3760#line 73
3761    return (-4);
3762  }
3763}
3764}
3765#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3766int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
3767{ int atomic_value_after_dec ;
3768
3769  {
3770#line 83
3771  if (ldv_mutex == 1) {
3772
3773  } else {
3774    {
3775#line 83
3776    ldv_blast_assert();
3777    }
3778  }
3779  {
3780#line 86
3781  atomic_value_after_dec = __VERIFIER_nondet_int();
3782  }
3783#line 89
3784  if (atomic_value_after_dec == 0) {
3785#line 92
3786    ldv_mutex = 2;
3787#line 94
3788    return (1);
3789  } else {
3790
3791  }
3792#line 98
3793  return (0);
3794}
3795}
3796#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3797void mutex_lock(struct mutex *lock ) 
3798{ 
3799
3800  {
3801#line 108
3802  if (ldv_mutex == 1) {
3803
3804  } else {
3805    {
3806#line 108
3807    ldv_blast_assert();
3808    }
3809  }
3810#line 110
3811  ldv_mutex = 2;
3812#line 111
3813  return;
3814}
3815}
3816#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3817int mutex_trylock(struct mutex *lock ) 
3818{ int nondetermined ;
3819
3820  {
3821#line 121
3822  if (ldv_mutex == 1) {
3823
3824  } else {
3825    {
3826#line 121
3827    ldv_blast_assert();
3828    }
3829  }
3830  {
3831#line 124
3832  nondetermined = __VERIFIER_nondet_int();
3833  }
3834#line 127
3835  if (nondetermined) {
3836#line 130
3837    ldv_mutex = 2;
3838#line 132
3839    return (1);
3840  } else {
3841#line 137
3842    return (0);
3843  }
3844}
3845}
3846#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3847void mutex_unlock(struct mutex *lock ) 
3848{ 
3849
3850  {
3851#line 147
3852  if (ldv_mutex == 2) {
3853
3854  } else {
3855    {
3856#line 147
3857    ldv_blast_assert();
3858    }
3859  }
3860#line 149
3861  ldv_mutex = 1;
3862#line 150
3863  return;
3864}
3865}
3866#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3867void ldv_check_final_state(void) 
3868{ 
3869
3870  {
3871#line 156
3872  if (ldv_mutex == 1) {
3873
3874  } else {
3875    {
3876#line 156
3877    ldv_blast_assert();
3878    }
3879  }
3880#line 157
3881  return;
3882}
3883}
3884#line 375 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6077/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/max1111.c.common.c"
3885long s__builtin_expect(long val , long res ) 
3886{ 
3887
3888  {
3889#line 376
3890  return (val);
3891}
3892}