Showing error 306

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--busses--i2c-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 4457
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 146 "include/linux/init.h"
 116typedef void (*ctor_fn_t)(void);
 117#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 118struct module;
 119#line 56
 120struct module;
 121#line 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 46 "include/linux/slub_def.h"
1056struct kmem_cache_cpu {
1057   void **freelist ;
1058   unsigned long tid ;
1059   struct page *page ;
1060   struct page *partial ;
1061   int node ;
1062   unsigned int stat[26] ;
1063};
1064#line 57 "include/linux/slub_def.h"
1065struct kmem_cache_node {
1066   spinlock_t list_lock ;
1067   unsigned long nr_partial ;
1068   struct list_head partial ;
1069   atomic_long_t nr_slabs ;
1070   atomic_long_t total_objects ;
1071   struct list_head full ;
1072};
1073#line 73 "include/linux/slub_def.h"
1074struct kmem_cache_order_objects {
1075   unsigned long x ;
1076};
1077#line 80 "include/linux/slub_def.h"
1078struct kmem_cache {
1079   struct kmem_cache_cpu *cpu_slab ;
1080   unsigned long flags ;
1081   unsigned long min_partial ;
1082   int size ;
1083   int objsize ;
1084   int offset ;
1085   int cpu_partial ;
1086   struct kmem_cache_order_objects oo ;
1087   struct kmem_cache_order_objects max ;
1088   struct kmem_cache_order_objects min ;
1089   gfp_t allocflags ;
1090   int refcount ;
1091   void (*ctor)(void * ) ;
1092   int inuse ;
1093   int align ;
1094   int reserved ;
1095   char const   *name ;
1096   struct list_head list ;
1097   struct kobject kobj ;
1098   int remote_node_defrag_ratio ;
1099   struct kmem_cache_node *node[1 << 10] ;
1100};
1101#line 219 "include/linux/mod_devicetable.h"
1102struct of_device_id {
1103   char name[32] ;
1104   char type[32] ;
1105   char compatible[128] ;
1106   void *data ;
1107};
1108#line 19 "include/linux/klist.h"
1109struct klist_node;
1110#line 19
1111struct klist_node;
1112#line 39 "include/linux/klist.h"
1113struct klist_node {
1114   void *n_klist ;
1115   struct list_head n_node ;
1116   struct kref n_ref ;
1117};
1118#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1119struct dma_map_ops;
1120#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1121struct dev_archdata {
1122   void *acpi_handle ;
1123   struct dma_map_ops *dma_ops ;
1124   void *iommu ;
1125};
1126#line 28 "include/linux/device.h"
1127struct device;
1128#line 29
1129struct device_private;
1130#line 29
1131struct device_private;
1132#line 30
1133struct device_driver;
1134#line 30
1135struct device_driver;
1136#line 31
1137struct driver_private;
1138#line 31
1139struct driver_private;
1140#line 32
1141struct module;
1142#line 33
1143struct class;
1144#line 33
1145struct class;
1146#line 34
1147struct subsys_private;
1148#line 34
1149struct subsys_private;
1150#line 35
1151struct bus_type;
1152#line 35
1153struct bus_type;
1154#line 36
1155struct device_node;
1156#line 36
1157struct device_node;
1158#line 37
1159struct iommu_ops;
1160#line 37
1161struct iommu_ops;
1162#line 39 "include/linux/device.h"
1163struct bus_attribute {
1164   struct attribute attr ;
1165   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
1166   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
1167};
1168#line 89
1169struct device_attribute;
1170#line 89
1171struct driver_attribute;
1172#line 89 "include/linux/device.h"
1173struct bus_type {
1174   char const   *name ;
1175   char const   *dev_name ;
1176   struct device *dev_root ;
1177   struct bus_attribute *bus_attrs ;
1178   struct device_attribute *dev_attrs ;
1179   struct driver_attribute *drv_attrs ;
1180   int (*match)(struct device *dev , struct device_driver *drv ) ;
1181   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1182   int (*probe)(struct device *dev ) ;
1183   int (*remove)(struct device *dev ) ;
1184   void (*shutdown)(struct device *dev ) ;
1185   int (*suspend)(struct device *dev , pm_message_t state ) ;
1186   int (*resume)(struct device *dev ) ;
1187   struct dev_pm_ops  const  *pm ;
1188   struct iommu_ops *iommu_ops ;
1189   struct subsys_private *p ;
1190};
1191#line 127
1192struct device_type;
1193#line 214 "include/linux/device.h"
1194struct device_driver {
1195   char const   *name ;
1196   struct bus_type *bus ;
1197   struct module *owner ;
1198   char const   *mod_name ;
1199   bool suppress_bind_attrs ;
1200   struct of_device_id  const  *of_match_table ;
1201   int (*probe)(struct device *dev ) ;
1202   int (*remove)(struct device *dev ) ;
1203   void (*shutdown)(struct device *dev ) ;
1204   int (*suspend)(struct device *dev , pm_message_t state ) ;
1205   int (*resume)(struct device *dev ) ;
1206   struct attribute_group  const  **groups ;
1207   struct dev_pm_ops  const  *pm ;
1208   struct driver_private *p ;
1209};
1210#line 249 "include/linux/device.h"
1211struct driver_attribute {
1212   struct attribute attr ;
1213   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1214   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
1215};
1216#line 330
1217struct class_attribute;
1218#line 330 "include/linux/device.h"
1219struct class {
1220   char const   *name ;
1221   struct module *owner ;
1222   struct class_attribute *class_attrs ;
1223   struct device_attribute *dev_attrs ;
1224   struct bin_attribute *dev_bin_attrs ;
1225   struct kobject *dev_kobj ;
1226   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1227   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1228   void (*class_release)(struct class *class ) ;
1229   void (*dev_release)(struct device *dev ) ;
1230   int (*suspend)(struct device *dev , pm_message_t state ) ;
1231   int (*resume)(struct device *dev ) ;
1232   struct kobj_ns_type_operations  const  *ns_type ;
1233   void const   *(*namespace)(struct device *dev ) ;
1234   struct dev_pm_ops  const  *pm ;
1235   struct subsys_private *p ;
1236};
1237#line 397 "include/linux/device.h"
1238struct class_attribute {
1239   struct attribute attr ;
1240   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1241   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
1242                    size_t count ) ;
1243   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
1244};
1245#line 465 "include/linux/device.h"
1246struct device_type {
1247   char const   *name ;
1248   struct attribute_group  const  **groups ;
1249   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1250   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1251   void (*release)(struct device *dev ) ;
1252   struct dev_pm_ops  const  *pm ;
1253};
1254#line 476 "include/linux/device.h"
1255struct device_attribute {
1256   struct attribute attr ;
1257   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1258   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
1259                    size_t count ) ;
1260};
1261#line 559 "include/linux/device.h"
1262struct device_dma_parameters {
1263   unsigned int max_segment_size ;
1264   unsigned long segment_boundary_mask ;
1265};
1266#line 627
1267struct dma_coherent_mem;
1268#line 627 "include/linux/device.h"
1269struct device {
1270   struct device *parent ;
1271   struct device_private *p ;
1272   struct kobject kobj ;
1273   char const   *init_name ;
1274   struct device_type  const  *type ;
1275   struct mutex mutex ;
1276   struct bus_type *bus ;
1277   struct device_driver *driver ;
1278   void *platform_data ;
1279   struct dev_pm_info power ;
1280   struct dev_pm_domain *pm_domain ;
1281   int numa_node ;
1282   u64 *dma_mask ;
1283   u64 coherent_dma_mask ;
1284   struct device_dma_parameters *dma_parms ;
1285   struct list_head dma_pools ;
1286   struct dma_coherent_mem *dma_mem ;
1287   struct dev_archdata archdata ;
1288   struct device_node *of_node ;
1289   dev_t devt ;
1290   u32 id ;
1291   spinlock_t devres_lock ;
1292   struct list_head devres_head ;
1293   struct klist_node knode_class ;
1294   struct class *class ;
1295   struct attribute_group  const  **groups ;
1296   void (*release)(struct device *dev ) ;
1297};
1298#line 43 "include/linux/pm_wakeup.h"
1299struct wakeup_source {
1300   char const   *name ;
1301   struct list_head entry ;
1302   spinlock_t lock ;
1303   struct timer_list timer ;
1304   unsigned long timer_expires ;
1305   ktime_t total_time ;
1306   ktime_t max_time ;
1307   ktime_t last_time ;
1308   unsigned long event_count ;
1309   unsigned long active_count ;
1310   unsigned long relax_count ;
1311   unsigned long hit_count ;
1312   unsigned int active : 1 ;
1313};
1314#line 18 "include/linux/capability.h"
1315struct task_struct;
1316#line 94 "include/linux/capability.h"
1317struct kernel_cap_struct {
1318   __u32 cap[2] ;
1319};
1320#line 94 "include/linux/capability.h"
1321typedef struct kernel_cap_struct kernel_cap_t;
1322#line 378
1323struct user_namespace;
1324#line 378
1325struct user_namespace;
1326#line 14 "include/linux/prio_tree.h"
1327struct prio_tree_node;
1328#line 14 "include/linux/prio_tree.h"
1329struct raw_prio_tree_node {
1330   struct prio_tree_node *left ;
1331   struct prio_tree_node *right ;
1332   struct prio_tree_node *parent ;
1333};
1334#line 20 "include/linux/prio_tree.h"
1335struct prio_tree_node {
1336   struct prio_tree_node *left ;
1337   struct prio_tree_node *right ;
1338   struct prio_tree_node *parent ;
1339   unsigned long start ;
1340   unsigned long last ;
1341};
1342#line 23 "include/linux/mm_types.h"
1343struct address_space;
1344#line 23
1345struct address_space;
1346#line 40 "include/linux/mm_types.h"
1347union __anonunion____missing_field_name_204 {
1348   unsigned long index ;
1349   void *freelist ;
1350};
1351#line 40 "include/linux/mm_types.h"
1352struct __anonstruct____missing_field_name_208 {
1353   unsigned int inuse : 16 ;
1354   unsigned int objects : 15 ;
1355   unsigned int frozen : 1 ;
1356};
1357#line 40 "include/linux/mm_types.h"
1358union __anonunion____missing_field_name_207 {
1359   atomic_t _mapcount ;
1360   struct __anonstruct____missing_field_name_208 __annonCompField34 ;
1361};
1362#line 40 "include/linux/mm_types.h"
1363struct __anonstruct____missing_field_name_206 {
1364   union __anonunion____missing_field_name_207 __annonCompField35 ;
1365   atomic_t _count ;
1366};
1367#line 40 "include/linux/mm_types.h"
1368union __anonunion____missing_field_name_205 {
1369   unsigned long counters ;
1370   struct __anonstruct____missing_field_name_206 __annonCompField36 ;
1371};
1372#line 40 "include/linux/mm_types.h"
1373struct __anonstruct____missing_field_name_203 {
1374   union __anonunion____missing_field_name_204 __annonCompField33 ;
1375   union __anonunion____missing_field_name_205 __annonCompField37 ;
1376};
1377#line 40 "include/linux/mm_types.h"
1378struct __anonstruct____missing_field_name_210 {
1379   struct page *next ;
1380   int pages ;
1381   int pobjects ;
1382};
1383#line 40 "include/linux/mm_types.h"
1384union __anonunion____missing_field_name_209 {
1385   struct list_head lru ;
1386   struct __anonstruct____missing_field_name_210 __annonCompField39 ;
1387};
1388#line 40 "include/linux/mm_types.h"
1389union __anonunion____missing_field_name_211 {
1390   unsigned long private ;
1391   struct kmem_cache *slab ;
1392   struct page *first_page ;
1393};
1394#line 40 "include/linux/mm_types.h"
1395struct page {
1396   unsigned long flags ;
1397   struct address_space *mapping ;
1398   struct __anonstruct____missing_field_name_203 __annonCompField38 ;
1399   union __anonunion____missing_field_name_209 __annonCompField40 ;
1400   union __anonunion____missing_field_name_211 __annonCompField41 ;
1401   unsigned long debug_flags ;
1402} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1403#line 200 "include/linux/mm_types.h"
1404struct __anonstruct_vm_set_213 {
1405   struct list_head list ;
1406   void *parent ;
1407   struct vm_area_struct *head ;
1408};
1409#line 200 "include/linux/mm_types.h"
1410union __anonunion_shared_212 {
1411   struct __anonstruct_vm_set_213 vm_set ;
1412   struct raw_prio_tree_node prio_tree_node ;
1413};
1414#line 200
1415struct anon_vma;
1416#line 200
1417struct vm_operations_struct;
1418#line 200
1419struct mempolicy;
1420#line 200 "include/linux/mm_types.h"
1421struct vm_area_struct {
1422   struct mm_struct *vm_mm ;
1423   unsigned long vm_start ;
1424   unsigned long vm_end ;
1425   struct vm_area_struct *vm_next ;
1426   struct vm_area_struct *vm_prev ;
1427   pgprot_t vm_page_prot ;
1428   unsigned long vm_flags ;
1429   struct rb_node vm_rb ;
1430   union __anonunion_shared_212 shared ;
1431   struct list_head anon_vma_chain ;
1432   struct anon_vma *anon_vma ;
1433   struct vm_operations_struct  const  *vm_ops ;
1434   unsigned long vm_pgoff ;
1435   struct file *vm_file ;
1436   void *vm_private_data ;
1437   struct mempolicy *vm_policy ;
1438};
1439#line 257 "include/linux/mm_types.h"
1440struct core_thread {
1441   struct task_struct *task ;
1442   struct core_thread *next ;
1443};
1444#line 262 "include/linux/mm_types.h"
1445struct core_state {
1446   atomic_t nr_threads ;
1447   struct core_thread dumper ;
1448   struct completion startup ;
1449};
1450#line 284 "include/linux/mm_types.h"
1451struct mm_rss_stat {
1452   atomic_long_t count[3] ;
1453};
1454#line 288
1455struct linux_binfmt;
1456#line 288
1457struct mmu_notifier_mm;
1458#line 288 "include/linux/mm_types.h"
1459struct mm_struct {
1460   struct vm_area_struct *mmap ;
1461   struct rb_root mm_rb ;
1462   struct vm_area_struct *mmap_cache ;
1463   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
1464                                      unsigned long pgoff , unsigned long flags ) ;
1465   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
1466   unsigned long mmap_base ;
1467   unsigned long task_size ;
1468   unsigned long cached_hole_size ;
1469   unsigned long free_area_cache ;
1470   pgd_t *pgd ;
1471   atomic_t mm_users ;
1472   atomic_t mm_count ;
1473   int map_count ;
1474   spinlock_t page_table_lock ;
1475   struct rw_semaphore mmap_sem ;
1476   struct list_head mmlist ;
1477   unsigned long hiwater_rss ;
1478   unsigned long hiwater_vm ;
1479   unsigned long total_vm ;
1480   unsigned long locked_vm ;
1481   unsigned long pinned_vm ;
1482   unsigned long shared_vm ;
1483   unsigned long exec_vm ;
1484   unsigned long stack_vm ;
1485   unsigned long reserved_vm ;
1486   unsigned long def_flags ;
1487   unsigned long nr_ptes ;
1488   unsigned long start_code ;
1489   unsigned long end_code ;
1490   unsigned long start_data ;
1491   unsigned long end_data ;
1492   unsigned long start_brk ;
1493   unsigned long brk ;
1494   unsigned long start_stack ;
1495   unsigned long arg_start ;
1496   unsigned long arg_end ;
1497   unsigned long env_start ;
1498   unsigned long env_end ;
1499   unsigned long saved_auxv[44] ;
1500   struct mm_rss_stat rss_stat ;
1501   struct linux_binfmt *binfmt ;
1502   cpumask_var_t cpu_vm_mask_var ;
1503   mm_context_t context ;
1504   unsigned int faultstamp ;
1505   unsigned int token_priority ;
1506   unsigned int last_interval ;
1507   unsigned long flags ;
1508   struct core_state *core_state ;
1509   spinlock_t ioctx_lock ;
1510   struct hlist_head ioctx_list ;
1511   struct task_struct *owner ;
1512   struct file *exe_file ;
1513   unsigned long num_exe_file_vmas ;
1514   struct mmu_notifier_mm *mmu_notifier_mm ;
1515   pgtable_t pmd_huge_pte ;
1516   struct cpumask cpumask_allocation ;
1517};
1518#line 7 "include/asm-generic/cputime.h"
1519typedef unsigned long cputime_t;
1520#line 84 "include/linux/sem.h"
1521struct task_struct;
1522#line 101
1523struct sem_undo_list;
1524#line 101 "include/linux/sem.h"
1525struct sysv_sem {
1526   struct sem_undo_list *undo_list ;
1527};
1528#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1529struct siginfo;
1530#line 10
1531struct siginfo;
1532#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1533struct __anonstruct_sigset_t_215 {
1534   unsigned long sig[1] ;
1535};
1536#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1537typedef struct __anonstruct_sigset_t_215 sigset_t;
1538#line 17 "include/asm-generic/signal-defs.h"
1539typedef void __signalfn_t(int  );
1540#line 18 "include/asm-generic/signal-defs.h"
1541typedef __signalfn_t *__sighandler_t;
1542#line 20 "include/asm-generic/signal-defs.h"
1543typedef void __restorefn_t(void);
1544#line 21 "include/asm-generic/signal-defs.h"
1545typedef __restorefn_t *__sigrestore_t;
1546#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1547struct sigaction {
1548   __sighandler_t sa_handler ;
1549   unsigned long sa_flags ;
1550   __sigrestore_t sa_restorer ;
1551   sigset_t sa_mask ;
1552};
1553#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1554struct k_sigaction {
1555   struct sigaction sa ;
1556};
1557#line 7 "include/asm-generic/siginfo.h"
1558union sigval {
1559   int sival_int ;
1560   void *sival_ptr ;
1561};
1562#line 7 "include/asm-generic/siginfo.h"
1563typedef union sigval sigval_t;
1564#line 48 "include/asm-generic/siginfo.h"
1565struct __anonstruct__kill_217 {
1566   __kernel_pid_t _pid ;
1567   __kernel_uid32_t _uid ;
1568};
1569#line 48 "include/asm-generic/siginfo.h"
1570struct __anonstruct__timer_218 {
1571   __kernel_timer_t _tid ;
1572   int _overrun ;
1573   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
1574   sigval_t _sigval ;
1575   int _sys_private ;
1576};
1577#line 48 "include/asm-generic/siginfo.h"
1578struct __anonstruct__rt_219 {
1579   __kernel_pid_t _pid ;
1580   __kernel_uid32_t _uid ;
1581   sigval_t _sigval ;
1582};
1583#line 48 "include/asm-generic/siginfo.h"
1584struct __anonstruct__sigchld_220 {
1585   __kernel_pid_t _pid ;
1586   __kernel_uid32_t _uid ;
1587   int _status ;
1588   __kernel_clock_t _utime ;
1589   __kernel_clock_t _stime ;
1590};
1591#line 48 "include/asm-generic/siginfo.h"
1592struct __anonstruct__sigfault_221 {
1593   void *_addr ;
1594   short _addr_lsb ;
1595};
1596#line 48 "include/asm-generic/siginfo.h"
1597struct __anonstruct__sigpoll_222 {
1598   long _band ;
1599   int _fd ;
1600};
1601#line 48 "include/asm-generic/siginfo.h"
1602union __anonunion__sifields_216 {
1603   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
1604   struct __anonstruct__kill_217 _kill ;
1605   struct __anonstruct__timer_218 _timer ;
1606   struct __anonstruct__rt_219 _rt ;
1607   struct __anonstruct__sigchld_220 _sigchld ;
1608   struct __anonstruct__sigfault_221 _sigfault ;
1609   struct __anonstruct__sigpoll_222 _sigpoll ;
1610};
1611#line 48 "include/asm-generic/siginfo.h"
1612struct siginfo {
1613   int si_signo ;
1614   int si_errno ;
1615   int si_code ;
1616   union __anonunion__sifields_216 _sifields ;
1617};
1618#line 48 "include/asm-generic/siginfo.h"
1619typedef struct siginfo siginfo_t;
1620#line 288
1621struct siginfo;
1622#line 10 "include/linux/signal.h"
1623struct task_struct;
1624#line 18
1625struct user_struct;
1626#line 28 "include/linux/signal.h"
1627struct sigpending {
1628   struct list_head list ;
1629   sigset_t signal ;
1630};
1631#line 239
1632struct timespec;
1633#line 240
1634struct pt_regs;
1635#line 50 "include/linux/pid.h"
1636struct pid_namespace;
1637#line 50 "include/linux/pid.h"
1638struct upid {
1639   int nr ;
1640   struct pid_namespace *ns ;
1641   struct hlist_node pid_chain ;
1642};
1643#line 57 "include/linux/pid.h"
1644struct pid {
1645   atomic_t count ;
1646   unsigned int level ;
1647   struct hlist_head tasks[3] ;
1648   struct rcu_head rcu ;
1649   struct upid numbers[1] ;
1650};
1651#line 69 "include/linux/pid.h"
1652struct pid_link {
1653   struct hlist_node node ;
1654   struct pid *pid ;
1655};
1656#line 100
1657struct pid_namespace;
1658#line 10 "include/linux/seccomp.h"
1659struct __anonstruct_seccomp_t_225 {
1660   int mode ;
1661};
1662#line 10 "include/linux/seccomp.h"
1663typedef struct __anonstruct_seccomp_t_225 seccomp_t;
1664#line 81 "include/linux/plist.h"
1665struct plist_head {
1666   struct list_head node_list ;
1667};
1668#line 85 "include/linux/plist.h"
1669struct plist_node {
1670   int prio ;
1671   struct list_head prio_list ;
1672   struct list_head node_list ;
1673};
1674#line 28 "include/linux/rtmutex.h"
1675struct rt_mutex {
1676   raw_spinlock_t wait_lock ;
1677   struct plist_head wait_list ;
1678   struct task_struct *owner ;
1679   int save_state ;
1680   char const   *name ;
1681   char const   *file ;
1682   int line ;
1683   void *magic ;
1684};
1685#line 40
1686struct rt_mutex_waiter;
1687#line 40
1688struct rt_mutex_waiter;
1689#line 42 "include/linux/resource.h"
1690struct rlimit {
1691   unsigned long rlim_cur ;
1692   unsigned long rlim_max ;
1693};
1694#line 81
1695struct task_struct;
1696#line 8 "include/linux/timerqueue.h"
1697struct timerqueue_node {
1698   struct rb_node node ;
1699   ktime_t expires ;
1700};
1701#line 13 "include/linux/timerqueue.h"
1702struct timerqueue_head {
1703   struct rb_root head ;
1704   struct timerqueue_node *next ;
1705};
1706#line 27 "include/linux/hrtimer.h"
1707struct hrtimer_clock_base;
1708#line 27
1709struct hrtimer_clock_base;
1710#line 28
1711struct hrtimer_cpu_base;
1712#line 28
1713struct hrtimer_cpu_base;
1714#line 44
1715enum hrtimer_restart {
1716    HRTIMER_NORESTART = 0,
1717    HRTIMER_RESTART = 1
1718} ;
1719#line 108 "include/linux/hrtimer.h"
1720struct hrtimer {
1721   struct timerqueue_node node ;
1722   ktime_t _softexpires ;
1723   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1724   struct hrtimer_clock_base *base ;
1725   unsigned long state ;
1726   int start_pid ;
1727   void *start_site ;
1728   char start_comm[16] ;
1729};
1730#line 145 "include/linux/hrtimer.h"
1731struct hrtimer_clock_base {
1732   struct hrtimer_cpu_base *cpu_base ;
1733   int index ;
1734   clockid_t clockid ;
1735   struct timerqueue_head active ;
1736   ktime_t resolution ;
1737   ktime_t (*get_time)(void) ;
1738   ktime_t softirq_time ;
1739   ktime_t offset ;
1740};
1741#line 178 "include/linux/hrtimer.h"
1742struct hrtimer_cpu_base {
1743   raw_spinlock_t lock ;
1744   unsigned long active_bases ;
1745   ktime_t expires_next ;
1746   int hres_active ;
1747   int hang_detected ;
1748   unsigned long nr_events ;
1749   unsigned long nr_retries ;
1750   unsigned long nr_hangs ;
1751   ktime_t max_hang_time ;
1752   struct hrtimer_clock_base clock_base[3] ;
1753};
1754#line 11 "include/linux/task_io_accounting.h"
1755struct task_io_accounting {
1756   u64 rchar ;
1757   u64 wchar ;
1758   u64 syscr ;
1759   u64 syscw ;
1760   u64 read_bytes ;
1761   u64 write_bytes ;
1762   u64 cancelled_write_bytes ;
1763};
1764#line 13 "include/linux/latencytop.h"
1765struct task_struct;
1766#line 20 "include/linux/latencytop.h"
1767struct latency_record {
1768   unsigned long backtrace[12] ;
1769   unsigned int count ;
1770   unsigned long time ;
1771   unsigned long max ;
1772};
1773#line 29 "include/linux/key.h"
1774typedef int32_t key_serial_t;
1775#line 32 "include/linux/key.h"
1776typedef uint32_t key_perm_t;
1777#line 34
1778struct key;
1779#line 34
1780struct key;
1781#line 75
1782struct user_struct;
1783#line 76
1784struct signal_struct;
1785#line 76
1786struct signal_struct;
1787#line 77
1788struct cred;
1789#line 79
1790struct key_type;
1791#line 79
1792struct key_type;
1793#line 81
1794struct keyring_list;
1795#line 81
1796struct keyring_list;
1797#line 124
1798struct key_user;
1799#line 124 "include/linux/key.h"
1800union __anonunion____missing_field_name_226 {
1801   time_t expiry ;
1802   time_t revoked_at ;
1803};
1804#line 124 "include/linux/key.h"
1805union __anonunion_type_data_227 {
1806   struct list_head link ;
1807   unsigned long x[2] ;
1808   void *p[2] ;
1809   int reject_error ;
1810};
1811#line 124 "include/linux/key.h"
1812union __anonunion_payload_228 {
1813   unsigned long value ;
1814   void *rcudata ;
1815   void *data ;
1816   struct keyring_list *subscriptions ;
1817};
1818#line 124 "include/linux/key.h"
1819struct key {
1820   atomic_t usage ;
1821   key_serial_t serial ;
1822   struct rb_node serial_node ;
1823   struct key_type *type ;
1824   struct rw_semaphore sem ;
1825   struct key_user *user ;
1826   void *security ;
1827   union __anonunion____missing_field_name_226 __annonCompField42 ;
1828   uid_t uid ;
1829   gid_t gid ;
1830   key_perm_t perm ;
1831   unsigned short quotalen ;
1832   unsigned short datalen ;
1833   unsigned long flags ;
1834   char *description ;
1835   union __anonunion_type_data_227 type_data ;
1836   union __anonunion_payload_228 payload ;
1837};
1838#line 18 "include/linux/selinux.h"
1839struct audit_context;
1840#line 18
1841struct audit_context;
1842#line 21 "include/linux/cred.h"
1843struct user_struct;
1844#line 22
1845struct cred;
1846#line 31 "include/linux/cred.h"
1847struct group_info {
1848   atomic_t usage ;
1849   int ngroups ;
1850   int nblocks ;
1851   gid_t small_block[32] ;
1852   gid_t *blocks[0] ;
1853};
1854#line 83 "include/linux/cred.h"
1855struct thread_group_cred {
1856   atomic_t usage ;
1857   pid_t tgid ;
1858   spinlock_t lock ;
1859   struct key *session_keyring ;
1860   struct key *process_keyring ;
1861   struct rcu_head rcu ;
1862};
1863#line 116 "include/linux/cred.h"
1864struct cred {
1865   atomic_t usage ;
1866   atomic_t subscribers ;
1867   void *put_addr ;
1868   unsigned int magic ;
1869   uid_t uid ;
1870   gid_t gid ;
1871   uid_t suid ;
1872   gid_t sgid ;
1873   uid_t euid ;
1874   gid_t egid ;
1875   uid_t fsuid ;
1876   gid_t fsgid ;
1877   unsigned int securebits ;
1878   kernel_cap_t cap_inheritable ;
1879   kernel_cap_t cap_permitted ;
1880   kernel_cap_t cap_effective ;
1881   kernel_cap_t cap_bset ;
1882   unsigned char jit_keyring ;
1883   struct key *thread_keyring ;
1884   struct key *request_key_auth ;
1885   struct thread_group_cred *tgcred ;
1886   void *security ;
1887   struct user_struct *user ;
1888   struct user_namespace *user_ns ;
1889   struct group_info *group_info ;
1890   struct rcu_head rcu ;
1891};
1892#line 61 "include/linux/llist.h"
1893struct llist_node;
1894#line 65 "include/linux/llist.h"
1895struct llist_node {
1896   struct llist_node *next ;
1897};
1898#line 97 "include/linux/sched.h"
1899struct futex_pi_state;
1900#line 97
1901struct futex_pi_state;
1902#line 98
1903struct robust_list_head;
1904#line 98
1905struct robust_list_head;
1906#line 99
1907struct bio_list;
1908#line 99
1909struct bio_list;
1910#line 100
1911struct fs_struct;
1912#line 100
1913struct fs_struct;
1914#line 101
1915struct perf_event_context;
1916#line 101
1917struct perf_event_context;
1918#line 102
1919struct blk_plug;
1920#line 102
1921struct blk_plug;
1922#line 151
1923struct cfs_rq;
1924#line 151
1925struct cfs_rq;
1926#line 259
1927struct task_struct;
1928#line 366
1929struct nsproxy;
1930#line 367
1931struct user_namespace;
1932#line 214 "include/linux/aio.h"
1933struct mm_struct;
1934#line 443 "include/linux/sched.h"
1935struct sighand_struct {
1936   atomic_t count ;
1937   struct k_sigaction action[64] ;
1938   spinlock_t siglock ;
1939   wait_queue_head_t signalfd_wqh ;
1940};
1941#line 450 "include/linux/sched.h"
1942struct pacct_struct {
1943   int ac_flag ;
1944   long ac_exitcode ;
1945   unsigned long ac_mem ;
1946   cputime_t ac_utime ;
1947   cputime_t ac_stime ;
1948   unsigned long ac_minflt ;
1949   unsigned long ac_majflt ;
1950};
1951#line 458 "include/linux/sched.h"
1952struct cpu_itimer {
1953   cputime_t expires ;
1954   cputime_t incr ;
1955   u32 error ;
1956   u32 incr_error ;
1957};
1958#line 476 "include/linux/sched.h"
1959struct task_cputime {
1960   cputime_t utime ;
1961   cputime_t stime ;
1962   unsigned long long sum_exec_runtime ;
1963};
1964#line 512 "include/linux/sched.h"
1965struct thread_group_cputimer {
1966   struct task_cputime cputime ;
1967   int running ;
1968   raw_spinlock_t lock ;
1969};
1970#line 519
1971struct autogroup;
1972#line 519
1973struct autogroup;
1974#line 528
1975struct tty_struct;
1976#line 528
1977struct taskstats;
1978#line 528
1979struct tty_audit_buf;
1980#line 528 "include/linux/sched.h"
1981struct signal_struct {
1982   atomic_t sigcnt ;
1983   atomic_t live ;
1984   int nr_threads ;
1985   wait_queue_head_t wait_chldexit ;
1986   struct task_struct *curr_target ;
1987   struct sigpending shared_pending ;
1988   int group_exit_code ;
1989   int notify_count ;
1990   struct task_struct *group_exit_task ;
1991   int group_stop_count ;
1992   unsigned int flags ;
1993   unsigned int is_child_subreaper : 1 ;
1994   unsigned int has_child_subreaper : 1 ;
1995   struct list_head posix_timers ;
1996   struct hrtimer real_timer ;
1997   struct pid *leader_pid ;
1998   ktime_t it_real_incr ;
1999   struct cpu_itimer it[2] ;
2000   struct thread_group_cputimer cputimer ;
2001   struct task_cputime cputime_expires ;
2002   struct list_head cpu_timers[3] ;
2003   struct pid *tty_old_pgrp ;
2004   int leader ;
2005   struct tty_struct *tty ;
2006   struct autogroup *autogroup ;
2007   cputime_t utime ;
2008   cputime_t stime ;
2009   cputime_t cutime ;
2010   cputime_t cstime ;
2011   cputime_t gtime ;
2012   cputime_t cgtime ;
2013   cputime_t prev_utime ;
2014   cputime_t prev_stime ;
2015   unsigned long nvcsw ;
2016   unsigned long nivcsw ;
2017   unsigned long cnvcsw ;
2018   unsigned long cnivcsw ;
2019   unsigned long min_flt ;
2020   unsigned long maj_flt ;
2021   unsigned long cmin_flt ;
2022   unsigned long cmaj_flt ;
2023   unsigned long inblock ;
2024   unsigned long oublock ;
2025   unsigned long cinblock ;
2026   unsigned long coublock ;
2027   unsigned long maxrss ;
2028   unsigned long cmaxrss ;
2029   struct task_io_accounting ioac ;
2030   unsigned long long sum_sched_runtime ;
2031   struct rlimit rlim[16] ;
2032   struct pacct_struct pacct ;
2033   struct taskstats *stats ;
2034   unsigned int audit_tty ;
2035   struct tty_audit_buf *tty_audit_buf ;
2036   struct rw_semaphore group_rwsem ;
2037   int oom_adj ;
2038   int oom_score_adj ;
2039   int oom_score_adj_min ;
2040   struct mutex cred_guard_mutex ;
2041};
2042#line 703 "include/linux/sched.h"
2043struct user_struct {
2044   atomic_t __count ;
2045   atomic_t processes ;
2046   atomic_t files ;
2047   atomic_t sigpending ;
2048   atomic_t inotify_watches ;
2049   atomic_t inotify_devs ;
2050   atomic_t fanotify_listeners ;
2051   atomic_long_t epoll_watches ;
2052   unsigned long mq_bytes ;
2053   unsigned long locked_shm ;
2054   struct key *uid_keyring ;
2055   struct key *session_keyring ;
2056   struct hlist_node uidhash_node ;
2057   uid_t uid ;
2058   struct user_namespace *user_ns ;
2059   atomic_long_t locked_vm ;
2060};
2061#line 747
2062struct backing_dev_info;
2063#line 747
2064struct backing_dev_info;
2065#line 748
2066struct reclaim_state;
2067#line 748
2068struct reclaim_state;
2069#line 751 "include/linux/sched.h"
2070struct sched_info {
2071   unsigned long pcount ;
2072   unsigned long long run_delay ;
2073   unsigned long long last_arrival ;
2074   unsigned long long last_queued ;
2075};
2076#line 763 "include/linux/sched.h"
2077struct task_delay_info {
2078   spinlock_t lock ;
2079   unsigned int flags ;
2080   struct timespec blkio_start ;
2081   struct timespec blkio_end ;
2082   u64 blkio_delay ;
2083   u64 swapin_delay ;
2084   u32 blkio_count ;
2085   u32 swapin_count ;
2086   struct timespec freepages_start ;
2087   struct timespec freepages_end ;
2088   u64 freepages_delay ;
2089   u32 freepages_count ;
2090};
2091#line 1088
2092struct io_context;
2093#line 1088
2094struct io_context;
2095#line 1097
2096struct audit_context;
2097#line 1098
2098struct mempolicy;
2099#line 1099
2100struct pipe_inode_info;
2101#line 1099
2102struct pipe_inode_info;
2103#line 1102
2104struct rq;
2105#line 1102
2106struct rq;
2107#line 1122 "include/linux/sched.h"
2108struct sched_class {
2109   struct sched_class  const  *next ;
2110   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2111   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2112   void (*yield_task)(struct rq *rq ) ;
2113   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
2114   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
2115   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
2116   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
2117   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
2118   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
2119   void (*post_schedule)(struct rq *this_rq ) ;
2120   void (*task_waking)(struct task_struct *task ) ;
2121   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
2122   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
2123   void (*rq_online)(struct rq *rq ) ;
2124   void (*rq_offline)(struct rq *rq ) ;
2125   void (*set_curr_task)(struct rq *rq ) ;
2126   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
2127   void (*task_fork)(struct task_struct *p ) ;
2128   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
2129   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
2130   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
2131   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
2132   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
2133};
2134#line 1167 "include/linux/sched.h"
2135struct load_weight {
2136   unsigned long weight ;
2137   unsigned long inv_weight ;
2138};
2139#line 1172 "include/linux/sched.h"
2140struct sched_statistics {
2141   u64 wait_start ;
2142   u64 wait_max ;
2143   u64 wait_count ;
2144   u64 wait_sum ;
2145   u64 iowait_count ;
2146   u64 iowait_sum ;
2147   u64 sleep_start ;
2148   u64 sleep_max ;
2149   s64 sum_sleep_runtime ;
2150   u64 block_start ;
2151   u64 block_max ;
2152   u64 exec_max ;
2153   u64 slice_max ;
2154   u64 nr_migrations_cold ;
2155   u64 nr_failed_migrations_affine ;
2156   u64 nr_failed_migrations_running ;
2157   u64 nr_failed_migrations_hot ;
2158   u64 nr_forced_migrations ;
2159   u64 nr_wakeups ;
2160   u64 nr_wakeups_sync ;
2161   u64 nr_wakeups_migrate ;
2162   u64 nr_wakeups_local ;
2163   u64 nr_wakeups_remote ;
2164   u64 nr_wakeups_affine ;
2165   u64 nr_wakeups_affine_attempts ;
2166   u64 nr_wakeups_passive ;
2167   u64 nr_wakeups_idle ;
2168};
2169#line 1207 "include/linux/sched.h"
2170struct sched_entity {
2171   struct load_weight load ;
2172   struct rb_node run_node ;
2173   struct list_head group_node ;
2174   unsigned int on_rq ;
2175   u64 exec_start ;
2176   u64 sum_exec_runtime ;
2177   u64 vruntime ;
2178   u64 prev_sum_exec_runtime ;
2179   u64 nr_migrations ;
2180   struct sched_statistics statistics ;
2181   struct sched_entity *parent ;
2182   struct cfs_rq *cfs_rq ;
2183   struct cfs_rq *my_q ;
2184};
2185#line 1233
2186struct rt_rq;
2187#line 1233 "include/linux/sched.h"
2188struct sched_rt_entity {
2189   struct list_head run_list ;
2190   unsigned long timeout ;
2191   unsigned int time_slice ;
2192   int nr_cpus_allowed ;
2193   struct sched_rt_entity *back ;
2194   struct sched_rt_entity *parent ;
2195   struct rt_rq *rt_rq ;
2196   struct rt_rq *my_q ;
2197};
2198#line 1264
2199struct files_struct;
2200#line 1264
2201struct css_set;
2202#line 1264
2203struct compat_robust_list_head;
2204#line 1264
2205struct mem_cgroup;
2206#line 1264 "include/linux/sched.h"
2207struct memcg_batch_info {
2208   int do_batch ;
2209   struct mem_cgroup *memcg ;
2210   unsigned long nr_pages ;
2211   unsigned long memsw_nr_pages ;
2212};
2213#line 1264 "include/linux/sched.h"
2214struct task_struct {
2215   long volatile   state ;
2216   void *stack ;
2217   atomic_t usage ;
2218   unsigned int flags ;
2219   unsigned int ptrace ;
2220   struct llist_node wake_entry ;
2221   int on_cpu ;
2222   int on_rq ;
2223   int prio ;
2224   int static_prio ;
2225   int normal_prio ;
2226   unsigned int rt_priority ;
2227   struct sched_class  const  *sched_class ;
2228   struct sched_entity se ;
2229   struct sched_rt_entity rt ;
2230   struct hlist_head preempt_notifiers ;
2231   unsigned char fpu_counter ;
2232   unsigned int policy ;
2233   cpumask_t cpus_allowed ;
2234   struct sched_info sched_info ;
2235   struct list_head tasks ;
2236   struct plist_node pushable_tasks ;
2237   struct mm_struct *mm ;
2238   struct mm_struct *active_mm ;
2239   unsigned int brk_randomized : 1 ;
2240   int exit_state ;
2241   int exit_code ;
2242   int exit_signal ;
2243   int pdeath_signal ;
2244   unsigned int jobctl ;
2245   unsigned int personality ;
2246   unsigned int did_exec : 1 ;
2247   unsigned int in_execve : 1 ;
2248   unsigned int in_iowait : 1 ;
2249   unsigned int sched_reset_on_fork : 1 ;
2250   unsigned int sched_contributes_to_load : 1 ;
2251   unsigned int irq_thread : 1 ;
2252   pid_t pid ;
2253   pid_t tgid ;
2254   unsigned long stack_canary ;
2255   struct task_struct *real_parent ;
2256   struct task_struct *parent ;
2257   struct list_head children ;
2258   struct list_head sibling ;
2259   struct task_struct *group_leader ;
2260   struct list_head ptraced ;
2261   struct list_head ptrace_entry ;
2262   struct pid_link pids[3] ;
2263   struct list_head thread_group ;
2264   struct completion *vfork_done ;
2265   int *set_child_tid ;
2266   int *clear_child_tid ;
2267   cputime_t utime ;
2268   cputime_t stime ;
2269   cputime_t utimescaled ;
2270   cputime_t stimescaled ;
2271   cputime_t gtime ;
2272   cputime_t prev_utime ;
2273   cputime_t prev_stime ;
2274   unsigned long nvcsw ;
2275   unsigned long nivcsw ;
2276   struct timespec start_time ;
2277   struct timespec real_start_time ;
2278   unsigned long min_flt ;
2279   unsigned long maj_flt ;
2280   struct task_cputime cputime_expires ;
2281   struct list_head cpu_timers[3] ;
2282   struct cred  const  *real_cred ;
2283   struct cred  const  *cred ;
2284   struct cred *replacement_session_keyring ;
2285   char comm[16] ;
2286   int link_count ;
2287   int total_link_count ;
2288   struct sysv_sem sysvsem ;
2289   unsigned long last_switch_count ;
2290   struct thread_struct thread ;
2291   struct fs_struct *fs ;
2292   struct files_struct *files ;
2293   struct nsproxy *nsproxy ;
2294   struct signal_struct *signal ;
2295   struct sighand_struct *sighand ;
2296   sigset_t blocked ;
2297   sigset_t real_blocked ;
2298   sigset_t saved_sigmask ;
2299   struct sigpending pending ;
2300   unsigned long sas_ss_sp ;
2301   size_t sas_ss_size ;
2302   int (*notifier)(void *priv ) ;
2303   void *notifier_data ;
2304   sigset_t *notifier_mask ;
2305   struct audit_context *audit_context ;
2306   uid_t loginuid ;
2307   unsigned int sessionid ;
2308   seccomp_t seccomp ;
2309   u32 parent_exec_id ;
2310   u32 self_exec_id ;
2311   spinlock_t alloc_lock ;
2312   raw_spinlock_t pi_lock ;
2313   struct plist_head pi_waiters ;
2314   struct rt_mutex_waiter *pi_blocked_on ;
2315   struct mutex_waiter *blocked_on ;
2316   unsigned int irq_events ;
2317   unsigned long hardirq_enable_ip ;
2318   unsigned long hardirq_disable_ip ;
2319   unsigned int hardirq_enable_event ;
2320   unsigned int hardirq_disable_event ;
2321   int hardirqs_enabled ;
2322   int hardirq_context ;
2323   unsigned long softirq_disable_ip ;
2324   unsigned long softirq_enable_ip ;
2325   unsigned int softirq_disable_event ;
2326   unsigned int softirq_enable_event ;
2327   int softirqs_enabled ;
2328   int softirq_context ;
2329   void *journal_info ;
2330   struct bio_list *bio_list ;
2331   struct blk_plug *plug ;
2332   struct reclaim_state *reclaim_state ;
2333   struct backing_dev_info *backing_dev_info ;
2334   struct io_context *io_context ;
2335   unsigned long ptrace_message ;
2336   siginfo_t *last_siginfo ;
2337   struct task_io_accounting ioac ;
2338   u64 acct_rss_mem1 ;
2339   u64 acct_vm_mem1 ;
2340   cputime_t acct_timexpd ;
2341   nodemask_t mems_allowed ;
2342   seqcount_t mems_allowed_seq ;
2343   int cpuset_mem_spread_rotor ;
2344   int cpuset_slab_spread_rotor ;
2345   struct css_set *cgroups ;
2346   struct list_head cg_list ;
2347   struct robust_list_head *robust_list ;
2348   struct compat_robust_list_head *compat_robust_list ;
2349   struct list_head pi_state_list ;
2350   struct futex_pi_state *pi_state_cache ;
2351   struct perf_event_context *perf_event_ctxp[2] ;
2352   struct mutex perf_event_mutex ;
2353   struct list_head perf_event_list ;
2354   struct mempolicy *mempolicy ;
2355   short il_next ;
2356   short pref_node_fork ;
2357   struct rcu_head rcu ;
2358   struct pipe_inode_info *splice_pipe ;
2359   struct task_delay_info *delays ;
2360   int make_it_fail ;
2361   int nr_dirtied ;
2362   int nr_dirtied_pause ;
2363   unsigned long dirty_paused_when ;
2364   int latency_record_count ;
2365   struct latency_record latency_record[32] ;
2366   unsigned long timer_slack_ns ;
2367   unsigned long default_timer_slack_ns ;
2368   struct list_head *scm_work_list ;
2369   unsigned long trace ;
2370   unsigned long trace_recursion ;
2371   struct memcg_batch_info memcg_batch ;
2372   atomic_t ptrace_bp_refcnt ;
2373};
2374#line 1681
2375struct pid_namespace;
2376#line 28 "include/linux/of.h"
2377typedef u32 phandle;
2378#line 31 "include/linux/of.h"
2379struct property {
2380   char *name ;
2381   int length ;
2382   void *value ;
2383   struct property *next ;
2384   unsigned long _flags ;
2385   unsigned int unique_id ;
2386};
2387#line 44
2388struct proc_dir_entry;
2389#line 44 "include/linux/of.h"
2390struct device_node {
2391   char const   *name ;
2392   char const   *type ;
2393   phandle phandle ;
2394   char *full_name ;
2395   struct property *properties ;
2396   struct property *deadprops ;
2397   struct device_node *parent ;
2398   struct device_node *child ;
2399   struct device_node *sibling ;
2400   struct device_node *next ;
2401   struct device_node *allnext ;
2402   struct proc_dir_entry *pde ;
2403   struct kref kref ;
2404   unsigned long _flags ;
2405   void *data ;
2406};
2407#line 44 "include/linux/i2c.h"
2408struct i2c_msg;
2409#line 44
2410struct i2c_msg;
2411#line 45
2412struct i2c_algorithm;
2413#line 45
2414struct i2c_algorithm;
2415#line 46
2416struct i2c_adapter;
2417#line 46
2418struct i2c_adapter;
2419#line 49
2420union i2c_smbus_data;
2421#line 49
2422union i2c_smbus_data;
2423#line 52
2424struct module;
2425#line 352 "include/linux/i2c.h"
2426struct i2c_algorithm {
2427   int (*master_xfer)(struct i2c_adapter *adap , struct i2c_msg *msgs , int num ) ;
2428   int (*smbus_xfer)(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2429                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2430   u32 (*functionality)(struct i2c_adapter * ) ;
2431};
2432#line 373 "include/linux/i2c.h"
2433struct i2c_adapter {
2434   struct module *owner ;
2435   unsigned int class ;
2436   struct i2c_algorithm  const  *algo ;
2437   void *algo_data ;
2438   struct rt_mutex bus_lock ;
2439   int timeout ;
2440   int retries ;
2441   struct device dev ;
2442   int nr ;
2443   char name[48] ;
2444   struct completion dev_released ;
2445   struct mutex userspace_clients_lock ;
2446   struct list_head userspace_clients ;
2447};
2448#line 538 "include/linux/i2c.h"
2449struct i2c_msg {
2450   __u16 addr ;
2451   __u16 flags ;
2452   __u16 len ;
2453   __u8 *buf ;
2454};
2455#line 596 "include/linux/i2c.h"
2456union i2c_smbus_data {
2457   __u8 byte ;
2458   __u16 word ;
2459   __u8 block[34] ;
2460};
2461#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2462struct __anonstruct_232 {
2463   int  : 0 ;
2464};
2465#line 46 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2466struct stub_chip {
2467   u8 pointer ;
2468   u16 words[256] ;
2469};
2470#line 1 "<compiler builtins>"
2471long __builtin_expect(long val , long res ) ;
2472#line 100 "include/linux/printk.h"
2473extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
2474#line 49 "include/linux/dynamic_debug.h"
2475extern int ( /* format attribute */  __dynamic_dev_dbg)(struct _ddebug *descriptor ,
2476                                                        struct device  const  *dev ,
2477                                                        char const   *fmt  , ...) ;
2478#line 152 "include/linux/mutex.h"
2479void mutex_lock(struct mutex *lock ) ;
2480#line 153
2481int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2482#line 154
2483int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2484#line 168
2485int mutex_trylock(struct mutex *lock ) ;
2486#line 169
2487void mutex_unlock(struct mutex *lock ) ;
2488#line 170
2489int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2490#line 351 "include/linux/moduleparam.h"
2491extern struct kernel_param_ops param_ops_ushort ;
2492#line 371
2493extern struct kernel_param_ops param_ops_ulong ;
2494#line 437
2495extern struct kernel_param_ops param_array_ops ;
2496#line 26 "include/linux/export.h"
2497extern struct module __this_module ;
2498#line 67 "include/linux/module.h"
2499int init_module(void) ;
2500#line 68
2501void cleanup_module(void) ;
2502#line 161 "include/linux/slab.h"
2503extern void kfree(void const   * ) ;
2504#line 221 "include/linux/slub_def.h"
2505extern void *__kmalloc(size_t size , gfp_t flags ) ;
2506#line 268
2507__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2508                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2509#line 268 "include/linux/slub_def.h"
2510__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2511                                                                    gfp_t flags ) 
2512{ void *tmp___2 ;
2513
2514  {
2515  {
2516#line 283
2517  tmp___2 = __kmalloc(size, flags);
2518  }
2519#line 283
2520  return (tmp___2);
2521}
2522}
2523#line 349 "include/linux/slab.h"
2524__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2525#line 349 "include/linux/slab.h"
2526__inline static void *kzalloc(size_t size , gfp_t flags ) 
2527{ void *tmp ;
2528  unsigned int __cil_tmp4 ;
2529
2530  {
2531  {
2532#line 351
2533  __cil_tmp4 = flags | 32768U;
2534#line 351
2535  tmp = kmalloc(size, __cil_tmp4);
2536  }
2537#line 351
2538  return (tmp);
2539}
2540}
2541#line 446 "include/linux/i2c.h"
2542extern int i2c_add_adapter(struct i2c_adapter * ) ;
2543#line 447
2544extern int i2c_del_adapter(struct i2c_adapter * ) ;
2545#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2546static unsigned short chip_addr[10]  ;
2547#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2548static struct kparam_array  const  __param_arr_chip_addr  =    {(unsigned int )(sizeof(chip_addr) / sizeof(chip_addr[0]) + sizeof(struct __anonstruct_232 )),
2549    (unsigned int )sizeof(chip_addr[0]), (unsigned int *)((void *)0), (struct kernel_param_ops  const  *)(& param_ops_ushort),
2550    (void *)(chip_addr)};
2551#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2552static char const   __param_str_chip_addr[10]  = 
2553#line 38
2554  {      (char const   )'c',      (char const   )'h',      (char const   )'i',      (char const   )'p', 
2555        (char const   )'_',      (char const   )'a',      (char const   )'d',      (char const   )'d', 
2556        (char const   )'r',      (char const   )'\000'};
2557#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2558static struct kernel_param  const  __param_chip_addr  __attribute__((__used__, __unused__,
2559__section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_chip_addr, (struct kernel_param_ops  const  *)(& param_array_ops),
2560    (u16 )292, (s16 )0, {.arr = & __param_arr_chip_addr}};
2561#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2562static char const   __mod_chip_addrtype38[35]  __attribute__((__used__, __unused__,
2563__section__(".modinfo"), __aligned__(1)))  = 
2564#line 38
2565  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2566        (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
2567        (char const   )'=',      (char const   )'c',      (char const   )'h',      (char const   )'i', 
2568        (char const   )'p',      (char const   )'_',      (char const   )'a',      (char const   )'d', 
2569        (char const   )'d',      (char const   )'r',      (char const   )':',      (char const   )'a', 
2570        (char const   )'r',      (char const   )'r',      (char const   )'a',      (char const   )'y', 
2571        (char const   )' ',      (char const   )'o',      (char const   )'f',      (char const   )' ', 
2572        (char const   )'u',      (char const   )'s',      (char const   )'h',      (char const   )'o', 
2573        (char const   )'r',      (char const   )'t',      (char const   )'\000'};
2574#line 39 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2575static char const   __mod_chip_addr40[64]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2576__aligned__(1)))  = 
2577#line 39
2578  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2579        (char const   )'=',      (char const   )'c',      (char const   )'h',      (char const   )'i', 
2580        (char const   )'p',      (char const   )'_',      (char const   )'a',      (char const   )'d', 
2581        (char const   )'d',      (char const   )'r',      (char const   )':',      (char const   )'C', 
2582        (char const   )'h',      (char const   )'i',      (char const   )'p',      (char const   )' ', 
2583        (char const   )'a',      (char const   )'d',      (char const   )'d',      (char const   )'r', 
2584        (char const   )'e',      (char const   )'s',      (char const   )'s',      (char const   )'e', 
2585        (char const   )'s',      (char const   )' ',      (char const   )'(',      (char const   )'u', 
2586        (char const   )'p',      (char const   )' ',      (char const   )'t',      (char const   )'o', 
2587        (char const   )' ',      (char const   )'1',      (char const   )'0',      (char const   )',', 
2588        (char const   )' ',      (char const   )'b',      (char const   )'e',      (char const   )'t', 
2589        (char const   )'w',      (char const   )'e',      (char const   )'e',      (char const   )'n', 
2590        (char const   )' ',      (char const   )'0',      (char const   )'x',      (char const   )'0', 
2591        (char const   )'3',      (char const   )' ',      (char const   )'a',      (char const   )'n', 
2592        (char const   )'d',      (char const   )' ',      (char const   )'0',      (char const   )'x', 
2593        (char const   )'7',      (char const   )'7',      (char const   )')',      (char const   )'\000'};
2594#line 42 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2595static unsigned long functionality  =    209649664UL;
2596#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2597static char const   __param_str_functionality[14]  = 
2598#line 43
2599  {      (char const   )'f',      (char const   )'u',      (char const   )'n',      (char const   )'c', 
2600        (char const   )'t',      (char const   )'i',      (char const   )'o',      (char const   )'n', 
2601        (char const   )'a',      (char const   )'l',      (char const   )'i',      (char const   )'t', 
2602        (char const   )'y',      (char const   )'\000'};
2603#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2604static struct kernel_param  const  __param_functionality  __attribute__((__used__,
2605__unused__, __section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_functionality, (struct kernel_param_ops  const  *)(& param_ops_ulong),
2606    (u16 )420, (s16 )0, {(void *)(& functionality)}};
2607#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2608static char const   __mod_functionalitytype43[29]  __attribute__((__used__, __unused__,
2609__section__(".modinfo"), __aligned__(1)))  = 
2610#line 43
2611  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2612        (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
2613        (char const   )'=',      (char const   )'f',      (char const   )'u',      (char const   )'n', 
2614        (char const   )'c',      (char const   )'t',      (char const   )'i',      (char const   )'o', 
2615        (char const   )'n',      (char const   )'a',      (char const   )'l',      (char const   )'i', 
2616        (char const   )'t',      (char const   )'y',      (char const   )':',      (char const   )'u', 
2617        (char const   )'l',      (char const   )'o',      (char const   )'n',      (char const   )'g', 
2618        (char const   )'\000'};
2619#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2620static char const   __mod_functionality44[51]  __attribute__((__used__, __unused__,
2621__section__(".modinfo"), __aligned__(1)))  = 
2622#line 44
2623  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2624        (char const   )'=',      (char const   )'f',      (char const   )'u',      (char const   )'n', 
2625        (char const   )'c',      (char const   )'t',      (char const   )'i',      (char const   )'o', 
2626        (char const   )'n',      (char const   )'a',      (char const   )'l',      (char const   )'i', 
2627        (char const   )'t',      (char const   )'y',      (char const   )':',      (char const   )'O', 
2628        (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )'r', 
2629        (char const   )'i',      (char const   )'d',      (char const   )'e',      (char const   )' ', 
2630        (char const   )'f',      (char const   )'u',      (char const   )'n',      (char const   )'c', 
2631        (char const   )'t',      (char const   )'i',      (char const   )'o',      (char const   )'n', 
2632        (char const   )'a',      (char const   )'l',      (char const   )'i',      (char const   )'t', 
2633        (char const   )'y',      (char const   )' ',      (char const   )'b',      (char const   )'i', 
2634        (char const   )'t',      (char const   )'f',      (char const   )'i',      (char const   )'e', 
2635        (char const   )'l',      (char const   )'d',      (char const   )'\000'};
2636#line 52 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2637static struct stub_chip *stub_chips  ;
2638#line 75
2639static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2640                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2641#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2642static struct _ddebug  __attribute__((__aligned__(8))) descriptor  __attribute__((__used__,
2643__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2644    "smbus quick - addr 0x%02x\n", 75U, 1U};
2645#line 82
2646static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2647                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2648#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2649static struct _ddebug  __attribute__((__aligned__(8))) descriptor___0  __attribute__((__used__,
2650__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2651    "smbus byte - addr 0x%02x, wrote 0x%02x.\n", 84U, 1U};
2652#line 87
2653static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2654                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2655#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2656static struct _ddebug  __attribute__((__aligned__(8))) descriptor___1  __attribute__((__used__,
2657__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2658    "smbus byte - addr 0x%02x, read  0x%02x.\n", 89U, 1U};
2659#line 99
2660static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2661                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2662#line 99 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2663static struct _ddebug  __attribute__((__aligned__(8))) descriptor___2  __attribute__((__used__,
2664__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2665    "smbus byte data - addr 0x%02x, wrote 0x%02x at 0x%02x.\n", 101U, 1U};
2666#line 104
2667static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2668                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2669#line 104 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2670static struct _ddebug  __attribute__((__aligned__(8))) descriptor___3  __attribute__((__used__,
2671__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2672    "smbus byte data - addr 0x%02x, read  0x%02x at 0x%02x.\n", 106U, 1U};
2673#line 116
2674static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2675                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2676#line 116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2677static struct _ddebug  __attribute__((__aligned__(8))) descriptor___4  __attribute__((__used__,
2678__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2679    "smbus word data - addr 0x%02x, wrote 0x%04x at 0x%02x.\n", 118U, 1U};
2680#line 121
2681static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2682                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2683#line 121 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2684static struct _ddebug  __attribute__((__aligned__(8))) descriptor___5  __attribute__((__used__,
2685__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2686    "smbus word data - addr 0x%02x, read  0x%04x at 0x%02x.\n", 123U, 1U};
2687#line 136
2688static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2689                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2690#line 136 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2691static struct _ddebug  __attribute__((__aligned__(8))) descriptor___6  __attribute__((__used__,
2692__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2693    "i2c block data - addr 0x%02x, wrote %d bytes at 0x%02x.\n", 138U, 1U};
2694#line 144
2695static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2696                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2697#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2698static struct _ddebug  __attribute__((__aligned__(8))) descriptor___7  __attribute__((__used__,
2699__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2700    "i2c block data - addr 0x%02x, read  %d bytes at 0x%02x.\n", 146U, 1U};
2701#line 153
2702static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2703                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2704#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2705static struct _ddebug  __attribute__((__aligned__(8))) descriptor___8  __attribute__((__used__,
2706__section__("__verbose")))  =    {"i2c_stub", "stub_xfer", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c",
2707    "Unsupported I2C/SMBus command\n", 153U, 1U};
2708#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
2709static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2710                     char read_write , u8 command , int size , union i2c_smbus_data *data ) 
2711{ s32 ret ;
2712  int i ;
2713  int len ;
2714  struct stub_chip *chip ;
2715  long tmp___7 ;
2716  long tmp___8 ;
2717  u8 tmp___9 ;
2718  long tmp___10 ;
2719  long tmp___11 ;
2720  long tmp___12 ;
2721  long tmp___13 ;
2722  long tmp___14 ;
2723  long tmp___15 ;
2724  long tmp___16 ;
2725  long tmp___17 ;
2726  void *__cil_tmp23 ;
2727  unsigned long __cil_tmp24 ;
2728  unsigned long __cil_tmp25 ;
2729  unsigned long __cil_tmp26 ;
2730  unsigned long __cil_tmp27 ;
2731  unsigned short __cil_tmp28 ;
2732  int __cil_tmp29 ;
2733  int __cil_tmp30 ;
2734  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp31 ;
2735  unsigned int __cil_tmp32 ;
2736  unsigned int __cil_tmp33 ;
2737  int __cil_tmp34 ;
2738  int __cil_tmp35 ;
2739  long __cil_tmp36 ;
2740  unsigned long __cil_tmp37 ;
2741  unsigned long __cil_tmp38 ;
2742  struct device *__cil_tmp39 ;
2743  struct device  const  *__cil_tmp40 ;
2744  int __cil_tmp41 ;
2745  int __cil_tmp42 ;
2746  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp43 ;
2747  unsigned int __cil_tmp44 ;
2748  unsigned int __cil_tmp45 ;
2749  int __cil_tmp46 ;
2750  int __cil_tmp47 ;
2751  long __cil_tmp48 ;
2752  unsigned long __cil_tmp49 ;
2753  unsigned long __cil_tmp50 ;
2754  struct device *__cil_tmp51 ;
2755  struct device  const  *__cil_tmp52 ;
2756  int __cil_tmp53 ;
2757  int __cil_tmp54 ;
2758  u8 __cil_tmp55 ;
2759  int __cil_tmp56 ;
2760  int __cil_tmp57 ;
2761  unsigned long __cil_tmp58 ;
2762  unsigned long __cil_tmp59 ;
2763  unsigned long __cil_tmp60 ;
2764  unsigned long __cil_tmp61 ;
2765  u16 __cil_tmp62 ;
2766  int __cil_tmp63 ;
2767  int __cil_tmp64 ;
2768  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp65 ;
2769  unsigned int __cil_tmp66 ;
2770  unsigned int __cil_tmp67 ;
2771  int __cil_tmp68 ;
2772  int __cil_tmp69 ;
2773  long __cil_tmp70 ;
2774  unsigned long __cil_tmp71 ;
2775  unsigned long __cil_tmp72 ;
2776  struct device *__cil_tmp73 ;
2777  struct device  const  *__cil_tmp74 ;
2778  int __cil_tmp75 ;
2779  __u8 __cil_tmp76 ;
2780  int __cil_tmp77 ;
2781  int __cil_tmp78 ;
2782  unsigned long __cil_tmp79 ;
2783  unsigned long __cil_tmp80 ;
2784  unsigned long __cil_tmp81 ;
2785  unsigned long __cil_tmp82 ;
2786  unsigned long __cil_tmp83 ;
2787  unsigned long __cil_tmp84 ;
2788  unsigned long __cil_tmp85 ;
2789  unsigned long __cil_tmp86 ;
2790  u16 __cil_tmp87 ;
2791  int __cil_tmp88 ;
2792  int __cil_tmp89 ;
2793  unsigned long __cil_tmp90 ;
2794  unsigned long __cil_tmp91 ;
2795  unsigned long __cil_tmp92 ;
2796  unsigned long __cil_tmp93 ;
2797  __u8 __cil_tmp94 ;
2798  int __cil_tmp95 ;
2799  unsigned long __cil_tmp96 ;
2800  unsigned long __cil_tmp97 ;
2801  unsigned long __cil_tmp98 ;
2802  unsigned long __cil_tmp99 ;
2803  u16 __cil_tmp100 ;
2804  int __cil_tmp101 ;
2805  int __cil_tmp102 ;
2806  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp103 ;
2807  unsigned int __cil_tmp104 ;
2808  unsigned int __cil_tmp105 ;
2809  int __cil_tmp106 ;
2810  int __cil_tmp107 ;
2811  long __cil_tmp108 ;
2812  unsigned long __cil_tmp109 ;
2813  unsigned long __cil_tmp110 ;
2814  struct device *__cil_tmp111 ;
2815  struct device  const  *__cil_tmp112 ;
2816  int __cil_tmp113 ;
2817  __u8 __cil_tmp114 ;
2818  int __cil_tmp115 ;
2819  int __cil_tmp116 ;
2820  unsigned long __cil_tmp117 ;
2821  unsigned long __cil_tmp118 ;
2822  unsigned long __cil_tmp119 ;
2823  unsigned long __cil_tmp120 ;
2824  u16 __cil_tmp121 ;
2825  int __cil_tmp122 ;
2826  int __cil_tmp123 ;
2827  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp124 ;
2828  unsigned int __cil_tmp125 ;
2829  unsigned int __cil_tmp126 ;
2830  int __cil_tmp127 ;
2831  int __cil_tmp128 ;
2832  long __cil_tmp129 ;
2833  unsigned long __cil_tmp130 ;
2834  unsigned long __cil_tmp131 ;
2835  struct device *__cil_tmp132 ;
2836  struct device  const  *__cil_tmp133 ;
2837  int __cil_tmp134 ;
2838  __u8 __cil_tmp135 ;
2839  int __cil_tmp136 ;
2840  int __cil_tmp137 ;
2841  int __cil_tmp138 ;
2842  int __cil_tmp139 ;
2843  int __cil_tmp140 ;
2844  unsigned long __cil_tmp141 ;
2845  unsigned long __cil_tmp142 ;
2846  unsigned long __cil_tmp143 ;
2847  unsigned long __cil_tmp144 ;
2848  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp145 ;
2849  unsigned int __cil_tmp146 ;
2850  unsigned int __cil_tmp147 ;
2851  int __cil_tmp148 ;
2852  int __cil_tmp149 ;
2853  long __cil_tmp150 ;
2854  unsigned long __cil_tmp151 ;
2855  unsigned long __cil_tmp152 ;
2856  struct device *__cil_tmp153 ;
2857  struct device  const  *__cil_tmp154 ;
2858  int __cil_tmp155 ;
2859  __u16 __cil_tmp156 ;
2860  int __cil_tmp157 ;
2861  int __cil_tmp158 ;
2862  unsigned long __cil_tmp159 ;
2863  unsigned long __cil_tmp160 ;
2864  unsigned long __cil_tmp161 ;
2865  unsigned long __cil_tmp162 ;
2866  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp163 ;
2867  unsigned int __cil_tmp164 ;
2868  unsigned int __cil_tmp165 ;
2869  int __cil_tmp166 ;
2870  int __cil_tmp167 ;
2871  long __cil_tmp168 ;
2872  unsigned long __cil_tmp169 ;
2873  unsigned long __cil_tmp170 ;
2874  struct device *__cil_tmp171 ;
2875  struct device  const  *__cil_tmp172 ;
2876  int __cil_tmp173 ;
2877  __u16 __cil_tmp174 ;
2878  int __cil_tmp175 ;
2879  int __cil_tmp176 ;
2880  unsigned long __cil_tmp177 ;
2881  unsigned long __cil_tmp178 ;
2882  unsigned long __cil_tmp179 ;
2883  unsigned long __cil_tmp180 ;
2884  __u8 __cil_tmp181 ;
2885  int __cil_tmp182 ;
2886  int __cil_tmp183 ;
2887  int __cil_tmp184 ;
2888  unsigned long __cil_tmp185 ;
2889  unsigned long __cil_tmp186 ;
2890  unsigned long __cil_tmp187 ;
2891  unsigned long __cil_tmp188 ;
2892  int __cil_tmp189 ;
2893  int __cil_tmp190 ;
2894  unsigned long __cil_tmp191 ;
2895  unsigned long __cil_tmp192 ;
2896  unsigned long __cil_tmp193 ;
2897  unsigned long __cil_tmp194 ;
2898  u16 __cil_tmp195 ;
2899  int __cil_tmp196 ;
2900  int __cil_tmp197 ;
2901  int __cil_tmp198 ;
2902  int __cil_tmp199 ;
2903  unsigned long __cil_tmp200 ;
2904  unsigned long __cil_tmp201 ;
2905  unsigned long __cil_tmp202 ;
2906  unsigned long __cil_tmp203 ;
2907  int __cil_tmp204 ;
2908  unsigned long __cil_tmp205 ;
2909  unsigned long __cil_tmp206 ;
2910  unsigned long __cil_tmp207 ;
2911  unsigned long __cil_tmp208 ;
2912  __u8 __cil_tmp209 ;
2913  int __cil_tmp210 ;
2914  int __cil_tmp211 ;
2915  int __cil_tmp212 ;
2916  unsigned long __cil_tmp213 ;
2917  unsigned long __cil_tmp214 ;
2918  unsigned long __cil_tmp215 ;
2919  unsigned long __cil_tmp216 ;
2920  u16 __cil_tmp217 ;
2921  int __cil_tmp218 ;
2922  int __cil_tmp219 ;
2923  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp220 ;
2924  unsigned int __cil_tmp221 ;
2925  unsigned int __cil_tmp222 ;
2926  int __cil_tmp223 ;
2927  int __cil_tmp224 ;
2928  long __cil_tmp225 ;
2929  unsigned long __cil_tmp226 ;
2930  unsigned long __cil_tmp227 ;
2931  struct device *__cil_tmp228 ;
2932  struct device  const  *__cil_tmp229 ;
2933  int __cil_tmp230 ;
2934  int __cil_tmp231 ;
2935  int __cil_tmp232 ;
2936  unsigned long __cil_tmp233 ;
2937  unsigned long __cil_tmp234 ;
2938  unsigned long __cil_tmp235 ;
2939  unsigned long __cil_tmp236 ;
2940  int __cil_tmp237 ;
2941  int __cil_tmp238 ;
2942  unsigned long __cil_tmp239 ;
2943  unsigned long __cil_tmp240 ;
2944  unsigned long __cil_tmp241 ;
2945  unsigned long __cil_tmp242 ;
2946  u16 __cil_tmp243 ;
2947  int __cil_tmp244 ;
2948  int __cil_tmp245 ;
2949  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp246 ;
2950  unsigned int __cil_tmp247 ;
2951  unsigned int __cil_tmp248 ;
2952  int __cil_tmp249 ;
2953  int __cil_tmp250 ;
2954  long __cil_tmp251 ;
2955  unsigned long __cil_tmp252 ;
2956  unsigned long __cil_tmp253 ;
2957  struct device *__cil_tmp254 ;
2958  struct device  const  *__cil_tmp255 ;
2959  int __cil_tmp256 ;
2960  int __cil_tmp257 ;
2961  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp258 ;
2962  unsigned int __cil_tmp259 ;
2963  unsigned int __cil_tmp260 ;
2964  int __cil_tmp261 ;
2965  int __cil_tmp262 ;
2966  long __cil_tmp263 ;
2967  unsigned long __cil_tmp264 ;
2968  unsigned long __cil_tmp265 ;
2969  struct device *__cil_tmp266 ;
2970  struct device  const  *__cil_tmp267 ;
2971
2972  {
2973#line 60
2974  __cil_tmp23 = (void *)0;
2975#line 60
2976  chip = (struct stub_chip *)__cil_tmp23;
2977#line 63
2978  i = 0;
2979  {
2980#line 63
2981  while (1) {
2982    while_continue: /* CIL Label */ ;
2983#line 63
2984    if (i < 10) {
2985      {
2986#line 63
2987      __cil_tmp24 = i * 2UL;
2988#line 63
2989      __cil_tmp25 = (unsigned long )(chip_addr) + __cil_tmp24;
2990#line 63
2991      if (*((unsigned short *)__cil_tmp25)) {
2992
2993      } else {
2994#line 63
2995        goto while_break;
2996      }
2997      }
2998    } else {
2999#line 63
3000      goto while_break;
3001    }
3002    {
3003#line 64
3004    __cil_tmp26 = i * 2UL;
3005#line 64
3006    __cil_tmp27 = (unsigned long )(chip_addr) + __cil_tmp26;
3007#line 64
3008    __cil_tmp28 = *((unsigned short *)__cil_tmp27);
3009#line 64
3010    __cil_tmp29 = (int )__cil_tmp28;
3011#line 64
3012    __cil_tmp30 = (int )addr;
3013#line 64
3014    if (__cil_tmp30 == __cil_tmp29) {
3015#line 65
3016      chip = stub_chips + i;
3017#line 66
3018      goto while_break;
3019    } else {
3020
3021    }
3022    }
3023#line 63
3024    i = i + 1;
3025  }
3026  while_break: /* CIL Label */ ;
3027  }
3028#line 69
3029  if (! chip) {
3030#line 70
3031    return (-19);
3032  } else {
3033
3034  }
3035#line 74
3036  if (size == 0) {
3037#line 74
3038    goto case_0;
3039  } else
3040#line 79
3041  if (size == 1) {
3042#line 79
3043    goto case_1;
3044  } else
3045#line 95
3046  if (size == 2) {
3047#line 95
3048    goto case_2;
3049  } else
3050#line 113
3051  if (size == 3) {
3052#line 113
3053    goto case_3;
3054  } else
3055#line 129
3056  if (size == 8) {
3057#line 129
3058    goto case_8;
3059  } else {
3060    {
3061#line 152
3062    goto switch_default;
3063#line 72
3064    if (0) {
3065      case_0: /* CIL Label */ 
3066      {
3067#line 75
3068      while (1) {
3069        while_continue___0: /* CIL Label */ ;
3070        {
3071#line 75
3072        while (1) {
3073          while_continue___1: /* CIL Label */ ;
3074          {
3075#line 75
3076          __cil_tmp31 = & descriptor;
3077#line 75
3078          __cil_tmp32 = __cil_tmp31->flags;
3079#line 75
3080          __cil_tmp33 = __cil_tmp32 & 1U;
3081#line 75
3082          __cil_tmp34 = ! __cil_tmp33;
3083#line 75
3084          __cil_tmp35 = ! __cil_tmp34;
3085#line 75
3086          __cil_tmp36 = (long )__cil_tmp35;
3087#line 75
3088          tmp___7 = __builtin_expect(__cil_tmp36, 0L);
3089          }
3090#line 75
3091          if (tmp___7) {
3092            {
3093#line 75
3094            __cil_tmp37 = (unsigned long )adap;
3095#line 75
3096            __cil_tmp38 = __cil_tmp37 + 128;
3097#line 75
3098            __cil_tmp39 = (struct device *)__cil_tmp38;
3099#line 75
3100            __cil_tmp40 = (struct device  const  *)__cil_tmp39;
3101#line 75
3102            __cil_tmp41 = (int )addr;
3103#line 75
3104            __dynamic_dev_dbg(& descriptor, __cil_tmp40, "smbus quick - addr 0x%02x\n",
3105                              __cil_tmp41);
3106            }
3107          } else {
3108
3109          }
3110#line 75
3111          goto while_break___1;
3112        }
3113        while_break___1: /* CIL Label */ ;
3114        }
3115#line 75
3116        goto while_break___0;
3117      }
3118      while_break___0: /* CIL Label */ ;
3119      }
3120#line 76
3121      ret = 0;
3122#line 77
3123      goto switch_break;
3124      case_1: /* CIL Label */ 
3125      {
3126#line 80
3127      __cil_tmp42 = (int )read_write;
3128#line 80
3129      if (__cil_tmp42 == 0) {
3130#line 81
3131        *((u8 *)chip) = command;
3132        {
3133#line 82
3134        while (1) {
3135          while_continue___2: /* CIL Label */ ;
3136          {
3137#line 82
3138          while (1) {
3139            while_continue___3: /* CIL Label */ ;
3140            {
3141#line 82
3142            __cil_tmp43 = & descriptor___0;
3143#line 82
3144            __cil_tmp44 = __cil_tmp43->flags;
3145#line 82
3146            __cil_tmp45 = __cil_tmp44 & 1U;
3147#line 82
3148            __cil_tmp46 = ! __cil_tmp45;
3149#line 82
3150            __cil_tmp47 = ! __cil_tmp46;
3151#line 82
3152            __cil_tmp48 = (long )__cil_tmp47;
3153#line 82
3154            tmp___8 = __builtin_expect(__cil_tmp48, 0L);
3155            }
3156#line 82
3157            if (tmp___8) {
3158              {
3159#line 82
3160              __cil_tmp49 = (unsigned long )adap;
3161#line 82
3162              __cil_tmp50 = __cil_tmp49 + 128;
3163#line 82
3164              __cil_tmp51 = (struct device *)__cil_tmp50;
3165#line 82
3166              __cil_tmp52 = (struct device  const  *)__cil_tmp51;
3167#line 82
3168              __cil_tmp53 = (int )addr;
3169#line 82
3170              __cil_tmp54 = (int )command;
3171#line 82
3172              __dynamic_dev_dbg(& descriptor___0, __cil_tmp52, "smbus byte - addr 0x%02x, wrote 0x%02x.\n",
3173                                __cil_tmp53, __cil_tmp54);
3174              }
3175            } else {
3176
3177            }
3178#line 82
3179            goto while_break___3;
3180          }
3181          while_break___3: /* CIL Label */ ;
3182          }
3183#line 82
3184          goto while_break___2;
3185        }
3186        while_break___2: /* CIL Label */ ;
3187        }
3188      } else {
3189#line 86
3190        tmp___9 = *((u8 *)chip);
3191#line 86
3192        __cil_tmp55 = *((u8 *)chip);
3193#line 86
3194        __cil_tmp56 = (int )__cil_tmp55;
3195#line 86
3196        __cil_tmp57 = __cil_tmp56 + 1;
3197#line 86
3198        *((u8 *)chip) = (u8 )__cil_tmp57;
3199#line 86
3200        __cil_tmp58 = tmp___9 * 2UL;
3201#line 86
3202        __cil_tmp59 = 2 + __cil_tmp58;
3203#line 86
3204        __cil_tmp60 = (unsigned long )chip;
3205#line 86
3206        __cil_tmp61 = __cil_tmp60 + __cil_tmp59;
3207#line 86
3208        __cil_tmp62 = *((u16 *)__cil_tmp61);
3209#line 86
3210        __cil_tmp63 = (int )__cil_tmp62;
3211#line 86
3212        __cil_tmp64 = __cil_tmp63 & 255;
3213#line 86
3214        *((__u8 *)data) = (__u8 )__cil_tmp64;
3215        {
3216#line 87
3217        while (1) {
3218          while_continue___4: /* CIL Label */ ;
3219          {
3220#line 87
3221          while (1) {
3222            while_continue___5: /* CIL Label */ ;
3223            {
3224#line 87
3225            __cil_tmp65 = & descriptor___1;
3226#line 87
3227            __cil_tmp66 = __cil_tmp65->flags;
3228#line 87
3229            __cil_tmp67 = __cil_tmp66 & 1U;
3230#line 87
3231            __cil_tmp68 = ! __cil_tmp67;
3232#line 87
3233            __cil_tmp69 = ! __cil_tmp68;
3234#line 87
3235            __cil_tmp70 = (long )__cil_tmp69;
3236#line 87
3237            tmp___10 = __builtin_expect(__cil_tmp70, 0L);
3238            }
3239#line 87
3240            if (tmp___10) {
3241              {
3242#line 87
3243              __cil_tmp71 = (unsigned long )adap;
3244#line 87
3245              __cil_tmp72 = __cil_tmp71 + 128;
3246#line 87
3247              __cil_tmp73 = (struct device *)__cil_tmp72;
3248#line 87
3249              __cil_tmp74 = (struct device  const  *)__cil_tmp73;
3250#line 87
3251              __cil_tmp75 = (int )addr;
3252#line 87
3253              __cil_tmp76 = *((__u8 *)data);
3254#line 87
3255              __cil_tmp77 = (int )__cil_tmp76;
3256#line 87
3257              __dynamic_dev_dbg(& descriptor___1, __cil_tmp74, "smbus byte - addr 0x%02x, read  0x%02x.\n",
3258                                __cil_tmp75, __cil_tmp77);
3259              }
3260            } else {
3261
3262            }
3263#line 87
3264            goto while_break___5;
3265          }
3266          while_break___5: /* CIL Label */ ;
3267          }
3268#line 87
3269          goto while_break___4;
3270        }
3271        while_break___4: /* CIL Label */ ;
3272        }
3273      }
3274      }
3275#line 92
3276      ret = 0;
3277#line 93
3278      goto switch_break;
3279      case_2: /* CIL Label */ 
3280      {
3281#line 96
3282      __cil_tmp78 = (int )read_write;
3283#line 96
3284      if (__cil_tmp78 == 0) {
3285#line 97
3286        __cil_tmp79 = command * 2UL;
3287#line 97
3288        __cil_tmp80 = 2 + __cil_tmp79;
3289#line 97
3290        __cil_tmp81 = (unsigned long )chip;
3291#line 97
3292        __cil_tmp82 = __cil_tmp81 + __cil_tmp80;
3293#line 97
3294        __cil_tmp83 = command * 2UL;
3295#line 97
3296        __cil_tmp84 = 2 + __cil_tmp83;
3297#line 97
3298        __cil_tmp85 = (unsigned long )chip;
3299#line 97
3300        __cil_tmp86 = __cil_tmp85 + __cil_tmp84;
3301#line 97
3302        __cil_tmp87 = *((u16 *)__cil_tmp86);
3303#line 97
3304        __cil_tmp88 = (int )__cil_tmp87;
3305#line 97
3306        __cil_tmp89 = __cil_tmp88 & 65280;
3307#line 97
3308        *((u16 *)__cil_tmp82) = (u16 )__cil_tmp89;
3309#line 98
3310        __cil_tmp90 = command * 2UL;
3311#line 98
3312        __cil_tmp91 = 2 + __cil_tmp90;
3313#line 98
3314        __cil_tmp92 = (unsigned long )chip;
3315#line 98
3316        __cil_tmp93 = __cil_tmp92 + __cil_tmp91;
3317#line 98
3318        __cil_tmp94 = *((__u8 *)data);
3319#line 98
3320        __cil_tmp95 = (int )__cil_tmp94;
3321#line 98
3322        __cil_tmp96 = command * 2UL;
3323#line 98
3324        __cil_tmp97 = 2 + __cil_tmp96;
3325#line 98
3326        __cil_tmp98 = (unsigned long )chip;
3327#line 98
3328        __cil_tmp99 = __cil_tmp98 + __cil_tmp97;
3329#line 98
3330        __cil_tmp100 = *((u16 *)__cil_tmp99);
3331#line 98
3332        __cil_tmp101 = (int )__cil_tmp100;
3333#line 98
3334        __cil_tmp102 = __cil_tmp101 | __cil_tmp95;
3335#line 98
3336        *((u16 *)__cil_tmp93) = (u16 )__cil_tmp102;
3337        {
3338#line 99
3339        while (1) {
3340          while_continue___6: /* CIL Label */ ;
3341          {
3342#line 99
3343          while (1) {
3344            while_continue___7: /* CIL Label */ ;
3345            {
3346#line 99
3347            __cil_tmp103 = & descriptor___2;
3348#line 99
3349            __cil_tmp104 = __cil_tmp103->flags;
3350#line 99
3351            __cil_tmp105 = __cil_tmp104 & 1U;
3352#line 99
3353            __cil_tmp106 = ! __cil_tmp105;
3354#line 99
3355            __cil_tmp107 = ! __cil_tmp106;
3356#line 99
3357            __cil_tmp108 = (long )__cil_tmp107;
3358#line 99
3359            tmp___11 = __builtin_expect(__cil_tmp108, 0L);
3360            }
3361#line 99
3362            if (tmp___11) {
3363              {
3364#line 99
3365              __cil_tmp109 = (unsigned long )adap;
3366#line 99
3367              __cil_tmp110 = __cil_tmp109 + 128;
3368#line 99
3369              __cil_tmp111 = (struct device *)__cil_tmp110;
3370#line 99
3371              __cil_tmp112 = (struct device  const  *)__cil_tmp111;
3372#line 99
3373              __cil_tmp113 = (int )addr;
3374#line 99
3375              __cil_tmp114 = *((__u8 *)data);
3376#line 99
3377              __cil_tmp115 = (int )__cil_tmp114;
3378#line 99
3379              __cil_tmp116 = (int )command;
3380#line 99
3381              __dynamic_dev_dbg(& descriptor___2, __cil_tmp112, "smbus byte data - addr 0x%02x, wrote 0x%02x at 0x%02x.\n",
3382                                __cil_tmp113, __cil_tmp115, __cil_tmp116);
3383              }
3384            } else {
3385
3386            }
3387#line 99
3388            goto while_break___7;
3389          }
3390          while_break___7: /* CIL Label */ ;
3391          }
3392#line 99
3393          goto while_break___6;
3394        }
3395        while_break___6: /* CIL Label */ ;
3396        }
3397      } else {
3398#line 103
3399        __cil_tmp117 = command * 2UL;
3400#line 103
3401        __cil_tmp118 = 2 + __cil_tmp117;
3402#line 103
3403        __cil_tmp119 = (unsigned long )chip;
3404#line 103
3405        __cil_tmp120 = __cil_tmp119 + __cil_tmp118;
3406#line 103
3407        __cil_tmp121 = *((u16 *)__cil_tmp120);
3408#line 103
3409        __cil_tmp122 = (int )__cil_tmp121;
3410#line 103
3411        __cil_tmp123 = __cil_tmp122 & 255;
3412#line 103
3413        *((__u8 *)data) = (__u8 )__cil_tmp123;
3414        {
3415#line 104
3416        while (1) {
3417          while_continue___8: /* CIL Label */ ;
3418          {
3419#line 104
3420          while (1) {
3421            while_continue___9: /* CIL Label */ ;
3422            {
3423#line 104
3424            __cil_tmp124 = & descriptor___3;
3425#line 104
3426            __cil_tmp125 = __cil_tmp124->flags;
3427#line 104
3428            __cil_tmp126 = __cil_tmp125 & 1U;
3429#line 104
3430            __cil_tmp127 = ! __cil_tmp126;
3431#line 104
3432            __cil_tmp128 = ! __cil_tmp127;
3433#line 104
3434            __cil_tmp129 = (long )__cil_tmp128;
3435#line 104
3436            tmp___12 = __builtin_expect(__cil_tmp129, 0L);
3437            }
3438#line 104
3439            if (tmp___12) {
3440              {
3441#line 104
3442              __cil_tmp130 = (unsigned long )adap;
3443#line 104
3444              __cil_tmp131 = __cil_tmp130 + 128;
3445#line 104
3446              __cil_tmp132 = (struct device *)__cil_tmp131;
3447#line 104
3448              __cil_tmp133 = (struct device  const  *)__cil_tmp132;
3449#line 104
3450              __cil_tmp134 = (int )addr;
3451#line 104
3452              __cil_tmp135 = *((__u8 *)data);
3453#line 104
3454              __cil_tmp136 = (int )__cil_tmp135;
3455#line 104
3456              __cil_tmp137 = (int )command;
3457#line 104
3458              __dynamic_dev_dbg(& descriptor___3, __cil_tmp133, "smbus byte data - addr 0x%02x, read  0x%02x at 0x%02x.\n",
3459                                __cil_tmp134, __cil_tmp136, __cil_tmp137);
3460              }
3461            } else {
3462
3463            }
3464#line 104
3465            goto while_break___9;
3466          }
3467          while_break___9: /* CIL Label */ ;
3468          }
3469#line 104
3470          goto while_break___8;
3471        }
3472        while_break___8: /* CIL Label */ ;
3473        }
3474      }
3475      }
3476#line 108
3477      __cil_tmp138 = (int )command;
3478#line 108
3479      __cil_tmp139 = __cil_tmp138 + 1;
3480#line 108
3481      *((u8 *)chip) = (u8 )__cil_tmp139;
3482#line 110
3483      ret = 0;
3484#line 111
3485      goto switch_break;
3486      case_3: /* CIL Label */ 
3487      {
3488#line 114
3489      __cil_tmp140 = (int )read_write;
3490#line 114
3491      if (__cil_tmp140 == 0) {
3492#line 115
3493        __cil_tmp141 = command * 2UL;
3494#line 115
3495        __cil_tmp142 = 2 + __cil_tmp141;
3496#line 115
3497        __cil_tmp143 = (unsigned long )chip;
3498#line 115
3499        __cil_tmp144 = __cil_tmp143 + __cil_tmp142;
3500#line 115
3501        *((u16 *)__cil_tmp144) = *((__u16 *)data);
3502        {
3503#line 116
3504        while (1) {
3505          while_continue___10: /* CIL Label */ ;
3506          {
3507#line 116
3508          while (1) {
3509            while_continue___11: /* CIL Label */ ;
3510            {
3511#line 116
3512            __cil_tmp145 = & descriptor___4;
3513#line 116
3514            __cil_tmp146 = __cil_tmp145->flags;
3515#line 116
3516            __cil_tmp147 = __cil_tmp146 & 1U;
3517#line 116
3518            __cil_tmp148 = ! __cil_tmp147;
3519#line 116
3520            __cil_tmp149 = ! __cil_tmp148;
3521#line 116
3522            __cil_tmp150 = (long )__cil_tmp149;
3523#line 116
3524            tmp___13 = __builtin_expect(__cil_tmp150, 0L);
3525            }
3526#line 116
3527            if (tmp___13) {
3528              {
3529#line 116
3530              __cil_tmp151 = (unsigned long )adap;
3531#line 116
3532              __cil_tmp152 = __cil_tmp151 + 128;
3533#line 116
3534              __cil_tmp153 = (struct device *)__cil_tmp152;
3535#line 116
3536              __cil_tmp154 = (struct device  const  *)__cil_tmp153;
3537#line 116
3538              __cil_tmp155 = (int )addr;
3539#line 116
3540              __cil_tmp156 = *((__u16 *)data);
3541#line 116
3542              __cil_tmp157 = (int )__cil_tmp156;
3543#line 116
3544              __cil_tmp158 = (int )command;
3545#line 116
3546              __dynamic_dev_dbg(& descriptor___4, __cil_tmp154, "smbus word data - addr 0x%02x, wrote 0x%04x at 0x%02x.\n",
3547                                __cil_tmp155, __cil_tmp157, __cil_tmp158);
3548              }
3549            } else {
3550
3551            }
3552#line 116
3553            goto while_break___11;
3554          }
3555          while_break___11: /* CIL Label */ ;
3556          }
3557#line 116
3558          goto while_break___10;
3559        }
3560        while_break___10: /* CIL Label */ ;
3561        }
3562      } else {
3563#line 120
3564        __cil_tmp159 = command * 2UL;
3565#line 120
3566        __cil_tmp160 = 2 + __cil_tmp159;
3567#line 120
3568        __cil_tmp161 = (unsigned long )chip;
3569#line 120
3570        __cil_tmp162 = __cil_tmp161 + __cil_tmp160;
3571#line 120
3572        *((__u16 *)data) = *((u16 *)__cil_tmp162);
3573        {
3574#line 121
3575        while (1) {
3576          while_continue___12: /* CIL Label */ ;
3577          {
3578#line 121
3579          while (1) {
3580            while_continue___13: /* CIL Label */ ;
3581            {
3582#line 121
3583            __cil_tmp163 = & descriptor___5;
3584#line 121
3585            __cil_tmp164 = __cil_tmp163->flags;
3586#line 121
3587            __cil_tmp165 = __cil_tmp164 & 1U;
3588#line 121
3589            __cil_tmp166 = ! __cil_tmp165;
3590#line 121
3591            __cil_tmp167 = ! __cil_tmp166;
3592#line 121
3593            __cil_tmp168 = (long )__cil_tmp167;
3594#line 121
3595            tmp___14 = __builtin_expect(__cil_tmp168, 0L);
3596            }
3597#line 121
3598            if (tmp___14) {
3599              {
3600#line 121
3601              __cil_tmp169 = (unsigned long )adap;
3602#line 121
3603              __cil_tmp170 = __cil_tmp169 + 128;
3604#line 121
3605              __cil_tmp171 = (struct device *)__cil_tmp170;
3606#line 121
3607              __cil_tmp172 = (struct device  const  *)__cil_tmp171;
3608#line 121
3609              __cil_tmp173 = (int )addr;
3610#line 121
3611              __cil_tmp174 = *((__u16 *)data);
3612#line 121
3613              __cil_tmp175 = (int )__cil_tmp174;
3614#line 121
3615              __cil_tmp176 = (int )command;
3616#line 121
3617              __dynamic_dev_dbg(& descriptor___5, __cil_tmp172, "smbus word data - addr 0x%02x, read  0x%04x at 0x%02x.\n",
3618                                __cil_tmp173, __cil_tmp175, __cil_tmp176);
3619              }
3620            } else {
3621
3622            }
3623#line 121
3624            goto while_break___13;
3625          }
3626          while_break___13: /* CIL Label */ ;
3627          }
3628#line 121
3629          goto while_break___12;
3630        }
3631        while_break___12: /* CIL Label */ ;
3632        }
3633      }
3634      }
3635#line 126
3636      ret = 0;
3637#line 127
3638      goto switch_break;
3639      case_8: /* CIL Label */ 
3640#line 130
3641      __cil_tmp177 = 0 * 1UL;
3642#line 130
3643      __cil_tmp178 = 0 + __cil_tmp177;
3644#line 130
3645      __cil_tmp179 = (unsigned long )data;
3646#line 130
3647      __cil_tmp180 = __cil_tmp179 + __cil_tmp178;
3648#line 130
3649      __cil_tmp181 = *((__u8 *)__cil_tmp180);
3650#line 130
3651      len = (int )__cil_tmp181;
3652      {
3653#line 131
3654      __cil_tmp182 = (int )read_write;
3655#line 131
3656      if (__cil_tmp182 == 0) {
3657#line 132
3658        i = 0;
3659        {
3660#line 132
3661        while (1) {
3662          while_continue___14: /* CIL Label */ ;
3663#line 132
3664          if (i < len) {
3665
3666          } else {
3667#line 132
3668            goto while_break___14;
3669          }
3670#line 133
3671          __cil_tmp183 = (int )command;
3672#line 133
3673          __cil_tmp184 = __cil_tmp183 + i;
3674#line 133
3675          __cil_tmp185 = __cil_tmp184 * 2UL;
3676#line 133
3677          __cil_tmp186 = 2 + __cil_tmp185;
3678#line 133
3679          __cil_tmp187 = (unsigned long )chip;
3680#line 133
3681          __cil_tmp188 = __cil_tmp187 + __cil_tmp186;
3682#line 133
3683          __cil_tmp189 = (int )command;
3684#line 133
3685          __cil_tmp190 = __cil_tmp189 + i;
3686#line 133
3687          __cil_tmp191 = __cil_tmp190 * 2UL;
3688#line 133
3689          __cil_tmp192 = 2 + __cil_tmp191;
3690#line 133
3691          __cil_tmp193 = (unsigned long )chip;
3692#line 133
3693          __cil_tmp194 = __cil_tmp193 + __cil_tmp192;
3694#line 133
3695          __cil_tmp195 = *((u16 *)__cil_tmp194);
3696#line 133
3697          __cil_tmp196 = (int )__cil_tmp195;
3698#line 133
3699          __cil_tmp197 = __cil_tmp196 & 65280;
3700#line 133
3701          *((u16 *)__cil_tmp188) = (u16 )__cil_tmp197;
3702#line 134
3703          __cil_tmp198 = (int )command;
3704#line 134
3705          __cil_tmp199 = __cil_tmp198 + i;
3706#line 134
3707          __cil_tmp200 = __cil_tmp199 * 2UL;
3708#line 134
3709          __cil_tmp201 = 2 + __cil_tmp200;
3710#line 134
3711          __cil_tmp202 = (unsigned long )chip;
3712#line 134
3713          __cil_tmp203 = __cil_tmp202 + __cil_tmp201;
3714#line 134
3715          __cil_tmp204 = 1 + i;
3716#line 134
3717          __cil_tmp205 = __cil_tmp204 * 1UL;
3718#line 134
3719          __cil_tmp206 = 0 + __cil_tmp205;
3720#line 134
3721          __cil_tmp207 = (unsigned long )data;
3722#line 134
3723          __cil_tmp208 = __cil_tmp207 + __cil_tmp206;
3724#line 134
3725          __cil_tmp209 = *((__u8 *)__cil_tmp208);
3726#line 134
3727          __cil_tmp210 = (int )__cil_tmp209;
3728#line 134
3729          __cil_tmp211 = (int )command;
3730#line 134
3731          __cil_tmp212 = __cil_tmp211 + i;
3732#line 134
3733          __cil_tmp213 = __cil_tmp212 * 2UL;
3734#line 134
3735          __cil_tmp214 = 2 + __cil_tmp213;
3736#line 134
3737          __cil_tmp215 = (unsigned long )chip;
3738#line 134
3739          __cil_tmp216 = __cil_tmp215 + __cil_tmp214;
3740#line 134
3741          __cil_tmp217 = *((u16 *)__cil_tmp216);
3742#line 134
3743          __cil_tmp218 = (int )__cil_tmp217;
3744#line 134
3745          __cil_tmp219 = __cil_tmp218 | __cil_tmp210;
3746#line 134
3747          *((u16 *)__cil_tmp203) = (u16 )__cil_tmp219;
3748#line 132
3749          i = i + 1;
3750        }
3751        while_break___14: /* CIL Label */ ;
3752        }
3753        {
3754#line 136
3755        while (1) {
3756          while_continue___15: /* CIL Label */ ;
3757          {
3758#line 136
3759          while (1) {
3760            while_continue___16: /* CIL Label */ ;
3761            {
3762#line 136
3763            __cil_tmp220 = & descriptor___6;
3764#line 136
3765            __cil_tmp221 = __cil_tmp220->flags;
3766#line 136
3767            __cil_tmp222 = __cil_tmp221 & 1U;
3768#line 136
3769            __cil_tmp223 = ! __cil_tmp222;
3770#line 136
3771            __cil_tmp224 = ! __cil_tmp223;
3772#line 136
3773            __cil_tmp225 = (long )__cil_tmp224;
3774#line 136
3775            tmp___15 = __builtin_expect(__cil_tmp225, 0L);
3776            }
3777#line 136
3778            if (tmp___15) {
3779              {
3780#line 136
3781              __cil_tmp226 = (unsigned long )adap;
3782#line 136
3783              __cil_tmp227 = __cil_tmp226 + 128;
3784#line 136
3785              __cil_tmp228 = (struct device *)__cil_tmp227;
3786#line 136
3787              __cil_tmp229 = (struct device  const  *)__cil_tmp228;
3788#line 136
3789              __cil_tmp230 = (int )addr;
3790#line 136
3791              __cil_tmp231 = (int )command;
3792#line 136
3793              __dynamic_dev_dbg(& descriptor___6, __cil_tmp229, "i2c block data - addr 0x%02x, wrote %d bytes at 0x%02x.\n",
3794                                __cil_tmp230, len, __cil_tmp231);
3795              }
3796            } else {
3797
3798            }
3799#line 136
3800            goto while_break___16;
3801          }
3802          while_break___16: /* CIL Label */ ;
3803          }
3804#line 136
3805          goto while_break___15;
3806        }
3807        while_break___15: /* CIL Label */ ;
3808        }
3809      } else {
3810#line 140
3811        i = 0;
3812        {
3813#line 140
3814        while (1) {
3815          while_continue___17: /* CIL Label */ ;
3816#line 140
3817          if (i < len) {
3818
3819          } else {
3820#line 140
3821            goto while_break___17;
3822          }
3823#line 141
3824          __cil_tmp232 = 1 + i;
3825#line 141
3826          __cil_tmp233 = __cil_tmp232 * 1UL;
3827#line 141
3828          __cil_tmp234 = 0 + __cil_tmp233;
3829#line 141
3830          __cil_tmp235 = (unsigned long )data;
3831#line 141
3832          __cil_tmp236 = __cil_tmp235 + __cil_tmp234;
3833#line 141
3834          __cil_tmp237 = (int )command;
3835#line 141
3836          __cil_tmp238 = __cil_tmp237 + i;
3837#line 141
3838          __cil_tmp239 = __cil_tmp238 * 2UL;
3839#line 141
3840          __cil_tmp240 = 2 + __cil_tmp239;
3841#line 141
3842          __cil_tmp241 = (unsigned long )chip;
3843#line 141
3844          __cil_tmp242 = __cil_tmp241 + __cil_tmp240;
3845#line 141
3846          __cil_tmp243 = *((u16 *)__cil_tmp242);
3847#line 141
3848          __cil_tmp244 = (int )__cil_tmp243;
3849#line 141
3850          __cil_tmp245 = __cil_tmp244 & 255;
3851#line 141
3852          *((__u8 *)__cil_tmp236) = (__u8 )__cil_tmp245;
3853#line 140
3854          i = i + 1;
3855        }
3856        while_break___17: /* CIL Label */ ;
3857        }
3858        {
3859#line 144
3860        while (1) {
3861          while_continue___18: /* CIL Label */ ;
3862          {
3863#line 144
3864          while (1) {
3865            while_continue___19: /* CIL Label */ ;
3866            {
3867#line 144
3868            __cil_tmp246 = & descriptor___7;
3869#line 144
3870            __cil_tmp247 = __cil_tmp246->flags;
3871#line 144
3872            __cil_tmp248 = __cil_tmp247 & 1U;
3873#line 144
3874            __cil_tmp249 = ! __cil_tmp248;
3875#line 144
3876            __cil_tmp250 = ! __cil_tmp249;
3877#line 144
3878            __cil_tmp251 = (long )__cil_tmp250;
3879#line 144
3880            tmp___16 = __builtin_expect(__cil_tmp251, 0L);
3881            }
3882#line 144
3883            if (tmp___16) {
3884              {
3885#line 144
3886              __cil_tmp252 = (unsigned long )adap;
3887#line 144
3888              __cil_tmp253 = __cil_tmp252 + 128;
3889#line 144
3890              __cil_tmp254 = (struct device *)__cil_tmp253;
3891#line 144
3892              __cil_tmp255 = (struct device  const  *)__cil_tmp254;
3893#line 144
3894              __cil_tmp256 = (int )addr;
3895#line 144
3896              __cil_tmp257 = (int )command;
3897#line 144
3898              __dynamic_dev_dbg(& descriptor___7, __cil_tmp255, "i2c block data - addr 0x%02x, read  %d bytes at 0x%02x.\n",
3899                                __cil_tmp256, len, __cil_tmp257);
3900              }
3901            } else {
3902
3903            }
3904#line 144
3905            goto while_break___19;
3906          }
3907          while_break___19: /* CIL Label */ ;
3908          }
3909#line 144
3910          goto while_break___18;
3911        }
3912        while_break___18: /* CIL Label */ ;
3913        }
3914      }
3915      }
3916#line 149
3917      ret = 0;
3918#line 150
3919      goto switch_break;
3920      switch_default: /* CIL Label */ 
3921      {
3922#line 153
3923      while (1) {
3924        while_continue___20: /* CIL Label */ ;
3925        {
3926#line 153
3927        while (1) {
3928          while_continue___21: /* CIL Label */ ;
3929          {
3930#line 153
3931          __cil_tmp258 = & descriptor___8;
3932#line 153
3933          __cil_tmp259 = __cil_tmp258->flags;
3934#line 153
3935          __cil_tmp260 = __cil_tmp259 & 1U;
3936#line 153
3937          __cil_tmp261 = ! __cil_tmp260;
3938#line 153
3939          __cil_tmp262 = ! __cil_tmp261;
3940#line 153
3941          __cil_tmp263 = (long )__cil_tmp262;
3942#line 153
3943          tmp___17 = __builtin_expect(__cil_tmp263, 0L);
3944          }
3945#line 153
3946          if (tmp___17) {
3947            {
3948#line 153
3949            __cil_tmp264 = (unsigned long )adap;
3950#line 153
3951            __cil_tmp265 = __cil_tmp264 + 128;
3952#line 153
3953            __cil_tmp266 = (struct device *)__cil_tmp265;
3954#line 153
3955            __cil_tmp267 = (struct device  const  *)__cil_tmp266;
3956#line 153
3957            __dynamic_dev_dbg(& descriptor___8, __cil_tmp267, "Unsupported I2C/SMBus command\n");
3958            }
3959          } else {
3960
3961          }
3962#line 153
3963          goto while_break___21;
3964        }
3965        while_break___21: /* CIL Label */ ;
3966        }
3967#line 153
3968        goto while_break___20;
3969      }
3970      while_break___20: /* CIL Label */ ;
3971      }
3972#line 154
3973      ret = -95;
3974#line 155
3975      goto switch_break;
3976    } else {
3977      switch_break: /* CIL Label */ ;
3978    }
3979    }
3980  }
3981#line 158
3982  return (ret);
3983}
3984}
3985#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
3986static u32 stub_func(struct i2c_adapter *adapter ) 
3987{ unsigned long *__cil_tmp2 ;
3988  unsigned long __cil_tmp3 ;
3989  unsigned long __cil_tmp4 ;
3990
3991  {
3992  {
3993#line 163
3994  __cil_tmp2 = & functionality;
3995#line 163
3996  __cil_tmp3 = *__cil_tmp2;
3997#line 163
3998  __cil_tmp4 = 209649664UL & __cil_tmp3;
3999#line 163
4000  return ((u32 )__cil_tmp4);
4001  }
4002}
4003}
4004#line 166 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4005static struct i2c_algorithm  const  smbus_algorithm  =    {(int (*)(struct i2c_adapter *adap , struct i2c_msg *msgs , int num ))0, & stub_xfer,
4006    & stub_func};
4007#line 171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4008static struct i2c_adapter stub_adapter  = 
4009#line 171
4010     {& __this_module, (unsigned int )(1 | (1 << 7)), & smbus_algorithm, (void *)0,
4011    {{{{0U}}, 0U, 0U, (void *)0}, {{(struct list_head *)0, (struct list_head *)0}},
4012     (struct task_struct *)0, 0, (char const   *)0, (char const   *)0, 0, (void *)0},
4013    0, 0, {(struct device *)0, (struct device_private *)0, {(char const   *)0, {(struct list_head *)0,
4014                                                                                (struct list_head *)0},
4015                                                            (struct kobject *)0, (struct kset *)0,
4016                                                            (struct kobj_type *)0,
4017                                                            (struct sysfs_dirent *)0,
4018                                                            {{0}}, 0U, 0U, 0U, 0U,
4019                                                            0U}, (char const   *)0,
4020           (struct device_type  const  *)0, {{0}, {{{{{0U}}, 0U, 0U, (void *)0}}},
4021                                             {(struct list_head *)0, (struct list_head *)0},
4022                                             (struct task_struct *)0, (char const   *)0,
4023                                             (void *)0}, (struct bus_type *)0, (struct device_driver *)0,
4024           (void *)0, {{0}, 0U, 0U, (_Bool)0, (_Bool)0, (_Bool)0, {{{{{0U}}, 0U, 0U,
4025                                                                     (void *)0}}},
4026                       {(struct list_head *)0, (struct list_head *)0}, {0U, {{{{{{0U}},
4027                                                                                0U,
4028                                                                                0U,
4029                                                                                (void *)0}}},
4030                                                                             {(struct list_head *)0,
4031                                                                              (struct list_head *)0}}},
4032                       (struct wakeup_source *)0, (_Bool)0, {{(struct list_head *)0,
4033                                                              (struct list_head *)0},
4034                                                             0UL, (struct tvec_base *)0,
4035                                                             (void (*)(unsigned long  ))0,
4036                                                             0UL, 0, 0, (void *)0,
4037                                                             {(char)0, (char)0, (char)0,
4038                                                              (char)0, (char)0, (char)0,
4039                                                              (char)0, (char)0, (char)0,
4040                                                              (char)0, (char)0, (char)0,
4041                                                              (char)0, (char)0, (char)0,
4042                                                              (char)0}}, 0UL, {{0L},
4043                                                                               {(struct list_head *)0,
4044                                                                                (struct list_head *)0},
4045                                                                               (void (*)(struct work_struct *work ))0},
4046                       {{{{{{0U}}, 0U, 0U, (void *)0}}}, {(struct list_head *)0, (struct list_head *)0}},
4047                       {0}, {0}, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0, 0, 0,
4048                       0, 0UL, 0UL, 0UL, 0UL, {0LL}, 0LL, (struct dev_pm_qos_request *)0,
4049                       (struct pm_subsys_data *)0, (struct pm_qos_constraints *)0},
4050           (struct dev_pm_domain *)0, 0, (u64 *)0, 0ULL, (struct device_dma_parameters *)0,
4051           {(struct list_head *)0, (struct list_head *)0}, (struct dma_coherent_mem *)0,
4052           {(void *)0, (struct dma_map_ops *)0, (void *)0}, (struct device_node *)0,
4053           0U, 0U, {{{{{0U}}, 0U, 0U, (void *)0}}}, {(struct list_head *)0, (struct list_head *)0},
4054           {(void *)0, {(struct list_head *)0, (struct list_head *)0}, {{0}}}, (struct class *)0,
4055           (struct attribute_group  const  **)0, (void (*)(struct device *dev ))0},
4056    0, {(char )'S', (char )'M', (char )'B', (char )'u', (char )'s', (char )' ', (char )'s',
4057        (char )'t', (char )'u', (char )'b', (char )' ', (char )'d', (char )'r', (char )'i',
4058        (char )'v', (char )'e', (char )'r', (char )'\000'}, {0U, {{{{{{0U}}, 0U, 0U,
4059                                                                     (void *)0}}},
4060                                                                  {(struct list_head *)0,
4061                                                                   (struct list_head *)0}}},
4062    {{0}, {{{{{0U}}, 0U, 0U, (void *)0}}}, {(struct list_head *)0, (struct list_head *)0},
4063     (struct task_struct *)0, (char const   *)0, (void *)0}, {(struct list_head *)0,
4064                                                              (struct list_head *)0}};
4065#line 178
4066static int i2c_stub_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
4067#line 178 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4068static int i2c_stub_init(void) 
4069{ int i ;
4070  int ret ;
4071  void *tmp___7 ;
4072  unsigned long __cil_tmp4 ;
4073  unsigned long __cil_tmp5 ;
4074  unsigned short __cil_tmp6 ;
4075  unsigned long __cil_tmp7 ;
4076  unsigned long __cil_tmp8 ;
4077  unsigned long __cil_tmp9 ;
4078  unsigned long __cil_tmp10 ;
4079  unsigned short __cil_tmp11 ;
4080  int __cil_tmp12 ;
4081  unsigned long __cil_tmp13 ;
4082  unsigned long __cil_tmp14 ;
4083  unsigned short __cil_tmp15 ;
4084  int __cil_tmp16 ;
4085  unsigned long __cil_tmp17 ;
4086  unsigned long __cil_tmp18 ;
4087  unsigned short __cil_tmp19 ;
4088  int __cil_tmp20 ;
4089  unsigned long __cil_tmp21 ;
4090  unsigned long __cil_tmp22 ;
4091  unsigned short __cil_tmp23 ;
4092  int __cil_tmp24 ;
4093  unsigned long __cil_tmp25 ;
4094  unsigned long __cil_tmp26 ;
4095  unsigned short __cil_tmp27 ;
4096  int __cil_tmp28 ;
4097  unsigned long __cil_tmp29 ;
4098  unsigned long __cil_tmp30 ;
4099  void const   *__cil_tmp31 ;
4100
4101  {
4102  {
4103#line 182
4104  __cil_tmp4 = 0 * 2UL;
4105#line 182
4106  __cil_tmp5 = (unsigned long )(chip_addr) + __cil_tmp4;
4107#line 182
4108  __cil_tmp6 = *((unsigned short *)__cil_tmp5);
4109#line 182
4110  if (! __cil_tmp6) {
4111    {
4112#line 183
4113    printk("<3>i2c-stub: Please specify a chip address\n");
4114    }
4115#line 184
4116    return (-19);
4117  } else {
4118
4119  }
4120  }
4121#line 187
4122  i = 0;
4123  {
4124#line 187
4125  while (1) {
4126    while_continue: /* CIL Label */ ;
4127#line 187
4128    if (i < 10) {
4129      {
4130#line 187
4131      __cil_tmp7 = i * 2UL;
4132#line 187
4133      __cil_tmp8 = (unsigned long )(chip_addr) + __cil_tmp7;
4134#line 187
4135      if (*((unsigned short *)__cil_tmp8)) {
4136
4137      } else {
4138#line 187
4139        goto while_break;
4140      }
4141      }
4142    } else {
4143#line 187
4144      goto while_break;
4145    }
4146    {
4147#line 188
4148    __cil_tmp9 = i * 2UL;
4149#line 188
4150    __cil_tmp10 = (unsigned long )(chip_addr) + __cil_tmp9;
4151#line 188
4152    __cil_tmp11 = *((unsigned short *)__cil_tmp10);
4153#line 188
4154    __cil_tmp12 = (int )__cil_tmp11;
4155#line 188
4156    if (__cil_tmp12 < 3) {
4157      {
4158#line 189
4159      __cil_tmp13 = i * 2UL;
4160#line 189
4161      __cil_tmp14 = (unsigned long )(chip_addr) + __cil_tmp13;
4162#line 189
4163      __cil_tmp15 = *((unsigned short *)__cil_tmp14);
4164#line 189
4165      __cil_tmp16 = (int )__cil_tmp15;
4166#line 189
4167      printk("<3>i2c-stub: Invalid chip address 0x%02x\n", __cil_tmp16);
4168      }
4169#line 191
4170      return (-22);
4171    } else {
4172      {
4173#line 188
4174      __cil_tmp17 = i * 2UL;
4175#line 188
4176      __cil_tmp18 = (unsigned long )(chip_addr) + __cil_tmp17;
4177#line 188
4178      __cil_tmp19 = *((unsigned short *)__cil_tmp18);
4179#line 188
4180      __cil_tmp20 = (int )__cil_tmp19;
4181#line 188
4182      if (__cil_tmp20 > 119) {
4183        {
4184#line 189
4185        __cil_tmp21 = i * 2UL;
4186#line 189
4187        __cil_tmp22 = (unsigned long )(chip_addr) + __cil_tmp21;
4188#line 189
4189        __cil_tmp23 = *((unsigned short *)__cil_tmp22);
4190#line 189
4191        __cil_tmp24 = (int )__cil_tmp23;
4192#line 189
4193        printk("<3>i2c-stub: Invalid chip address 0x%02x\n", __cil_tmp24);
4194        }
4195#line 191
4196        return (-22);
4197      } else {
4198
4199      }
4200      }
4201    }
4202    }
4203    {
4204#line 194
4205    __cil_tmp25 = i * 2UL;
4206#line 194
4207    __cil_tmp26 = (unsigned long )(chip_addr) + __cil_tmp25;
4208#line 194
4209    __cil_tmp27 = *((unsigned short *)__cil_tmp26);
4210#line 194
4211    __cil_tmp28 = (int )__cil_tmp27;
4212#line 194
4213    printk("<6>i2c-stub: Virtual chip at 0x%02x\n", __cil_tmp28);
4214#line 187
4215    i = i + 1;
4216    }
4217  }
4218  while_break: /* CIL Label */ ;
4219  }
4220  {
4221#line 199
4222  __cil_tmp29 = (unsigned long )i;
4223#line 199
4224  __cil_tmp30 = __cil_tmp29 * 514UL;
4225#line 199
4226  tmp___7 = kzalloc(__cil_tmp30, 208U);
4227#line 199
4228  stub_chips = (struct stub_chip *)tmp___7;
4229  }
4230#line 200
4231  if (! stub_chips) {
4232    {
4233#line 201
4234    printk("<3>i2c-stub: Out of memory\n");
4235    }
4236#line 202
4237    return (-12);
4238  } else {
4239
4240  }
4241  {
4242#line 205
4243  ret = i2c_add_adapter(& stub_adapter);
4244  }
4245#line 206
4246  if (ret) {
4247    {
4248#line 207
4249    __cil_tmp31 = (void const   *)stub_chips;
4250#line 207
4251    kfree(__cil_tmp31);
4252    }
4253  } else {
4254
4255  }
4256#line 208
4257  return (ret);
4258}
4259}
4260#line 211
4261static void i2c_stub_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
4262#line 211 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4263static void i2c_stub_exit(void) 
4264{ void const   *__cil_tmp1 ;
4265
4266  {
4267  {
4268#line 213
4269  i2c_del_adapter(& stub_adapter);
4270#line 214
4271  __cil_tmp1 = (void const   *)stub_chips;
4272#line 214
4273  kfree(__cil_tmp1);
4274  }
4275#line 215
4276  return;
4277}
4278}
4279#line 217 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4280static char const   __mod_author217[48]  __attribute__((__used__, __unused__, __section__(".modinfo"),
4281__aligned__(1)))  = 
4282#line 217
4283  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
4284        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'M', 
4285        (char const   )'a',      (char const   )'r',      (char const   )'k',      (char const   )' ', 
4286        (char const   )'M',      (char const   )'.',      (char const   )' ',      (char const   )'H', 
4287        (char const   )'o',      (char const   )'f',      (char const   )'f',      (char const   )'m', 
4288        (char const   )'a',      (char const   )'n',      (char const   )' ',      (char const   )'<', 
4289        (char const   )'m',      (char const   )'h',      (char const   )'o',      (char const   )'f', 
4290        (char const   )'f',      (char const   )'m',      (char const   )'a',      (char const   )'n', 
4291        (char const   )'@',      (char const   )'l',      (char const   )'i',      (char const   )'g', 
4292        (char const   )'h',      (char const   )'t',      (char const   )'l',      (char const   )'i', 
4293        (char const   )'n',      (char const   )'k',      (char const   )'.',      (char const   )'c', 
4294        (char const   )'o',      (char const   )'m',      (char const   )'>',      (char const   )'\000'};
4295#line 218 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4296static char const   __mod_description218[28]  __attribute__((__used__, __unused__,
4297__section__(".modinfo"), __aligned__(1)))  = 
4298#line 218
4299  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
4300        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
4301        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
4302        (char const   )'I',      (char const   )'2',      (char const   )'C',      (char const   )' ', 
4303        (char const   )'s',      (char const   )'t',      (char const   )'u',      (char const   )'b', 
4304        (char const   )' ',      (char const   )'d',      (char const   )'r',      (char const   )'i', 
4305        (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )'\000'};
4306#line 219 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4307static char const   __mod_license219[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
4308__aligned__(1)))  = 
4309#line 219
4310  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
4311        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
4312        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
4313#line 221 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4314int init_module(void) 
4315{ int tmp___7 ;
4316
4317  {
4318  {
4319#line 221
4320  tmp___7 = i2c_stub_init();
4321  }
4322#line 221
4323  return (tmp___7);
4324}
4325}
4326#line 222 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4327void cleanup_module(void) 
4328{ 
4329
4330  {
4331  {
4332#line 222
4333  i2c_stub_exit();
4334  }
4335#line 222
4336  return;
4337}
4338}
4339#line 241
4340void ldv_check_final_state(void) ;
4341#line 247
4342extern void ldv_initialize(void) ;
4343#line 250
4344extern int __VERIFIER_nondet_int(void) ;
4345#line 253 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4346int LDV_IN_INTERRUPT  ;
4347#line 256 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4348void main(void) 
4349{ struct i2c_adapter *var_group1 ;
4350  u16 var_stub_xfer_0_p1 ;
4351  unsigned int var_stub_xfer_0_p2 ;
4352  char var_stub_xfer_0_p3 ;
4353  u8 var_stub_xfer_0_p4 ;
4354  int var_stub_xfer_0_p5 ;
4355  union i2c_smbus_data *var_stub_xfer_0_p6 ;
4356  int tmp___7 ;
4357  int tmp___8 ;
4358  int tmp___9 ;
4359  unsigned short __cil_tmp11 ;
4360
4361  {
4362  {
4363#line 300
4364  LDV_IN_INTERRUPT = 1;
4365#line 309
4366  ldv_initialize();
4367#line 321
4368  tmp___7 = i2c_stub_init();
4369  }
4370#line 321
4371  if (tmp___7) {
4372#line 322
4373    goto ldv_final;
4374  } else {
4375
4376  }
4377  {
4378#line 326
4379  while (1) {
4380    while_continue: /* CIL Label */ ;
4381    {
4382#line 326
4383    tmp___9 = __VERIFIER_nondet_int();
4384    }
4385#line 326
4386    if (tmp___9) {
4387
4388    } else {
4389#line 326
4390      goto while_break;
4391    }
4392    {
4393#line 329
4394    tmp___8 = __VERIFIER_nondet_int();
4395    }
4396#line 331
4397    if (tmp___8 == 0) {
4398#line 331
4399      goto case_0;
4400    } else
4401#line 353
4402    if (tmp___8 == 1) {
4403#line 353
4404      goto case_1;
4405    } else {
4406      {
4407#line 375
4408      goto switch_default;
4409#line 329
4410      if (0) {
4411        case_0: /* CIL Label */ 
4412        {
4413#line 345
4414        stub_func(var_group1);
4415        }
4416#line 352
4417        goto switch_break;
4418        case_1: /* CIL Label */ 
4419        {
4420#line 367
4421        __cil_tmp11 = (unsigned short )var_stub_xfer_0_p2;
4422#line 367
4423        stub_xfer(var_group1, var_stub_xfer_0_p1, __cil_tmp11, var_stub_xfer_0_p3,
4424                  var_stub_xfer_0_p4, var_stub_xfer_0_p5, var_stub_xfer_0_p6);
4425        }
4426#line 374
4427        goto switch_break;
4428        switch_default: /* CIL Label */ 
4429#line 375
4430        goto switch_break;
4431      } else {
4432        switch_break: /* CIL Label */ ;
4433      }
4434      }
4435    }
4436  }
4437  while_break: /* CIL Label */ ;
4438  }
4439  {
4440#line 393
4441  i2c_stub_exit();
4442  }
4443  ldv_final: 
4444  {
4445#line 396
4446  ldv_check_final_state();
4447  }
4448#line 399
4449  return;
4450}
4451}
4452#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4453void ldv_blast_assert(void) 
4454{ 
4455
4456  {
4457  ERROR: 
4458#line 6
4459  goto ERROR;
4460}
4461}
4462#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4463extern int __VERIFIER_nondet_int(void) ;
4464#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4465int ldv_mutex  =    1;
4466#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4467int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
4468{ int nondetermined ;
4469
4470  {
4471#line 29
4472  if (ldv_mutex == 1) {
4473
4474  } else {
4475    {
4476#line 29
4477    ldv_blast_assert();
4478    }
4479  }
4480  {
4481#line 32
4482  nondetermined = __VERIFIER_nondet_int();
4483  }
4484#line 35
4485  if (nondetermined) {
4486#line 38
4487    ldv_mutex = 2;
4488#line 40
4489    return (0);
4490  } else {
4491#line 45
4492    return (-4);
4493  }
4494}
4495}
4496#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4497int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
4498{ int nondetermined ;
4499
4500  {
4501#line 57
4502  if (ldv_mutex == 1) {
4503
4504  } else {
4505    {
4506#line 57
4507    ldv_blast_assert();
4508    }
4509  }
4510  {
4511#line 60
4512  nondetermined = __VERIFIER_nondet_int();
4513  }
4514#line 63
4515  if (nondetermined) {
4516#line 66
4517    ldv_mutex = 2;
4518#line 68
4519    return (0);
4520  } else {
4521#line 73
4522    return (-4);
4523  }
4524}
4525}
4526#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4527int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
4528{ int atomic_value_after_dec ;
4529
4530  {
4531#line 83
4532  if (ldv_mutex == 1) {
4533
4534  } else {
4535    {
4536#line 83
4537    ldv_blast_assert();
4538    }
4539  }
4540  {
4541#line 86
4542  atomic_value_after_dec = __VERIFIER_nondet_int();
4543  }
4544#line 89
4545  if (atomic_value_after_dec == 0) {
4546#line 92
4547    ldv_mutex = 2;
4548#line 94
4549    return (1);
4550  } else {
4551
4552  }
4553#line 98
4554  return (0);
4555}
4556}
4557#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4558void mutex_lock(struct mutex *lock ) 
4559{ 
4560
4561  {
4562#line 108
4563  if (ldv_mutex == 1) {
4564
4565  } else {
4566    {
4567#line 108
4568    ldv_blast_assert();
4569    }
4570  }
4571#line 110
4572  ldv_mutex = 2;
4573#line 111
4574  return;
4575}
4576}
4577#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4578int mutex_trylock(struct mutex *lock ) 
4579{ int nondetermined ;
4580
4581  {
4582#line 121
4583  if (ldv_mutex == 1) {
4584
4585  } else {
4586    {
4587#line 121
4588    ldv_blast_assert();
4589    }
4590  }
4591  {
4592#line 124
4593  nondetermined = __VERIFIER_nondet_int();
4594  }
4595#line 127
4596  if (nondetermined) {
4597#line 130
4598    ldv_mutex = 2;
4599#line 132
4600    return (1);
4601  } else {
4602#line 137
4603    return (0);
4604  }
4605}
4606}
4607#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4608void mutex_unlock(struct mutex *lock ) 
4609{ 
4610
4611  {
4612#line 147
4613  if (ldv_mutex == 2) {
4614
4615  } else {
4616    {
4617#line 147
4618    ldv_blast_assert();
4619    }
4620  }
4621#line 149
4622  ldv_mutex = 1;
4623#line 150
4624  return;
4625}
4626}
4627#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4628void ldv_check_final_state(void) 
4629{ 
4630
4631  {
4632#line 156
4633  if (ldv_mutex == 1) {
4634
4635  } else {
4636    {
4637#line 156
4638    ldv_blast_assert();
4639    }
4640  }
4641#line 157
4642  return;
4643}
4644}
4645#line 408 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/drivers/i2c/busses/i2c-stub.c.common.c"
4646long s__builtin_expect(long val , long res ) 
4647{ 
4648
4649  {
4650#line 409
4651  return (val);
4652}
4653}