Showing error 308

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