Showing error 1240

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--staging--media--cxd2099--cxd2099.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 7000
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 19 "include/asm-generic/int-ll64.h"
   5typedef signed char __s8;
   6#line 20 "include/asm-generic/int-ll64.h"
   7typedef unsigned char __u8;
   8#line 22 "include/asm-generic/int-ll64.h"
   9typedef short __s16;
  10#line 23 "include/asm-generic/int-ll64.h"
  11typedef unsigned short __u16;
  12#line 25 "include/asm-generic/int-ll64.h"
  13typedef int __s32;
  14#line 26 "include/asm-generic/int-ll64.h"
  15typedef unsigned int __u32;
  16#line 29 "include/asm-generic/int-ll64.h"
  17typedef long long __s64;
  18#line 30 "include/asm-generic/int-ll64.h"
  19typedef unsigned long long __u64;
  20#line 43 "include/asm-generic/int-ll64.h"
  21typedef unsigned char u8;
  22#line 45 "include/asm-generic/int-ll64.h"
  23typedef short s16;
  24#line 46 "include/asm-generic/int-ll64.h"
  25typedef unsigned short u16;
  26#line 48 "include/asm-generic/int-ll64.h"
  27typedef int s32;
  28#line 49 "include/asm-generic/int-ll64.h"
  29typedef unsigned int u32;
  30#line 51 "include/asm-generic/int-ll64.h"
  31typedef long long s64;
  32#line 52 "include/asm-generic/int-ll64.h"
  33typedef unsigned long long u64;
  34#line 14 "include/asm-generic/posix_types.h"
  35typedef long __kernel_long_t;
  36#line 15 "include/asm-generic/posix_types.h"
  37typedef unsigned long __kernel_ulong_t;
  38#line 31 "include/asm-generic/posix_types.h"
  39typedef int __kernel_pid_t;
  40#line 52 "include/asm-generic/posix_types.h"
  41typedef unsigned int __kernel_uid32_t;
  42#line 53 "include/asm-generic/posix_types.h"
  43typedef unsigned int __kernel_gid32_t;
  44#line 75 "include/asm-generic/posix_types.h"
  45typedef __kernel_ulong_t __kernel_size_t;
  46#line 76 "include/asm-generic/posix_types.h"
  47typedef __kernel_long_t __kernel_ssize_t;
  48#line 91 "include/asm-generic/posix_types.h"
  49typedef long long __kernel_loff_t;
  50#line 92 "include/asm-generic/posix_types.h"
  51typedef __kernel_long_t __kernel_time_t;
  52#line 93 "include/asm-generic/posix_types.h"
  53typedef __kernel_long_t __kernel_clock_t;
  54#line 94 "include/asm-generic/posix_types.h"
  55typedef int __kernel_timer_t;
  56#line 95 "include/asm-generic/posix_types.h"
  57typedef int __kernel_clockid_t;
  58#line 21 "include/linux/types.h"
  59typedef __u32 __kernel_dev_t;
  60#line 24 "include/linux/types.h"
  61typedef __kernel_dev_t dev_t;
  62#line 27 "include/linux/types.h"
  63typedef unsigned short umode_t;
  64#line 30 "include/linux/types.h"
  65typedef __kernel_pid_t pid_t;
  66#line 35 "include/linux/types.h"
  67typedef __kernel_clockid_t clockid_t;
  68#line 38 "include/linux/types.h"
  69typedef _Bool bool;
  70#line 40 "include/linux/types.h"
  71typedef __kernel_uid32_t uid_t;
  72#line 41 "include/linux/types.h"
  73typedef __kernel_gid32_t gid_t;
  74#line 54 "include/linux/types.h"
  75typedef __kernel_loff_t loff_t;
  76#line 63 "include/linux/types.h"
  77typedef __kernel_size_t size_t;
  78#line 68 "include/linux/types.h"
  79typedef __kernel_ssize_t ssize_t;
  80#line 78 "include/linux/types.h"
  81typedef __kernel_time_t time_t;
  82#line 111 "include/linux/types.h"
  83typedef __s32 int32_t;
  84#line 117 "include/linux/types.h"
  85typedef __u32 uint32_t;
  86#line 142 "include/linux/types.h"
  87typedef unsigned long sector_t;
  88#line 143 "include/linux/types.h"
  89typedef unsigned long blkcnt_t;
  90#line 202 "include/linux/types.h"
  91typedef unsigned int gfp_t;
  92#line 203 "include/linux/types.h"
  93typedef unsigned int fmode_t;
  94#line 221 "include/linux/types.h"
  95struct __anonstruct_atomic_t_6 {
  96   int counter ;
  97};
  98#line 221 "include/linux/types.h"
  99typedef struct __anonstruct_atomic_t_6 atomic_t;
 100#line 226 "include/linux/types.h"
 101struct __anonstruct_atomic64_t_7 {
 102   long counter ;
 103};
 104#line 226 "include/linux/types.h"
 105typedef struct __anonstruct_atomic64_t_7 atomic64_t;
 106#line 227 "include/linux/types.h"
 107struct list_head {
 108   struct list_head *next ;
 109   struct list_head *prev ;
 110};
 111#line 232
 112struct hlist_node;
 113#line 232 "include/linux/types.h"
 114struct hlist_head {
 115   struct hlist_node *first ;
 116};
 117#line 236 "include/linux/types.h"
 118struct hlist_node {
 119   struct hlist_node *next ;
 120   struct hlist_node **pprev ;
 121};
 122#line 247 "include/linux/types.h"
 123struct rcu_head {
 124   struct rcu_head *next ;
 125   void (*func)(struct rcu_head * ) ;
 126};
 127#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 128struct module;
 129#line 55
 130struct module;
 131#line 146 "include/linux/init.h"
 132typedef void (*ctor_fn_t)(void);
 133#line 46 "include/linux/dynamic_debug.h"
 134struct device;
 135#line 46
 136struct device;
 137#line 57
 138struct completion;
 139#line 57
 140struct completion;
 141#line 58
 142struct pt_regs;
 143#line 58
 144struct pt_regs;
 145#line 348 "include/linux/kernel.h"
 146struct pid;
 147#line 348
 148struct pid;
 149#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
 150struct timespec;
 151#line 112
 152struct timespec;
 153#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
 154struct page;
 155#line 58
 156struct page;
 157#line 26 "include/asm-generic/getorder.h"
 158struct task_struct;
 159#line 26
 160struct task_struct;
 161#line 28
 162struct mm_struct;
 163#line 28
 164struct mm_struct;
 165#line 268 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/segment.h"
 166struct pt_regs {
 167   unsigned long r15 ;
 168   unsigned long r14 ;
 169   unsigned long r13 ;
 170   unsigned long r12 ;
 171   unsigned long bp ;
 172   unsigned long bx ;
 173   unsigned long r11 ;
 174   unsigned long r10 ;
 175   unsigned long r9 ;
 176   unsigned long r8 ;
 177   unsigned long ax ;
 178   unsigned long cx ;
 179   unsigned long dx ;
 180   unsigned long si ;
 181   unsigned long di ;
 182   unsigned long orig_ax ;
 183   unsigned long ip ;
 184   unsigned long cs ;
 185   unsigned long flags ;
 186   unsigned long sp ;
 187   unsigned long ss ;
 188};
 189#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 190struct __anonstruct_ldv_2180_13 {
 191   unsigned int a ;
 192   unsigned int b ;
 193};
 194#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 195struct __anonstruct_ldv_2195_14 {
 196   u16 limit0 ;
 197   u16 base0 ;
 198   unsigned char base1 ;
 199   unsigned char type : 4 ;
 200   unsigned char s : 1 ;
 201   unsigned char dpl : 2 ;
 202   unsigned char p : 1 ;
 203   unsigned char limit : 4 ;
 204   unsigned char avl : 1 ;
 205   unsigned char l : 1 ;
 206   unsigned char d : 1 ;
 207   unsigned char g : 1 ;
 208   unsigned char base2 ;
 209};
 210#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 211union __anonunion_ldv_2196_12 {
 212   struct __anonstruct_ldv_2180_13 ldv_2180 ;
 213   struct __anonstruct_ldv_2195_14 ldv_2195 ;
 214};
 215#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 216struct desc_struct {
 217   union __anonunion_ldv_2196_12 ldv_2196 ;
 218};
 219#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 220typedef unsigned long pgdval_t;
 221#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 222typedef unsigned long pgprotval_t;
 223#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 224struct pgprot {
 225   pgprotval_t pgprot ;
 226};
 227#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 228typedef struct pgprot pgprot_t;
 229#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 230struct __anonstruct_pgd_t_16 {
 231   pgdval_t pgd ;
 232};
 233#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 234typedef struct __anonstruct_pgd_t_16 pgd_t;
 235#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 236typedef struct page *pgtable_t;
 237#line 290
 238struct file;
 239#line 290
 240struct file;
 241#line 305
 242struct seq_file;
 243#line 305
 244struct seq_file;
 245#line 337
 246struct thread_struct;
 247#line 337
 248struct thread_struct;
 249#line 339
 250struct cpumask;
 251#line 339
 252struct cpumask;
 253#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 254struct arch_spinlock;
 255#line 327
 256struct arch_spinlock;
 257#line 300 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 258struct kernel_vm86_regs {
 259   struct pt_regs pt ;
 260   unsigned short es ;
 261   unsigned short __esh ;
 262   unsigned short ds ;
 263   unsigned short __dsh ;
 264   unsigned short fs ;
 265   unsigned short __fsh ;
 266   unsigned short gs ;
 267   unsigned short __gsh ;
 268};
 269#line 203 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 270union __anonunion_ldv_2824_19 {
 271   struct pt_regs *regs ;
 272   struct kernel_vm86_regs *vm86 ;
 273};
 274#line 203 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 275struct math_emu_info {
 276   long ___orig_eip ;
 277   union __anonunion_ldv_2824_19 ldv_2824 ;
 278};
 279#line 306 "include/linux/bitmap.h"
 280struct bug_entry {
 281   int bug_addr_disp ;
 282   int file_disp ;
 283   unsigned short line ;
 284   unsigned short flags ;
 285};
 286#line 89 "include/linux/bug.h"
 287struct cpumask {
 288   unsigned long bits[64U] ;
 289};
 290#line 14 "include/linux/cpumask.h"
 291typedef struct cpumask cpumask_t;
 292#line 637 "include/linux/cpumask.h"
 293typedef struct cpumask *cpumask_var_t;
 294#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 295struct static_key;
 296#line 234
 297struct static_key;
 298#line 287 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 299struct i387_fsave_struct {
 300   u32 cwd ;
 301   u32 swd ;
 302   u32 twd ;
 303   u32 fip ;
 304   u32 fcs ;
 305   u32 foo ;
 306   u32 fos ;
 307   u32 st_space[20U] ;
 308   u32 status ;
 309};
 310#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 311struct __anonstruct_ldv_5180_24 {
 312   u64 rip ;
 313   u64 rdp ;
 314};
 315#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 316struct __anonstruct_ldv_5186_25 {
 317   u32 fip ;
 318   u32 fcs ;
 319   u32 foo ;
 320   u32 fos ;
 321};
 322#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 323union __anonunion_ldv_5187_23 {
 324   struct __anonstruct_ldv_5180_24 ldv_5180 ;
 325   struct __anonstruct_ldv_5186_25 ldv_5186 ;
 326};
 327#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 328union __anonunion_ldv_5196_26 {
 329   u32 padding1[12U] ;
 330   u32 sw_reserved[12U] ;
 331};
 332#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 333struct i387_fxsave_struct {
 334   u16 cwd ;
 335   u16 swd ;
 336   u16 twd ;
 337   u16 fop ;
 338   union __anonunion_ldv_5187_23 ldv_5187 ;
 339   u32 mxcsr ;
 340   u32 mxcsr_mask ;
 341   u32 st_space[32U] ;
 342   u32 xmm_space[64U] ;
 343   u32 padding[12U] ;
 344   union __anonunion_ldv_5196_26 ldv_5196 ;
 345};
 346#line 339 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 347struct i387_soft_struct {
 348   u32 cwd ;
 349   u32 swd ;
 350   u32 twd ;
 351   u32 fip ;
 352   u32 fcs ;
 353   u32 foo ;
 354   u32 fos ;
 355   u32 st_space[20U] ;
 356   u8 ftop ;
 357   u8 changed ;
 358   u8 lookahead ;
 359   u8 no_update ;
 360   u8 rm ;
 361   u8 alimit ;
 362   struct math_emu_info *info ;
 363   u32 entry_eip ;
 364};
 365#line 360 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 366struct ymmh_struct {
 367   u32 ymmh_space[64U] ;
 368};
 369#line 365 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 370struct xsave_hdr_struct {
 371   u64 xstate_bv ;
 372   u64 reserved1[2U] ;
 373   u64 reserved2[5U] ;
 374};
 375#line 371 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 376struct xsave_struct {
 377   struct i387_fxsave_struct i387 ;
 378   struct xsave_hdr_struct xsave_hdr ;
 379   struct ymmh_struct ymmh ;
 380};
 381#line 377 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 382union thread_xstate {
 383   struct i387_fsave_struct fsave ;
 384   struct i387_fxsave_struct fxsave ;
 385   struct i387_soft_struct soft ;
 386   struct xsave_struct xsave ;
 387};
 388#line 385 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 389struct fpu {
 390   unsigned int last_cpu ;
 391   unsigned int has_fpu ;
 392   union thread_xstate *state ;
 393};
 394#line 433
 395struct kmem_cache;
 396#line 434
 397struct perf_event;
 398#line 434
 399struct perf_event;
 400#line 435 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 401struct thread_struct {
 402   struct desc_struct tls_array[3U] ;
 403   unsigned long sp0 ;
 404   unsigned long sp ;
 405   unsigned long usersp ;
 406   unsigned short es ;
 407   unsigned short ds ;
 408   unsigned short fsindex ;
 409   unsigned short gsindex ;
 410   unsigned long fs ;
 411   unsigned long gs ;
 412   struct perf_event *ptrace_bps[4U] ;
 413   unsigned long debugreg6 ;
 414   unsigned long ptrace_dr7 ;
 415   unsigned long cr2 ;
 416   unsigned long trap_nr ;
 417   unsigned long error_code ;
 418   struct fpu fpu ;
 419   unsigned long *io_bitmap_ptr ;
 420   unsigned long iopl ;
 421   unsigned int io_bitmap_max ;
 422};
 423#line 23 "include/asm-generic/atomic-long.h"
 424typedef atomic64_t atomic_long_t;
 425#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 426typedef u16 __ticket_t;
 427#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 428typedef u32 __ticketpair_t;
 429#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 430struct __raw_tickets {
 431   __ticket_t head ;
 432   __ticket_t tail ;
 433};
 434#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 435union __anonunion_ldv_5907_29 {
 436   __ticketpair_t head_tail ;
 437   struct __raw_tickets tickets ;
 438};
 439#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 440struct arch_spinlock {
 441   union __anonunion_ldv_5907_29 ldv_5907 ;
 442};
 443#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 444typedef struct arch_spinlock arch_spinlock_t;
 445#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 446struct __anonstruct_ldv_5914_31 {
 447   u32 read ;
 448   s32 write ;
 449};
 450#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 451union __anonunion_arch_rwlock_t_30 {
 452   s64 lock ;
 453   struct __anonstruct_ldv_5914_31 ldv_5914 ;
 454};
 455#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 456typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
 457#line 34
 458struct lockdep_map;
 459#line 34
 460struct lockdep_map;
 461#line 55 "include/linux/debug_locks.h"
 462struct stack_trace {
 463   unsigned int nr_entries ;
 464   unsigned int max_entries ;
 465   unsigned long *entries ;
 466   int skip ;
 467};
 468#line 26 "include/linux/stacktrace.h"
 469struct lockdep_subclass_key {
 470   char __one_byte ;
 471};
 472#line 53 "include/linux/lockdep.h"
 473struct lock_class_key {
 474   struct lockdep_subclass_key subkeys[8U] ;
 475};
 476#line 59 "include/linux/lockdep.h"
 477struct lock_class {
 478   struct list_head hash_entry ;
 479   struct list_head lock_entry ;
 480   struct lockdep_subclass_key *key ;
 481   unsigned int subclass ;
 482   unsigned int dep_gen_id ;
 483   unsigned long usage_mask ;
 484   struct stack_trace usage_traces[13U] ;
 485   struct list_head locks_after ;
 486   struct list_head locks_before ;
 487   unsigned int version ;
 488   unsigned long ops ;
 489   char const   *name ;
 490   int name_version ;
 491   unsigned long contention_point[4U] ;
 492   unsigned long contending_point[4U] ;
 493};
 494#line 144 "include/linux/lockdep.h"
 495struct lockdep_map {
 496   struct lock_class_key *key ;
 497   struct lock_class *class_cache[2U] ;
 498   char const   *name ;
 499   int cpu ;
 500   unsigned long ip ;
 501};
 502#line 187 "include/linux/lockdep.h"
 503struct held_lock {
 504   u64 prev_chain_key ;
 505   unsigned long acquire_ip ;
 506   struct lockdep_map *instance ;
 507   struct lockdep_map *nest_lock ;
 508   u64 waittime_stamp ;
 509   u64 holdtime_stamp ;
 510   unsigned short class_idx : 13 ;
 511   unsigned char irq_context : 2 ;
 512   unsigned char trylock : 1 ;
 513   unsigned char read : 2 ;
 514   unsigned char check : 2 ;
 515   unsigned char hardirqs_off : 1 ;
 516   unsigned short references : 11 ;
 517};
 518#line 556 "include/linux/lockdep.h"
 519struct raw_spinlock {
 520   arch_spinlock_t raw_lock ;
 521   unsigned int magic ;
 522   unsigned int owner_cpu ;
 523   void *owner ;
 524   struct lockdep_map dep_map ;
 525};
 526#line 32 "include/linux/spinlock_types.h"
 527typedef struct raw_spinlock raw_spinlock_t;
 528#line 33 "include/linux/spinlock_types.h"
 529struct __anonstruct_ldv_6122_33 {
 530   u8 __padding[24U] ;
 531   struct lockdep_map dep_map ;
 532};
 533#line 33 "include/linux/spinlock_types.h"
 534union __anonunion_ldv_6123_32 {
 535   struct raw_spinlock rlock ;
 536   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 537};
 538#line 33 "include/linux/spinlock_types.h"
 539struct spinlock {
 540   union __anonunion_ldv_6123_32 ldv_6123 ;
 541};
 542#line 76 "include/linux/spinlock_types.h"
 543typedef struct spinlock spinlock_t;
 544#line 23 "include/linux/rwlock_types.h"
 545struct __anonstruct_rwlock_t_34 {
 546   arch_rwlock_t raw_lock ;
 547   unsigned int magic ;
 548   unsigned int owner_cpu ;
 549   void *owner ;
 550   struct lockdep_map dep_map ;
 551};
 552#line 23 "include/linux/rwlock_types.h"
 553typedef struct __anonstruct_rwlock_t_34 rwlock_t;
 554#line 110 "include/linux/seqlock.h"
 555struct seqcount {
 556   unsigned int sequence ;
 557};
 558#line 121 "include/linux/seqlock.h"
 559typedef struct seqcount seqcount_t;
 560#line 254 "include/linux/seqlock.h"
 561struct timespec {
 562   __kernel_time_t tv_sec ;
 563   long tv_nsec ;
 564};
 565#line 286 "include/linux/time.h"
 566struct kstat {
 567   u64 ino ;
 568   dev_t dev ;
 569   umode_t mode ;
 570   unsigned int nlink ;
 571   uid_t uid ;
 572   gid_t gid ;
 573   dev_t rdev ;
 574   loff_t size ;
 575   struct timespec atime ;
 576   struct timespec mtime ;
 577   struct timespec ctime ;
 578   unsigned long blksize ;
 579   unsigned long long blocks ;
 580};
 581#line 48 "include/linux/wait.h"
 582struct __wait_queue_head {
 583   spinlock_t lock ;
 584   struct list_head task_list ;
 585};
 586#line 53 "include/linux/wait.h"
 587typedef struct __wait_queue_head wait_queue_head_t;
 588#line 98 "include/linux/nodemask.h"
 589struct __anonstruct_nodemask_t_36 {
 590   unsigned long bits[16U] ;
 591};
 592#line 98 "include/linux/nodemask.h"
 593typedef struct __anonstruct_nodemask_t_36 nodemask_t;
 594#line 670 "include/linux/mmzone.h"
 595struct mutex {
 596   atomic_t count ;
 597   spinlock_t wait_lock ;
 598   struct list_head wait_list ;
 599   struct task_struct *owner ;
 600   char const   *name ;
 601   void *magic ;
 602   struct lockdep_map dep_map ;
 603};
 604#line 63 "include/linux/mutex.h"
 605struct mutex_waiter {
 606   struct list_head list ;
 607   struct task_struct *task ;
 608   void *magic ;
 609};
 610#line 171
 611struct rw_semaphore;
 612#line 171
 613struct rw_semaphore;
 614#line 172 "include/linux/mutex.h"
 615struct rw_semaphore {
 616   long count ;
 617   raw_spinlock_t wait_lock ;
 618   struct list_head wait_list ;
 619   struct lockdep_map dep_map ;
 620};
 621#line 128 "include/linux/rwsem.h"
 622struct completion {
 623   unsigned int done ;
 624   wait_queue_head_t wait ;
 625};
 626#line 312 "include/linux/jiffies.h"
 627union ktime {
 628   s64 tv64 ;
 629};
 630#line 59 "include/linux/ktime.h"
 631typedef union ktime ktime_t;
 632#line 341
 633struct tvec_base;
 634#line 341
 635struct tvec_base;
 636#line 342 "include/linux/ktime.h"
 637struct timer_list {
 638   struct list_head entry ;
 639   unsigned long expires ;
 640   struct tvec_base *base ;
 641   void (*function)(unsigned long  ) ;
 642   unsigned long data ;
 643   int slack ;
 644   int start_pid ;
 645   void *start_site ;
 646   char start_comm[16U] ;
 647   struct lockdep_map lockdep_map ;
 648};
 649#line 289 "include/linux/timer.h"
 650struct hrtimer;
 651#line 289
 652struct hrtimer;
 653#line 290
 654enum hrtimer_restart;
 655#line 302
 656struct work_struct;
 657#line 302
 658struct work_struct;
 659#line 45 "include/linux/workqueue.h"
 660struct work_struct {
 661   atomic_long_t data ;
 662   struct list_head entry ;
 663   void (*func)(struct work_struct * ) ;
 664   struct lockdep_map lockdep_map ;
 665};
 666#line 86 "include/linux/workqueue.h"
 667struct delayed_work {
 668   struct work_struct work ;
 669   struct timer_list timer ;
 670};
 671#line 46 "include/linux/pm.h"
 672struct pm_message {
 673   int event ;
 674};
 675#line 52 "include/linux/pm.h"
 676typedef struct pm_message pm_message_t;
 677#line 53 "include/linux/pm.h"
 678struct dev_pm_ops {
 679   int (*prepare)(struct device * ) ;
 680   void (*complete)(struct device * ) ;
 681   int (*suspend)(struct device * ) ;
 682   int (*resume)(struct device * ) ;
 683   int (*freeze)(struct device * ) ;
 684   int (*thaw)(struct device * ) ;
 685   int (*poweroff)(struct device * ) ;
 686   int (*restore)(struct device * ) ;
 687   int (*suspend_late)(struct device * ) ;
 688   int (*resume_early)(struct device * ) ;
 689   int (*freeze_late)(struct device * ) ;
 690   int (*thaw_early)(struct device * ) ;
 691   int (*poweroff_late)(struct device * ) ;
 692   int (*restore_early)(struct device * ) ;
 693   int (*suspend_noirq)(struct device * ) ;
 694   int (*resume_noirq)(struct device * ) ;
 695   int (*freeze_noirq)(struct device * ) ;
 696   int (*thaw_noirq)(struct device * ) ;
 697   int (*poweroff_noirq)(struct device * ) ;
 698   int (*restore_noirq)(struct device * ) ;
 699   int (*runtime_suspend)(struct device * ) ;
 700   int (*runtime_resume)(struct device * ) ;
 701   int (*runtime_idle)(struct device * ) ;
 702};
 703#line 289
 704enum rpm_status {
 705    RPM_ACTIVE = 0,
 706    RPM_RESUMING = 1,
 707    RPM_SUSPENDED = 2,
 708    RPM_SUSPENDING = 3
 709} ;
 710#line 296
 711enum rpm_request {
 712    RPM_REQ_NONE = 0,
 713    RPM_REQ_IDLE = 1,
 714    RPM_REQ_SUSPEND = 2,
 715    RPM_REQ_AUTOSUSPEND = 3,
 716    RPM_REQ_RESUME = 4
 717} ;
 718#line 304
 719struct wakeup_source;
 720#line 304
 721struct wakeup_source;
 722#line 494 "include/linux/pm.h"
 723struct pm_subsys_data {
 724   spinlock_t lock ;
 725   unsigned int refcount ;
 726};
 727#line 499
 728struct dev_pm_qos_request;
 729#line 499
 730struct pm_qos_constraints;
 731#line 499 "include/linux/pm.h"
 732struct dev_pm_info {
 733   pm_message_t power_state ;
 734   unsigned char can_wakeup : 1 ;
 735   unsigned char async_suspend : 1 ;
 736   bool is_prepared ;
 737   bool is_suspended ;
 738   bool ignore_children ;
 739   spinlock_t lock ;
 740   struct list_head entry ;
 741   struct completion completion ;
 742   struct wakeup_source *wakeup ;
 743   bool wakeup_path ;
 744   struct timer_list suspend_timer ;
 745   unsigned long timer_expires ;
 746   struct work_struct work ;
 747   wait_queue_head_t wait_queue ;
 748   atomic_t usage_count ;
 749   atomic_t child_count ;
 750   unsigned char disable_depth : 3 ;
 751   unsigned char idle_notification : 1 ;
 752   unsigned char request_pending : 1 ;
 753   unsigned char deferred_resume : 1 ;
 754   unsigned char run_wake : 1 ;
 755   unsigned char runtime_auto : 1 ;
 756   unsigned char no_callbacks : 1 ;
 757   unsigned char irq_safe : 1 ;
 758   unsigned char use_autosuspend : 1 ;
 759   unsigned char timer_autosuspends : 1 ;
 760   enum rpm_request request ;
 761   enum rpm_status runtime_status ;
 762   int runtime_error ;
 763   int autosuspend_delay ;
 764   unsigned long last_busy ;
 765   unsigned long active_jiffies ;
 766   unsigned long suspended_jiffies ;
 767   unsigned long accounting_timestamp ;
 768   ktime_t suspend_time ;
 769   s64 max_time_suspended_ns ;
 770   struct dev_pm_qos_request *pq_req ;
 771   struct pm_subsys_data *subsys_data ;
 772   struct pm_qos_constraints *constraints ;
 773};
 774#line 558 "include/linux/pm.h"
 775struct dev_pm_domain {
 776   struct dev_pm_ops ops ;
 777};
 778#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 779struct __anonstruct_mm_context_t_101 {
 780   void *ldt ;
 781   int size ;
 782   unsigned short ia32_compat ;
 783   struct mutex lock ;
 784   void *vdso ;
 785};
 786#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 787typedef struct __anonstruct_mm_context_t_101 mm_context_t;
 788#line 18 "include/asm-generic/pci_iomap.h"
 789struct vm_area_struct;
 790#line 18
 791struct vm_area_struct;
 792#line 835 "include/linux/sysctl.h"
 793struct rb_node {
 794   unsigned long rb_parent_color ;
 795   struct rb_node *rb_right ;
 796   struct rb_node *rb_left ;
 797};
 798#line 108 "include/linux/rbtree.h"
 799struct rb_root {
 800   struct rb_node *rb_node ;
 801};
 802#line 176
 803struct nsproxy;
 804#line 176
 805struct nsproxy;
 806#line 37 "include/linux/kmod.h"
 807struct cred;
 808#line 37
 809struct cred;
 810#line 18 "include/linux/elf.h"
 811typedef __u64 Elf64_Addr;
 812#line 19 "include/linux/elf.h"
 813typedef __u16 Elf64_Half;
 814#line 23 "include/linux/elf.h"
 815typedef __u32 Elf64_Word;
 816#line 24 "include/linux/elf.h"
 817typedef __u64 Elf64_Xword;
 818#line 193 "include/linux/elf.h"
 819struct elf64_sym {
 820   Elf64_Word st_name ;
 821   unsigned char st_info ;
 822   unsigned char st_other ;
 823   Elf64_Half st_shndx ;
 824   Elf64_Addr st_value ;
 825   Elf64_Xword st_size ;
 826};
 827#line 201 "include/linux/elf.h"
 828typedef struct elf64_sym Elf64_Sym;
 829#line 445
 830struct sock;
 831#line 445
 832struct sock;
 833#line 446
 834struct kobject;
 835#line 446
 836struct kobject;
 837#line 447
 838enum kobj_ns_type {
 839    KOBJ_NS_TYPE_NONE = 0,
 840    KOBJ_NS_TYPE_NET = 1,
 841    KOBJ_NS_TYPES = 2
 842} ;
 843#line 453 "include/linux/elf.h"
 844struct kobj_ns_type_operations {
 845   enum kobj_ns_type type ;
 846   void *(*grab_current_ns)(void) ;
 847   void const   *(*netlink_ns)(struct sock * ) ;
 848   void const   *(*initial_ns)(void) ;
 849   void (*drop_ns)(void * ) ;
 850};
 851#line 57 "include/linux/kobject_ns.h"
 852struct attribute {
 853   char const   *name ;
 854   umode_t mode ;
 855   struct lock_class_key *key ;
 856   struct lock_class_key skey ;
 857};
 858#line 33 "include/linux/sysfs.h"
 859struct attribute_group {
 860   char const   *name ;
 861   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 862   struct attribute **attrs ;
 863};
 864#line 62 "include/linux/sysfs.h"
 865struct bin_attribute {
 866   struct attribute attr ;
 867   size_t size ;
 868   void *private ;
 869   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 870                   loff_t  , size_t  ) ;
 871   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 872                    loff_t  , size_t  ) ;
 873   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
 874};
 875#line 98 "include/linux/sysfs.h"
 876struct sysfs_ops {
 877   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 878   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 879   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 880};
 881#line 117
 882struct sysfs_dirent;
 883#line 117
 884struct sysfs_dirent;
 885#line 182 "include/linux/sysfs.h"
 886struct kref {
 887   atomic_t refcount ;
 888};
 889#line 49 "include/linux/kobject.h"
 890struct kset;
 891#line 49
 892struct kobj_type;
 893#line 49 "include/linux/kobject.h"
 894struct kobject {
 895   char const   *name ;
 896   struct list_head entry ;
 897   struct kobject *parent ;
 898   struct kset *kset ;
 899   struct kobj_type *ktype ;
 900   struct sysfs_dirent *sd ;
 901   struct kref kref ;
 902   unsigned char state_initialized : 1 ;
 903   unsigned char state_in_sysfs : 1 ;
 904   unsigned char state_add_uevent_sent : 1 ;
 905   unsigned char state_remove_uevent_sent : 1 ;
 906   unsigned char uevent_suppress : 1 ;
 907};
 908#line 107 "include/linux/kobject.h"
 909struct kobj_type {
 910   void (*release)(struct kobject * ) ;
 911   struct sysfs_ops  const  *sysfs_ops ;
 912   struct attribute **default_attrs ;
 913   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 914   void const   *(*namespace)(struct kobject * ) ;
 915};
 916#line 115 "include/linux/kobject.h"
 917struct kobj_uevent_env {
 918   char *envp[32U] ;
 919   int envp_idx ;
 920   char buf[2048U] ;
 921   int buflen ;
 922};
 923#line 122 "include/linux/kobject.h"
 924struct kset_uevent_ops {
 925   int (* const  filter)(struct kset * , struct kobject * ) ;
 926   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 927   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 928};
 929#line 139 "include/linux/kobject.h"
 930struct kset {
 931   struct list_head list ;
 932   spinlock_t list_lock ;
 933   struct kobject kobj ;
 934   struct kset_uevent_ops  const  *uevent_ops ;
 935};
 936#line 215
 937struct kernel_param;
 938#line 215
 939struct kernel_param;
 940#line 216 "include/linux/kobject.h"
 941struct kernel_param_ops {
 942   int (*set)(char const   * , struct kernel_param  const  * ) ;
 943   int (*get)(char * , struct kernel_param  const  * ) ;
 944   void (*free)(void * ) ;
 945};
 946#line 49 "include/linux/moduleparam.h"
 947struct kparam_string;
 948#line 49
 949struct kparam_array;
 950#line 49 "include/linux/moduleparam.h"
 951union __anonunion_ldv_13363_134 {
 952   void *arg ;
 953   struct kparam_string  const  *str ;
 954   struct kparam_array  const  *arr ;
 955};
 956#line 49 "include/linux/moduleparam.h"
 957struct kernel_param {
 958   char const   *name ;
 959   struct kernel_param_ops  const  *ops ;
 960   u16 perm ;
 961   s16 level ;
 962   union __anonunion_ldv_13363_134 ldv_13363 ;
 963};
 964#line 61 "include/linux/moduleparam.h"
 965struct kparam_string {
 966   unsigned int maxlen ;
 967   char *string ;
 968};
 969#line 67 "include/linux/moduleparam.h"
 970struct kparam_array {
 971   unsigned int max ;
 972   unsigned int elemsize ;
 973   unsigned int *num ;
 974   struct kernel_param_ops  const  *ops ;
 975   void *elem ;
 976};
 977#line 458 "include/linux/moduleparam.h"
 978struct static_key {
 979   atomic_t enabled ;
 980};
 981#line 225 "include/linux/jump_label.h"
 982struct tracepoint;
 983#line 225
 984struct tracepoint;
 985#line 226 "include/linux/jump_label.h"
 986struct tracepoint_func {
 987   void *func ;
 988   void *data ;
 989};
 990#line 29 "include/linux/tracepoint.h"
 991struct tracepoint {
 992   char const   *name ;
 993   struct static_key key ;
 994   void (*regfunc)(void) ;
 995   void (*unregfunc)(void) ;
 996   struct tracepoint_func *funcs ;
 997};
 998#line 86 "include/linux/tracepoint.h"
 999struct kernel_symbol {
1000   unsigned long value ;
1001   char const   *name ;
1002};
1003#line 27 "include/linux/export.h"
1004struct mod_arch_specific {
1005
1006};
1007#line 34 "include/linux/module.h"
1008struct module_param_attrs;
1009#line 34 "include/linux/module.h"
1010struct module_kobject {
1011   struct kobject kobj ;
1012   struct module *mod ;
1013   struct kobject *drivers_dir ;
1014   struct module_param_attrs *mp ;
1015};
1016#line 43 "include/linux/module.h"
1017struct module_attribute {
1018   struct attribute attr ;
1019   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
1020   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
1021                    size_t  ) ;
1022   void (*setup)(struct module * , char const   * ) ;
1023   int (*test)(struct module * ) ;
1024   void (*free)(struct module * ) ;
1025};
1026#line 69
1027struct exception_table_entry;
1028#line 69
1029struct exception_table_entry;
1030#line 198
1031enum module_state {
1032    MODULE_STATE_LIVE = 0,
1033    MODULE_STATE_COMING = 1,
1034    MODULE_STATE_GOING = 2
1035} ;
1036#line 204 "include/linux/module.h"
1037struct module_ref {
1038   unsigned long incs ;
1039   unsigned long decs ;
1040};
1041#line 219
1042struct module_sect_attrs;
1043#line 219
1044struct module_notes_attrs;
1045#line 219
1046struct ftrace_event_call;
1047#line 219 "include/linux/module.h"
1048struct module {
1049   enum module_state state ;
1050   struct list_head list ;
1051   char name[56U] ;
1052   struct module_kobject mkobj ;
1053   struct module_attribute *modinfo_attrs ;
1054   char const   *version ;
1055   char const   *srcversion ;
1056   struct kobject *holders_dir ;
1057   struct kernel_symbol  const  *syms ;
1058   unsigned long const   *crcs ;
1059   unsigned int num_syms ;
1060   struct kernel_param *kp ;
1061   unsigned int num_kp ;
1062   unsigned int num_gpl_syms ;
1063   struct kernel_symbol  const  *gpl_syms ;
1064   unsigned long const   *gpl_crcs ;
1065   struct kernel_symbol  const  *unused_syms ;
1066   unsigned long const   *unused_crcs ;
1067   unsigned int num_unused_syms ;
1068   unsigned int num_unused_gpl_syms ;
1069   struct kernel_symbol  const  *unused_gpl_syms ;
1070   unsigned long const   *unused_gpl_crcs ;
1071   struct kernel_symbol  const  *gpl_future_syms ;
1072   unsigned long const   *gpl_future_crcs ;
1073   unsigned int num_gpl_future_syms ;
1074   unsigned int num_exentries ;
1075   struct exception_table_entry *extable ;
1076   int (*init)(void) ;
1077   void *module_init ;
1078   void *module_core ;
1079   unsigned int init_size ;
1080   unsigned int core_size ;
1081   unsigned int init_text_size ;
1082   unsigned int core_text_size ;
1083   unsigned int init_ro_size ;
1084   unsigned int core_ro_size ;
1085   struct mod_arch_specific arch ;
1086   unsigned int taints ;
1087   unsigned int num_bugs ;
1088   struct list_head bug_list ;
1089   struct bug_entry *bug_table ;
1090   Elf64_Sym *symtab ;
1091   Elf64_Sym *core_symtab ;
1092   unsigned int num_symtab ;
1093   unsigned int core_num_syms ;
1094   char *strtab ;
1095   char *core_strtab ;
1096   struct module_sect_attrs *sect_attrs ;
1097   struct module_notes_attrs *notes_attrs ;
1098   char *args ;
1099   void *percpu ;
1100   unsigned int percpu_size ;
1101   unsigned int num_tracepoints ;
1102   struct tracepoint * const  *tracepoints_ptrs ;
1103   unsigned int num_trace_bprintk_fmt ;
1104   char const   **trace_bprintk_fmt_start ;
1105   struct ftrace_event_call **trace_events ;
1106   unsigned int num_trace_events ;
1107   struct list_head source_list ;
1108   struct list_head target_list ;
1109   struct task_struct *waiter ;
1110   void (*exit)(void) ;
1111   struct module_ref *refptr ;
1112   ctor_fn_t (**ctors)(void) ;
1113   unsigned int num_ctors ;
1114};
1115#line 88 "include/linux/kmemleak.h"
1116struct kmem_cache_cpu {
1117   void **freelist ;
1118   unsigned long tid ;
1119   struct page *page ;
1120   struct page *partial ;
1121   int node ;
1122   unsigned int stat[26U] ;
1123};
1124#line 55 "include/linux/slub_def.h"
1125struct kmem_cache_node {
1126   spinlock_t list_lock ;
1127   unsigned long nr_partial ;
1128   struct list_head partial ;
1129   atomic_long_t nr_slabs ;
1130   atomic_long_t total_objects ;
1131   struct list_head full ;
1132};
1133#line 66 "include/linux/slub_def.h"
1134struct kmem_cache_order_objects {
1135   unsigned long x ;
1136};
1137#line 76 "include/linux/slub_def.h"
1138struct kmem_cache {
1139   struct kmem_cache_cpu *cpu_slab ;
1140   unsigned long flags ;
1141   unsigned long min_partial ;
1142   int size ;
1143   int objsize ;
1144   int offset ;
1145   int cpu_partial ;
1146   struct kmem_cache_order_objects oo ;
1147   struct kmem_cache_order_objects max ;
1148   struct kmem_cache_order_objects min ;
1149   gfp_t allocflags ;
1150   int refcount ;
1151   void (*ctor)(void * ) ;
1152   int inuse ;
1153   int align ;
1154   int reserved ;
1155   char const   *name ;
1156   struct list_head list ;
1157   struct kobject kobj ;
1158   int remote_node_defrag_ratio ;
1159   struct kmem_cache_node *node[1024U] ;
1160};
1161#line 215 "include/linux/mod_devicetable.h"
1162struct of_device_id {
1163   char name[32U] ;
1164   char type[32U] ;
1165   char compatible[128U] ;
1166   void *data ;
1167};
1168#line 584
1169struct klist_node;
1170#line 584
1171struct klist_node;
1172#line 37 "include/linux/klist.h"
1173struct klist_node {
1174   void *n_klist ;
1175   struct list_head n_node ;
1176   struct kref n_ref ;
1177};
1178#line 67
1179struct dma_map_ops;
1180#line 67 "include/linux/klist.h"
1181struct dev_archdata {
1182   void *acpi_handle ;
1183   struct dma_map_ops *dma_ops ;
1184   void *iommu ;
1185};
1186#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1187struct device_private;
1188#line 17
1189struct device_private;
1190#line 18
1191struct device_driver;
1192#line 18
1193struct device_driver;
1194#line 19
1195struct driver_private;
1196#line 19
1197struct driver_private;
1198#line 20
1199struct class;
1200#line 20
1201struct class;
1202#line 21
1203struct subsys_private;
1204#line 21
1205struct subsys_private;
1206#line 22
1207struct bus_type;
1208#line 22
1209struct bus_type;
1210#line 23
1211struct device_node;
1212#line 23
1213struct device_node;
1214#line 24
1215struct iommu_ops;
1216#line 24
1217struct iommu_ops;
1218#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1219struct bus_attribute {
1220   struct attribute attr ;
1221   ssize_t (*show)(struct bus_type * , char * ) ;
1222   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
1223};
1224#line 51 "include/linux/device.h"
1225struct device_attribute;
1226#line 51
1227struct driver_attribute;
1228#line 51 "include/linux/device.h"
1229struct bus_type {
1230   char const   *name ;
1231   char const   *dev_name ;
1232   struct device *dev_root ;
1233   struct bus_attribute *bus_attrs ;
1234   struct device_attribute *dev_attrs ;
1235   struct driver_attribute *drv_attrs ;
1236   int (*match)(struct device * , struct device_driver * ) ;
1237   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1238   int (*probe)(struct device * ) ;
1239   int (*remove)(struct device * ) ;
1240   void (*shutdown)(struct device * ) ;
1241   int (*suspend)(struct device * , pm_message_t  ) ;
1242   int (*resume)(struct device * ) ;
1243   struct dev_pm_ops  const  *pm ;
1244   struct iommu_ops *iommu_ops ;
1245   struct subsys_private *p ;
1246};
1247#line 125
1248struct device_type;
1249#line 182 "include/linux/device.h"
1250struct device_driver {
1251   char const   *name ;
1252   struct bus_type *bus ;
1253   struct module *owner ;
1254   char const   *mod_name ;
1255   bool suppress_bind_attrs ;
1256   struct of_device_id  const  *of_match_table ;
1257   int (*probe)(struct device * ) ;
1258   int (*remove)(struct device * ) ;
1259   void (*shutdown)(struct device * ) ;
1260   int (*suspend)(struct device * , pm_message_t  ) ;
1261   int (*resume)(struct device * ) ;
1262   struct attribute_group  const  **groups ;
1263   struct dev_pm_ops  const  *pm ;
1264   struct driver_private *p ;
1265};
1266#line 245 "include/linux/device.h"
1267struct driver_attribute {
1268   struct attribute attr ;
1269   ssize_t (*show)(struct device_driver * , char * ) ;
1270   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
1271};
1272#line 299
1273struct class_attribute;
1274#line 299 "include/linux/device.h"
1275struct class {
1276   char const   *name ;
1277   struct module *owner ;
1278   struct class_attribute *class_attrs ;
1279   struct device_attribute *dev_attrs ;
1280   struct bin_attribute *dev_bin_attrs ;
1281   struct kobject *dev_kobj ;
1282   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
1283   char *(*devnode)(struct device * , umode_t * ) ;
1284   void (*class_release)(struct class * ) ;
1285   void (*dev_release)(struct device * ) ;
1286   int (*suspend)(struct device * , pm_message_t  ) ;
1287   int (*resume)(struct device * ) ;
1288   struct kobj_ns_type_operations  const  *ns_type ;
1289   void const   *(*namespace)(struct device * ) ;
1290   struct dev_pm_ops  const  *pm ;
1291   struct subsys_private *p ;
1292};
1293#line 394 "include/linux/device.h"
1294struct class_attribute {
1295   struct attribute attr ;
1296   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
1297   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
1298   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
1299};
1300#line 447 "include/linux/device.h"
1301struct device_type {
1302   char const   *name ;
1303   struct attribute_group  const  **groups ;
1304   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1305   char *(*devnode)(struct device * , umode_t * ) ;
1306   void (*release)(struct device * ) ;
1307   struct dev_pm_ops  const  *pm ;
1308};
1309#line 474 "include/linux/device.h"
1310struct device_attribute {
1311   struct attribute attr ;
1312   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
1313   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
1314                    size_t  ) ;
1315};
1316#line 557 "include/linux/device.h"
1317struct device_dma_parameters {
1318   unsigned int max_segment_size ;
1319   unsigned long segment_boundary_mask ;
1320};
1321#line 567
1322struct dma_coherent_mem;
1323#line 567 "include/linux/device.h"
1324struct device {
1325   struct device *parent ;
1326   struct device_private *p ;
1327   struct kobject kobj ;
1328   char const   *init_name ;
1329   struct device_type  const  *type ;
1330   struct mutex mutex ;
1331   struct bus_type *bus ;
1332   struct device_driver *driver ;
1333   void *platform_data ;
1334   struct dev_pm_info power ;
1335   struct dev_pm_domain *pm_domain ;
1336   int numa_node ;
1337   u64 *dma_mask ;
1338   u64 coherent_dma_mask ;
1339   struct device_dma_parameters *dma_parms ;
1340   struct list_head dma_pools ;
1341   struct dma_coherent_mem *dma_mem ;
1342   struct dev_archdata archdata ;
1343   struct device_node *of_node ;
1344   dev_t devt ;
1345   u32 id ;
1346   spinlock_t devres_lock ;
1347   struct list_head devres_head ;
1348   struct klist_node knode_class ;
1349   struct class *class ;
1350   struct attribute_group  const  **groups ;
1351   void (*release)(struct device * ) ;
1352};
1353#line 681 "include/linux/device.h"
1354struct wakeup_source {
1355   char const   *name ;
1356   struct list_head entry ;
1357   spinlock_t lock ;
1358   struct timer_list timer ;
1359   unsigned long timer_expires ;
1360   ktime_t total_time ;
1361   ktime_t max_time ;
1362   ktime_t last_time ;
1363   unsigned long event_count ;
1364   unsigned long active_count ;
1365   unsigned long relax_count ;
1366   unsigned long hit_count ;
1367   unsigned char active : 1 ;
1368};
1369#line 93 "include/linux/capability.h"
1370struct kernel_cap_struct {
1371   __u32 cap[2U] ;
1372};
1373#line 96 "include/linux/capability.h"
1374typedef struct kernel_cap_struct kernel_cap_t;
1375#line 104
1376struct dentry;
1377#line 104
1378struct dentry;
1379#line 105
1380struct user_namespace;
1381#line 105
1382struct user_namespace;
1383#line 554
1384struct prio_tree_node;
1385#line 554 "include/linux/capability.h"
1386struct raw_prio_tree_node {
1387   struct prio_tree_node *left ;
1388   struct prio_tree_node *right ;
1389   struct prio_tree_node *parent ;
1390};
1391#line 19 "include/linux/prio_tree.h"
1392struct prio_tree_node {
1393   struct prio_tree_node *left ;
1394   struct prio_tree_node *right ;
1395   struct prio_tree_node *parent ;
1396   unsigned long start ;
1397   unsigned long last ;
1398};
1399#line 27 "include/linux/prio_tree.h"
1400struct prio_tree_root {
1401   struct prio_tree_node *prio_tree_node ;
1402   unsigned short index_bits ;
1403   unsigned short raw ;
1404};
1405#line 116
1406struct address_space;
1407#line 116
1408struct address_space;
1409#line 117 "include/linux/prio_tree.h"
1410union __anonunion_ldv_15299_138 {
1411   unsigned long index ;
1412   void *freelist ;
1413};
1414#line 117 "include/linux/prio_tree.h"
1415struct __anonstruct_ldv_15309_142 {
1416   unsigned short inuse ;
1417   unsigned short objects : 15 ;
1418   unsigned char frozen : 1 ;
1419};
1420#line 117 "include/linux/prio_tree.h"
1421union __anonunion_ldv_15310_141 {
1422   atomic_t _mapcount ;
1423   struct __anonstruct_ldv_15309_142 ldv_15309 ;
1424};
1425#line 117 "include/linux/prio_tree.h"
1426struct __anonstruct_ldv_15312_140 {
1427   union __anonunion_ldv_15310_141 ldv_15310 ;
1428   atomic_t _count ;
1429};
1430#line 117 "include/linux/prio_tree.h"
1431union __anonunion_ldv_15313_139 {
1432   unsigned long counters ;
1433   struct __anonstruct_ldv_15312_140 ldv_15312 ;
1434};
1435#line 117 "include/linux/prio_tree.h"
1436struct __anonstruct_ldv_15314_137 {
1437   union __anonunion_ldv_15299_138 ldv_15299 ;
1438   union __anonunion_ldv_15313_139 ldv_15313 ;
1439};
1440#line 117 "include/linux/prio_tree.h"
1441struct __anonstruct_ldv_15321_144 {
1442   struct page *next ;
1443   int pages ;
1444   int pobjects ;
1445};
1446#line 117 "include/linux/prio_tree.h"
1447union __anonunion_ldv_15322_143 {
1448   struct list_head lru ;
1449   struct __anonstruct_ldv_15321_144 ldv_15321 ;
1450};
1451#line 117 "include/linux/prio_tree.h"
1452union __anonunion_ldv_15327_145 {
1453   unsigned long private ;
1454   struct kmem_cache *slab ;
1455   struct page *first_page ;
1456};
1457#line 117 "include/linux/prio_tree.h"
1458struct page {
1459   unsigned long flags ;
1460   struct address_space *mapping ;
1461   struct __anonstruct_ldv_15314_137 ldv_15314 ;
1462   union __anonunion_ldv_15322_143 ldv_15322 ;
1463   union __anonunion_ldv_15327_145 ldv_15327 ;
1464   unsigned long debug_flags ;
1465};
1466#line 192 "include/linux/mm_types.h"
1467struct __anonstruct_vm_set_147 {
1468   struct list_head list ;
1469   void *parent ;
1470   struct vm_area_struct *head ;
1471};
1472#line 192 "include/linux/mm_types.h"
1473union __anonunion_shared_146 {
1474   struct __anonstruct_vm_set_147 vm_set ;
1475   struct raw_prio_tree_node prio_tree_node ;
1476};
1477#line 192
1478struct anon_vma;
1479#line 192
1480struct vm_operations_struct;
1481#line 192
1482struct mempolicy;
1483#line 192 "include/linux/mm_types.h"
1484struct vm_area_struct {
1485   struct mm_struct *vm_mm ;
1486   unsigned long vm_start ;
1487   unsigned long vm_end ;
1488   struct vm_area_struct *vm_next ;
1489   struct vm_area_struct *vm_prev ;
1490   pgprot_t vm_page_prot ;
1491   unsigned long vm_flags ;
1492   struct rb_node vm_rb ;
1493   union __anonunion_shared_146 shared ;
1494   struct list_head anon_vma_chain ;
1495   struct anon_vma *anon_vma ;
1496   struct vm_operations_struct  const  *vm_ops ;
1497   unsigned long vm_pgoff ;
1498   struct file *vm_file ;
1499   void *vm_private_data ;
1500   struct mempolicy *vm_policy ;
1501};
1502#line 255 "include/linux/mm_types.h"
1503struct core_thread {
1504   struct task_struct *task ;
1505   struct core_thread *next ;
1506};
1507#line 261 "include/linux/mm_types.h"
1508struct core_state {
1509   atomic_t nr_threads ;
1510   struct core_thread dumper ;
1511   struct completion startup ;
1512};
1513#line 274 "include/linux/mm_types.h"
1514struct mm_rss_stat {
1515   atomic_long_t count[3U] ;
1516};
1517#line 287
1518struct linux_binfmt;
1519#line 287
1520struct mmu_notifier_mm;
1521#line 287 "include/linux/mm_types.h"
1522struct mm_struct {
1523   struct vm_area_struct *mmap ;
1524   struct rb_root mm_rb ;
1525   struct vm_area_struct *mmap_cache ;
1526   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1527                                      unsigned long  , unsigned long  ) ;
1528   void (*unmap_area)(struct mm_struct * , unsigned long  ) ;
1529   unsigned long mmap_base ;
1530   unsigned long task_size ;
1531   unsigned long cached_hole_size ;
1532   unsigned long free_area_cache ;
1533   pgd_t *pgd ;
1534   atomic_t mm_users ;
1535   atomic_t mm_count ;
1536   int map_count ;
1537   spinlock_t page_table_lock ;
1538   struct rw_semaphore mmap_sem ;
1539   struct list_head mmlist ;
1540   unsigned long hiwater_rss ;
1541   unsigned long hiwater_vm ;
1542   unsigned long total_vm ;
1543   unsigned long locked_vm ;
1544   unsigned long pinned_vm ;
1545   unsigned long shared_vm ;
1546   unsigned long exec_vm ;
1547   unsigned long stack_vm ;
1548   unsigned long reserved_vm ;
1549   unsigned long def_flags ;
1550   unsigned long nr_ptes ;
1551   unsigned long start_code ;
1552   unsigned long end_code ;
1553   unsigned long start_data ;
1554   unsigned long end_data ;
1555   unsigned long start_brk ;
1556   unsigned long brk ;
1557   unsigned long start_stack ;
1558   unsigned long arg_start ;
1559   unsigned long arg_end ;
1560   unsigned long env_start ;
1561   unsigned long env_end ;
1562   unsigned long saved_auxv[44U] ;
1563   struct mm_rss_stat rss_stat ;
1564   struct linux_binfmt *binfmt ;
1565   cpumask_var_t cpu_vm_mask_var ;
1566   mm_context_t context ;
1567   unsigned int faultstamp ;
1568   unsigned int token_priority ;
1569   unsigned int last_interval ;
1570   unsigned long flags ;
1571   struct core_state *core_state ;
1572   spinlock_t ioctx_lock ;
1573   struct hlist_head ioctx_list ;
1574   struct task_struct *owner ;
1575   struct file *exe_file ;
1576   unsigned long num_exe_file_vmas ;
1577   struct mmu_notifier_mm *mmu_notifier_mm ;
1578   pgtable_t pmd_huge_pte ;
1579   struct cpumask cpumask_allocation ;
1580};
1581#line 7 "include/asm-generic/cputime.h"
1582typedef unsigned long cputime_t;
1583#line 98 "include/linux/sem.h"
1584struct sem_undo_list;
1585#line 98 "include/linux/sem.h"
1586struct sysv_sem {
1587   struct sem_undo_list *undo_list ;
1588};
1589#line 107
1590struct siginfo;
1591#line 107
1592struct siginfo;
1593#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1594struct __anonstruct_sigset_t_148 {
1595   unsigned long sig[1U] ;
1596};
1597#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1598typedef struct __anonstruct_sigset_t_148 sigset_t;
1599#line 17 "include/asm-generic/signal-defs.h"
1600typedef void __signalfn_t(int  );
1601#line 18 "include/asm-generic/signal-defs.h"
1602typedef __signalfn_t *__sighandler_t;
1603#line 20 "include/asm-generic/signal-defs.h"
1604typedef void __restorefn_t(void);
1605#line 21 "include/asm-generic/signal-defs.h"
1606typedef __restorefn_t *__sigrestore_t;
1607#line 126 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1608struct sigaction {
1609   __sighandler_t sa_handler ;
1610   unsigned long sa_flags ;
1611   __sigrestore_t sa_restorer ;
1612   sigset_t sa_mask ;
1613};
1614#line 173 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1615struct k_sigaction {
1616   struct sigaction sa ;
1617};
1618#line 185 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1619union sigval {
1620   int sival_int ;
1621   void *sival_ptr ;
1622};
1623#line 10 "include/asm-generic/siginfo.h"
1624typedef union sigval sigval_t;
1625#line 11 "include/asm-generic/siginfo.h"
1626struct __anonstruct__kill_150 {
1627   __kernel_pid_t _pid ;
1628   __kernel_uid32_t _uid ;
1629};
1630#line 11 "include/asm-generic/siginfo.h"
1631struct __anonstruct__timer_151 {
1632   __kernel_timer_t _tid ;
1633   int _overrun ;
1634   char _pad[0U] ;
1635   sigval_t _sigval ;
1636   int _sys_private ;
1637};
1638#line 11 "include/asm-generic/siginfo.h"
1639struct __anonstruct__rt_152 {
1640   __kernel_pid_t _pid ;
1641   __kernel_uid32_t _uid ;
1642   sigval_t _sigval ;
1643};
1644#line 11 "include/asm-generic/siginfo.h"
1645struct __anonstruct__sigchld_153 {
1646   __kernel_pid_t _pid ;
1647   __kernel_uid32_t _uid ;
1648   int _status ;
1649   __kernel_clock_t _utime ;
1650   __kernel_clock_t _stime ;
1651};
1652#line 11 "include/asm-generic/siginfo.h"
1653struct __anonstruct__sigfault_154 {
1654   void *_addr ;
1655   short _addr_lsb ;
1656};
1657#line 11 "include/asm-generic/siginfo.h"
1658struct __anonstruct__sigpoll_155 {
1659   long _band ;
1660   int _fd ;
1661};
1662#line 11 "include/asm-generic/siginfo.h"
1663union __anonunion__sifields_149 {
1664   int _pad[28U] ;
1665   struct __anonstruct__kill_150 _kill ;
1666   struct __anonstruct__timer_151 _timer ;
1667   struct __anonstruct__rt_152 _rt ;
1668   struct __anonstruct__sigchld_153 _sigchld ;
1669   struct __anonstruct__sigfault_154 _sigfault ;
1670   struct __anonstruct__sigpoll_155 _sigpoll ;
1671};
1672#line 11 "include/asm-generic/siginfo.h"
1673struct siginfo {
1674   int si_signo ;
1675   int si_errno ;
1676   int si_code ;
1677   union __anonunion__sifields_149 _sifields ;
1678};
1679#line 102 "include/asm-generic/siginfo.h"
1680typedef struct siginfo siginfo_t;
1681#line 14 "include/linux/signal.h"
1682struct user_struct;
1683#line 24 "include/linux/signal.h"
1684struct sigpending {
1685   struct list_head list ;
1686   sigset_t signal ;
1687};
1688#line 388
1689enum pid_type {
1690    PIDTYPE_PID = 0,
1691    PIDTYPE_PGID = 1,
1692    PIDTYPE_SID = 2,
1693    PIDTYPE_MAX = 3
1694} ;
1695#line 395
1696struct pid_namespace;
1697#line 395 "include/linux/signal.h"
1698struct upid {
1699   int nr ;
1700   struct pid_namespace *ns ;
1701   struct hlist_node pid_chain ;
1702};
1703#line 56 "include/linux/pid.h"
1704struct pid {
1705   atomic_t count ;
1706   unsigned int level ;
1707   struct hlist_head tasks[3U] ;
1708   struct rcu_head rcu ;
1709   struct upid numbers[1U] ;
1710};
1711#line 68 "include/linux/pid.h"
1712struct pid_link {
1713   struct hlist_node node ;
1714   struct pid *pid ;
1715};
1716#line 10 "include/linux/seccomp.h"
1717struct __anonstruct_seccomp_t_158 {
1718   int mode ;
1719};
1720#line 10 "include/linux/seccomp.h"
1721typedef struct __anonstruct_seccomp_t_158 seccomp_t;
1722#line 427 "include/linux/rculist.h"
1723struct plist_head {
1724   struct list_head node_list ;
1725};
1726#line 84 "include/linux/plist.h"
1727struct plist_node {
1728   int prio ;
1729   struct list_head prio_list ;
1730   struct list_head node_list ;
1731};
1732#line 20 "include/linux/rtmutex.h"
1733struct rt_mutex {
1734   raw_spinlock_t wait_lock ;
1735   struct plist_head wait_list ;
1736   struct task_struct *owner ;
1737   int save_state ;
1738   char const   *name ;
1739   char const   *file ;
1740   int line ;
1741   void *magic ;
1742};
1743#line 38
1744struct rt_mutex_waiter;
1745#line 38
1746struct rt_mutex_waiter;
1747#line 41 "include/linux/resource.h"
1748struct rlimit {
1749   unsigned long rlim_cur ;
1750   unsigned long rlim_max ;
1751};
1752#line 85 "include/linux/resource.h"
1753struct timerqueue_node {
1754   struct rb_node node ;
1755   ktime_t expires ;
1756};
1757#line 12 "include/linux/timerqueue.h"
1758struct timerqueue_head {
1759   struct rb_root head ;
1760   struct timerqueue_node *next ;
1761};
1762#line 50
1763struct hrtimer_clock_base;
1764#line 50
1765struct hrtimer_clock_base;
1766#line 51
1767struct hrtimer_cpu_base;
1768#line 51
1769struct hrtimer_cpu_base;
1770#line 60
1771enum hrtimer_restart {
1772    HRTIMER_NORESTART = 0,
1773    HRTIMER_RESTART = 1
1774} ;
1775#line 65 "include/linux/timerqueue.h"
1776struct hrtimer {
1777   struct timerqueue_node node ;
1778   ktime_t _softexpires ;
1779   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1780   struct hrtimer_clock_base *base ;
1781   unsigned long state ;
1782   int start_pid ;
1783   void *start_site ;
1784   char start_comm[16U] ;
1785};
1786#line 132 "include/linux/hrtimer.h"
1787struct hrtimer_clock_base {
1788   struct hrtimer_cpu_base *cpu_base ;
1789   int index ;
1790   clockid_t clockid ;
1791   struct timerqueue_head active ;
1792   ktime_t resolution ;
1793   ktime_t (*get_time)(void) ;
1794   ktime_t softirq_time ;
1795   ktime_t offset ;
1796};
1797#line 162 "include/linux/hrtimer.h"
1798struct hrtimer_cpu_base {
1799   raw_spinlock_t lock ;
1800   unsigned long active_bases ;
1801   ktime_t expires_next ;
1802   int hres_active ;
1803   int hang_detected ;
1804   unsigned long nr_events ;
1805   unsigned long nr_retries ;
1806   unsigned long nr_hangs ;
1807   ktime_t max_hang_time ;
1808   struct hrtimer_clock_base clock_base[3U] ;
1809};
1810#line 452 "include/linux/hrtimer.h"
1811struct task_io_accounting {
1812   u64 rchar ;
1813   u64 wchar ;
1814   u64 syscr ;
1815   u64 syscw ;
1816   u64 read_bytes ;
1817   u64 write_bytes ;
1818   u64 cancelled_write_bytes ;
1819};
1820#line 45 "include/linux/task_io_accounting.h"
1821struct latency_record {
1822   unsigned long backtrace[12U] ;
1823   unsigned int count ;
1824   unsigned long time ;
1825   unsigned long max ;
1826};
1827#line 29 "include/linux/key.h"
1828typedef int32_t key_serial_t;
1829#line 32 "include/linux/key.h"
1830typedef uint32_t key_perm_t;
1831#line 33
1832struct key;
1833#line 33
1834struct key;
1835#line 34
1836struct signal_struct;
1837#line 34
1838struct signal_struct;
1839#line 35
1840struct key_type;
1841#line 35
1842struct key_type;
1843#line 37
1844struct keyring_list;
1845#line 37
1846struct keyring_list;
1847#line 115
1848struct key_user;
1849#line 115 "include/linux/key.h"
1850union __anonunion_ldv_16563_159 {
1851   time_t expiry ;
1852   time_t revoked_at ;
1853};
1854#line 115 "include/linux/key.h"
1855union __anonunion_type_data_160 {
1856   struct list_head link ;
1857   unsigned long x[2U] ;
1858   void *p[2U] ;
1859   int reject_error ;
1860};
1861#line 115 "include/linux/key.h"
1862union __anonunion_payload_161 {
1863   unsigned long value ;
1864   void *rcudata ;
1865   void *data ;
1866   struct keyring_list *subscriptions ;
1867};
1868#line 115 "include/linux/key.h"
1869struct key {
1870   atomic_t usage ;
1871   key_serial_t serial ;
1872   struct rb_node serial_node ;
1873   struct key_type *type ;
1874   struct rw_semaphore sem ;
1875   struct key_user *user ;
1876   void *security ;
1877   union __anonunion_ldv_16563_159 ldv_16563 ;
1878   uid_t uid ;
1879   gid_t gid ;
1880   key_perm_t perm ;
1881   unsigned short quotalen ;
1882   unsigned short datalen ;
1883   unsigned long flags ;
1884   char *description ;
1885   union __anonunion_type_data_160 type_data ;
1886   union __anonunion_payload_161 payload ;
1887};
1888#line 316
1889struct audit_context;
1890#line 316
1891struct audit_context;
1892#line 27 "include/linux/selinux.h"
1893struct inode;
1894#line 27
1895struct inode;
1896#line 28 "include/linux/selinux.h"
1897struct group_info {
1898   atomic_t usage ;
1899   int ngroups ;
1900   int nblocks ;
1901   gid_t small_block[32U] ;
1902   gid_t *blocks[0U] ;
1903};
1904#line 77 "include/linux/cred.h"
1905struct thread_group_cred {
1906   atomic_t usage ;
1907   pid_t tgid ;
1908   spinlock_t lock ;
1909   struct key *session_keyring ;
1910   struct key *process_keyring ;
1911   struct rcu_head rcu ;
1912};
1913#line 91 "include/linux/cred.h"
1914struct cred {
1915   atomic_t usage ;
1916   atomic_t subscribers ;
1917   void *put_addr ;
1918   unsigned int magic ;
1919   uid_t uid ;
1920   gid_t gid ;
1921   uid_t suid ;
1922   gid_t sgid ;
1923   uid_t euid ;
1924   gid_t egid ;
1925   uid_t fsuid ;
1926   gid_t fsgid ;
1927   unsigned int securebits ;
1928   kernel_cap_t cap_inheritable ;
1929   kernel_cap_t cap_permitted ;
1930   kernel_cap_t cap_effective ;
1931   kernel_cap_t cap_bset ;
1932   unsigned char jit_keyring ;
1933   struct key *thread_keyring ;
1934   struct key *request_key_auth ;
1935   struct thread_group_cred *tgcred ;
1936   void *security ;
1937   struct user_struct *user ;
1938   struct user_namespace *user_ns ;
1939   struct group_info *group_info ;
1940   struct rcu_head rcu ;
1941};
1942#line 264
1943struct llist_node;
1944#line 64 "include/linux/llist.h"
1945struct llist_node {
1946   struct llist_node *next ;
1947};
1948#line 185
1949struct futex_pi_state;
1950#line 185
1951struct futex_pi_state;
1952#line 186
1953struct robust_list_head;
1954#line 186
1955struct robust_list_head;
1956#line 187
1957struct bio_list;
1958#line 187
1959struct bio_list;
1960#line 188
1961struct fs_struct;
1962#line 188
1963struct fs_struct;
1964#line 189
1965struct perf_event_context;
1966#line 189
1967struct perf_event_context;
1968#line 190
1969struct blk_plug;
1970#line 190
1971struct blk_plug;
1972#line 149 "include/linux/sched.h"
1973struct cfs_rq;
1974#line 149
1975struct cfs_rq;
1976#line 44 "include/linux/aio_abi.h"
1977struct io_event {
1978   __u64 data ;
1979   __u64 obj ;
1980   __s64 res ;
1981   __s64 res2 ;
1982};
1983#line 106 "include/linux/aio_abi.h"
1984struct iovec {
1985   void *iov_base ;
1986   __kernel_size_t iov_len ;
1987};
1988#line 54 "include/linux/uio.h"
1989struct kioctx;
1990#line 54
1991struct kioctx;
1992#line 55 "include/linux/uio.h"
1993union __anonunion_ki_obj_162 {
1994   void *user ;
1995   struct task_struct *tsk ;
1996};
1997#line 55
1998struct eventfd_ctx;
1999#line 55 "include/linux/uio.h"
2000struct kiocb {
2001   struct list_head ki_run_list ;
2002   unsigned long ki_flags ;
2003   int ki_users ;
2004   unsigned int ki_key ;
2005   struct file *ki_filp ;
2006   struct kioctx *ki_ctx ;
2007   int (*ki_cancel)(struct kiocb * , struct io_event * ) ;
2008   ssize_t (*ki_retry)(struct kiocb * ) ;
2009   void (*ki_dtor)(struct kiocb * ) ;
2010   union __anonunion_ki_obj_162 ki_obj ;
2011   __u64 ki_user_data ;
2012   loff_t ki_pos ;
2013   void *private ;
2014   unsigned short ki_opcode ;
2015   size_t ki_nbytes ;
2016   char *ki_buf ;
2017   size_t ki_left ;
2018   struct iovec ki_inline_vec ;
2019   struct iovec *ki_iovec ;
2020   unsigned long ki_nr_segs ;
2021   unsigned long ki_cur_seg ;
2022   struct list_head ki_list ;
2023   struct list_head ki_batch ;
2024   struct eventfd_ctx *ki_eventfd ;
2025};
2026#line 162 "include/linux/aio.h"
2027struct aio_ring_info {
2028   unsigned long mmap_base ;
2029   unsigned long mmap_size ;
2030   struct page **ring_pages ;
2031   spinlock_t ring_lock ;
2032   long nr_pages ;
2033   unsigned int nr ;
2034   unsigned int tail ;
2035   struct page *internal_pages[8U] ;
2036};
2037#line 178 "include/linux/aio.h"
2038struct kioctx {
2039   atomic_t users ;
2040   int dead ;
2041   struct mm_struct *mm ;
2042   unsigned long user_id ;
2043   struct hlist_node list ;
2044   wait_queue_head_t wait ;
2045   spinlock_t ctx_lock ;
2046   int reqs_active ;
2047   struct list_head active_reqs ;
2048   struct list_head run_list ;
2049   unsigned int max_reqs ;
2050   struct aio_ring_info ring_info ;
2051   struct delayed_work wq ;
2052   struct rcu_head rcu_head ;
2053};
2054#line 406 "include/linux/sched.h"
2055struct sighand_struct {
2056   atomic_t count ;
2057   struct k_sigaction action[64U] ;
2058   spinlock_t siglock ;
2059   wait_queue_head_t signalfd_wqh ;
2060};
2061#line 449 "include/linux/sched.h"
2062struct pacct_struct {
2063   int ac_flag ;
2064   long ac_exitcode ;
2065   unsigned long ac_mem ;
2066   cputime_t ac_utime ;
2067   cputime_t ac_stime ;
2068   unsigned long ac_minflt ;
2069   unsigned long ac_majflt ;
2070};
2071#line 457 "include/linux/sched.h"
2072struct cpu_itimer {
2073   cputime_t expires ;
2074   cputime_t incr ;
2075   u32 error ;
2076   u32 incr_error ;
2077};
2078#line 464 "include/linux/sched.h"
2079struct task_cputime {
2080   cputime_t utime ;
2081   cputime_t stime ;
2082   unsigned long long sum_exec_runtime ;
2083};
2084#line 481 "include/linux/sched.h"
2085struct thread_group_cputimer {
2086   struct task_cputime cputime ;
2087   int running ;
2088   raw_spinlock_t lock ;
2089};
2090#line 517
2091struct autogroup;
2092#line 517
2093struct autogroup;
2094#line 518
2095struct tty_struct;
2096#line 518
2097struct taskstats;
2098#line 518
2099struct tty_audit_buf;
2100#line 518 "include/linux/sched.h"
2101struct signal_struct {
2102   atomic_t sigcnt ;
2103   atomic_t live ;
2104   int nr_threads ;
2105   wait_queue_head_t wait_chldexit ;
2106   struct task_struct *curr_target ;
2107   struct sigpending shared_pending ;
2108   int group_exit_code ;
2109   int notify_count ;
2110   struct task_struct *group_exit_task ;
2111   int group_stop_count ;
2112   unsigned int flags ;
2113   unsigned char is_child_subreaper : 1 ;
2114   unsigned char has_child_subreaper : 1 ;
2115   struct list_head posix_timers ;
2116   struct hrtimer real_timer ;
2117   struct pid *leader_pid ;
2118   ktime_t it_real_incr ;
2119   struct cpu_itimer it[2U] ;
2120   struct thread_group_cputimer cputimer ;
2121   struct task_cputime cputime_expires ;
2122   struct list_head cpu_timers[3U] ;
2123   struct pid *tty_old_pgrp ;
2124   int leader ;
2125   struct tty_struct *tty ;
2126   struct autogroup *autogroup ;
2127   cputime_t utime ;
2128   cputime_t stime ;
2129   cputime_t cutime ;
2130   cputime_t cstime ;
2131   cputime_t gtime ;
2132   cputime_t cgtime ;
2133   cputime_t prev_utime ;
2134   cputime_t prev_stime ;
2135   unsigned long nvcsw ;
2136   unsigned long nivcsw ;
2137   unsigned long cnvcsw ;
2138   unsigned long cnivcsw ;
2139   unsigned long min_flt ;
2140   unsigned long maj_flt ;
2141   unsigned long cmin_flt ;
2142   unsigned long cmaj_flt ;
2143   unsigned long inblock ;
2144   unsigned long oublock ;
2145   unsigned long cinblock ;
2146   unsigned long coublock ;
2147   unsigned long maxrss ;
2148   unsigned long cmaxrss ;
2149   struct task_io_accounting ioac ;
2150   unsigned long long sum_sched_runtime ;
2151   struct rlimit rlim[16U] ;
2152   struct pacct_struct pacct ;
2153   struct taskstats *stats ;
2154   unsigned int audit_tty ;
2155   struct tty_audit_buf *tty_audit_buf ;
2156   struct rw_semaphore group_rwsem ;
2157   int oom_adj ;
2158   int oom_score_adj ;
2159   int oom_score_adj_min ;
2160   struct mutex cred_guard_mutex ;
2161};
2162#line 699 "include/linux/sched.h"
2163struct user_struct {
2164   atomic_t __count ;
2165   atomic_t processes ;
2166   atomic_t files ;
2167   atomic_t sigpending ;
2168   atomic_t inotify_watches ;
2169   atomic_t inotify_devs ;
2170   atomic_t fanotify_listeners ;
2171   atomic_long_t epoll_watches ;
2172   unsigned long mq_bytes ;
2173   unsigned long locked_shm ;
2174   struct key *uid_keyring ;
2175   struct key *session_keyring ;
2176   struct hlist_node uidhash_node ;
2177   uid_t uid ;
2178   struct user_namespace *user_ns ;
2179   atomic_long_t locked_vm ;
2180};
2181#line 744
2182struct backing_dev_info;
2183#line 744
2184struct backing_dev_info;
2185#line 745
2186struct reclaim_state;
2187#line 745
2188struct reclaim_state;
2189#line 746 "include/linux/sched.h"
2190struct sched_info {
2191   unsigned long pcount ;
2192   unsigned long long run_delay ;
2193   unsigned long long last_arrival ;
2194   unsigned long long last_queued ;
2195};
2196#line 760 "include/linux/sched.h"
2197struct task_delay_info {
2198   spinlock_t lock ;
2199   unsigned int flags ;
2200   struct timespec blkio_start ;
2201   struct timespec blkio_end ;
2202   u64 blkio_delay ;
2203   u64 swapin_delay ;
2204   u32 blkio_count ;
2205   u32 swapin_count ;
2206   struct timespec freepages_start ;
2207   struct timespec freepages_end ;
2208   u64 freepages_delay ;
2209   u32 freepages_count ;
2210};
2211#line 1069
2212struct io_context;
2213#line 1069
2214struct io_context;
2215#line 1097
2216struct pipe_inode_info;
2217#line 1097
2218struct pipe_inode_info;
2219#line 1099
2220struct rq;
2221#line 1099
2222struct rq;
2223#line 1100 "include/linux/sched.h"
2224struct sched_class {
2225   struct sched_class  const  *next ;
2226   void (*enqueue_task)(struct rq * , struct task_struct * , int  ) ;
2227   void (*dequeue_task)(struct rq * , struct task_struct * , int  ) ;
2228   void (*yield_task)(struct rq * ) ;
2229   bool (*yield_to_task)(struct rq * , struct task_struct * , bool  ) ;
2230   void (*check_preempt_curr)(struct rq * , struct task_struct * , int  ) ;
2231   struct task_struct *(*pick_next_task)(struct rq * ) ;
2232   void (*put_prev_task)(struct rq * , struct task_struct * ) ;
2233   int (*select_task_rq)(struct task_struct * , int  , int  ) ;
2234   void (*pre_schedule)(struct rq * , struct task_struct * ) ;
2235   void (*post_schedule)(struct rq * ) ;
2236   void (*task_waking)(struct task_struct * ) ;
2237   void (*task_woken)(struct rq * , struct task_struct * ) ;
2238   void (*set_cpus_allowed)(struct task_struct * , struct cpumask  const  * ) ;
2239   void (*rq_online)(struct rq * ) ;
2240   void (*rq_offline)(struct rq * ) ;
2241   void (*set_curr_task)(struct rq * ) ;
2242   void (*task_tick)(struct rq * , struct task_struct * , int  ) ;
2243   void (*task_fork)(struct task_struct * ) ;
2244   void (*switched_from)(struct rq * , struct task_struct * ) ;
2245   void (*switched_to)(struct rq * , struct task_struct * ) ;
2246   void (*prio_changed)(struct rq * , struct task_struct * , int  ) ;
2247   unsigned int (*get_rr_interval)(struct rq * , struct task_struct * ) ;
2248   void (*task_move_group)(struct task_struct * , int  ) ;
2249};
2250#line 1165 "include/linux/sched.h"
2251struct load_weight {
2252   unsigned long weight ;
2253   unsigned long inv_weight ;
2254};
2255#line 1170 "include/linux/sched.h"
2256struct sched_statistics {
2257   u64 wait_start ;
2258   u64 wait_max ;
2259   u64 wait_count ;
2260   u64 wait_sum ;
2261   u64 iowait_count ;
2262   u64 iowait_sum ;
2263   u64 sleep_start ;
2264   u64 sleep_max ;
2265   s64 sum_sleep_runtime ;
2266   u64 block_start ;
2267   u64 block_max ;
2268   u64 exec_max ;
2269   u64 slice_max ;
2270   u64 nr_migrations_cold ;
2271   u64 nr_failed_migrations_affine ;
2272   u64 nr_failed_migrations_running ;
2273   u64 nr_failed_migrations_hot ;
2274   u64 nr_forced_migrations ;
2275   u64 nr_wakeups ;
2276   u64 nr_wakeups_sync ;
2277   u64 nr_wakeups_migrate ;
2278   u64 nr_wakeups_local ;
2279   u64 nr_wakeups_remote ;
2280   u64 nr_wakeups_affine ;
2281   u64 nr_wakeups_affine_attempts ;
2282   u64 nr_wakeups_passive ;
2283   u64 nr_wakeups_idle ;
2284};
2285#line 1205 "include/linux/sched.h"
2286struct sched_entity {
2287   struct load_weight load ;
2288   struct rb_node run_node ;
2289   struct list_head group_node ;
2290   unsigned int on_rq ;
2291   u64 exec_start ;
2292   u64 sum_exec_runtime ;
2293   u64 vruntime ;
2294   u64 prev_sum_exec_runtime ;
2295   u64 nr_migrations ;
2296   struct sched_statistics statistics ;
2297   struct sched_entity *parent ;
2298   struct cfs_rq *cfs_rq ;
2299   struct cfs_rq *my_q ;
2300};
2301#line 1231
2302struct rt_rq;
2303#line 1231 "include/linux/sched.h"
2304struct sched_rt_entity {
2305   struct list_head run_list ;
2306   unsigned long timeout ;
2307   unsigned int time_slice ;
2308   int nr_cpus_allowed ;
2309   struct sched_rt_entity *back ;
2310   struct sched_rt_entity *parent ;
2311   struct rt_rq *rt_rq ;
2312   struct rt_rq *my_q ;
2313};
2314#line 1255
2315struct mem_cgroup;
2316#line 1255 "include/linux/sched.h"
2317struct memcg_batch_info {
2318   int do_batch ;
2319   struct mem_cgroup *memcg ;
2320   unsigned long nr_pages ;
2321   unsigned long memsw_nr_pages ;
2322};
2323#line 1616
2324struct files_struct;
2325#line 1616
2326struct css_set;
2327#line 1616
2328struct compat_robust_list_head;
2329#line 1616 "include/linux/sched.h"
2330struct task_struct {
2331   long volatile   state ;
2332   void *stack ;
2333   atomic_t usage ;
2334   unsigned int flags ;
2335   unsigned int ptrace ;
2336   struct llist_node wake_entry ;
2337   int on_cpu ;
2338   int on_rq ;
2339   int prio ;
2340   int static_prio ;
2341   int normal_prio ;
2342   unsigned int rt_priority ;
2343   struct sched_class  const  *sched_class ;
2344   struct sched_entity se ;
2345   struct sched_rt_entity rt ;
2346   struct hlist_head preempt_notifiers ;
2347   unsigned char fpu_counter ;
2348   unsigned int policy ;
2349   cpumask_t cpus_allowed ;
2350   struct sched_info sched_info ;
2351   struct list_head tasks ;
2352   struct plist_node pushable_tasks ;
2353   struct mm_struct *mm ;
2354   struct mm_struct *active_mm ;
2355   unsigned char brk_randomized : 1 ;
2356   int exit_state ;
2357   int exit_code ;
2358   int exit_signal ;
2359   int pdeath_signal ;
2360   unsigned int jobctl ;
2361   unsigned int personality ;
2362   unsigned char did_exec : 1 ;
2363   unsigned char in_execve : 1 ;
2364   unsigned char in_iowait : 1 ;
2365   unsigned char sched_reset_on_fork : 1 ;
2366   unsigned char sched_contributes_to_load : 1 ;
2367   unsigned char irq_thread : 1 ;
2368   pid_t pid ;
2369   pid_t tgid ;
2370   unsigned long stack_canary ;
2371   struct task_struct *real_parent ;
2372   struct task_struct *parent ;
2373   struct list_head children ;
2374   struct list_head sibling ;
2375   struct task_struct *group_leader ;
2376   struct list_head ptraced ;
2377   struct list_head ptrace_entry ;
2378   struct pid_link pids[3U] ;
2379   struct list_head thread_group ;
2380   struct completion *vfork_done ;
2381   int *set_child_tid ;
2382   int *clear_child_tid ;
2383   cputime_t utime ;
2384   cputime_t stime ;
2385   cputime_t utimescaled ;
2386   cputime_t stimescaled ;
2387   cputime_t gtime ;
2388   cputime_t prev_utime ;
2389   cputime_t prev_stime ;
2390   unsigned long nvcsw ;
2391   unsigned long nivcsw ;
2392   struct timespec start_time ;
2393   struct timespec real_start_time ;
2394   unsigned long min_flt ;
2395   unsigned long maj_flt ;
2396   struct task_cputime cputime_expires ;
2397   struct list_head cpu_timers[3U] ;
2398   struct cred  const  *real_cred ;
2399   struct cred  const  *cred ;
2400   struct cred *replacement_session_keyring ;
2401   char comm[16U] ;
2402   int link_count ;
2403   int total_link_count ;
2404   struct sysv_sem sysvsem ;
2405   unsigned long last_switch_count ;
2406   struct thread_struct thread ;
2407   struct fs_struct *fs ;
2408   struct files_struct *files ;
2409   struct nsproxy *nsproxy ;
2410   struct signal_struct *signal ;
2411   struct sighand_struct *sighand ;
2412   sigset_t blocked ;
2413   sigset_t real_blocked ;
2414   sigset_t saved_sigmask ;
2415   struct sigpending pending ;
2416   unsigned long sas_ss_sp ;
2417   size_t sas_ss_size ;
2418   int (*notifier)(void * ) ;
2419   void *notifier_data ;
2420   sigset_t *notifier_mask ;
2421   struct audit_context *audit_context ;
2422   uid_t loginuid ;
2423   unsigned int sessionid ;
2424   seccomp_t seccomp ;
2425   u32 parent_exec_id ;
2426   u32 self_exec_id ;
2427   spinlock_t alloc_lock ;
2428   raw_spinlock_t pi_lock ;
2429   struct plist_head pi_waiters ;
2430   struct rt_mutex_waiter *pi_blocked_on ;
2431   struct mutex_waiter *blocked_on ;
2432   unsigned int irq_events ;
2433   unsigned long hardirq_enable_ip ;
2434   unsigned long hardirq_disable_ip ;
2435   unsigned int hardirq_enable_event ;
2436   unsigned int hardirq_disable_event ;
2437   int hardirqs_enabled ;
2438   int hardirq_context ;
2439   unsigned long softirq_disable_ip ;
2440   unsigned long softirq_enable_ip ;
2441   unsigned int softirq_disable_event ;
2442   unsigned int softirq_enable_event ;
2443   int softirqs_enabled ;
2444   int softirq_context ;
2445   u64 curr_chain_key ;
2446   int lockdep_depth ;
2447   unsigned int lockdep_recursion ;
2448   struct held_lock held_locks[48U] ;
2449   gfp_t lockdep_reclaim_gfp ;
2450   void *journal_info ;
2451   struct bio_list *bio_list ;
2452   struct blk_plug *plug ;
2453   struct reclaim_state *reclaim_state ;
2454   struct backing_dev_info *backing_dev_info ;
2455   struct io_context *io_context ;
2456   unsigned long ptrace_message ;
2457   siginfo_t *last_siginfo ;
2458   struct task_io_accounting ioac ;
2459   u64 acct_rss_mem1 ;
2460   u64 acct_vm_mem1 ;
2461   cputime_t acct_timexpd ;
2462   nodemask_t mems_allowed ;
2463   seqcount_t mems_allowed_seq ;
2464   int cpuset_mem_spread_rotor ;
2465   int cpuset_slab_spread_rotor ;
2466   struct css_set *cgroups ;
2467   struct list_head cg_list ;
2468   struct robust_list_head *robust_list ;
2469   struct compat_robust_list_head *compat_robust_list ;
2470   struct list_head pi_state_list ;
2471   struct futex_pi_state *pi_state_cache ;
2472   struct perf_event_context *perf_event_ctxp[2U] ;
2473   struct mutex perf_event_mutex ;
2474   struct list_head perf_event_list ;
2475   struct mempolicy *mempolicy ;
2476   short il_next ;
2477   short pref_node_fork ;
2478   struct rcu_head rcu ;
2479   struct pipe_inode_info *splice_pipe ;
2480   struct task_delay_info *delays ;
2481   int make_it_fail ;
2482   int nr_dirtied ;
2483   int nr_dirtied_pause ;
2484   unsigned long dirty_paused_when ;
2485   int latency_record_count ;
2486   struct latency_record latency_record[32U] ;
2487   unsigned long timer_slack_ns ;
2488   unsigned long default_timer_slack_ns ;
2489   struct list_head *scm_work_list ;
2490   unsigned long trace ;
2491   unsigned long trace_recursion ;
2492   struct memcg_batch_info memcg_batch ;
2493   atomic_t ptrace_bp_refcnt ;
2494};
2495#line 28 "include/linux/of.h"
2496typedef u32 phandle;
2497#line 30 "include/linux/of.h"
2498struct property {
2499   char *name ;
2500   int length ;
2501   void *value ;
2502   struct property *next ;
2503   unsigned long _flags ;
2504   unsigned int unique_id ;
2505};
2506#line 39
2507struct proc_dir_entry;
2508#line 39 "include/linux/of.h"
2509struct device_node {
2510   char const   *name ;
2511   char const   *type ;
2512   phandle phandle ;
2513   char *full_name ;
2514   struct property *properties ;
2515   struct property *deadprops ;
2516   struct device_node *parent ;
2517   struct device_node *child ;
2518   struct device_node *sibling ;
2519   struct device_node *next ;
2520   struct device_node *allnext ;
2521   struct proc_dir_entry *pde ;
2522   struct kref kref ;
2523   unsigned long _flags ;
2524   void *data ;
2525};
2526#line 41 "include/linux/i2c.h"
2527struct i2c_msg;
2528#line 41
2529struct i2c_msg;
2530#line 42
2531struct i2c_algorithm;
2532#line 42
2533struct i2c_algorithm;
2534#line 43
2535struct i2c_adapter;
2536#line 43
2537struct i2c_adapter;
2538#line 46
2539union i2c_smbus_data;
2540#line 46
2541union i2c_smbus_data;
2542#line 336 "include/linux/i2c.h"
2543struct i2c_algorithm {
2544   int (*master_xfer)(struct i2c_adapter * , struct i2c_msg * , int  ) ;
2545   int (*smbus_xfer)(struct i2c_adapter * , u16  , unsigned short  , char  , u8  ,
2546                     int  , union i2c_smbus_data * ) ;
2547   u32 (*functionality)(struct i2c_adapter * ) ;
2548};
2549#line 368 "include/linux/i2c.h"
2550struct i2c_adapter {
2551   struct module *owner ;
2552   unsigned int class ;
2553   struct i2c_algorithm  const  *algo ;
2554   void *algo_data ;
2555   struct rt_mutex bus_lock ;
2556   int timeout ;
2557   int retries ;
2558   struct device dev ;
2559   int nr ;
2560   char name[48U] ;
2561   struct completion dev_released ;
2562   struct mutex userspace_clients_lock ;
2563   struct list_head userspace_clients ;
2564};
2565#line 486 "include/linux/i2c.h"
2566struct i2c_msg {
2567   __u16 addr ;
2568   __u16 flags ;
2569   __u16 len ;
2570   __u8 *buf ;
2571};
2572#line 551 "include/linux/i2c.h"
2573union i2c_smbus_data {
2574   __u8 byte ;
2575   __u16 word ;
2576   __u8 block[34U] ;
2577};
2578#line 41 "include/asm-generic/poll.h"
2579struct block_device;
2580#line 41
2581struct block_device;
2582#line 93 "include/linux/bit_spinlock.h"
2583struct hlist_bl_node;
2584#line 93 "include/linux/bit_spinlock.h"
2585struct hlist_bl_head {
2586   struct hlist_bl_node *first ;
2587};
2588#line 36 "include/linux/list_bl.h"
2589struct hlist_bl_node {
2590   struct hlist_bl_node *next ;
2591   struct hlist_bl_node **pprev ;
2592};
2593#line 114 "include/linux/rculist_bl.h"
2594struct nameidata;
2595#line 114
2596struct nameidata;
2597#line 115
2598struct path;
2599#line 115
2600struct path;
2601#line 116
2602struct vfsmount;
2603#line 116
2604struct vfsmount;
2605#line 117 "include/linux/rculist_bl.h"
2606struct qstr {
2607   unsigned int hash ;
2608   unsigned int len ;
2609   unsigned char const   *name ;
2610};
2611#line 72 "include/linux/dcache.h"
2612struct dentry_operations;
2613#line 72
2614struct super_block;
2615#line 72 "include/linux/dcache.h"
2616union __anonunion_d_u_164 {
2617   struct list_head d_child ;
2618   struct rcu_head d_rcu ;
2619};
2620#line 72 "include/linux/dcache.h"
2621struct dentry {
2622   unsigned int d_flags ;
2623   seqcount_t d_seq ;
2624   struct hlist_bl_node d_hash ;
2625   struct dentry *d_parent ;
2626   struct qstr d_name ;
2627   struct inode *d_inode ;
2628   unsigned char d_iname[32U] ;
2629   unsigned int d_count ;
2630   spinlock_t d_lock ;
2631   struct dentry_operations  const  *d_op ;
2632   struct super_block *d_sb ;
2633   unsigned long d_time ;
2634   void *d_fsdata ;
2635   struct list_head d_lru ;
2636   union __anonunion_d_u_164 d_u ;
2637   struct list_head d_subdirs ;
2638   struct list_head d_alias ;
2639};
2640#line 123 "include/linux/dcache.h"
2641struct dentry_operations {
2642   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
2643   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
2644   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
2645                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
2646   int (*d_delete)(struct dentry  const  * ) ;
2647   void (*d_release)(struct dentry * ) ;
2648   void (*d_prune)(struct dentry * ) ;
2649   void (*d_iput)(struct dentry * , struct inode * ) ;
2650   char *(*d_dname)(struct dentry * , char * , int  ) ;
2651   struct vfsmount *(*d_automount)(struct path * ) ;
2652   int (*d_manage)(struct dentry * , bool  ) ;
2653};
2654#line 402 "include/linux/dcache.h"
2655struct path {
2656   struct vfsmount *mnt ;
2657   struct dentry *dentry ;
2658};
2659#line 58 "include/linux/radix-tree.h"
2660struct radix_tree_node;
2661#line 58 "include/linux/radix-tree.h"
2662struct radix_tree_root {
2663   unsigned int height ;
2664   gfp_t gfp_mask ;
2665   struct radix_tree_node *rnode ;
2666};
2667#line 45 "include/linux/semaphore.h"
2668struct fiemap_extent {
2669   __u64 fe_logical ;
2670   __u64 fe_physical ;
2671   __u64 fe_length ;
2672   __u64 fe_reserved64[2U] ;
2673   __u32 fe_flags ;
2674   __u32 fe_reserved[3U] ;
2675};
2676#line 38 "include/linux/fiemap.h"
2677struct shrink_control {
2678   gfp_t gfp_mask ;
2679   unsigned long nr_to_scan ;
2680};
2681#line 14 "include/linux/shrinker.h"
2682struct shrinker {
2683   int (*shrink)(struct shrinker * , struct shrink_control * ) ;
2684   int seeks ;
2685   long batch ;
2686   struct list_head list ;
2687   atomic_long_t nr_in_batch ;
2688};
2689#line 43
2690enum migrate_mode {
2691    MIGRATE_ASYNC = 0,
2692    MIGRATE_SYNC_LIGHT = 1,
2693    MIGRATE_SYNC = 2
2694} ;
2695#line 49
2696struct export_operations;
2697#line 49
2698struct export_operations;
2699#line 51
2700struct poll_table_struct;
2701#line 51
2702struct poll_table_struct;
2703#line 52
2704struct kstatfs;
2705#line 52
2706struct kstatfs;
2707#line 435 "include/linux/fs.h"
2708struct iattr {
2709   unsigned int ia_valid ;
2710   umode_t ia_mode ;
2711   uid_t ia_uid ;
2712   gid_t ia_gid ;
2713   loff_t ia_size ;
2714   struct timespec ia_atime ;
2715   struct timespec ia_mtime ;
2716   struct timespec ia_ctime ;
2717   struct file *ia_file ;
2718};
2719#line 119 "include/linux/quota.h"
2720struct if_dqinfo {
2721   __u64 dqi_bgrace ;
2722   __u64 dqi_igrace ;
2723   __u32 dqi_flags ;
2724   __u32 dqi_valid ;
2725};
2726#line 152 "include/linux/quota.h"
2727struct fs_disk_quota {
2728   __s8 d_version ;
2729   __s8 d_flags ;
2730   __u16 d_fieldmask ;
2731   __u32 d_id ;
2732   __u64 d_blk_hardlimit ;
2733   __u64 d_blk_softlimit ;
2734   __u64 d_ino_hardlimit ;
2735   __u64 d_ino_softlimit ;
2736   __u64 d_bcount ;
2737   __u64 d_icount ;
2738   __s32 d_itimer ;
2739   __s32 d_btimer ;
2740   __u16 d_iwarns ;
2741   __u16 d_bwarns ;
2742   __s32 d_padding2 ;
2743   __u64 d_rtb_hardlimit ;
2744   __u64 d_rtb_softlimit ;
2745   __u64 d_rtbcount ;
2746   __s32 d_rtbtimer ;
2747   __u16 d_rtbwarns ;
2748   __s16 d_padding3 ;
2749   char d_padding4[8U] ;
2750};
2751#line 75 "include/linux/dqblk_xfs.h"
2752struct fs_qfilestat {
2753   __u64 qfs_ino ;
2754   __u64 qfs_nblks ;
2755   __u32 qfs_nextents ;
2756};
2757#line 150 "include/linux/dqblk_xfs.h"
2758typedef struct fs_qfilestat fs_qfilestat_t;
2759#line 151 "include/linux/dqblk_xfs.h"
2760struct fs_quota_stat {
2761   __s8 qs_version ;
2762   __u16 qs_flags ;
2763   __s8 qs_pad ;
2764   fs_qfilestat_t qs_uquota ;
2765   fs_qfilestat_t qs_gquota ;
2766   __u32 qs_incoredqs ;
2767   __s32 qs_btimelimit ;
2768   __s32 qs_itimelimit ;
2769   __s32 qs_rtbtimelimit ;
2770   __u16 qs_bwarnlimit ;
2771   __u16 qs_iwarnlimit ;
2772};
2773#line 165
2774struct dquot;
2775#line 165
2776struct dquot;
2777#line 185 "include/linux/quota.h"
2778typedef __kernel_uid32_t qid_t;
2779#line 186 "include/linux/quota.h"
2780typedef long long qsize_t;
2781#line 189 "include/linux/quota.h"
2782struct mem_dqblk {
2783   qsize_t dqb_bhardlimit ;
2784   qsize_t dqb_bsoftlimit ;
2785   qsize_t dqb_curspace ;
2786   qsize_t dqb_rsvspace ;
2787   qsize_t dqb_ihardlimit ;
2788   qsize_t dqb_isoftlimit ;
2789   qsize_t dqb_curinodes ;
2790   time_t dqb_btime ;
2791   time_t dqb_itime ;
2792};
2793#line 211
2794struct quota_format_type;
2795#line 211
2796struct quota_format_type;
2797#line 212 "include/linux/quota.h"
2798struct mem_dqinfo {
2799   struct quota_format_type *dqi_format ;
2800   int dqi_fmt_id ;
2801   struct list_head dqi_dirty_list ;
2802   unsigned long dqi_flags ;
2803   unsigned int dqi_bgrace ;
2804   unsigned int dqi_igrace ;
2805   qsize_t dqi_maxblimit ;
2806   qsize_t dqi_maxilimit ;
2807   void *dqi_priv ;
2808};
2809#line 275 "include/linux/quota.h"
2810struct dquot {
2811   struct hlist_node dq_hash ;
2812   struct list_head dq_inuse ;
2813   struct list_head dq_free ;
2814   struct list_head dq_dirty ;
2815   struct mutex dq_lock ;
2816   atomic_t dq_count ;
2817   wait_queue_head_t dq_wait_unused ;
2818   struct super_block *dq_sb ;
2819   unsigned int dq_id ;
2820   loff_t dq_off ;
2821   unsigned long dq_flags ;
2822   short dq_type ;
2823   struct mem_dqblk dq_dqb ;
2824};
2825#line 303 "include/linux/quota.h"
2826struct quota_format_ops {
2827   int (*check_quota_file)(struct super_block * , int  ) ;
2828   int (*read_file_info)(struct super_block * , int  ) ;
2829   int (*write_file_info)(struct super_block * , int  ) ;
2830   int (*free_file_info)(struct super_block * , int  ) ;
2831   int (*read_dqblk)(struct dquot * ) ;
2832   int (*commit_dqblk)(struct dquot * ) ;
2833   int (*release_dqblk)(struct dquot * ) ;
2834};
2835#line 314 "include/linux/quota.h"
2836struct dquot_operations {
2837   int (*write_dquot)(struct dquot * ) ;
2838   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
2839   void (*destroy_dquot)(struct dquot * ) ;
2840   int (*acquire_dquot)(struct dquot * ) ;
2841   int (*release_dquot)(struct dquot * ) ;
2842   int (*mark_dirty)(struct dquot * ) ;
2843   int (*write_info)(struct super_block * , int  ) ;
2844   qsize_t *(*get_reserved_space)(struct inode * ) ;
2845};
2846#line 328 "include/linux/quota.h"
2847struct quotactl_ops {
2848   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
2849   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
2850   int (*quota_off)(struct super_block * , int  ) ;
2851   int (*quota_sync)(struct super_block * , int  , int  ) ;
2852   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
2853   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
2854   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
2855   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
2856   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
2857   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
2858};
2859#line 344 "include/linux/quota.h"
2860struct quota_format_type {
2861   int qf_fmt_id ;
2862   struct quota_format_ops  const  *qf_ops ;
2863   struct module *qf_owner ;
2864   struct quota_format_type *qf_next ;
2865};
2866#line 390 "include/linux/quota.h"
2867struct quota_info {
2868   unsigned int flags ;
2869   struct mutex dqio_mutex ;
2870   struct mutex dqonoff_mutex ;
2871   struct rw_semaphore dqptr_sem ;
2872   struct inode *files[2U] ;
2873   struct mem_dqinfo info[2U] ;
2874   struct quota_format_ops  const  *ops[2U] ;
2875};
2876#line 421
2877struct writeback_control;
2878#line 421
2879struct writeback_control;
2880#line 585 "include/linux/fs.h"
2881union __anonunion_arg_166 {
2882   char *buf ;
2883   void *data ;
2884};
2885#line 585 "include/linux/fs.h"
2886struct __anonstruct_read_descriptor_t_165 {
2887   size_t written ;
2888   size_t count ;
2889   union __anonunion_arg_166 arg ;
2890   int error ;
2891};
2892#line 585 "include/linux/fs.h"
2893typedef struct __anonstruct_read_descriptor_t_165 read_descriptor_t;
2894#line 588 "include/linux/fs.h"
2895struct address_space_operations {
2896   int (*writepage)(struct page * , struct writeback_control * ) ;
2897   int (*readpage)(struct file * , struct page * ) ;
2898   int (*writepages)(struct address_space * , struct writeback_control * ) ;
2899   int (*set_page_dirty)(struct page * ) ;
2900   int (*readpages)(struct file * , struct address_space * , struct list_head * ,
2901                    unsigned int  ) ;
2902   int (*write_begin)(struct file * , struct address_space * , loff_t  , unsigned int  ,
2903                      unsigned int  , struct page ** , void ** ) ;
2904   int (*write_end)(struct file * , struct address_space * , loff_t  , unsigned int  ,
2905                    unsigned int  , struct page * , void * ) ;
2906   sector_t (*bmap)(struct address_space * , sector_t  ) ;
2907   void (*invalidatepage)(struct page * , unsigned long  ) ;
2908   int (*releasepage)(struct page * , gfp_t  ) ;
2909   void (*freepage)(struct page * ) ;
2910   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  * , loff_t  ,
2911                        unsigned long  ) ;
2912   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
2913   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
2914   int (*launder_page)(struct page * ) ;
2915   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
2916   int (*error_remove_page)(struct address_space * , struct page * ) ;
2917};
2918#line 642 "include/linux/fs.h"
2919struct address_space {
2920   struct inode *host ;
2921   struct radix_tree_root page_tree ;
2922   spinlock_t tree_lock ;
2923   unsigned int i_mmap_writable ;
2924   struct prio_tree_root i_mmap ;
2925   struct list_head i_mmap_nonlinear ;
2926   struct mutex i_mmap_mutex ;
2927   unsigned long nrpages ;
2928   unsigned long writeback_index ;
2929   struct address_space_operations  const  *a_ops ;
2930   unsigned long flags ;
2931   struct backing_dev_info *backing_dev_info ;
2932   spinlock_t private_lock ;
2933   struct list_head private_list ;
2934   struct address_space *assoc_mapping ;
2935};
2936#line 664
2937struct request_queue;
2938#line 664
2939struct request_queue;
2940#line 665
2941struct hd_struct;
2942#line 665
2943struct gendisk;
2944#line 665 "include/linux/fs.h"
2945struct block_device {
2946   dev_t bd_dev ;
2947   int bd_openers ;
2948   struct inode *bd_inode ;
2949   struct super_block *bd_super ;
2950   struct mutex bd_mutex ;
2951   struct list_head bd_inodes ;
2952   void *bd_claiming ;
2953   void *bd_holder ;
2954   int bd_holders ;
2955   bool bd_write_holder ;
2956   struct list_head bd_holder_disks ;
2957   struct block_device *bd_contains ;
2958   unsigned int bd_block_size ;
2959   struct hd_struct *bd_part ;
2960   unsigned int bd_part_count ;
2961   int bd_invalidated ;
2962   struct gendisk *bd_disk ;
2963   struct request_queue *bd_queue ;
2964   struct list_head bd_list ;
2965   unsigned long bd_private ;
2966   int bd_fsfreeze_count ;
2967   struct mutex bd_fsfreeze_mutex ;
2968};
2969#line 737
2970struct posix_acl;
2971#line 737
2972struct posix_acl;
2973#line 738
2974struct inode_operations;
2975#line 738 "include/linux/fs.h"
2976union __anonunion_ldv_20070_167 {
2977   unsigned int const   i_nlink ;
2978   unsigned int __i_nlink ;
2979};
2980#line 738 "include/linux/fs.h"
2981union __anonunion_ldv_20089_168 {
2982   struct list_head i_dentry ;
2983   struct rcu_head i_rcu ;
2984};
2985#line 738
2986struct file_operations;
2987#line 738
2988struct file_lock;
2989#line 738
2990struct cdev;
2991#line 738 "include/linux/fs.h"
2992union __anonunion_ldv_20107_169 {
2993   struct pipe_inode_info *i_pipe ;
2994   struct block_device *i_bdev ;
2995   struct cdev *i_cdev ;
2996};
2997#line 738 "include/linux/fs.h"
2998struct inode {
2999   umode_t i_mode ;
3000   unsigned short i_opflags ;
3001   uid_t i_uid ;
3002   gid_t i_gid ;
3003   unsigned int i_flags ;
3004   struct posix_acl *i_acl ;
3005   struct posix_acl *i_default_acl ;
3006   struct inode_operations  const  *i_op ;
3007   struct super_block *i_sb ;
3008   struct address_space *i_mapping ;
3009   void *i_security ;
3010   unsigned long i_ino ;
3011   union __anonunion_ldv_20070_167 ldv_20070 ;
3012   dev_t i_rdev ;
3013   struct timespec i_atime ;
3014   struct timespec i_mtime ;
3015   struct timespec i_ctime ;
3016   spinlock_t i_lock ;
3017   unsigned short i_bytes ;
3018   blkcnt_t i_blocks ;
3019   loff_t i_size ;
3020   unsigned long i_state ;
3021   struct mutex i_mutex ;
3022   unsigned long dirtied_when ;
3023   struct hlist_node i_hash ;
3024   struct list_head i_wb_list ;
3025   struct list_head i_lru ;
3026   struct list_head i_sb_list ;
3027   union __anonunion_ldv_20089_168 ldv_20089 ;
3028   atomic_t i_count ;
3029   unsigned int i_blkbits ;
3030   u64 i_version ;
3031   atomic_t i_dio_count ;
3032   atomic_t i_writecount ;
3033   struct file_operations  const  *i_fop ;
3034   struct file_lock *i_flock ;
3035   struct address_space i_data ;
3036   struct dquot *i_dquot[2U] ;
3037   struct list_head i_devices ;
3038   union __anonunion_ldv_20107_169 ldv_20107 ;
3039   __u32 i_generation ;
3040   __u32 i_fsnotify_mask ;
3041   struct hlist_head i_fsnotify_marks ;
3042   atomic_t i_readcount ;
3043   void *i_private ;
3044};
3045#line 941 "include/linux/fs.h"
3046struct fown_struct {
3047   rwlock_t lock ;
3048   struct pid *pid ;
3049   enum pid_type pid_type ;
3050   uid_t uid ;
3051   uid_t euid ;
3052   int signum ;
3053};
3054#line 949 "include/linux/fs.h"
3055struct file_ra_state {
3056   unsigned long start ;
3057   unsigned int size ;
3058   unsigned int async_size ;
3059   unsigned int ra_pages ;
3060   unsigned int mmap_miss ;
3061   loff_t prev_pos ;
3062};
3063#line 972 "include/linux/fs.h"
3064union __anonunion_f_u_170 {
3065   struct list_head fu_list ;
3066   struct rcu_head fu_rcuhead ;
3067};
3068#line 972 "include/linux/fs.h"
3069struct file {
3070   union __anonunion_f_u_170 f_u ;
3071   struct path f_path ;
3072   struct file_operations  const  *f_op ;
3073   spinlock_t f_lock ;
3074   int f_sb_list_cpu ;
3075   atomic_long_t f_count ;
3076   unsigned int f_flags ;
3077   fmode_t f_mode ;
3078   loff_t f_pos ;
3079   struct fown_struct f_owner ;
3080   struct cred  const  *f_cred ;
3081   struct file_ra_state f_ra ;
3082   u64 f_version ;
3083   void *f_security ;
3084   void *private_data ;
3085   struct list_head f_ep_links ;
3086   struct list_head f_tfile_llink ;
3087   struct address_space *f_mapping ;
3088   unsigned long f_mnt_write_state ;
3089};
3090#line 1111 "include/linux/fs.h"
3091typedef struct files_struct *fl_owner_t;
3092#line 1112 "include/linux/fs.h"
3093struct file_lock_operations {
3094   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
3095   void (*fl_release_private)(struct file_lock * ) ;
3096};
3097#line 1117 "include/linux/fs.h"
3098struct lock_manager_operations {
3099   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
3100   void (*lm_notify)(struct file_lock * ) ;
3101   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
3102   void (*lm_release_private)(struct file_lock * ) ;
3103   void (*lm_break)(struct file_lock * ) ;
3104   int (*lm_change)(struct file_lock ** , int  ) ;
3105};
3106#line 1134
3107struct nlm_lockowner;
3108#line 1134
3109struct nlm_lockowner;
3110#line 1135 "include/linux/fs.h"
3111struct nfs_lock_info {
3112   u32 state ;
3113   struct nlm_lockowner *owner ;
3114   struct list_head list ;
3115};
3116#line 14 "include/linux/nfs_fs_i.h"
3117struct nfs4_lock_state;
3118#line 14
3119struct nfs4_lock_state;
3120#line 15 "include/linux/nfs_fs_i.h"
3121struct nfs4_lock_info {
3122   struct nfs4_lock_state *owner ;
3123};
3124#line 19
3125struct fasync_struct;
3126#line 19 "include/linux/nfs_fs_i.h"
3127struct __anonstruct_afs_172 {
3128   struct list_head link ;
3129   int state ;
3130};
3131#line 19 "include/linux/nfs_fs_i.h"
3132union __anonunion_fl_u_171 {
3133   struct nfs_lock_info nfs_fl ;
3134   struct nfs4_lock_info nfs4_fl ;
3135   struct __anonstruct_afs_172 afs ;
3136};
3137#line 19 "include/linux/nfs_fs_i.h"
3138struct file_lock {
3139   struct file_lock *fl_next ;
3140   struct list_head fl_link ;
3141   struct list_head fl_block ;
3142   fl_owner_t fl_owner ;
3143   unsigned int fl_flags ;
3144   unsigned char fl_type ;
3145   unsigned int fl_pid ;
3146   struct pid *fl_nspid ;
3147   wait_queue_head_t fl_wait ;
3148   struct file *fl_file ;
3149   loff_t fl_start ;
3150   loff_t fl_end ;
3151   struct fasync_struct *fl_fasync ;
3152   unsigned long fl_break_time ;
3153   unsigned long fl_downgrade_time ;
3154   struct file_lock_operations  const  *fl_ops ;
3155   struct lock_manager_operations  const  *fl_lmops ;
3156   union __anonunion_fl_u_171 fl_u ;
3157};
3158#line 1221 "include/linux/fs.h"
3159struct fasync_struct {
3160   spinlock_t fa_lock ;
3161   int magic ;
3162   int fa_fd ;
3163   struct fasync_struct *fa_next ;
3164   struct file *fa_file ;
3165   struct rcu_head fa_rcu ;
3166};
3167#line 1417
3168struct file_system_type;
3169#line 1417
3170struct super_operations;
3171#line 1417
3172struct xattr_handler;
3173#line 1417
3174struct mtd_info;
3175#line 1417 "include/linux/fs.h"
3176struct super_block {
3177   struct list_head s_list ;
3178   dev_t s_dev ;
3179   unsigned char s_dirt ;
3180   unsigned char s_blocksize_bits ;
3181   unsigned long s_blocksize ;
3182   loff_t s_maxbytes ;
3183   struct file_system_type *s_type ;
3184   struct super_operations  const  *s_op ;
3185   struct dquot_operations  const  *dq_op ;
3186   struct quotactl_ops  const  *s_qcop ;
3187   struct export_operations  const  *s_export_op ;
3188   unsigned long s_flags ;
3189   unsigned long s_magic ;
3190   struct dentry *s_root ;
3191   struct rw_semaphore s_umount ;
3192   struct mutex s_lock ;
3193   int s_count ;
3194   atomic_t s_active ;
3195   void *s_security ;
3196   struct xattr_handler  const  **s_xattr ;
3197   struct list_head s_inodes ;
3198   struct hlist_bl_head s_anon ;
3199   struct list_head *s_files ;
3200   struct list_head s_mounts ;
3201   struct list_head s_dentry_lru ;
3202   int s_nr_dentry_unused ;
3203   spinlock_t s_inode_lru_lock ;
3204   struct list_head s_inode_lru ;
3205   int s_nr_inodes_unused ;
3206   struct block_device *s_bdev ;
3207   struct backing_dev_info *s_bdi ;
3208   struct mtd_info *s_mtd ;
3209   struct hlist_node s_instances ;
3210   struct quota_info s_dquot ;
3211   int s_frozen ;
3212   wait_queue_head_t s_wait_unfrozen ;
3213   char s_id[32U] ;
3214   u8 s_uuid[16U] ;
3215   void *s_fs_info ;
3216   unsigned int s_max_links ;
3217   fmode_t s_mode ;
3218   u32 s_time_gran ;
3219   struct mutex s_vfs_rename_mutex ;
3220   char *s_subtype ;
3221   char *s_options ;
3222   struct dentry_operations  const  *s_d_op ;
3223   int cleancache_poolid ;
3224   struct shrinker s_shrink ;
3225   atomic_long_t s_remove_count ;
3226   int s_readonly_remount ;
3227};
3228#line 1563 "include/linux/fs.h"
3229struct fiemap_extent_info {
3230   unsigned int fi_flags ;
3231   unsigned int fi_extents_mapped ;
3232   unsigned int fi_extents_max ;
3233   struct fiemap_extent *fi_extents_start ;
3234};
3235#line 1602 "include/linux/fs.h"
3236struct file_operations {
3237   struct module *owner ;
3238   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
3239   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
3240   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
3241   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
3242                       loff_t  ) ;
3243   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
3244                        loff_t  ) ;
3245   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
3246                                                   loff_t  , u64  , unsigned int  ) ) ;
3247   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
3248   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
3249   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
3250   int (*mmap)(struct file * , struct vm_area_struct * ) ;
3251   int (*open)(struct inode * , struct file * ) ;
3252   int (*flush)(struct file * , fl_owner_t  ) ;
3253   int (*release)(struct inode * , struct file * ) ;
3254   int (*fsync)(struct file * , loff_t  , loff_t  , int  ) ;
3255   int (*aio_fsync)(struct kiocb * , int  ) ;
3256   int (*fasync)(int  , struct file * , int  ) ;
3257   int (*lock)(struct file * , int  , struct file_lock * ) ;
3258   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
3259                       int  ) ;
3260   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
3261                                      unsigned long  , unsigned long  ) ;
3262   int (*check_flags)(int  ) ;
3263   int (*flock)(struct file * , int  , struct file_lock * ) ;
3264   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
3265                           unsigned int  ) ;
3266   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
3267                          unsigned int  ) ;
3268   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
3269   long (*fallocate)(struct file * , int  , loff_t  , loff_t  ) ;
3270};
3271#line 1637 "include/linux/fs.h"
3272struct inode_operations {
3273   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
3274   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
3275   int (*permission)(struct inode * , int  ) ;
3276   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
3277   int (*readlink)(struct dentry * , char * , int  ) ;
3278   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
3279   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
3280   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
3281   int (*unlink)(struct inode * , struct dentry * ) ;
3282   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
3283   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
3284   int (*rmdir)(struct inode * , struct dentry * ) ;
3285   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
3286   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
3287   void (*truncate)(struct inode * ) ;
3288   int (*setattr)(struct dentry * , struct iattr * ) ;
3289   int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
3290   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
3291   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
3292   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
3293   int (*removexattr)(struct dentry * , char const   * ) ;
3294   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
3295   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64  , u64  ) ;
3296};
3297#line 1682 "include/linux/fs.h"
3298struct super_operations {
3299   struct inode *(*alloc_inode)(struct super_block * ) ;
3300   void (*destroy_inode)(struct inode * ) ;
3301   void (*dirty_inode)(struct inode * , int  ) ;
3302   int (*write_inode)(struct inode * , struct writeback_control * ) ;
3303   int (*drop_inode)(struct inode * ) ;
3304   void (*evict_inode)(struct inode * ) ;
3305   void (*put_super)(struct super_block * ) ;
3306   void (*write_super)(struct super_block * ) ;
3307   int (*sync_fs)(struct super_block * , int  ) ;
3308   int (*freeze_fs)(struct super_block * ) ;
3309   int (*unfreeze_fs)(struct super_block * ) ;
3310   int (*statfs)(struct dentry * , struct kstatfs * ) ;
3311   int (*remount_fs)(struct super_block * , int * , char * ) ;
3312   void (*umount_begin)(struct super_block * ) ;
3313   int (*show_options)(struct seq_file * , struct dentry * ) ;
3314   int (*show_devname)(struct seq_file * , struct dentry * ) ;
3315   int (*show_path)(struct seq_file * , struct dentry * ) ;
3316   int (*show_stats)(struct seq_file * , struct dentry * ) ;
3317   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
3318   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
3319                          loff_t  ) ;
3320   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
3321   int (*nr_cached_objects)(struct super_block * ) ;
3322   void (*free_cached_objects)(struct super_block * , int  ) ;
3323};
3324#line 1834 "include/linux/fs.h"
3325struct file_system_type {
3326   char const   *name ;
3327   int fs_flags ;
3328   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
3329   void (*kill_sb)(struct super_block * ) ;
3330   struct module *owner ;
3331   struct file_system_type *next ;
3332   struct hlist_head fs_supers ;
3333   struct lock_class_key s_lock_key ;
3334   struct lock_class_key s_umount_key ;
3335   struct lock_class_key s_vfs_rename_key ;
3336   struct lock_class_key i_lock_key ;
3337   struct lock_class_key i_mutex_key ;
3338   struct lock_class_key i_mutex_dir_key ;
3339};
3340#line 2674 "include/linux/fs.h"
3341struct exception_table_entry {
3342   unsigned long insn ;
3343   unsigned long fixup ;
3344};
3345#line 34 "include/linux/poll.h"
3346struct poll_table_struct {
3347   void (*_qproc)(struct file * , wait_queue_head_t * , struct poll_table_struct * ) ;
3348   unsigned long _key ;
3349};
3350#line 148 "drivers/media/dvb/dvb-core/dvbdev.h"
3351struct dvb_ca_en50221 {
3352   struct module *owner ;
3353   int (*read_attribute_mem)(struct dvb_ca_en50221 * , int  , int  ) ;
3354   int (*write_attribute_mem)(struct dvb_ca_en50221 * , int  , int  , u8  ) ;
3355   int (*read_cam_control)(struct dvb_ca_en50221 * , int  , u8  ) ;
3356   int (*write_cam_control)(struct dvb_ca_en50221 * , int  , u8  , u8  ) ;
3357   int (*slot_reset)(struct dvb_ca_en50221 * , int  ) ;
3358   int (*slot_shutdown)(struct dvb_ca_en50221 * , int  ) ;
3359   int (*slot_ts_enable)(struct dvb_ca_en50221 * , int  ) ;
3360   int (*poll_slot_status)(struct dvb_ca_en50221 * , int  , int  ) ;
3361   void *data ;
3362   void *private ;
3363};
3364#line 133 "drivers/media/dvb/dvb-core/dvb_ca_en50221.h"
3365struct cxd2099_cfg {
3366   u32 bitrate ;
3367   u8 adr ;
3368   unsigned char polarity : 1 ;
3369   unsigned char clock_mode : 1 ;
3370};
3371#line 40 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/media/cxd2099/cxd2099.h"
3372struct cxd {
3373   struct dvb_ca_en50221 en ;
3374   struct i2c_adapter *i2c ;
3375   struct cxd2099_cfg cfg ;
3376   u8 regs[35U] ;
3377   u8 lastaddress ;
3378   u8 clk_reg_f ;
3379   u8 clk_reg_b ;
3380   int mode ;
3381   int ready ;
3382   int dr ;
3383   int slot_stat ;
3384   u8 amem[1024U] ;
3385   int amem_read ;
3386   int cammode ;
3387   struct mutex lock ;
3388};
3389#line 1 "<compiler builtins>"
3390
3391#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3392void ldv_spin_lock(void) ;
3393#line 3
3394void ldv_spin_unlock(void) ;
3395#line 4
3396int ldv_spin_trylock(void) ;
3397#line 101 "include/linux/printk.h"
3398extern int printk(char const   *  , ...) ;
3399#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
3400extern void *__memcpy(void * , void const   * , size_t  ) ;
3401#line 55
3402extern void *memset(void * , int  , size_t  ) ;
3403#line 115 "include/linux/mutex.h"
3404extern void __mutex_init(struct mutex * , char const   * , struct lock_class_key * ) ;
3405#line 134
3406extern void mutex_lock_nested(struct mutex * , unsigned int  ) ;
3407#line 169
3408extern void mutex_unlock(struct mutex * ) ;
3409#line 220 "include/linux/slub_def.h"
3410extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
3411#line 223
3412void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
3413#line 225
3414extern void *__kmalloc(size_t  , gfp_t  ) ;
3415#line 268 "include/linux/slub_def.h"
3416__inline static void *ldv_kmalloc_12(size_t size , gfp_t flags ) 
3417{ void *tmp___2 ;
3418
3419  {
3420  {
3421#line 283
3422  tmp___2 = __kmalloc(size, flags);
3423  }
3424#line 283
3425  return (tmp___2);
3426}
3427}
3428#line 268
3429__inline static void *kmalloc(size_t size , gfp_t flags ) ;
3430#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3431void ldv_check_alloc_flags(gfp_t flags ) ;
3432#line 12
3433void ldv_check_alloc_nonatomic(void) ;
3434#line 14
3435struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
3436#line 69 "include/linux/i2c.h"
3437extern int i2c_transfer(struct i2c_adapter * , struct i2c_msg * , int  ) ;
3438#line 46 "include/linux/delay.h"
3439extern void msleep(unsigned int  ) ;
3440#line 39 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/media/cxd2099/cxd2099.h"
3441struct dvb_ca_en50221 *cxd2099_attach(struct cxd2099_cfg *cfg , void *priv , struct i2c_adapter *i2c ) ;
3442#line 77 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3443static int i2c_write_reg(struct i2c_adapter *adapter , u8 adr , u8 reg , u8 data ) 
3444{ u8 m[2U] ;
3445  struct i2c_msg msg ;
3446  int tmp ;
3447  unsigned long __cil_tmp8 ;
3448  unsigned long __cil_tmp9 ;
3449  unsigned long __cil_tmp10 ;
3450  unsigned long __cil_tmp11 ;
3451  struct i2c_msg *__cil_tmp12 ;
3452  unsigned long __cil_tmp13 ;
3453  unsigned long __cil_tmp14 ;
3454  unsigned long __cil_tmp15 ;
3455  int __cil_tmp16 ;
3456  int __cil_tmp17 ;
3457
3458  {
3459  {
3460#line 80
3461  __cil_tmp8 = 0 * 1UL;
3462#line 80
3463  __cil_tmp9 = (unsigned long )(m) + __cil_tmp8;
3464#line 80
3465  *((u8 *)__cil_tmp9) = reg;
3466#line 80
3467  __cil_tmp10 = 1 * 1UL;
3468#line 80
3469  __cil_tmp11 = (unsigned long )(m) + __cil_tmp10;
3470#line 80
3471  *((u8 *)__cil_tmp11) = data;
3472#line 81
3473  __cil_tmp12 = & msg;
3474#line 81
3475  *((__u16 *)__cil_tmp12) = (unsigned short )adr;
3476#line 81
3477  __cil_tmp13 = (unsigned long )(& msg) + 2;
3478#line 81
3479  *((__u16 *)__cil_tmp13) = (__u16 )0U;
3480#line 81
3481  __cil_tmp14 = (unsigned long )(& msg) + 4;
3482#line 81
3483  *((__u16 *)__cil_tmp14) = (__u16 )2U;
3484#line 81
3485  __cil_tmp15 = (unsigned long )(& msg) + 8;
3486#line 81
3487  *((__u8 **)__cil_tmp15) = (__u8 *)(& m);
3488#line 83
3489  tmp = i2c_transfer(adapter, & msg, 1);
3490  }
3491#line 83
3492  if (tmp != 1) {
3493    {
3494#line 84
3495    __cil_tmp16 = (int )reg;
3496#line 84
3497    __cil_tmp17 = (int )adr;
3498#line 84
3499    printk("<3>Failed to write to I2C register %02x@%02x!\n", __cil_tmp16, __cil_tmp17);
3500    }
3501#line 86
3502    return (-1);
3503  } else {
3504
3505  }
3506#line 88
3507  return (0);
3508}
3509}
3510#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3511static int i2c_write(struct i2c_adapter *adapter , u8 adr , u8 *data , u8 len ) 
3512{ struct i2c_msg msg ;
3513  int tmp ;
3514  struct i2c_msg *__cil_tmp7 ;
3515  unsigned long __cil_tmp8 ;
3516  unsigned long __cil_tmp9 ;
3517  unsigned long __cil_tmp10 ;
3518
3519  {
3520  {
3521#line 94
3522  __cil_tmp7 = & msg;
3523#line 94
3524  *((__u16 *)__cil_tmp7) = (unsigned short )adr;
3525#line 94
3526  __cil_tmp8 = (unsigned long )(& msg) + 2;
3527#line 94
3528  *((__u16 *)__cil_tmp8) = (__u16 )0U;
3529#line 94
3530  __cil_tmp9 = (unsigned long )(& msg) + 4;
3531#line 94
3532  *((__u16 *)__cil_tmp9) = (unsigned short )len;
3533#line 94
3534  __cil_tmp10 = (unsigned long )(& msg) + 8;
3535#line 94
3536  *((__u8 **)__cil_tmp10) = data;
3537#line 96
3538  tmp = i2c_transfer(adapter, & msg, 1);
3539  }
3540#line 96
3541  if (tmp != 1) {
3542    {
3543#line 97
3544    printk("<3>Failed to write to I2C!\n");
3545    }
3546#line 98
3547    return (-1);
3548  } else {
3549
3550  }
3551#line 100
3552  return (0);
3553}
3554}
3555#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3556static int i2c_read_reg(struct i2c_adapter *adapter , u8 adr , u8 reg , u8 *val ) 
3557{ struct i2c_msg msgs[2U] ;
3558  int tmp ;
3559  unsigned long __cil_tmp7 ;
3560  unsigned long __cil_tmp8 ;
3561  unsigned long __cil_tmp9 ;
3562  unsigned long __cil_tmp10 ;
3563  unsigned long __cil_tmp11 ;
3564  unsigned long __cil_tmp12 ;
3565  unsigned long __cil_tmp13 ;
3566  unsigned long __cil_tmp14 ;
3567  unsigned long __cil_tmp15 ;
3568  unsigned long __cil_tmp16 ;
3569  unsigned long __cil_tmp17 ;
3570  unsigned long __cil_tmp18 ;
3571  unsigned long __cil_tmp19 ;
3572  unsigned long __cil_tmp20 ;
3573  unsigned long __cil_tmp21 ;
3574  unsigned long __cil_tmp22 ;
3575  unsigned long __cil_tmp23 ;
3576  unsigned long __cil_tmp24 ;
3577  unsigned long __cil_tmp25 ;
3578  unsigned long __cil_tmp26 ;
3579  unsigned long __cil_tmp27 ;
3580  unsigned long __cil_tmp28 ;
3581  struct i2c_msg *__cil_tmp29 ;
3582
3583  {
3584  {
3585#line 106
3586  __cil_tmp7 = 0 * 16UL;
3587#line 106
3588  __cil_tmp8 = (unsigned long )(msgs) + __cil_tmp7;
3589#line 106
3590  *((__u16 *)__cil_tmp8) = (unsigned short )adr;
3591#line 106
3592  __cil_tmp9 = 0 * 16UL;
3593#line 106
3594  __cil_tmp10 = __cil_tmp9 + 2;
3595#line 106
3596  __cil_tmp11 = (unsigned long )(msgs) + __cil_tmp10;
3597#line 106
3598  *((__u16 *)__cil_tmp11) = (__u16 )0U;
3599#line 106
3600  __cil_tmp12 = 0 * 16UL;
3601#line 106
3602  __cil_tmp13 = __cil_tmp12 + 4;
3603#line 106
3604  __cil_tmp14 = (unsigned long )(msgs) + __cil_tmp13;
3605#line 106
3606  *((__u16 *)__cil_tmp14) = (__u16 )1U;
3607#line 106
3608  __cil_tmp15 = 0 * 16UL;
3609#line 106
3610  __cil_tmp16 = __cil_tmp15 + 8;
3611#line 106
3612  __cil_tmp17 = (unsigned long )(msgs) + __cil_tmp16;
3613#line 106
3614  *((__u8 **)__cil_tmp17) = & reg;
3615#line 106
3616  __cil_tmp18 = 1 * 16UL;
3617#line 106
3618  __cil_tmp19 = (unsigned long )(msgs) + __cil_tmp18;
3619#line 106
3620  *((__u16 *)__cil_tmp19) = (unsigned short )adr;
3621#line 106
3622  __cil_tmp20 = 1 * 16UL;
3623#line 106
3624  __cil_tmp21 = __cil_tmp20 + 2;
3625#line 106
3626  __cil_tmp22 = (unsigned long )(msgs) + __cil_tmp21;
3627#line 106
3628  *((__u16 *)__cil_tmp22) = (__u16 )1U;
3629#line 106
3630  __cil_tmp23 = 1 * 16UL;
3631#line 106
3632  __cil_tmp24 = __cil_tmp23 + 4;
3633#line 106
3634  __cil_tmp25 = (unsigned long )(msgs) + __cil_tmp24;
3635#line 106
3636  *((__u16 *)__cil_tmp25) = (__u16 )1U;
3637#line 106
3638  __cil_tmp26 = 1 * 16UL;
3639#line 106
3640  __cil_tmp27 = __cil_tmp26 + 8;
3641#line 106
3642  __cil_tmp28 = (unsigned long )(msgs) + __cil_tmp27;
3643#line 106
3644  *((__u8 **)__cil_tmp28) = val;
3645#line 111
3646  __cil_tmp29 = (struct i2c_msg *)(& msgs);
3647#line 111
3648  tmp = i2c_transfer(adapter, __cil_tmp29, 2);
3649  }
3650#line 111
3651  if (tmp != 2) {
3652    {
3653#line 112
3654    printk("<3>error in i2c_read_reg\n");
3655    }
3656#line 113
3657    return (-1);
3658  } else {
3659
3660  }
3661#line 115
3662  return (0);
3663}
3664}
3665#line 118 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3666static int i2c_read(struct i2c_adapter *adapter , u8 adr , u8 reg , u8 *data , u8 n ) 
3667{ struct i2c_msg msgs[2U] ;
3668  int tmp ;
3669  unsigned long __cil_tmp8 ;
3670  unsigned long __cil_tmp9 ;
3671  unsigned long __cil_tmp10 ;
3672  unsigned long __cil_tmp11 ;
3673  unsigned long __cil_tmp12 ;
3674  unsigned long __cil_tmp13 ;
3675  unsigned long __cil_tmp14 ;
3676  unsigned long __cil_tmp15 ;
3677  unsigned long __cil_tmp16 ;
3678  unsigned long __cil_tmp17 ;
3679  unsigned long __cil_tmp18 ;
3680  unsigned long __cil_tmp19 ;
3681  unsigned long __cil_tmp20 ;
3682  unsigned long __cil_tmp21 ;
3683  unsigned long __cil_tmp22 ;
3684  unsigned long __cil_tmp23 ;
3685  unsigned long __cil_tmp24 ;
3686  unsigned long __cil_tmp25 ;
3687  unsigned long __cil_tmp26 ;
3688  unsigned long __cil_tmp27 ;
3689  unsigned long __cil_tmp28 ;
3690  unsigned long __cil_tmp29 ;
3691  struct i2c_msg *__cil_tmp30 ;
3692
3693  {
3694  {
3695#line 121
3696  __cil_tmp8 = 0 * 16UL;
3697#line 121
3698  __cil_tmp9 = (unsigned long )(msgs) + __cil_tmp8;
3699#line 121
3700  *((__u16 *)__cil_tmp9) = (unsigned short )adr;
3701#line 121
3702  __cil_tmp10 = 0 * 16UL;
3703#line 121
3704  __cil_tmp11 = __cil_tmp10 + 2;
3705#line 121
3706  __cil_tmp12 = (unsigned long )(msgs) + __cil_tmp11;
3707#line 121
3708  *((__u16 *)__cil_tmp12) = (__u16 )0U;
3709#line 121
3710  __cil_tmp13 = 0 * 16UL;
3711#line 121
3712  __cil_tmp14 = __cil_tmp13 + 4;
3713#line 121
3714  __cil_tmp15 = (unsigned long )(msgs) + __cil_tmp14;
3715#line 121
3716  *((__u16 *)__cil_tmp15) = (__u16 )1U;
3717#line 121
3718  __cil_tmp16 = 0 * 16UL;
3719#line 121
3720  __cil_tmp17 = __cil_tmp16 + 8;
3721#line 121
3722  __cil_tmp18 = (unsigned long )(msgs) + __cil_tmp17;
3723#line 121
3724  *((__u8 **)__cil_tmp18) = & reg;
3725#line 121
3726  __cil_tmp19 = 1 * 16UL;
3727#line 121
3728  __cil_tmp20 = (unsigned long )(msgs) + __cil_tmp19;
3729#line 121
3730  *((__u16 *)__cil_tmp20) = (unsigned short )adr;
3731#line 121
3732  __cil_tmp21 = 1 * 16UL;
3733#line 121
3734  __cil_tmp22 = __cil_tmp21 + 2;
3735#line 121
3736  __cil_tmp23 = (unsigned long )(msgs) + __cil_tmp22;
3737#line 121
3738  *((__u16 *)__cil_tmp23) = (__u16 )1U;
3739#line 121
3740  __cil_tmp24 = 1 * 16UL;
3741#line 121
3742  __cil_tmp25 = __cil_tmp24 + 4;
3743#line 121
3744  __cil_tmp26 = (unsigned long )(msgs) + __cil_tmp25;
3745#line 121
3746  *((__u16 *)__cil_tmp26) = (unsigned short )n;
3747#line 121
3748  __cil_tmp27 = 1 * 16UL;
3749#line 121
3750  __cil_tmp28 = __cil_tmp27 + 8;
3751#line 121
3752  __cil_tmp29 = (unsigned long )(msgs) + __cil_tmp28;
3753#line 121
3754  *((__u8 **)__cil_tmp29) = data;
3755#line 126
3756  __cil_tmp30 = (struct i2c_msg *)(& msgs);
3757#line 126
3758  tmp = i2c_transfer(adapter, __cil_tmp30, 2);
3759  }
3760#line 126
3761  if (tmp != 2) {
3762    {
3763#line 127
3764    printk("<3>error in i2c_read\n");
3765    }
3766#line 128
3767    return (-1);
3768  } else {
3769
3770  }
3771#line 130
3772  return (0);
3773}
3774}
3775#line 133 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3776static int read_block(struct cxd *ci , u8 adr , u8 *data , u8 n ) 
3777{ int status ;
3778  unsigned long __cil_tmp6 ;
3779  unsigned long __cil_tmp7 ;
3780  struct i2c_adapter *__cil_tmp8 ;
3781  unsigned long __cil_tmp9 ;
3782  unsigned long __cil_tmp10 ;
3783  unsigned long __cil_tmp11 ;
3784  u8 __cil_tmp12 ;
3785  int __cil_tmp13 ;
3786  u8 __cil_tmp14 ;
3787  u8 __cil_tmp15 ;
3788  int __cil_tmp16 ;
3789  u8 __cil_tmp17 ;
3790  unsigned long __cil_tmp18 ;
3791  unsigned long __cil_tmp19 ;
3792  unsigned long __cil_tmp20 ;
3793  unsigned long __cil_tmp21 ;
3794  struct i2c_adapter *__cil_tmp22 ;
3795  unsigned long __cil_tmp23 ;
3796  unsigned long __cil_tmp24 ;
3797  unsigned long __cil_tmp25 ;
3798  u8 __cil_tmp26 ;
3799  int __cil_tmp27 ;
3800  u8 __cil_tmp28 ;
3801  u8 __cil_tmp29 ;
3802  int __cil_tmp30 ;
3803  u8 __cil_tmp31 ;
3804
3805  {
3806  {
3807#line 137
3808  __cil_tmp6 = (unsigned long )ci;
3809#line 137
3810  __cil_tmp7 = __cil_tmp6 + 88;
3811#line 137
3812  __cil_tmp8 = *((struct i2c_adapter **)__cil_tmp7);
3813#line 137
3814  __cil_tmp9 = 96 + 4;
3815#line 137
3816  __cil_tmp10 = (unsigned long )ci;
3817#line 137
3818  __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
3819#line 137
3820  __cil_tmp12 = *((u8 *)__cil_tmp11);
3821#line 137
3822  __cil_tmp13 = (int )__cil_tmp12;
3823#line 137
3824  __cil_tmp14 = (u8 )__cil_tmp13;
3825#line 137
3826  __cil_tmp15 = (u8 )0;
3827#line 137
3828  __cil_tmp16 = (int )adr;
3829#line 137
3830  __cil_tmp17 = (u8 )__cil_tmp16;
3831#line 137
3832  status = i2c_write_reg(__cil_tmp8, __cil_tmp14, __cil_tmp15, __cil_tmp17);
3833  }
3834#line 138
3835  if (status == 0) {
3836    {
3837#line 139
3838    __cil_tmp18 = (unsigned long )ci;
3839#line 139
3840    __cil_tmp19 = __cil_tmp18 + 139;
3841#line 139
3842    *((u8 *)__cil_tmp19) = adr;
3843#line 140
3844    __cil_tmp20 = (unsigned long )ci;
3845#line 140
3846    __cil_tmp21 = __cil_tmp20 + 88;
3847#line 140
3848    __cil_tmp22 = *((struct i2c_adapter **)__cil_tmp21);
3849#line 140
3850    __cil_tmp23 = 96 + 4;
3851#line 140
3852    __cil_tmp24 = (unsigned long )ci;
3853#line 140
3854    __cil_tmp25 = __cil_tmp24 + __cil_tmp23;
3855#line 140
3856    __cil_tmp26 = *((u8 *)__cil_tmp25);
3857#line 140
3858    __cil_tmp27 = (int )__cil_tmp26;
3859#line 140
3860    __cil_tmp28 = (u8 )__cil_tmp27;
3861#line 140
3862    __cil_tmp29 = (u8 )1;
3863#line 140
3864    __cil_tmp30 = (int )n;
3865#line 140
3866    __cil_tmp31 = (u8 )__cil_tmp30;
3867#line 140
3868    status = i2c_read(__cil_tmp22, __cil_tmp28, __cil_tmp29, data, __cil_tmp31);
3869    }
3870  } else {
3871
3872  }
3873#line 142
3874  return (status);
3875}
3876}
3877#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3878static int read_reg(struct cxd *ci , u8 reg , u8 *val ) 
3879{ int tmp ;
3880  int __cil_tmp5 ;
3881  u8 __cil_tmp6 ;
3882  u8 __cil_tmp7 ;
3883
3884  {
3885  {
3886#line 147
3887  __cil_tmp5 = (int )reg;
3888#line 147
3889  __cil_tmp6 = (u8 )__cil_tmp5;
3890#line 147
3891  __cil_tmp7 = (u8 )1;
3892#line 147
3893  tmp = read_block(ci, __cil_tmp6, val, __cil_tmp7);
3894  }
3895#line 147
3896  return (tmp);
3897}
3898}
3899#line 151 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
3900static int read_pccard(struct cxd *ci , u16 address , u8 *data , u8 n ) 
3901{ int status ;
3902  u8 addr[3U] ;
3903  unsigned long __cil_tmp7 ;
3904  unsigned long __cil_tmp8 ;
3905  unsigned long __cil_tmp9 ;
3906  unsigned long __cil_tmp10 ;
3907  unsigned long __cil_tmp11 ;
3908  unsigned long __cil_tmp12 ;
3909  int __cil_tmp13 ;
3910  int __cil_tmp14 ;
3911  unsigned long __cil_tmp15 ;
3912  unsigned long __cil_tmp16 ;
3913  struct i2c_adapter *__cil_tmp17 ;
3914  unsigned long __cil_tmp18 ;
3915  unsigned long __cil_tmp19 ;
3916  unsigned long __cil_tmp20 ;
3917  u8 __cil_tmp21 ;
3918  int __cil_tmp22 ;
3919  u8 __cil_tmp23 ;
3920  u8 *__cil_tmp24 ;
3921  u8 __cil_tmp25 ;
3922  unsigned long __cil_tmp26 ;
3923  unsigned long __cil_tmp27 ;
3924  struct i2c_adapter *__cil_tmp28 ;
3925  unsigned long __cil_tmp29 ;
3926  unsigned long __cil_tmp30 ;
3927  unsigned long __cil_tmp31 ;
3928  u8 __cil_tmp32 ;
3929  int __cil_tmp33 ;
3930  u8 __cil_tmp34 ;
3931  u8 __cil_tmp35 ;
3932  int __cil_tmp36 ;
3933  u8 __cil_tmp37 ;
3934
3935  {
3936  {
3937#line 154
3938  __cil_tmp7 = 0 * 1UL;
3939#line 154
3940  __cil_tmp8 = (unsigned long )(addr) + __cil_tmp7;
3941#line 154
3942  *((u8 *)__cil_tmp8) = (u8 )2U;
3943#line 154
3944  __cil_tmp9 = 1 * 1UL;
3945#line 154
3946  __cil_tmp10 = (unsigned long )(addr) + __cil_tmp9;
3947#line 154
3948  *((u8 *)__cil_tmp10) = (unsigned char )address;
3949#line 154
3950  __cil_tmp11 = 2 * 1UL;
3951#line 154
3952  __cil_tmp12 = (unsigned long )(addr) + __cil_tmp11;
3953#line 154
3954  __cil_tmp13 = (int )address;
3955#line 154
3956  __cil_tmp14 = __cil_tmp13 >> 8;
3957#line 154
3958  *((u8 *)__cil_tmp12) = (unsigned char )__cil_tmp14;
3959#line 156
3960  __cil_tmp15 = (unsigned long )ci;
3961#line 156
3962  __cil_tmp16 = __cil_tmp15 + 88;
3963#line 156
3964  __cil_tmp17 = *((struct i2c_adapter **)__cil_tmp16);
3965#line 156
3966  __cil_tmp18 = 96 + 4;
3967#line 156
3968  __cil_tmp19 = (unsigned long )ci;
3969#line 156
3970  __cil_tmp20 = __cil_tmp19 + __cil_tmp18;
3971#line 156
3972  __cil_tmp21 = *((u8 *)__cil_tmp20);
3973#line 156
3974  __cil_tmp22 = (int )__cil_tmp21;
3975#line 156
3976  __cil_tmp23 = (u8 )__cil_tmp22;
3977#line 156
3978  __cil_tmp24 = (u8 *)(& addr);
3979#line 156
3980  __cil_tmp25 = (u8 )3;
3981#line 156
3982  status = i2c_write(__cil_tmp17, __cil_tmp23, __cil_tmp24, __cil_tmp25);
3983  }
3984#line 157
3985  if (status == 0) {
3986    {
3987#line 158
3988    __cil_tmp26 = (unsigned long )ci;
3989#line 158
3990    __cil_tmp27 = __cil_tmp26 + 88;
3991#line 158
3992    __cil_tmp28 = *((struct i2c_adapter **)__cil_tmp27);
3993#line 158
3994    __cil_tmp29 = 96 + 4;
3995#line 158
3996    __cil_tmp30 = (unsigned long )ci;
3997#line 158
3998    __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
3999#line 158
4000    __cil_tmp32 = *((u8 *)__cil_tmp31);
4001#line 158
4002    __cil_tmp33 = (int )__cil_tmp32;
4003#line 158
4004    __cil_tmp34 = (u8 )__cil_tmp33;
4005#line 158
4006    __cil_tmp35 = (u8 )3;
4007#line 158
4008    __cil_tmp36 = (int )n;
4009#line 158
4010    __cil_tmp37 = (u8 )__cil_tmp36;
4011#line 158
4012    status = i2c_read(__cil_tmp28, __cil_tmp34, __cil_tmp35, data, __cil_tmp37);
4013    }
4014  } else {
4015
4016  }
4017#line 159
4018  return (status);
4019}
4020}
4021#line 162 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
4022static int write_pccard(struct cxd *ci , u16 address , u8 *data , u8 n ) 
4023{ int status ;
4024  u8 addr[3U] ;
4025  u8 buf[256U] ;
4026  size_t __len ;
4027  void *__ret ;
4028  unsigned long __cil_tmp10 ;
4029  unsigned long __cil_tmp11 ;
4030  unsigned long __cil_tmp12 ;
4031  unsigned long __cil_tmp13 ;
4032  unsigned long __cil_tmp14 ;
4033  unsigned long __cil_tmp15 ;
4034  int __cil_tmp16 ;
4035  int __cil_tmp17 ;
4036  unsigned long __cil_tmp18 ;
4037  unsigned long __cil_tmp19 ;
4038  struct i2c_adapter *__cil_tmp20 ;
4039  unsigned long __cil_tmp21 ;
4040  unsigned long __cil_tmp22 ;
4041  unsigned long __cil_tmp23 ;
4042  u8 __cil_tmp24 ;
4043  int __cil_tmp25 ;
4044  u8 __cil_tmp26 ;
4045  u8 *__cil_tmp27 ;
4046  u8 __cil_tmp28 ;
4047  unsigned long __cil_tmp29 ;
4048  unsigned long __cil_tmp30 ;
4049  void *__cil_tmp31 ;
4050  void *__cil_tmp32 ;
4051  void const   *__cil_tmp33 ;
4052  unsigned long __cil_tmp34 ;
4053  unsigned long __cil_tmp35 ;
4054  struct i2c_adapter *__cil_tmp36 ;
4055  unsigned long __cil_tmp37 ;
4056  unsigned long __cil_tmp38 ;
4057  unsigned long __cil_tmp39 ;
4058  u8 __cil_tmp40 ;
4059  int __cil_tmp41 ;
4060  u8 __cil_tmp42 ;
4061  u8 *__cil_tmp43 ;
4062  unsigned int __cil_tmp44 ;
4063  unsigned int __cil_tmp45 ;
4064  int __cil_tmp46 ;
4065  u8 __cil_tmp47 ;
4066
4067  {
4068  {
4069#line 165
4070  __cil_tmp10 = 0 * 1UL;
4071#line 165
4072  __cil_tmp11 = (unsigned long )(addr) + __cil_tmp10;
4073#line 165
4074  *((u8 *)__cil_tmp11) = (u8 )2U;
4075#line 165
4076  __cil_tmp12 = 1 * 1UL;
4077#line 165
4078  __cil_tmp13 = (unsigned long )(addr) + __cil_tmp12;
4079#line 165
4080  *((u8 *)__cil_tmp13) = (unsigned char )address;
4081#line 165
4082  __cil_tmp14 = 2 * 1UL;
4083#line 165
4084  __cil_tmp15 = (unsigned long )(addr) + __cil_tmp14;
4085#line 165
4086  __cil_tmp16 = (int )address;
4087#line 165
4088  __cil_tmp17 = __cil_tmp16 >> 8;
4089#line 165
4090  *((u8 *)__cil_tmp15) = (unsigned char )__cil_tmp17;
4091#line 167
4092  __cil_tmp18 = (unsigned long )ci;
4093#line 167
4094  __cil_tmp19 = __cil_tmp18 + 88;
4095#line 167
4096  __cil_tmp20 = *((struct i2c_adapter **)__cil_tmp19);
4097#line 167
4098  __cil_tmp21 = 96 + 4;
4099#line 167
4100  __cil_tmp22 = (unsigned long )ci;
4101#line 167
4102  __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
4103#line 167
4104  __cil_tmp24 = *((u8 *)__cil_tmp23);
4105#line 167
4106  __cil_tmp25 = (int )__cil_tmp24;
4107#line 167
4108  __cil_tmp26 = (u8 )__cil_tmp25;
4109#line 167
4110  __cil_tmp27 = (u8 *)(& addr);
4111#line 167
4112  __cil_tmp28 = (u8 )3;
4113#line 167
4114  status = i2c_write(__cil_tmp20, __cil_tmp26, __cil_tmp27, __cil_tmp28);
4115  }
4116#line 168
4117  if (status == 0) {
4118    {
4119#line 169
4120    __cil_tmp29 = 0 * 1UL;
4121#line 169
4122    __cil_tmp30 = (unsigned long )(buf) + __cil_tmp29;
4123#line 169
4124    *((u8 *)__cil_tmp30) = (u8 )3U;
4125#line 170
4126    __len = (size_t )n;
4127#line 170
4128    __cil_tmp31 = (void *)(& buf);
4129#line 170
4130    __cil_tmp32 = __cil_tmp31 + 1U;
4131#line 170
4132    __cil_tmp33 = (void const   *)data;
4133#line 170
4134    __ret = __builtin_memcpy(__cil_tmp32, __cil_tmp33, __len);
4135#line 171
4136    __cil_tmp34 = (unsigned long )ci;
4137#line 171
4138    __cil_tmp35 = __cil_tmp34 + 88;
4139#line 171
4140    __cil_tmp36 = *((struct i2c_adapter **)__cil_tmp35);
4141#line 171
4142    __cil_tmp37 = 96 + 4;
4143#line 171
4144    __cil_tmp38 = (unsigned long )ci;
4145#line 171
4146    __cil_tmp39 = __cil_tmp38 + __cil_tmp37;
4147#line 171
4148    __cil_tmp40 = *((u8 *)__cil_tmp39);
4149#line 171
4150    __cil_tmp41 = (int )__cil_tmp40;
4151#line 171
4152    __cil_tmp42 = (u8 )__cil_tmp41;
4153#line 171
4154    __cil_tmp43 = (u8 *)(& buf);
4155#line 171
4156    __cil_tmp44 = (unsigned int )n;
4157#line 171
4158    __cil_tmp45 = __cil_tmp44 + 1U;
4159#line 171
4160    __cil_tmp46 = (int )__cil_tmp45;
4161#line 171
4162    __cil_tmp47 = (u8 )__cil_tmp46;
4163#line 171
4164    status = i2c_write(__cil_tmp36, __cil_tmp42, __cil_tmp43, __cil_tmp47);
4165    }
4166  } else {
4167
4168  }
4169#line 173
4170  return (status);
4171}
4172}
4173#line 176 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
4174static int read_io(struct cxd *ci , u16 address , u8 *val ) 
4175{ int status ;
4176  u8 addr[3U] ;
4177  unsigned long __cil_tmp6 ;
4178  unsigned long __cil_tmp7 ;
4179  unsigned long __cil_tmp8 ;
4180  unsigned long __cil_tmp9 ;
4181  unsigned long __cil_tmp10 ;
4182  unsigned long __cil_tmp11 ;
4183  int __cil_tmp12 ;
4184  int __cil_tmp13 ;
4185  unsigned long __cil_tmp14 ;
4186  unsigned long __cil_tmp15 ;
4187  struct i2c_adapter *__cil_tmp16 ;
4188  unsigned long __cil_tmp17 ;
4189  unsigned long __cil_tmp18 ;
4190  unsigned long __cil_tmp19 ;
4191  u8 __cil_tmp20 ;
4192  int __cil_tmp21 ;
4193  u8 __cil_tmp22 ;
4194  u8 *__cil_tmp23 ;
4195  u8 __cil_tmp24 ;
4196  unsigned long __cil_tmp25 ;
4197  unsigned long __cil_tmp26 ;
4198  struct i2c_adapter *__cil_tmp27 ;
4199  unsigned long __cil_tmp28 ;
4200  unsigned long __cil_tmp29 ;
4201  unsigned long __cil_tmp30 ;
4202  u8 __cil_tmp31 ;
4203  int __cil_tmp32 ;
4204  u8 __cil_tmp33 ;
4205  u8 __cil_tmp34 ;
4206  u8 __cil_tmp35 ;
4207
4208  {
4209  {
4210#line 179
4211  __cil_tmp6 = 0 * 1UL;
4212#line 179
4213  __cil_tmp7 = (unsigned long )(addr) + __cil_tmp6;
4214#line 179
4215  *((u8 *)__cil_tmp7) = (u8 )2U;
4216#line 179
4217  __cil_tmp8 = 1 * 1UL;
4218#line 179
4219  __cil_tmp9 = (unsigned long )(addr) + __cil_tmp8;
4220#line 179
4221  *((u8 *)__cil_tmp9) = (unsigned char )address;
4222#line 179
4223  __cil_tmp10 = 2 * 1UL;
4224#line 179
4225  __cil_tmp11 = (unsigned long )(addr) + __cil_tmp10;
4226#line 179
4227  __cil_tmp12 = (int )address;
4228#line 179
4229  __cil_tmp13 = __cil_tmp12 >> 8;
4230#line 179
4231  *((u8 *)__cil_tmp11) = (unsigned char )__cil_tmp13;
4232#line 181
4233  __cil_tmp14 = (unsigned long )ci;
4234#line 181
4235  __cil_tmp15 = __cil_tmp14 + 88;
4236#line 181
4237  __cil_tmp16 = *((struct i2c_adapter **)__cil_tmp15);
4238#line 181
4239  __cil_tmp17 = 96 + 4;
4240#line 181
4241  __cil_tmp18 = (unsigned long )ci;
4242#line 181
4243  __cil_tmp19 = __cil_tmp18 + __cil_tmp17;
4244#line 181
4245  __cil_tmp20 = *((u8 *)__cil_tmp19);
4246#line 181
4247  __cil_tmp21 = (int )__cil_tmp20;
4248#line 181
4249  __cil_tmp22 = (u8 )__cil_tmp21;
4250#line 181
4251  __cil_tmp23 = (u8 *)(& addr);
4252#line 181
4253  __cil_tmp24 = (u8 )3;
4254#line 181
4255  status = i2c_write(__cil_tmp16, __cil_tmp22, __cil_tmp23, __cil_tmp24);
4256  }
4257#line 182
4258  if (status == 0) {
4259    {
4260#line 183
4261    __cil_tmp25 = (unsigned long )ci;
4262#line 183
4263    __cil_tmp26 = __cil_tmp25 + 88;
4264#line 183
4265    __cil_tmp27 = *((struct i2c_adapter **)__cil_tmp26);
4266#line 183
4267    __cil_tmp28 = 96 + 4;
4268#line 183
4269    __cil_tmp29 = (unsigned long )ci;
4270#line 183
4271    __cil_tmp30 = __cil_tmp29 + __cil_tmp28;
4272#line 183
4273    __cil_tmp31 = *((u8 *)__cil_tmp30);
4274#line 183
4275    __cil_tmp32 = (int )__cil_tmp31;
4276#line 183
4277    __cil_tmp33 = (u8 )__cil_tmp32;
4278#line 183
4279    __cil_tmp34 = (u8 )3;
4280#line 183
4281    __cil_tmp35 = (u8 )1;
4282#line 183
4283    status = i2c_read(__cil_tmp27, __cil_tmp33, __cil_tmp34, val, __cil_tmp35);
4284    }
4285  } else {
4286
4287  }
4288#line 184
4289  return (status);
4290}
4291}
4292#line 187 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
4293static int write_io(struct cxd *ci , u16 address , u8 val ) 
4294{ int status ;
4295  u8 addr[3U] ;
4296  u8 buf[2U] ;
4297  unsigned long __cil_tmp7 ;
4298  unsigned long __cil_tmp8 ;
4299  unsigned long __cil_tmp9 ;
4300  unsigned long __cil_tmp10 ;
4301  unsigned long __cil_tmp11 ;
4302  unsigned long __cil_tmp12 ;
4303  int __cil_tmp13 ;
4304  int __cil_tmp14 ;
4305  unsigned long __cil_tmp15 ;
4306  unsigned long __cil_tmp16 ;
4307  unsigned long __cil_tmp17 ;
4308  unsigned long __cil_tmp18 ;
4309  unsigned long __cil_tmp19 ;
4310  unsigned long __cil_tmp20 ;
4311  struct i2c_adapter *__cil_tmp21 ;
4312  unsigned long __cil_tmp22 ;
4313  unsigned long __cil_tmp23 ;
4314  unsigned long __cil_tmp24 ;
4315  u8 __cil_tmp25 ;
4316  int __cil_tmp26 ;
4317  u8 __cil_tmp27 ;
4318  u8 *__cil_tmp28 ;
4319  u8 __cil_tmp29 ;
4320  unsigned long __cil_tmp30 ;
4321  unsigned long __cil_tmp31 ;
4322  struct i2c_adapter *__cil_tmp32 ;
4323  unsigned long __cil_tmp33 ;
4324  unsigned long __cil_tmp34 ;
4325  unsigned long __cil_tmp35 ;
4326  u8 __cil_tmp36 ;
4327  int __cil_tmp37 ;
4328  u8 __cil_tmp38 ;
4329  u8 *__cil_tmp39 ;
4330  u8 __cil_tmp40 ;
4331
4332  {
4333  {
4334#line 190
4335  __cil_tmp7 = 0 * 1UL;
4336#line 190
4337  __cil_tmp8 = (unsigned long )(addr) + __cil_tmp7;
4338#line 190
4339  *((u8 *)__cil_tmp8) = (u8 )2U;
4340#line 190
4341  __cil_tmp9 = 1 * 1UL;
4342#line 190
4343  __cil_tmp10 = (unsigned long )(addr) + __cil_tmp9;
4344#line 190
4345  *((u8 *)__cil_tmp10) = (unsigned char )address;
4346#line 190
4347  __cil_tmp11 = 2 * 1UL;
4348#line 190
4349  __cil_tmp12 = (unsigned long )(addr) + __cil_tmp11;
4350#line 190
4351  __cil_tmp13 = (int )address;
4352#line 190
4353  __cil_tmp14 = __cil_tmp13 >> 8;
4354#line 190
4355  *((u8 *)__cil_tmp12) = (unsigned char )__cil_tmp14;
4356#line 191
4357  __cil_tmp15 = 0 * 1UL;
4358#line 191
4359  __cil_tmp16 = (unsigned long )(buf) + __cil_tmp15;
4360#line 191
4361  *((u8 *)__cil_tmp16) = (u8 )3U;
4362#line 191
4363  __cil_tmp17 = 1 * 1UL;
4364#line 191
4365  __cil_tmp18 = (unsigned long )(buf) + __cil_tmp17;
4366#line 191
4367  *((u8 *)__cil_tmp18) = val;
4368#line 193
4369  __cil_tmp19 = (unsigned long )ci;
4370#line 193
4371  __cil_tmp20 = __cil_tmp19 + 88;
4372#line 193
4373  __cil_tmp21 = *((struct i2c_adapter **)__cil_tmp20);
4374#line 193
4375  __cil_tmp22 = 96 + 4;
4376#line 193
4377  __cil_tmp23 = (unsigned long )ci;
4378#line 193
4379  __cil_tmp24 = __cil_tmp23 + __cil_tmp22;
4380#line 193
4381  __cil_tmp25 = *((u8 *)__cil_tmp24);
4382#line 193
4383  __cil_tmp26 = (int )__cil_tmp25;
4384#line 193
4385  __cil_tmp27 = (u8 )__cil_tmp26;
4386#line 193
4387  __cil_tmp28 = (u8 *)(& addr);
4388#line 193
4389  __cil_tmp29 = (u8 )3;
4390#line 193
4391  status = i2c_write(__cil_tmp21, __cil_tmp27, __cil_tmp28, __cil_tmp29);
4392  }
4393#line 194
4394  if (status == 0) {
4395    {
4396#line 195
4397    __cil_tmp30 = (unsigned long )ci;
4398#line 195
4399    __cil_tmp31 = __cil_tmp30 + 88;
4400#line 195
4401    __cil_tmp32 = *((struct i2c_adapter **)__cil_tmp31);
4402#line 195
4403    __cil_tmp33 = 96 + 4;
4404#line 195
4405    __cil_tmp34 = (unsigned long )ci;
4406#line 195
4407    __cil_tmp35 = __cil_tmp34 + __cil_tmp33;
4408#line 195
4409    __cil_tmp36 = *((u8 *)__cil_tmp35);
4410#line 195
4411    __cil_tmp37 = (int )__cil_tmp36;
4412#line 195
4413    __cil_tmp38 = (u8 )__cil_tmp37;
4414#line 195
4415    __cil_tmp39 = (u8 *)(& buf);
4416#line 195
4417    __cil_tmp40 = (u8 )2;
4418#line 195
4419    status = i2c_write(__cil_tmp32, __cil_tmp38, __cil_tmp39, __cil_tmp40);
4420    }
4421  } else {
4422
4423  }
4424#line 196
4425  return (status);
4426}
4427}
4428#line 226 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
4429static int write_regm(struct cxd *ci , u8 reg , u8 val , u8 mask ) 
4430{ int status ;
4431  unsigned long __cil_tmp6 ;
4432  unsigned long __cil_tmp7 ;
4433  struct i2c_adapter *__cil_tmp8 ;
4434  unsigned long __cil_tmp9 ;
4435  unsigned long __cil_tmp10 ;
4436  unsigned long __cil_tmp11 ;
4437  u8 __cil_tmp12 ;
4438  int __cil_tmp13 ;
4439  u8 __cil_tmp14 ;
4440  u8 __cil_tmp15 ;
4441  int __cil_tmp16 ;
4442  u8 __cil_tmp17 ;
4443  unsigned int __cil_tmp18 ;
4444  unsigned int __cil_tmp19 ;
4445  unsigned int __cil_tmp20 ;
4446  unsigned long __cil_tmp21 ;
4447  unsigned long __cil_tmp22 ;
4448  struct i2c_adapter *__cil_tmp23 ;
4449  unsigned long __cil_tmp24 ;
4450  unsigned long __cil_tmp25 ;
4451  unsigned long __cil_tmp26 ;
4452  u8 __cil_tmp27 ;
4453  int __cil_tmp28 ;
4454  u8 __cil_tmp29 ;
4455  u8 __cil_tmp30 ;
4456  unsigned long __cil_tmp31 ;
4457  unsigned long __cil_tmp32 ;
4458  unsigned long __cil_tmp33 ;
4459  u8 (*__cil_tmp34)[35U] ;
4460  u8 *__cil_tmp35 ;
4461  u8 *__cil_tmp36 ;
4462  int __cil_tmp37 ;
4463  unsigned long __cil_tmp38 ;
4464  unsigned long __cil_tmp39 ;
4465  unsigned long __cil_tmp40 ;
4466  unsigned long __cil_tmp41 ;
4467  signed char __cil_tmp42 ;
4468  int __cil_tmp43 ;
4469  signed char __cil_tmp44 ;
4470  int __cil_tmp45 ;
4471  int __cil_tmp46 ;
4472  int __cil_tmp47 ;
4473  unsigned long __cil_tmp48 ;
4474  unsigned long __cil_tmp49 ;
4475  unsigned long __cil_tmp50 ;
4476  unsigned long __cil_tmp51 ;
4477  u8 __cil_tmp52 ;
4478  signed char __cil_tmp53 ;
4479  int __cil_tmp54 ;
4480  int __cil_tmp55 ;
4481  int __cil_tmp56 ;
4482  unsigned long __cil_tmp57 ;
4483  unsigned long __cil_tmp58 ;
4484  unsigned long __cil_tmp59 ;
4485  unsigned long __cil_tmp60 ;
4486  struct i2c_adapter *__cil_tmp61 ;
4487  unsigned long __cil_tmp62 ;
4488  unsigned long __cil_tmp63 ;
4489  unsigned long __cil_tmp64 ;
4490  u8 __cil_tmp65 ;
4491  int __cil_tmp66 ;
4492  u8 __cil_tmp67 ;
4493  u8 __cil_tmp68 ;
4494  int __cil_tmp69 ;
4495  unsigned long __cil_tmp70 ;
4496  unsigned long __cil_tmp71 ;
4497  unsigned long __cil_tmp72 ;
4498  unsigned long __cil_tmp73 ;
4499  u8 __cil_tmp74 ;
4500  int __cil_tmp75 ;
4501  u8 __cil_tmp76 ;
4502  unsigned int __cil_tmp77 ;
4503  int __cil_tmp78 ;
4504  unsigned long __cil_tmp79 ;
4505  unsigned long __cil_tmp80 ;
4506  unsigned long __cil_tmp81 ;
4507  unsigned long __cil_tmp82 ;
4508  int __cil_tmp83 ;
4509  unsigned long __cil_tmp84 ;
4510  unsigned long __cil_tmp85 ;
4511  unsigned long __cil_tmp86 ;
4512  unsigned long __cil_tmp87 ;
4513  u8 __cil_tmp88 ;
4514  unsigned int __cil_tmp89 ;
4515  unsigned int __cil_tmp90 ;
4516
4517  {
4518  {
4519#line 230
4520  __cil_tmp6 = (unsigned long )ci;
4521#line 230
4522  __cil_tmp7 = __cil_tmp6 + 88;
4523#line 230
4524  __cil_tmp8 = *((struct i2c_adapter **)__cil_tmp7);
4525#line 230
4526  __cil_tmp9 = 96 + 4;
4527#line 230
4528  __cil_tmp10 = (unsigned long )ci;
4529#line 230
4530  __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
4531#line 230
4532  __cil_tmp12 = *((u8 *)__cil_tmp11);
4533#line 230
4534  __cil_tmp13 = (int )__cil_tmp12;
4535#line 230
4536  __cil_tmp14 = (u8 )__cil_tmp13;
4537#line 230
4538  __cil_tmp15 = (u8 )0;
4539#line 230
4540  __cil_tmp16 = (int )reg;
4541#line 230
4542  __cil_tmp17 = (u8 )__cil_tmp16;
4543#line 230
4544  status = i2c_write_reg(__cil_tmp8, __cil_tmp14, __cil_tmp15, __cil_tmp17);
4545  }
4546#line 231
4547  if (status == 0) {
4548    {
4549#line 231
4550    __cil_tmp18 = (unsigned int )reg;
4551#line 231
4552    if (__cil_tmp18 > 5U) {
4553      {
4554#line 231
4555      __cil_tmp19 = (unsigned int )reg;
4556#line 231
4557      if (__cil_tmp19 <= 8U) {
4558        {
4559#line 231
4560        __cil_tmp20 = (unsigned int )mask;
4561#line 231
4562        if (__cil_tmp20 != 255U) {
4563          {
4564#line 232
4565          __cil_tmp21 = (unsigned long )ci;
4566#line 232
4567          __cil_tmp22 = __cil_tmp21 + 88;
4568#line 232
4569          __cil_tmp23 = *((struct i2c_adapter **)__cil_tmp22);
4570#line 232
4571          __cil_tmp24 = 96 + 4;
4572#line 232
4573          __cil_tmp25 = (unsigned long )ci;
4574#line 232
4575          __cil_tmp26 = __cil_tmp25 + __cil_tmp24;
4576#line 232
4577          __cil_tmp27 = *((u8 *)__cil_tmp26);
4578#line 232
4579          __cil_tmp28 = (int )__cil_tmp27;
4580#line 232
4581          __cil_tmp29 = (u8 )__cil_tmp28;
4582#line 232
4583          __cil_tmp30 = (u8 )1;
4584#line 232
4585          __cil_tmp31 = (unsigned long )reg;
4586#line 232
4587          __cil_tmp32 = (unsigned long )ci;
4588#line 232
4589          __cil_tmp33 = __cil_tmp32 + 104;
4590#line 232
4591          __cil_tmp34 = (u8 (*)[35U])__cil_tmp33;
4592#line 232
4593          __cil_tmp35 = (u8 *)__cil_tmp34;
4594#line 232
4595          __cil_tmp36 = __cil_tmp35 + __cil_tmp31;
4596#line 232
4597          status = i2c_read_reg(__cil_tmp23, __cil_tmp29, __cil_tmp30, __cil_tmp36);
4598          }
4599        } else {
4600
4601        }
4602        }
4603      } else {
4604
4605      }
4606      }
4607    } else {
4608
4609    }
4610    }
4611  } else {
4612
4613  }
4614#line 233
4615  __cil_tmp37 = (int )reg;
4616#line 233
4617  __cil_tmp38 = __cil_tmp37 * 1UL;
4618#line 233
4619  __cil_tmp39 = 104 + __cil_tmp38;
4620#line 233
4621  __cil_tmp40 = (unsigned long )ci;
4622#line 233
4623  __cil_tmp41 = __cil_tmp40 + __cil_tmp39;
4624#line 233
4625  __cil_tmp42 = (signed char )val;
4626#line 233
4627  __cil_tmp43 = (int )__cil_tmp42;
4628#line 233
4629  __cil_tmp44 = (signed char )mask;
4630#line 233
4631  __cil_tmp45 = (int )__cil_tmp44;
4632#line 233
4633  __cil_tmp46 = ~ __cil_tmp45;
4634#line 233
4635  __cil_tmp47 = (int )reg;
4636#line 233
4637  __cil_tmp48 = __cil_tmp47 * 1UL;
4638#line 233
4639  __cil_tmp49 = 104 + __cil_tmp48;
4640#line 233
4641  __cil_tmp50 = (unsigned long )ci;
4642#line 233
4643  __cil_tmp51 = __cil_tmp50 + __cil_tmp49;
4644#line 233
4645  __cil_tmp52 = *((u8 *)__cil_tmp51);
4646#line 233
4647  __cil_tmp53 = (signed char )__cil_tmp52;
4648#line 233
4649  __cil_tmp54 = (int )__cil_tmp53;
4650#line 233
4651  __cil_tmp55 = __cil_tmp54 & __cil_tmp46;
4652#line 233
4653  __cil_tmp56 = __cil_tmp55 | __cil_tmp43;
4654#line 233
4655  *((u8 *)__cil_tmp41) = (u8 )__cil_tmp56;
4656#line 234
4657  if (status == 0) {
4658    {
4659#line 235
4660    __cil_tmp57 = (unsigned long )ci;
4661#line 235
4662    __cil_tmp58 = __cil_tmp57 + 139;
4663#line 235
4664    *((u8 *)__cil_tmp58) = reg;
4665#line 236
4666    __cil_tmp59 = (unsigned long )ci;
4667#line 236
4668    __cil_tmp60 = __cil_tmp59 + 88;
4669#line 236
4670    __cil_tmp61 = *((struct i2c_adapter **)__cil_tmp60);
4671#line 236
4672    __cil_tmp62 = 96 + 4;
4673#line 236
4674    __cil_tmp63 = (unsigned long )ci;
4675#line 236
4676    __cil_tmp64 = __cil_tmp63 + __cil_tmp62;
4677#line 236
4678    __cil_tmp65 = *((u8 *)__cil_tmp64);
4679#line 236
4680    __cil_tmp66 = (int )__cil_tmp65;
4681#line 236
4682    __cil_tmp67 = (u8 )__cil_tmp66;
4683#line 236
4684    __cil_tmp68 = (u8 )1;
4685#line 236
4686    __cil_tmp69 = (int )reg;
4687#line 236
4688    __cil_tmp70 = __cil_tmp69 * 1UL;
4689#line 236
4690    __cil_tmp71 = 104 + __cil_tmp70;
4691#line 236
4692    __cil_tmp72 = (unsigned long )ci;
4693#line 236
4694    __cil_tmp73 = __cil_tmp72 + __cil_tmp71;
4695#line 236
4696    __cil_tmp74 = *((u8 *)__cil_tmp73);
4697#line 236
4698    __cil_tmp75 = (int )__cil_tmp74;
4699#line 236
4700    __cil_tmp76 = (u8 )__cil_tmp75;
4701#line 236
4702    status = i2c_write_reg(__cil_tmp61, __cil_tmp67, __cil_tmp68, __cil_tmp76);
4703    }
4704  } else {
4705
4706  }
4707  {
4708#line 238
4709  __cil_tmp77 = (unsigned int )reg;
4710#line 238
4711  if (__cil_tmp77 == 32U) {
4712#line 239
4713    __cil_tmp78 = (int )reg;
4714#line 239
4715    __cil_tmp79 = __cil_tmp78 * 1UL;
4716#line 239
4717    __cil_tmp80 = 104 + __cil_tmp79;
4718#line 239
4719    __cil_tmp81 = (unsigned long )ci;
4720#line 239
4721    __cil_tmp82 = __cil_tmp81 + __cil_tmp80;
4722#line 239
4723    __cil_tmp83 = (int )reg;
4724#line 239
4725    __cil_tmp84 = __cil_tmp83 * 1UL;
4726#line 239
4727    __cil_tmp85 = 104 + __cil_tmp84;
4728#line 239
4729    __cil_tmp86 = (unsigned long )ci;
4730#line 239
4731    __cil_tmp87 = __cil_tmp86 + __cil_tmp85;
4732#line 239
4733    __cil_tmp88 = *((u8 *)__cil_tmp87);
4734#line 239
4735    __cil_tmp89 = (unsigned int )__cil_tmp88;
4736#line 239
4737    __cil_tmp90 = __cil_tmp89 & 127U;
4738#line 239
4739    *((u8 *)__cil_tmp82) = (u8 )__cil_tmp90;
4740  } else {
4741
4742  }
4743  }
4744#line 240
4745  return (status);
4746}
4747}
4748#line 243 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
4749static int write_reg(struct cxd *ci , u8 reg , u8 val ) 
4750{ int tmp ;
4751  int __cil_tmp5 ;
4752  u8 __cil_tmp6 ;
4753  int __cil_tmp7 ;
4754  u8 __cil_tmp8 ;
4755  u8 __cil_tmp9 ;
4756
4757  {
4758  {
4759#line 245
4760  __cil_tmp5 = (int )reg;
4761#line 245
4762  __cil_tmp6 = (u8 )__cil_tmp5;
4763#line 245
4764  __cil_tmp7 = (int )val;
4765#line 245
4766  __cil_tmp8 = (u8 )__cil_tmp7;
4767#line 245
4768  __cil_tmp9 = (u8 )255;
4769#line 245
4770  tmp = write_regm(ci, __cil_tmp6, __cil_tmp8, __cil_tmp9);
4771  }
4772#line 245
4773  return (tmp);
4774}
4775}
4776#line 264 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
4777static void set_mode(struct cxd *ci , int mode ) 
4778{ unsigned long __cil_tmp3 ;
4779  unsigned long __cil_tmp4 ;
4780  int __cil_tmp5 ;
4781  u8 __cil_tmp6 ;
4782  u8 __cil_tmp7 ;
4783  u8 __cil_tmp8 ;
4784  u8 __cil_tmp9 ;
4785  u8 __cil_tmp10 ;
4786  u8 __cil_tmp11 ;
4787  unsigned long __cil_tmp12 ;
4788  unsigned long __cil_tmp13 ;
4789
4790  {
4791  {
4792#line 266
4793  __cil_tmp3 = (unsigned long )ci;
4794#line 266
4795  __cil_tmp4 = __cil_tmp3 + 144;
4796#line 266
4797  __cil_tmp5 = *((int *)__cil_tmp4);
4798#line 266
4799  if (__cil_tmp5 == mode) {
4800#line 267
4801    return;
4802  } else {
4803
4804  }
4805  }
4806#line 270
4807  if (mode == 0) {
4808#line 270
4809    goto case_0;
4810  } else
4811#line 273
4812  if (mode == 1) {
4813#line 273
4814    goto case_1;
4815  } else {
4816    {
4817#line 276
4818    goto switch_default;
4819#line 269
4820    if (0) {
4821      case_0: /* CIL Label */ 
4822      {
4823#line 271
4824      __cil_tmp6 = (u8 )6;
4825#line 271
4826      __cil_tmp7 = (u8 )0;
4827#line 271
4828      __cil_tmp8 = (u8 )7;
4829#line 271
4830      write_regm(ci, __cil_tmp6, __cil_tmp7, __cil_tmp8);
4831      }
4832#line 272
4833      goto ldv_22483;
4834      case_1: /* CIL Label */ 
4835      {
4836#line 274
4837      __cil_tmp9 = (u8 )6;
4838#line 274
4839      __cil_tmp10 = (u8 )2;
4840#line 274
4841      __cil_tmp11 = (u8 )7;
4842#line 274
4843      write_regm(ci, __cil_tmp9, __cil_tmp10, __cil_tmp11);
4844      }
4845#line 275
4846      goto ldv_22483;
4847      switch_default: /* CIL Label */ ;
4848#line 277
4849      goto ldv_22483;
4850    } else {
4851      switch_break: /* CIL Label */ ;
4852    }
4853    }
4854  }
4855  ldv_22483: 
4856#line 279
4857  __cil_tmp12 = (unsigned long )ci;
4858#line 279
4859  __cil_tmp13 = __cil_tmp12 + 144;
4860#line 279
4861  *((int *)__cil_tmp13) = mode;
4862#line 280
4863  return;
4864}
4865}
4866#line 282 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
4867static void cam_mode(struct cxd *ci , int mode ) 
4868{ unsigned long __cil_tmp3 ;
4869  unsigned long __cil_tmp4 ;
4870  int __cil_tmp5 ;
4871  u8 __cil_tmp6 ;
4872  u8 __cil_tmp7 ;
4873  u8 __cil_tmp8 ;
4874  unsigned long __cil_tmp9 ;
4875  unsigned long __cil_tmp10 ;
4876
4877  {
4878  {
4879#line 284
4880  __cil_tmp3 = (unsigned long )ci;
4881#line 284
4882  __cil_tmp4 = __cil_tmp3 + 1188;
4883#line 284
4884  __cil_tmp5 = *((int *)__cil_tmp4);
4885#line 284
4886  if (__cil_tmp5 == mode) {
4887#line 285
4888    return;
4889  } else {
4890
4891  }
4892  }
4893#line 288
4894  if (mode == 0) {
4895#line 288
4896    goto case_0;
4897  } else
4898#line 291
4899  if (mode == 1) {
4900#line 291
4901    goto case_1;
4902  } else {
4903    {
4904#line 303
4905    goto switch_default;
4906#line 287
4907    if (0) {
4908      case_0: /* CIL Label */ 
4909      {
4910#line 289
4911      __cil_tmp6 = (u8 )32;
4912#line 289
4913      __cil_tmp7 = (u8 )128;
4914#line 289
4915      __cil_tmp8 = (u8 )128;
4916#line 289
4917      write_regm(ci, __cil_tmp6, __cil_tmp7, __cil_tmp8);
4918      }
4919#line 290
4920      goto ldv_22491;
4921      case_1: /* CIL Label */ ;
4922#line 302
4923      goto ldv_22491;
4924      switch_default: /* CIL Label */ ;
4925#line 304
4926      goto ldv_22491;
4927    } else {
4928      switch_break: /* CIL Label */ ;
4929    }
4930    }
4931  }
4932  ldv_22491: 
4933#line 306
4934  __cil_tmp9 = (unsigned long )ci;
4935#line 306
4936  __cil_tmp10 = __cil_tmp9 + 1188;
4937#line 306
4938  *((int *)__cil_tmp10) = mode;
4939#line 307
4940  return;
4941}
4942}
4943#line 311 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
4944static int init(struct cxd *ci ) 
4945{ int status ;
4946  unsigned long __cil_tmp3 ;
4947  unsigned long __cil_tmp4 ;
4948  struct mutex *__cil_tmp5 ;
4949  unsigned long __cil_tmp6 ;
4950  unsigned long __cil_tmp7 ;
4951  u8 __cil_tmp8 ;
4952  u8 __cil_tmp9 ;
4953  u8 __cil_tmp10 ;
4954  u8 __cil_tmp11 ;
4955  u8 __cil_tmp12 ;
4956  u8 __cil_tmp13 ;
4957  u8 __cil_tmp14 ;
4958  u8 __cil_tmp15 ;
4959  u8 __cil_tmp16 ;
4960  u8 __cil_tmp17 ;
4961  u8 __cil_tmp18 ;
4962  u8 __cil_tmp19 ;
4963  u8 __cil_tmp20 ;
4964  u8 __cil_tmp21 ;
4965  u8 __cil_tmp22 ;
4966  u8 __cil_tmp23 ;
4967  u8 __cil_tmp24 ;
4968  u8 __cil_tmp25 ;
4969  u8 __cil_tmp26 ;
4970  u8 __cil_tmp27 ;
4971  u8 __cil_tmp28 ;
4972  u8 __cil_tmp29 ;
4973  u8 __cil_tmp30 ;
4974  u8 __cil_tmp31 ;
4975  u8 __cil_tmp32 ;
4976  u8 __cil_tmp33 ;
4977  u8 __cil_tmp34 ;
4978  u8 __cil_tmp35 ;
4979  unsigned long __cil_tmp36 ;
4980  unsigned long __cil_tmp37 ;
4981  u8 __cil_tmp38 ;
4982  int __cil_tmp39 ;
4983  u8 __cil_tmp40 ;
4984  u8 __cil_tmp41 ;
4985  u8 __cil_tmp42 ;
4986  u8 __cil_tmp43 ;
4987  u8 __cil_tmp44 ;
4988  unsigned long __cil_tmp45 ;
4989  unsigned long __cil_tmp46 ;
4990  u8 __cil_tmp47 ;
4991  int __cil_tmp48 ;
4992  u8 __cil_tmp49 ;
4993  unsigned char *__cil_tmp50 ;
4994  unsigned char *__cil_tmp51 ;
4995  unsigned char __cil_tmp52 ;
4996  unsigned int __cil_tmp53 ;
4997  unsigned char *__cil_tmp54 ;
4998  unsigned char *__cil_tmp55 ;
4999  unsigned char __cil_tmp56 ;
5000  unsigned int __cil_tmp57 ;
5001  u8 __cil_tmp58 ;
5002  u8 __cil_tmp59 ;
5003  u8 __cil_tmp60 ;
5004  u8 __cil_tmp61 ;
5005  u8 __cil_tmp62 ;
5006  u8 __cil_tmp63 ;
5007  u8 __cil_tmp64 ;
5008  u8 __cil_tmp65 ;
5009  u8 __cil_tmp66 ;
5010  u8 __cil_tmp67 ;
5011  unsigned char *__cil_tmp68 ;
5012  unsigned char *__cil_tmp69 ;
5013  unsigned char __cil_tmp70 ;
5014  unsigned int __cil_tmp71 ;
5015  u8 __cil_tmp72 ;
5016  u8 __cil_tmp73 ;
5017  u8 __cil_tmp74 ;
5018  u8 __cil_tmp75 ;
5019  u8 __cil_tmp76 ;
5020  u8 __cil_tmp77 ;
5021  u8 __cil_tmp78 ;
5022  u8 __cil_tmp79 ;
5023  u8 __cil_tmp80 ;
5024  u8 __cil_tmp81 ;
5025  u8 __cil_tmp82 ;
5026  u8 __cil_tmp83 ;
5027  u8 __cil_tmp84 ;
5028  u8 __cil_tmp85 ;
5029  u8 __cil_tmp86 ;
5030  u8 __cil_tmp87 ;
5031  u8 __cil_tmp88 ;
5032  u8 __cil_tmp89 ;
5033  u8 __cil_tmp90 ;
5034  u8 __cil_tmp91 ;
5035  u8 __cil_tmp92 ;
5036  u8 __cil_tmp93 ;
5037  u8 __cil_tmp94 ;
5038  unsigned long __cil_tmp95 ;
5039  unsigned long __cil_tmp96 ;
5040  unsigned long __cil_tmp97 ;
5041  unsigned long __cil_tmp98 ;
5042  struct mutex *__cil_tmp99 ;
5043
5044  {
5045  {
5046#line 315
5047  __cil_tmp3 = (unsigned long )ci;
5048#line 315
5049  __cil_tmp4 = __cil_tmp3 + 1192;
5050#line 315
5051  __cil_tmp5 = (struct mutex *)__cil_tmp4;
5052#line 315
5053  mutex_lock_nested(__cil_tmp5, 0U);
5054#line 316
5055  __cil_tmp6 = (unsigned long )ci;
5056#line 316
5057  __cil_tmp7 = __cil_tmp6 + 144;
5058#line 316
5059  *((int *)__cil_tmp7) = -1;
5060#line 318
5061  __cil_tmp8 = (u8 )0;
5062#line 318
5063  __cil_tmp9 = (u8 )0;
5064#line 318
5065  status = write_reg(ci, __cil_tmp8, __cil_tmp9);
5066  }
5067#line 319
5068  if (status < 0) {
5069#line 320
5070    goto ldv_22498;
5071  } else {
5072
5073  }
5074  {
5075#line 321
5076  __cil_tmp10 = (u8 )1;
5077#line 321
5078  __cil_tmp11 = (u8 )0;
5079#line 321
5080  status = write_reg(ci, __cil_tmp10, __cil_tmp11);
5081  }
5082#line 322
5083  if (status < 0) {
5084#line 323
5085    goto ldv_22498;
5086  } else {
5087
5088  }
5089  {
5090#line 324
5091  __cil_tmp12 = (u8 )2;
5092#line 324
5093  __cil_tmp13 = (u8 )16;
5094#line 324
5095  status = write_reg(ci, __cil_tmp12, __cil_tmp13);
5096  }
5097#line 325
5098  if (status < 0) {
5099#line 326
5100    goto ldv_22498;
5101  } else {
5102
5103  }
5104  {
5105#line 327
5106  __cil_tmp14 = (u8 )3;
5107#line 327
5108  __cil_tmp15 = (u8 )0;
5109#line 327
5110  status = write_reg(ci, __cil_tmp14, __cil_tmp15);
5111  }
5112#line 328
5113  if (status < 0) {
5114#line 329
5115    goto ldv_22498;
5116  } else {
5117
5118  }
5119  {
5120#line 330
5121  __cil_tmp16 = (u8 )5;
5122#line 330
5123  __cil_tmp17 = (u8 )255;
5124#line 330
5125  status = write_reg(ci, __cil_tmp16, __cil_tmp17);
5126  }
5127#line 331
5128  if (status < 0) {
5129#line 332
5130    goto ldv_22498;
5131  } else {
5132
5133  }
5134  {
5135#line 333
5136  __cil_tmp18 = (u8 )6;
5137#line 333
5138  __cil_tmp19 = (u8 )31;
5139#line 333
5140  status = write_reg(ci, __cil_tmp18, __cil_tmp19);
5141  }
5142#line 334
5143  if (status < 0) {
5144#line 335
5145    goto ldv_22498;
5146  } else {
5147
5148  }
5149  {
5150#line 336
5151  __cil_tmp20 = (u8 )7;
5152#line 336
5153  __cil_tmp21 = (u8 )31;
5154#line 336
5155  status = write_reg(ci, __cil_tmp20, __cil_tmp21);
5156  }
5157#line 337
5158  if (status < 0) {
5159#line 338
5160    goto ldv_22498;
5161  } else {
5162
5163  }
5164  {
5165#line 339
5166  __cil_tmp22 = (u8 )8;
5167#line 339
5168  __cil_tmp23 = (u8 )40;
5169#line 339
5170  status = write_reg(ci, __cil_tmp22, __cil_tmp23);
5171  }
5172#line 340
5173  if (status < 0) {
5174#line 341
5175    goto ldv_22498;
5176  } else {
5177
5178  }
5179  {
5180#line 342
5181  __cil_tmp24 = (u8 )20;
5182#line 342
5183  __cil_tmp25 = (u8 )32;
5184#line 342
5185  status = write_reg(ci, __cil_tmp24, __cil_tmp25);
5186  }
5187#line 343
5188  if (status < 0) {
5189#line 344
5190    goto ldv_22498;
5191  } else {
5192
5193  }
5194  {
5195#line 351
5196  __cil_tmp26 = (u8 )10;
5197#line 351
5198  __cil_tmp27 = (u8 )167;
5199#line 351
5200  status = write_reg(ci, __cil_tmp26, __cil_tmp27);
5201  }
5202#line 352
5203  if (status < 0) {
5204#line 353
5205    goto ldv_22498;
5206  } else {
5207
5208  }
5209  {
5210#line 355
5211  __cil_tmp28 = (u8 )11;
5212#line 355
5213  __cil_tmp29 = (u8 )51;
5214#line 355
5215  status = write_reg(ci, __cil_tmp28, __cil_tmp29);
5216  }
5217#line 356
5218  if (status < 0) {
5219#line 357
5220    goto ldv_22498;
5221  } else {
5222
5223  }
5224  {
5225#line 358
5226  __cil_tmp30 = (u8 )12;
5227#line 358
5228  __cil_tmp31 = (u8 )51;
5229#line 358
5230  status = write_reg(ci, __cil_tmp30, __cil_tmp31);
5231  }
5232#line 359
5233  if (status < 0) {
5234#line 360
5235    goto ldv_22498;
5236  } else {
5237
5238  }
5239  {
5240#line 362
5241  __cil_tmp32 = (u8 )20;
5242#line 362
5243  __cil_tmp33 = (u8 )0;
5244#line 362
5245  __cil_tmp34 = (u8 )15;
5246#line 362
5247  status = write_regm(ci, __cil_tmp32, __cil_tmp33, __cil_tmp34);
5248  }
5249#line 363
5250  if (status < 0) {
5251#line 364
5252    goto ldv_22498;
5253  } else {
5254
5255  }
5256  {
5257#line 365
5258  __cil_tmp35 = (u8 )21;
5259#line 365
5260  __cil_tmp36 = (unsigned long )ci;
5261#line 365
5262  __cil_tmp37 = __cil_tmp36 + 141;
5263#line 365
5264  __cil_tmp38 = *((u8 *)__cil_tmp37);
5265#line 365
5266  __cil_tmp39 = (int )__cil_tmp38;
5267#line 365
5268  __cil_tmp40 = (u8 )__cil_tmp39;
5269#line 365
5270  status = write_reg(ci, __cil_tmp35, __cil_tmp40);
5271  }
5272#line 366
5273  if (status < 0) {
5274#line 367
5275    goto ldv_22498;
5276  } else {
5277
5278  }
5279  {
5280#line 368
5281  __cil_tmp41 = (u8 )22;
5282#line 368
5283  __cil_tmp42 = (u8 )0;
5284#line 368
5285  __cil_tmp43 = (u8 )15;
5286#line 368
5287  status = write_regm(ci, __cil_tmp41, __cil_tmp42, __cil_tmp43);
5288  }
5289#line 369
5290  if (status < 0) {
5291#line 370
5292    goto ldv_22498;
5293  } else {
5294
5295  }
5296  {
5297#line 371
5298  __cil_tmp44 = (u8 )23;
5299#line 371
5300  __cil_tmp45 = (unsigned long )ci;
5301#line 371
5302  __cil_tmp46 = __cil_tmp45 + 140;
5303#line 371
5304  __cil_tmp47 = *((u8 *)__cil_tmp46);
5305#line 371
5306  __cil_tmp48 = (int )__cil_tmp47;
5307#line 371
5308  __cil_tmp49 = (u8 )__cil_tmp48;
5309#line 371
5310  status = write_reg(ci, __cil_tmp44, __cil_tmp49);
5311  }
5312#line 372
5313  if (status < 0) {
5314#line 373
5315    goto ldv_22498;
5316  } else {
5317
5318  }
5319  {
5320#line 375
5321  __cil_tmp50 = (unsigned char *)ci;
5322#line 375
5323  __cil_tmp51 = __cil_tmp50 + 101UL;
5324#line 375
5325  __cil_tmp52 = *__cil_tmp51;
5326#line 375
5327  __cil_tmp53 = (unsigned int )__cil_tmp52;
5328#line 375
5329  if (__cil_tmp53 != 0U) {
5330    {
5331#line 376
5332    __cil_tmp54 = (unsigned char *)ci;
5333#line 376
5334    __cil_tmp55 = __cil_tmp54 + 101UL;
5335#line 376
5336    __cil_tmp56 = *__cil_tmp55;
5337#line 376
5338    __cil_tmp57 = (unsigned int )__cil_tmp56;
5339#line 376
5340    if (__cil_tmp57 != 0U) {
5341      {
5342#line 377
5343      __cil_tmp58 = (u8 )9;
5344#line 377
5345      __cil_tmp59 = (u8 )111;
5346#line 377
5347      status = write_reg(ci, __cil_tmp58, __cil_tmp59);
5348      }
5349#line 378
5350      if (status < 0) {
5351#line 379
5352        goto ldv_22498;
5353      } else {
5354
5355      }
5356    } else {
5357      {
5358#line 381
5359      __cil_tmp60 = (u8 )9;
5360#line 381
5361      __cil_tmp61 = (u8 )109;
5362#line 381
5363      status = write_reg(ci, __cil_tmp60, __cil_tmp61);
5364      }
5365#line 382
5366      if (status < 0) {
5367#line 383
5368        goto ldv_22498;
5369      } else {
5370
5371      }
5372    }
5373    }
5374    {
5375#line 385
5376    __cil_tmp62 = (u8 )32;
5377#line 385
5378    __cil_tmp63 = (u8 )104;
5379#line 385
5380    status = write_reg(ci, __cil_tmp62, __cil_tmp63);
5381    }
5382#line 386
5383    if (status < 0) {
5384#line 387
5385      goto ldv_22498;
5386    } else {
5387
5388    }
5389    {
5390#line 388
5391    __cil_tmp64 = (u8 )33;
5392#line 388
5393    __cil_tmp65 = (u8 )0;
5394#line 388
5395    status = write_reg(ci, __cil_tmp64, __cil_tmp65);
5396    }
5397#line 389
5398    if (status < 0) {
5399#line 390
5400      goto ldv_22498;
5401    } else {
5402
5403    }
5404    {
5405#line 391
5406    __cil_tmp66 = (u8 )34;
5407#line 391
5408    __cil_tmp67 = (u8 )2;
5409#line 391
5410    status = write_reg(ci, __cil_tmp66, __cil_tmp67);
5411    }
5412#line 392
5413    if (status < 0) {
5414#line 393
5415      goto ldv_22498;
5416    } else {
5417
5418    }
5419  } else {
5420    {
5421#line 395
5422    __cil_tmp68 = (unsigned char *)ci;
5423#line 395
5424    __cil_tmp69 = __cil_tmp68 + 101UL;
5425#line 395
5426    __cil_tmp70 = *__cil_tmp69;
5427#line 395
5428    __cil_tmp71 = (unsigned int )__cil_tmp70;
5429#line 395
5430    if (__cil_tmp71 != 0U) {
5431      {
5432#line 396
5433      __cil_tmp72 = (u8 )9;
5434#line 396
5435      __cil_tmp73 = (u8 )79;
5436#line 396
5437      status = write_reg(ci, __cil_tmp72, __cil_tmp73);
5438      }
5439#line 397
5440      if (status < 0) {
5441#line 398
5442        goto ldv_22498;
5443      } else {
5444
5445      }
5446    } else {
5447      {
5448#line 400
5449      __cil_tmp74 = (u8 )9;
5450#line 400
5451      __cil_tmp75 = (u8 )77;
5452#line 400
5453      status = write_reg(ci, __cil_tmp74, __cil_tmp75);
5454      }
5455#line 401
5456      if (status < 0) {
5457#line 402
5458        goto ldv_22498;
5459      } else {
5460
5461      }
5462    }
5463    }
5464    {
5465#line 405
5466    __cil_tmp76 = (u8 )32;
5467#line 405
5468    __cil_tmp77 = (u8 )40;
5469#line 405
5470    status = write_reg(ci, __cil_tmp76, __cil_tmp77);
5471    }
5472#line 406
5473    if (status < 0) {
5474#line 407
5475      goto ldv_22498;
5476    } else {
5477
5478    }
5479    {
5480#line 408
5481    __cil_tmp78 = (u8 )33;
5482#line 408
5483    __cil_tmp79 = (u8 )0;
5484#line 408
5485    status = write_reg(ci, __cil_tmp78, __cil_tmp79);
5486    }
5487#line 409
5488    if (status < 0) {
5489#line 410
5490      goto ldv_22498;
5491    } else {
5492
5493    }
5494    {
5495#line 411
5496    __cil_tmp80 = (u8 )34;
5497#line 411
5498    __cil_tmp81 = (u8 )7;
5499#line 411
5500    status = write_reg(ci, __cil_tmp80, __cil_tmp81);
5501    }
5502#line 412
5503    if (status < 0) {
5504#line 413
5505      goto ldv_22498;
5506    } else {
5507
5508    }
5509  }
5510  }
5511  {
5512#line 416
5513  __cil_tmp82 = (u8 )32;
5514#line 416
5515  __cil_tmp83 = (u8 )128;
5516#line 416
5517  __cil_tmp84 = (u8 )128;
5518#line 416
5519  status = write_regm(ci, __cil_tmp82, __cil_tmp83, __cil_tmp84);
5520  }
5521#line 417
5522  if (status < 0) {
5523#line 418
5524    goto ldv_22498;
5525  } else {
5526
5527  }
5528  {
5529#line 419
5530  __cil_tmp85 = (u8 )3;
5531#line 419
5532  __cil_tmp86 = (u8 )2;
5533#line 419
5534  __cil_tmp87 = (u8 )2;
5535#line 419
5536  status = write_regm(ci, __cil_tmp85, __cil_tmp86, __cil_tmp87);
5537  }
5538#line 420
5539  if (status < 0) {
5540#line 421
5541    goto ldv_22498;
5542  } else {
5543
5544  }
5545  {
5546#line 422
5547  __cil_tmp88 = (u8 )1;
5548#line 422
5549  __cil_tmp89 = (u8 )4;
5550#line 422
5551  status = write_reg(ci, __cil_tmp88, __cil_tmp89);
5552  }
5553#line 423
5554  if (status < 0) {
5555#line 424
5556    goto ldv_22498;
5557  } else {
5558
5559  }
5560  {
5561#line 425
5562  __cil_tmp90 = (u8 )0;
5563#line 425
5564  __cil_tmp91 = (u8 )49;
5565#line 425
5566  status = write_reg(ci, __cil_tmp90, __cil_tmp91);
5567  }
5568#line 426
5569  if (status < 0) {
5570#line 427
5571    goto ldv_22498;
5572  } else {
5573
5574  }
5575  {
5576#line 430
5577  __cil_tmp92 = (u8 )9;
5578#line 430
5579  __cil_tmp93 = (u8 )8;
5580#line 430
5581  __cil_tmp94 = (u8 )8;
5582#line 430
5583  status = write_regm(ci, __cil_tmp92, __cil_tmp93, __cil_tmp94);
5584  }
5585#line 431
5586  if (status < 0) {
5587#line 432
5588    goto ldv_22498;
5589  } else {
5590
5591  }
5592  {
5593#line 433
5594  __cil_tmp95 = (unsigned long )ci;
5595#line 433
5596  __cil_tmp96 = __cil_tmp95 + 1188;
5597#line 433
5598  *((int *)__cil_tmp96) = -1;
5599#line 434
5600  cam_mode(ci, 0);
5601  }
5602  ldv_22498: 
5603  {
5604#line 436
5605  __cil_tmp97 = (unsigned long )ci;
5606#line 436
5607  __cil_tmp98 = __cil_tmp97 + 1192;
5608#line 436
5609  __cil_tmp99 = (struct mutex *)__cil_tmp98;
5610#line 436
5611  mutex_unlock(__cil_tmp99);
5612  }
5613#line 438
5614  return (0);
5615}
5616}
5617#line 441 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
5618static int read_attribute_mem(struct dvb_ca_en50221 *ca , int slot , int address ) 
5619{ struct cxd *ci ;
5620  u8 val ;
5621  unsigned long __cil_tmp6 ;
5622  unsigned long __cil_tmp7 ;
5623  void *__cil_tmp8 ;
5624  unsigned long __cil_tmp9 ;
5625  unsigned long __cil_tmp10 ;
5626  struct mutex *__cil_tmp11 ;
5627  u16 __cil_tmp12 ;
5628  int __cil_tmp13 ;
5629  u16 __cil_tmp14 ;
5630  u8 __cil_tmp15 ;
5631  unsigned long __cil_tmp16 ;
5632  unsigned long __cil_tmp17 ;
5633  struct mutex *__cil_tmp18 ;
5634  u8 *__cil_tmp19 ;
5635  u8 __cil_tmp20 ;
5636
5637  {
5638  {
5639#line 444
5640  __cil_tmp6 = (unsigned long )ca;
5641#line 444
5642  __cil_tmp7 = __cil_tmp6 + 72;
5643#line 444
5644  __cil_tmp8 = *((void **)__cil_tmp7);
5645#line 444
5646  ci = (struct cxd *)__cil_tmp8;
5647#line 463
5648  __cil_tmp9 = (unsigned long )ci;
5649#line 463
5650  __cil_tmp10 = __cil_tmp9 + 1192;
5651#line 463
5652  __cil_tmp11 = (struct mutex *)__cil_tmp10;
5653#line 463
5654  mutex_lock_nested(__cil_tmp11, 0U);
5655#line 464
5656  set_mode(ci, 1);
5657#line 465
5658  __cil_tmp12 = (u16 )address;
5659#line 465
5660  __cil_tmp13 = (int )__cil_tmp12;
5661#line 465
5662  __cil_tmp14 = (u16 )__cil_tmp13;
5663#line 465
5664  __cil_tmp15 = (u8 )1;
5665#line 465
5666  read_pccard(ci, __cil_tmp14, & val, __cil_tmp15);
5667#line 466
5668  __cil_tmp16 = (unsigned long )ci;
5669#line 466
5670  __cil_tmp17 = __cil_tmp16 + 1192;
5671#line 466
5672  __cil_tmp18 = (struct mutex *)__cil_tmp17;
5673#line 466
5674  mutex_unlock(__cil_tmp18);
5675  }
5676  {
5677#line 468
5678  __cil_tmp19 = & val;
5679#line 468
5680  __cil_tmp20 = *__cil_tmp19;
5681#line 468
5682  return ((int )__cil_tmp20);
5683  }
5684}
5685}
5686#line 472 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
5687static int write_attribute_mem(struct dvb_ca_en50221 *ca , int slot , int address ,
5688                               u8 value ) 
5689{ struct cxd *ci ;
5690  unsigned long __cil_tmp6 ;
5691  unsigned long __cil_tmp7 ;
5692  void *__cil_tmp8 ;
5693  unsigned long __cil_tmp9 ;
5694  unsigned long __cil_tmp10 ;
5695  struct mutex *__cil_tmp11 ;
5696  u16 __cil_tmp12 ;
5697  int __cil_tmp13 ;
5698  u16 __cil_tmp14 ;
5699  u8 __cil_tmp15 ;
5700  unsigned long __cil_tmp16 ;
5701  unsigned long __cil_tmp17 ;
5702  struct mutex *__cil_tmp18 ;
5703
5704  {
5705  {
5706#line 475
5707  __cil_tmp6 = (unsigned long )ca;
5708#line 475
5709  __cil_tmp7 = __cil_tmp6 + 72;
5710#line 475
5711  __cil_tmp8 = *((void **)__cil_tmp7);
5712#line 475
5713  ci = (struct cxd *)__cil_tmp8;
5714#line 477
5715  __cil_tmp9 = (unsigned long )ci;
5716#line 477
5717  __cil_tmp10 = __cil_tmp9 + 1192;
5718#line 477
5719  __cil_tmp11 = (struct mutex *)__cil_tmp10;
5720#line 477
5721  mutex_lock_nested(__cil_tmp11, 0U);
5722#line 478
5723  set_mode(ci, 1);
5724#line 479
5725  __cil_tmp12 = (u16 )address;
5726#line 479
5727  __cil_tmp13 = (int )__cil_tmp12;
5728#line 479
5729  __cil_tmp14 = (u16 )__cil_tmp13;
5730#line 479
5731  __cil_tmp15 = (u8 )1;
5732#line 479
5733  write_pccard(ci, __cil_tmp14, & value, __cil_tmp15);
5734#line 480
5735  __cil_tmp16 = (unsigned long )ci;
5736#line 480
5737  __cil_tmp17 = __cil_tmp16 + 1192;
5738#line 480
5739  __cil_tmp18 = (struct mutex *)__cil_tmp17;
5740#line 480
5741  mutex_unlock(__cil_tmp18);
5742  }
5743#line 481
5744  return (0);
5745}
5746}
5747#line 484 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
5748static int read_cam_control(struct dvb_ca_en50221 *ca , int slot , u8 address ) 
5749{ struct cxd *ci ;
5750  u8 val ;
5751  unsigned long __cil_tmp6 ;
5752  unsigned long __cil_tmp7 ;
5753  void *__cil_tmp8 ;
5754  unsigned long __cil_tmp9 ;
5755  unsigned long __cil_tmp10 ;
5756  struct mutex *__cil_tmp11 ;
5757  int __cil_tmp12 ;
5758  u16 __cil_tmp13 ;
5759  unsigned long __cil_tmp14 ;
5760  unsigned long __cil_tmp15 ;
5761  struct mutex *__cil_tmp16 ;
5762  u8 *__cil_tmp17 ;
5763  u8 __cil_tmp18 ;
5764
5765  {
5766  {
5767#line 487
5768  __cil_tmp6 = (unsigned long )ca;
5769#line 487
5770  __cil_tmp7 = __cil_tmp6 + 72;
5771#line 487
5772  __cil_tmp8 = *((void **)__cil_tmp7);
5773#line 487
5774  ci = (struct cxd *)__cil_tmp8;
5775#line 490
5776  __cil_tmp9 = (unsigned long )ci;
5777#line 490
5778  __cil_tmp10 = __cil_tmp9 + 1192;
5779#line 490
5780  __cil_tmp11 = (struct mutex *)__cil_tmp10;
5781#line 490
5782  mutex_lock_nested(__cil_tmp11, 0U);
5783#line 491
5784  set_mode(ci, 0);
5785#line 492
5786  __cil_tmp12 = (int )address;
5787#line 492
5788  __cil_tmp13 = (u16 )__cil_tmp12;
5789#line 492
5790  read_io(ci, __cil_tmp13, & val);
5791#line 493
5792  __cil_tmp14 = (unsigned long )ci;
5793#line 493
5794  __cil_tmp15 = __cil_tmp14 + 1192;
5795#line 493
5796  __cil_tmp16 = (struct mutex *)__cil_tmp15;
5797#line 493
5798  mutex_unlock(__cil_tmp16);
5799  }
5800  {
5801#line 494
5802  __cil_tmp17 = & val;
5803#line 494
5804  __cil_tmp18 = *__cil_tmp17;
5805#line 494
5806  return ((int )__cil_tmp18);
5807  }
5808}
5809}
5810#line 497 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
5811static int write_cam_control(struct dvb_ca_en50221 *ca , int slot , u8 address , u8 value ) 
5812{ struct cxd *ci ;
5813  unsigned long __cil_tmp6 ;
5814  unsigned long __cil_tmp7 ;
5815  void *__cil_tmp8 ;
5816  unsigned long __cil_tmp9 ;
5817  unsigned long __cil_tmp10 ;
5818  struct mutex *__cil_tmp11 ;
5819  int __cil_tmp12 ;
5820  u16 __cil_tmp13 ;
5821  int __cil_tmp14 ;
5822  u8 __cil_tmp15 ;
5823  unsigned long __cil_tmp16 ;
5824  unsigned long __cil_tmp17 ;
5825  struct mutex *__cil_tmp18 ;
5826
5827  {
5828  {
5829#line 500
5830  __cil_tmp6 = (unsigned long )ca;
5831#line 500
5832  __cil_tmp7 = __cil_tmp6 + 72;
5833#line 500
5834  __cil_tmp8 = *((void **)__cil_tmp7);
5835#line 500
5836  ci = (struct cxd *)__cil_tmp8;
5837#line 502
5838  __cil_tmp9 = (unsigned long )ci;
5839#line 502
5840  __cil_tmp10 = __cil_tmp9 + 1192;
5841#line 502
5842  __cil_tmp11 = (struct mutex *)__cil_tmp10;
5843#line 502
5844  mutex_lock_nested(__cil_tmp11, 0U);
5845#line 503
5846  set_mode(ci, 0);
5847#line 504
5848  __cil_tmp12 = (int )address;
5849#line 504
5850  __cil_tmp13 = (u16 )__cil_tmp12;
5851#line 504
5852  __cil_tmp14 = (int )value;
5853#line 504
5854  __cil_tmp15 = (u8 )__cil_tmp14;
5855#line 504
5856  write_io(ci, __cil_tmp13, __cil_tmp15);
5857#line 505
5858  __cil_tmp16 = (unsigned long )ci;
5859#line 505
5860  __cil_tmp17 = __cil_tmp16 + 1192;
5861#line 505
5862  __cil_tmp18 = (struct mutex *)__cil_tmp17;
5863#line 505
5864  mutex_unlock(__cil_tmp18);
5865  }
5866#line 506
5867  return (0);
5868}
5869}
5870#line 509 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
5871static int slot_reset(struct dvb_ca_en50221 *ca , int slot ) 
5872{ struct cxd *ci ;
5873  int i ;
5874  unsigned long __cil_tmp5 ;
5875  unsigned long __cil_tmp6 ;
5876  void *__cil_tmp7 ;
5877  unsigned long __cil_tmp8 ;
5878  unsigned long __cil_tmp9 ;
5879  struct mutex *__cil_tmp10 ;
5880  u8 __cil_tmp11 ;
5881  u8 __cil_tmp12 ;
5882  u8 __cil_tmp13 ;
5883  u8 __cil_tmp14 ;
5884  u8 __cil_tmp15 ;
5885  u8 __cil_tmp16 ;
5886  u8 __cil_tmp17 ;
5887  u8 __cil_tmp18 ;
5888  u8 __cil_tmp19 ;
5889  u8 __cil_tmp20 ;
5890  u8 __cil_tmp21 ;
5891  unsigned long __cil_tmp22 ;
5892  unsigned long __cil_tmp23 ;
5893  unsigned long __cil_tmp24 ;
5894  unsigned long __cil_tmp25 ;
5895  unsigned long __cil_tmp26 ;
5896  unsigned long __cil_tmp27 ;
5897  int __cil_tmp28 ;
5898  unsigned long __cil_tmp29 ;
5899  unsigned long __cil_tmp30 ;
5900  struct mutex *__cil_tmp31 ;
5901
5902  {
5903  {
5904#line 511
5905  __cil_tmp5 = (unsigned long )ca;
5906#line 511
5907  __cil_tmp6 = __cil_tmp5 + 72;
5908#line 511
5909  __cil_tmp7 = *((void **)__cil_tmp6);
5910#line 511
5911  ci = (struct cxd *)__cil_tmp7;
5912#line 513
5913  __cil_tmp8 = (unsigned long )ci;
5914#line 513
5915  __cil_tmp9 = __cil_tmp8 + 1192;
5916#line 513
5917  __cil_tmp10 = (struct mutex *)__cil_tmp9;
5918#line 513
5919  mutex_lock_nested(__cil_tmp10, 0U);
5920#line 523
5921  cam_mode(ci, 0);
5922#line 524
5923  __cil_tmp11 = (u8 )0;
5924#line 524
5925  __cil_tmp12 = (u8 )33;
5926#line 524
5927  write_reg(ci, __cil_tmp11, __cil_tmp12);
5928#line 525
5929  __cil_tmp13 = (u8 )6;
5930#line 525
5931  __cil_tmp14 = (u8 )31;
5932#line 525
5933  write_reg(ci, __cil_tmp13, __cil_tmp14);
5934#line 526
5935  __cil_tmp15 = (u8 )0;
5936#line 526
5937  __cil_tmp16 = (u8 )49;
5938#line 526
5939  write_reg(ci, __cil_tmp15, __cil_tmp16);
5940#line 527
5941  __cil_tmp17 = (u8 )32;
5942#line 527
5943  __cil_tmp18 = (u8 )128;
5944#line 527
5945  __cil_tmp19 = (u8 )128;
5946#line 527
5947  write_regm(ci, __cil_tmp17, __cil_tmp18, __cil_tmp19);
5948#line 528
5949  __cil_tmp20 = (u8 )3;
5950#line 528
5951  __cil_tmp21 = (u8 )2;
5952#line 528
5953  write_reg(ci, __cil_tmp20, __cil_tmp21);
5954#line 529
5955  __cil_tmp22 = (unsigned long )ci;
5956#line 529
5957  __cil_tmp23 = __cil_tmp22 + 148;
5958#line 529
5959  *((int *)__cil_tmp23) = 0;
5960#line 532
5961  __cil_tmp24 = (unsigned long )ci;
5962#line 532
5963  __cil_tmp25 = __cil_tmp24 + 144;
5964#line 532
5965  *((int *)__cil_tmp25) = -1;
5966#line 538
5967  i = 0;
5968  }
5969#line 538
5970  goto ldv_22535;
5971  ldv_22534: 
5972  {
5973#line 539
5974  msleep(10U);
5975  }
5976  {
5977#line 546
5978  __cil_tmp26 = (unsigned long )ci;
5979#line 546
5980  __cil_tmp27 = __cil_tmp26 + 148;
5981#line 546
5982  __cil_tmp28 = *((int *)__cil_tmp27);
5983#line 546
5984  if (__cil_tmp28 != 0) {
5985#line 547
5986    goto ldv_22533;
5987  } else {
5988
5989  }
5990  }
5991#line 538
5992  i = i + 1;
5993  ldv_22535: ;
5994#line 538
5995  if (i <= 99) {
5996#line 539
5997    goto ldv_22534;
5998  } else {
5999#line 541
6000    goto ldv_22533;
6001  }
6002  ldv_22533: 
6003  {
6004#line 551
6005  __cil_tmp29 = (unsigned long )ci;
6006#line 551
6007  __cil_tmp30 = __cil_tmp29 + 1192;
6008#line 551
6009  __cil_tmp31 = (struct mutex *)__cil_tmp30;
6010#line 551
6011  mutex_unlock(__cil_tmp31);
6012  }
6013#line 553
6014  return (0);
6015}
6016}
6017#line 556 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
6018static int slot_shutdown(struct dvb_ca_en50221 *ca , int slot ) 
6019{ struct cxd *ci ;
6020  unsigned long __cil_tmp4 ;
6021  unsigned long __cil_tmp5 ;
6022  void *__cil_tmp6 ;
6023  unsigned long __cil_tmp7 ;
6024  unsigned long __cil_tmp8 ;
6025  struct mutex *__cil_tmp9 ;
6026  u8 __cil_tmp10 ;
6027  u8 __cil_tmp11 ;
6028  u8 __cil_tmp12 ;
6029  u8 __cil_tmp13 ;
6030  u8 __cil_tmp14 ;
6031  u8 __cil_tmp15 ;
6032  u8 __cil_tmp16 ;
6033  u8 __cil_tmp17 ;
6034  u8 __cil_tmp18 ;
6035  unsigned long __cil_tmp19 ;
6036  unsigned long __cil_tmp20 ;
6037  unsigned long __cil_tmp21 ;
6038  unsigned long __cil_tmp22 ;
6039  struct mutex *__cil_tmp23 ;
6040
6041  {
6042  {
6043#line 558
6044  __cil_tmp4 = (unsigned long )ca;
6045#line 558
6046  __cil_tmp5 = __cil_tmp4 + 72;
6047#line 558
6048  __cil_tmp6 = *((void **)__cil_tmp5);
6049#line 558
6050  ci = (struct cxd *)__cil_tmp6;
6051#line 560
6052  printk("<6>slot_shutdown\n");
6053#line 561
6054  __cil_tmp7 = (unsigned long )ci;
6055#line 561
6056  __cil_tmp8 = __cil_tmp7 + 1192;
6057#line 561
6058  __cil_tmp9 = (struct mutex *)__cil_tmp8;
6059#line 561
6060  mutex_lock_nested(__cil_tmp9, 0U);
6061#line 562
6062  __cil_tmp10 = (u8 )9;
6063#line 562
6064  __cil_tmp11 = (u8 )8;
6065#line 562
6066  __cil_tmp12 = (u8 )8;
6067#line 562
6068  write_regm(ci, __cil_tmp10, __cil_tmp11, __cil_tmp12);
6069#line 563
6070  __cil_tmp13 = (u8 )32;
6071#line 563
6072  __cil_tmp14 = (u8 )128;
6073#line 563
6074  __cil_tmp15 = (u8 )128;
6075#line 563
6076  write_regm(ci, __cil_tmp13, __cil_tmp14, __cil_tmp15);
6077#line 564
6078  __cil_tmp16 = (u8 )6;
6079#line 564
6080  __cil_tmp17 = (u8 )7;
6081#line 564
6082  __cil_tmp18 = (u8 )7;
6083#line 564
6084  write_regm(ci, __cil_tmp16, __cil_tmp17, __cil_tmp18);
6085#line 565
6086  __cil_tmp19 = (unsigned long )ci;
6087#line 565
6088  __cil_tmp20 = __cil_tmp19 + 144;
6089#line 565
6090  *((int *)__cil_tmp20) = -1;
6091#line 566
6092  __cil_tmp21 = (unsigned long )ci;
6093#line 566
6094  __cil_tmp22 = __cil_tmp21 + 1192;
6095#line 566
6096  __cil_tmp23 = (struct mutex *)__cil_tmp22;
6097#line 566
6098  mutex_unlock(__cil_tmp23);
6099  }
6100#line 567
6101  return (0);
6102}
6103}
6104#line 570 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
6105static int slot_ts_enable(struct dvb_ca_en50221 *ca , int slot ) 
6106{ struct cxd *ci ;
6107  unsigned long __cil_tmp4 ;
6108  unsigned long __cil_tmp5 ;
6109  void *__cil_tmp6 ;
6110  unsigned long __cil_tmp7 ;
6111  unsigned long __cil_tmp8 ;
6112  struct mutex *__cil_tmp9 ;
6113  u8 __cil_tmp10 ;
6114  u8 __cil_tmp11 ;
6115  u8 __cil_tmp12 ;
6116  unsigned long __cil_tmp13 ;
6117  unsigned long __cil_tmp14 ;
6118  struct mutex *__cil_tmp15 ;
6119
6120  {
6121  {
6122#line 572
6123  __cil_tmp4 = (unsigned long )ca;
6124#line 572
6125  __cil_tmp5 = __cil_tmp4 + 72;
6126#line 572
6127  __cil_tmp6 = *((void **)__cil_tmp5);
6128#line 572
6129  ci = (struct cxd *)__cil_tmp6;
6130#line 574
6131  __cil_tmp7 = (unsigned long )ci;
6132#line 574
6133  __cil_tmp8 = __cil_tmp7 + 1192;
6134#line 574
6135  __cil_tmp9 = (struct mutex *)__cil_tmp8;
6136#line 574
6137  mutex_lock_nested(__cil_tmp9, 0U);
6138#line 575
6139  __cil_tmp10 = (u8 )9;
6140#line 575
6141  __cil_tmp11 = (u8 )0;
6142#line 575
6143  __cil_tmp12 = (u8 )8;
6144#line 575
6145  write_regm(ci, __cil_tmp10, __cil_tmp11, __cil_tmp12);
6146#line 576
6147  set_mode(ci, 0);
6148#line 580
6149  __cil_tmp13 = (unsigned long )ci;
6150#line 580
6151  __cil_tmp14 = __cil_tmp13 + 1192;
6152#line 580
6153  __cil_tmp15 = (struct mutex *)__cil_tmp14;
6154#line 580
6155  mutex_unlock(__cil_tmp15);
6156  }
6157#line 581
6158  return (0);
6159}
6160}
6161#line 585 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
6162static int campoll(struct cxd *ci ) 
6163{ u8 istat ;
6164  u8 slotstat ;
6165  u8 __cil_tmp4 ;
6166  u8 *__cil_tmp5 ;
6167  u8 __cil_tmp6 ;
6168  unsigned int __cil_tmp7 ;
6169  u8 __cil_tmp8 ;
6170  u8 *__cil_tmp9 ;
6171  u8 __cil_tmp10 ;
6172  int __cil_tmp11 ;
6173  u8 __cil_tmp12 ;
6174  u8 *__cil_tmp13 ;
6175  u8 __cil_tmp14 ;
6176  int __cil_tmp15 ;
6177  int __cil_tmp16 ;
6178  unsigned long __cil_tmp17 ;
6179  unsigned long __cil_tmp18 ;
6180  u8 *__cil_tmp19 ;
6181  u8 __cil_tmp20 ;
6182  int __cil_tmp21 ;
6183  int __cil_tmp22 ;
6184  u8 *__cil_tmp23 ;
6185  u8 __cil_tmp24 ;
6186  int __cil_tmp25 ;
6187  int __cil_tmp26 ;
6188  u8 __cil_tmp27 ;
6189  u8 *__cil_tmp28 ;
6190  u8 __cil_tmp29 ;
6191  unsigned int __cil_tmp30 ;
6192  unsigned int __cil_tmp31 ;
6193  unsigned long __cil_tmp32 ;
6194  unsigned long __cil_tmp33 ;
6195  int __cil_tmp34 ;
6196  unsigned long __cil_tmp35 ;
6197  unsigned long __cil_tmp36 ;
6198  unsigned long __cil_tmp37 ;
6199  unsigned long __cil_tmp38 ;
6200  int __cil_tmp39 ;
6201  u8 __cil_tmp40 ;
6202  u8 __cil_tmp41 ;
6203  u8 __cil_tmp42 ;
6204  unsigned long __cil_tmp43 ;
6205  unsigned long __cil_tmp44 ;
6206  int __cil_tmp45 ;
6207  unsigned long __cil_tmp46 ;
6208  unsigned long __cil_tmp47 ;
6209  u8 __cil_tmp48 ;
6210  u8 __cil_tmp49 ;
6211  u8 __cil_tmp50 ;
6212  unsigned long __cil_tmp51 ;
6213  unsigned long __cil_tmp52 ;
6214  u8 *__cil_tmp53 ;
6215  u8 __cil_tmp54 ;
6216  int __cil_tmp55 ;
6217  int __cil_tmp56 ;
6218  unsigned long __cil_tmp57 ;
6219  unsigned long __cil_tmp58 ;
6220  int __cil_tmp59 ;
6221  unsigned long __cil_tmp60 ;
6222  unsigned long __cil_tmp61 ;
6223  unsigned long __cil_tmp62 ;
6224  unsigned long __cil_tmp63 ;
6225  unsigned long __cil_tmp64 ;
6226  unsigned long __cil_tmp65 ;
6227  int __cil_tmp66 ;
6228
6229  {
6230  {
6231#line 589
6232  __cil_tmp4 = (u8 )4;
6233#line 589
6234  read_reg(ci, __cil_tmp4, & istat);
6235  }
6236  {
6237#line 590
6238  __cil_tmp5 = & istat;
6239#line 590
6240  __cil_tmp6 = *__cil_tmp5;
6241#line 590
6242  __cil_tmp7 = (unsigned int )__cil_tmp6;
6243#line 590
6244  if (__cil_tmp7 == 0U) {
6245#line 591
6246    return (0);
6247  } else {
6248
6249  }
6250  }
6251  {
6252#line 592
6253  __cil_tmp8 = (u8 )5;
6254#line 592
6255  __cil_tmp9 = & istat;
6256#line 592
6257  __cil_tmp10 = *__cil_tmp9;
6258#line 592
6259  __cil_tmp11 = (int )__cil_tmp10;
6260#line 592
6261  __cil_tmp12 = (u8 )__cil_tmp11;
6262#line 592
6263  write_reg(ci, __cil_tmp8, __cil_tmp12);
6264  }
6265  {
6266#line 594
6267  __cil_tmp13 = & istat;
6268#line 594
6269  __cil_tmp14 = *__cil_tmp13;
6270#line 594
6271  __cil_tmp15 = (int )__cil_tmp14;
6272#line 594
6273  __cil_tmp16 = __cil_tmp15 & 64;
6274#line 594
6275  if (__cil_tmp16 != 0) {
6276    {
6277#line 595
6278    __cil_tmp17 = (unsigned long )ci;
6279#line 595
6280    __cil_tmp18 = __cil_tmp17 + 152;
6281#line 595
6282    *((int *)__cil_tmp18) = 1;
6283#line 596
6284    printk("<6>DR\n");
6285    }
6286  } else {
6287
6288  }
6289  }
6290  {
6291#line 598
6292  __cil_tmp19 = & istat;
6293#line 598
6294  __cil_tmp20 = *__cil_tmp19;
6295#line 598
6296  __cil_tmp21 = (int )__cil_tmp20;
6297#line 598
6298  __cil_tmp22 = __cil_tmp21 & 32;
6299#line 598
6300  if (__cil_tmp22 != 0) {
6301    {
6302#line 599
6303    printk("<6>WC\n");
6304    }
6305  } else {
6306
6307  }
6308  }
6309  {
6310#line 601
6311  __cil_tmp23 = & istat;
6312#line 601
6313  __cil_tmp24 = *__cil_tmp23;
6314#line 601
6315  __cil_tmp25 = (int )__cil_tmp24;
6316#line 601
6317  __cil_tmp26 = __cil_tmp25 & 2;
6318#line 601
6319  if (__cil_tmp26 != 0) {
6320    {
6321#line 604
6322    __cil_tmp27 = (u8 )1;
6323#line 604
6324    read_reg(ci, __cil_tmp27, & slotstat);
6325    }
6326    {
6327#line 605
6328    __cil_tmp28 = & slotstat;
6329#line 605
6330    __cil_tmp29 = *__cil_tmp28;
6331#line 605
6332    __cil_tmp30 = (unsigned int )__cil_tmp29;
6333#line 605
6334    __cil_tmp31 = __cil_tmp30 & 2U;
6335#line 605
6336    if (__cil_tmp31 == 0U) {
6337      {
6338#line 606
6339      __cil_tmp32 = (unsigned long )ci;
6340#line 606
6341      __cil_tmp33 = __cil_tmp32 + 156;
6342#line 606
6343      __cil_tmp34 = *((int *)__cil_tmp33);
6344#line 606
6345      if (__cil_tmp34 == 0) {
6346        {
6347#line 607
6348        __cil_tmp35 = (unsigned long )ci;
6349#line 607
6350        __cil_tmp36 = __cil_tmp35 + 156;
6351#line 607
6352        __cil_tmp37 = (unsigned long )ci;
6353#line 607
6354        __cil_tmp38 = __cil_tmp37 + 156;
6355#line 607
6356        __cil_tmp39 = *((int *)__cil_tmp38);
6357#line 607
6358        *((int *)__cil_tmp36) = __cil_tmp39 | 1;
6359#line 608
6360        __cil_tmp40 = (u8 )3;
6361#line 608
6362        __cil_tmp41 = (u8 )8;
6363#line 608
6364        __cil_tmp42 = (u8 )8;
6365#line 608
6366        write_regm(ci, __cil_tmp40, __cil_tmp41, __cil_tmp42);
6367        }
6368      } else {
6369        {
6370#line 612
6371        __cil_tmp43 = (unsigned long )ci;
6372#line 612
6373        __cil_tmp44 = __cil_tmp43 + 156;
6374#line 612
6375        __cil_tmp45 = *((int *)__cil_tmp44);
6376#line 612
6377        if (__cil_tmp45 != 0) {
6378          {
6379#line 613
6380          __cil_tmp46 = (unsigned long )ci;
6381#line 613
6382          __cil_tmp47 = __cil_tmp46 + 156;
6383#line 613
6384          *((int *)__cil_tmp47) = 0;
6385#line 614
6386          __cil_tmp48 = (u8 )3;
6387#line 614
6388          __cil_tmp49 = (u8 )0;
6389#line 614
6390          __cil_tmp50 = (u8 )8;
6391#line 614
6392          write_regm(ci, __cil_tmp48, __cil_tmp49, __cil_tmp50);
6393#line 615
6394          printk("<6>NO CAM\n");
6395#line 616
6396          __cil_tmp51 = (unsigned long )ci;
6397#line 616
6398          __cil_tmp52 = __cil_tmp51 + 148;
6399#line 616
6400          *((int *)__cil_tmp52) = 0;
6401          }
6402        } else {
6403
6404        }
6405        }
6406      }
6407      }
6408    } else {
6409
6410    }
6411    }
6412    {
6413#line 619
6414    __cil_tmp53 = & istat;
6415#line 619
6416    __cil_tmp54 = *__cil_tmp53;
6417#line 619
6418    __cil_tmp55 = (int )__cil_tmp54;
6419#line 619
6420    __cil_tmp56 = __cil_tmp55 & 8;
6421#line 619
6422    if (__cil_tmp56 != 0) {
6423      {
6424#line 619
6425      __cil_tmp57 = (unsigned long )ci;
6426#line 619
6427      __cil_tmp58 = __cil_tmp57 + 156;
6428#line 619
6429      __cil_tmp59 = *((int *)__cil_tmp58);
6430#line 619
6431      if (__cil_tmp59 == 1) {
6432#line 620
6433        __cil_tmp60 = (unsigned long )ci;
6434#line 620
6435        __cil_tmp61 = __cil_tmp60 + 148;
6436#line 620
6437        *((int *)__cil_tmp61) = 1;
6438#line 621
6439        __cil_tmp62 = (unsigned long )ci;
6440#line 621
6441        __cil_tmp63 = __cil_tmp62 + 156;
6442#line 621
6443        __cil_tmp64 = (unsigned long )ci;
6444#line 621
6445        __cil_tmp65 = __cil_tmp64 + 156;
6446#line 621
6447        __cil_tmp66 = *((int *)__cil_tmp65);
6448#line 621
6449        *((int *)__cil_tmp63) = __cil_tmp66 | 4;
6450      } else {
6451
6452      }
6453      }
6454    } else {
6455
6456    }
6457    }
6458  } else {
6459
6460  }
6461  }
6462#line 624
6463  return (0);
6464}
6465}
6466#line 628 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
6467static int poll_slot_status(struct dvb_ca_en50221 *ca , int slot , int open ) 
6468{ struct cxd *ci ;
6469  u8 slotstat ;
6470  unsigned long __cil_tmp6 ;
6471  unsigned long __cil_tmp7 ;
6472  void *__cil_tmp8 ;
6473  unsigned long __cil_tmp9 ;
6474  unsigned long __cil_tmp10 ;
6475  struct mutex *__cil_tmp11 ;
6476  u8 __cil_tmp12 ;
6477  unsigned long __cil_tmp13 ;
6478  unsigned long __cil_tmp14 ;
6479  struct mutex *__cil_tmp15 ;
6480  unsigned long __cil_tmp16 ;
6481  unsigned long __cil_tmp17 ;
6482
6483  {
6484  {
6485#line 630
6486  __cil_tmp6 = (unsigned long )ca;
6487#line 630
6488  __cil_tmp7 = __cil_tmp6 + 72;
6489#line 630
6490  __cil_tmp8 = *((void **)__cil_tmp7);
6491#line 630
6492  ci = (struct cxd *)__cil_tmp8;
6493#line 633
6494  __cil_tmp9 = (unsigned long )ci;
6495#line 633
6496  __cil_tmp10 = __cil_tmp9 + 1192;
6497#line 633
6498  __cil_tmp11 = (struct mutex *)__cil_tmp10;
6499#line 633
6500  mutex_lock_nested(__cil_tmp11, 0U);
6501#line 634
6502  campoll(ci);
6503#line 635
6504  __cil_tmp12 = (u8 )1;
6505#line 635
6506  read_reg(ci, __cil_tmp12, & slotstat);
6507#line 636
6508  __cil_tmp13 = (unsigned long )ci;
6509#line 636
6510  __cil_tmp14 = __cil_tmp13 + 1192;
6511#line 636
6512  __cil_tmp15 = (struct mutex *)__cil_tmp14;
6513#line 636
6514  mutex_unlock(__cil_tmp15);
6515  }
6516  {
6517#line 638
6518  __cil_tmp16 = (unsigned long )ci;
6519#line 638
6520  __cil_tmp17 = __cil_tmp16 + 156;
6521#line 638
6522  return (*((int *)__cil_tmp17));
6523  }
6524}
6525}
6526#line 681 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
6527static struct dvb_ca_en50221 en_templ  = 
6528#line 681
6529     {(struct module *)0, & read_attribute_mem, & write_attribute_mem, & read_cam_control,
6530    & write_cam_control, & slot_reset, & slot_shutdown, & slot_ts_enable, & poll_slot_status,
6531    (void *)0, (void *)0};
6532#line 697 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
6533struct dvb_ca_en50221 *cxd2099_attach(struct cxd2099_cfg *cfg , void *priv , struct i2c_adapter *i2c ) 
6534{ struct cxd *ci ;
6535  u8 val ;
6536  int tmp ;
6537  void *tmp___0 ;
6538  struct lock_class_key __key ;
6539  size_t __len ;
6540  void *__ret ;
6541  size_t __len___0 ;
6542  void *__ret___0 ;
6543  unsigned long __cil_tmp13 ;
6544  unsigned long __cil_tmp14 ;
6545  u8 __cil_tmp15 ;
6546  int __cil_tmp16 ;
6547  u8 __cil_tmp17 ;
6548  u8 __cil_tmp18 ;
6549  unsigned long __cil_tmp19 ;
6550  unsigned long __cil_tmp20 ;
6551  u8 __cil_tmp21 ;
6552  int __cil_tmp22 ;
6553  struct cxd *__cil_tmp23 ;
6554  unsigned long __cil_tmp24 ;
6555  unsigned long __cil_tmp25 ;
6556  void *__cil_tmp26 ;
6557  unsigned long __cil_tmp27 ;
6558  unsigned long __cil_tmp28 ;
6559  struct mutex *__cil_tmp29 ;
6560  unsigned long __cil_tmp30 ;
6561  unsigned long __cil_tmp31 ;
6562  struct cxd2099_cfg *__cil_tmp32 ;
6563  void *__cil_tmp33 ;
6564  void const   *__cil_tmp34 ;
6565  unsigned long __cil_tmp35 ;
6566  unsigned long __cil_tmp36 ;
6567  struct cxd2099_cfg *__cil_tmp37 ;
6568  void *__cil_tmp38 ;
6569  void const   *__cil_tmp39 ;
6570  unsigned long __cil_tmp40 ;
6571  unsigned long __cil_tmp41 ;
6572  unsigned long __cil_tmp42 ;
6573  unsigned long __cil_tmp43 ;
6574  unsigned long __cil_tmp44 ;
6575  unsigned long __cil_tmp45 ;
6576  unsigned long __cil_tmp46 ;
6577  unsigned long __cil_tmp47 ;
6578  struct dvb_ca_en50221 *__cil_tmp48 ;
6579  void *__cil_tmp49 ;
6580  void const   *__cil_tmp50 ;
6581  struct dvb_ca_en50221 *__cil_tmp51 ;
6582  void *__cil_tmp52 ;
6583  void const   *__cil_tmp53 ;
6584  unsigned long __cil_tmp54 ;
6585  unsigned long __cil_tmp55 ;
6586  unsigned long __cil_tmp56 ;
6587  unsigned long __cil_tmp57 ;
6588  unsigned long __cil_tmp58 ;
6589  unsigned long __cil_tmp59 ;
6590  u8 __cil_tmp60 ;
6591  int __cil_tmp61 ;
6592
6593  {
6594  {
6595#line 701
6596  ci = (struct cxd *)0;
6597#line 704
6598  __cil_tmp13 = (unsigned long )cfg;
6599#line 704
6600  __cil_tmp14 = __cil_tmp13 + 4;
6601#line 704
6602  __cil_tmp15 = *((u8 *)__cil_tmp14);
6603#line 704
6604  __cil_tmp16 = (int )__cil_tmp15;
6605#line 704
6606  __cil_tmp17 = (u8 )__cil_tmp16;
6607#line 704
6608  __cil_tmp18 = (u8 )0;
6609#line 704
6610  tmp = i2c_read_reg(i2c, __cil_tmp17, __cil_tmp18, & val);
6611  }
6612#line 704
6613  if (tmp < 0) {
6614    {
6615#line 705
6616    __cil_tmp19 = (unsigned long )cfg;
6617#line 705
6618    __cil_tmp20 = __cil_tmp19 + 4;
6619#line 705
6620    __cil_tmp21 = *((u8 *)__cil_tmp20);
6621#line 705
6622    __cil_tmp22 = (int )__cil_tmp21;
6623#line 705
6624    printk("<6>No CXD2099 detected at %02x\n", __cil_tmp22);
6625    }
6626#line 706
6627    return ((struct dvb_ca_en50221 *)0);
6628  } else {
6629
6630  }
6631  {
6632#line 709
6633  tmp___0 = kmalloc(1360UL, 208U);
6634#line 709
6635  ci = (struct cxd *)tmp___0;
6636  }
6637  {
6638#line 710
6639  __cil_tmp23 = (struct cxd *)0;
6640#line 710
6641  __cil_tmp24 = (unsigned long )__cil_tmp23;
6642#line 710
6643  __cil_tmp25 = (unsigned long )ci;
6644#line 710
6645  if (__cil_tmp25 == __cil_tmp24) {
6646#line 711
6647    return ((struct dvb_ca_en50221 *)0);
6648  } else {
6649
6650  }
6651  }
6652  {
6653#line 712
6654  __cil_tmp26 = (void *)ci;
6655#line 712
6656  memset(__cil_tmp26, 0, 1360UL);
6657#line 714
6658  __cil_tmp27 = (unsigned long )ci;
6659#line 714
6660  __cil_tmp28 = __cil_tmp27 + 1192;
6661#line 714
6662  __cil_tmp29 = (struct mutex *)__cil_tmp28;
6663#line 714
6664  __mutex_init(__cil_tmp29, "&ci->lock", & __key);
6665#line 715
6666  __len = 8UL;
6667  }
6668#line 715
6669  if (__len > 63UL) {
6670    {
6671#line 715
6672    __cil_tmp30 = (unsigned long )ci;
6673#line 715
6674    __cil_tmp31 = __cil_tmp30 + 96;
6675#line 715
6676    __cil_tmp32 = (struct cxd2099_cfg *)__cil_tmp31;
6677#line 715
6678    __cil_tmp33 = (void *)__cil_tmp32;
6679#line 715
6680    __cil_tmp34 = (void const   *)cfg;
6681#line 715
6682    __ret = __memcpy(__cil_tmp33, __cil_tmp34, __len);
6683    }
6684  } else {
6685    {
6686#line 715
6687    __cil_tmp35 = (unsigned long )ci;
6688#line 715
6689    __cil_tmp36 = __cil_tmp35 + 96;
6690#line 715
6691    __cil_tmp37 = (struct cxd2099_cfg *)__cil_tmp36;
6692#line 715
6693    __cil_tmp38 = (void *)__cil_tmp37;
6694#line 715
6695    __cil_tmp39 = (void const   *)cfg;
6696#line 715
6697    __ret = __builtin_memcpy(__cil_tmp38, __cil_tmp39, __len);
6698    }
6699  }
6700#line 716
6701  __cil_tmp40 = (unsigned long )ci;
6702#line 716
6703  __cil_tmp41 = __cil_tmp40 + 88;
6704#line 716
6705  *((struct i2c_adapter **)__cil_tmp41) = i2c;
6706#line 717
6707  __cil_tmp42 = (unsigned long )ci;
6708#line 717
6709  __cil_tmp43 = __cil_tmp42 + 139;
6710#line 717
6711  *((u8 *)__cil_tmp43) = (u8 )255U;
6712#line 718
6713  __cil_tmp44 = (unsigned long )ci;
6714#line 718
6715  __cil_tmp45 = __cil_tmp44 + 141;
6716#line 718
6717  *((u8 *)__cil_tmp45) = (u8 )74U;
6718#line 719
6719  __cil_tmp46 = (unsigned long )ci;
6720#line 719
6721  __cil_tmp47 = __cil_tmp46 + 140;
6722#line 719
6723  *((u8 *)__cil_tmp47) = (u8 )27U;
6724#line 721
6725  __len___0 = 88UL;
6726#line 721
6727  if (__len___0 > 63UL) {
6728    {
6729#line 721
6730    __cil_tmp48 = (struct dvb_ca_en50221 *)ci;
6731#line 721
6732    __cil_tmp49 = (void *)__cil_tmp48;
6733#line 721
6734    __cil_tmp50 = (void const   *)(& en_templ);
6735#line 721
6736    __ret___0 = __memcpy(__cil_tmp49, __cil_tmp50, __len___0);
6737    }
6738  } else {
6739    {
6740#line 721
6741    __cil_tmp51 = (struct dvb_ca_en50221 *)ci;
6742#line 721
6743    __cil_tmp52 = (void *)__cil_tmp51;
6744#line 721
6745    __cil_tmp53 = (void const   *)(& en_templ);
6746#line 721
6747    __ret___0 = __builtin_memcpy(__cil_tmp52, __cil_tmp53, __len___0);
6748    }
6749  }
6750  {
6751#line 722
6752  __cil_tmp54 = 0 + 72;
6753#line 722
6754  __cil_tmp55 = (unsigned long )ci;
6755#line 722
6756  __cil_tmp56 = __cil_tmp55 + __cil_tmp54;
6757#line 722
6758  *((void **)__cil_tmp56) = (void *)ci;
6759#line 723
6760  init(ci);
6761#line 724
6762  __cil_tmp57 = 96 + 4;
6763#line 724
6764  __cil_tmp58 = (unsigned long )ci;
6765#line 724
6766  __cil_tmp59 = __cil_tmp58 + __cil_tmp57;
6767#line 724
6768  __cil_tmp60 = *((u8 *)__cil_tmp59);
6769#line 724
6770  __cil_tmp61 = (int )__cil_tmp60;
6771#line 724
6772  printk("<6>Attached CXD2099AR at %02x\n", __cil_tmp61);
6773  }
6774#line 725
6775  return ((struct dvb_ca_en50221 *)ci);
6776}
6777}
6778#line 749
6779extern void ldv_check_final_state(void) ;
6780#line 755
6781extern void ldv_initialize(void) ;
6782#line 758
6783extern int __VERIFIER_nondet_int(void) ;
6784#line 761 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
6785int LDV_IN_INTERRUPT  ;
6786#line 764 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
6787void main(void) 
6788{ struct dvb_ca_en50221 *var_group1 ;
6789  int var_read_attribute_mem_18_p1 ;
6790  int var_read_attribute_mem_18_p2 ;
6791  int var_write_attribute_mem_19_p1 ;
6792  int var_write_attribute_mem_19_p2 ;
6793  u8 var_write_attribute_mem_19_p3 ;
6794  int var_read_cam_control_20_p1 ;
6795  u8 var_read_cam_control_20_p2 ;
6796  int var_write_cam_control_21_p1 ;
6797  u8 var_write_cam_control_21_p2 ;
6798  u8 var_write_cam_control_21_p3 ;
6799  int var_slot_reset_22_p1 ;
6800  int var_slot_shutdown_23_p1 ;
6801  int var_slot_ts_enable_24_p1 ;
6802  int var_poll_slot_status_26_p1 ;
6803  int var_poll_slot_status_26_p2 ;
6804  int tmp ;
6805  int tmp___0 ;
6806  int __cil_tmp19 ;
6807  u8 __cil_tmp20 ;
6808  int __cil_tmp21 ;
6809  u8 __cil_tmp22 ;
6810  int __cil_tmp23 ;
6811  u8 __cil_tmp24 ;
6812  int __cil_tmp25 ;
6813  u8 __cil_tmp26 ;
6814
6815  {
6816  {
6817#line 1146
6818  LDV_IN_INTERRUPT = 1;
6819#line 1155
6820  ldv_initialize();
6821  }
6822#line 1159
6823  goto ldv_22625;
6824  ldv_22624: 
6825  {
6826#line 1162
6827  tmp = __VERIFIER_nondet_int();
6828  }
6829#line 1164
6830  if (tmp == 0) {
6831#line 1164
6832    goto case_0;
6833  } else
6834#line 1209
6835  if (tmp == 1) {
6836#line 1209
6837    goto case_1;
6838  } else
6839#line 1257
6840  if (tmp == 2) {
6841#line 1257
6842    goto case_2;
6843  } else
6844#line 1305
6845  if (tmp == 3) {
6846#line 1305
6847    goto case_3;
6848  } else
6849#line 1353
6850  if (tmp == 4) {
6851#line 1353
6852    goto case_4;
6853  } else
6854#line 1390
6855  if (tmp == 5) {
6856#line 1390
6857    goto case_5;
6858  } else
6859#line 1438
6860  if (tmp == 6) {
6861#line 1438
6862    goto case_6;
6863  } else
6864#line 1484
6865  if (tmp == 7) {
6866#line 1484
6867    goto case_7;
6868  } else
6869#line 1532
6870  if (tmp == 8) {
6871#line 1532
6872    goto case_8;
6873  } else
6874#line 1580
6875  if (tmp == 9) {
6876#line 1580
6877    goto case_9;
6878  } else {
6879    {
6880#line 1628
6881    goto switch_default;
6882#line 1162
6883    if (0) {
6884      case_0: /* CIL Label */ 
6885      {
6886#line 1182
6887      read_attribute_mem(var_group1, var_read_attribute_mem_18_p1, var_read_attribute_mem_18_p2);
6888      }
6889#line 1208
6890      goto ldv_22613;
6891      case_1: /* CIL Label */ 
6892      {
6893#line 1230
6894      __cil_tmp19 = (int )var_write_attribute_mem_19_p3;
6895#line 1230
6896      __cil_tmp20 = (u8 )__cil_tmp19;
6897#line 1230
6898      write_attribute_mem(var_group1, var_write_attribute_mem_19_p1, var_write_attribute_mem_19_p2,
6899                          __cil_tmp20);
6900      }
6901#line 1256
6902      goto ldv_22613;
6903      case_2: /* CIL Label */ 
6904      {
6905#line 1278
6906      __cil_tmp21 = (int )var_read_cam_control_20_p2;
6907#line 1278
6908      __cil_tmp22 = (u8 )__cil_tmp21;
6909#line 1278
6910      read_cam_control(var_group1, var_read_cam_control_20_p1, __cil_tmp22);
6911      }
6912#line 1304
6913      goto ldv_22613;
6914      case_3: /* CIL Label */ 
6915      {
6916#line 1326
6917      __cil_tmp23 = (int )var_write_cam_control_21_p2;
6918#line 1326
6919      __cil_tmp24 = (u8 )__cil_tmp23;
6920#line 1326
6921      __cil_tmp25 = (int )var_write_cam_control_21_p3;
6922#line 1326
6923      __cil_tmp26 = (u8 )__cil_tmp25;
6924#line 1326
6925      write_cam_control(var_group1, var_write_cam_control_21_p1, __cil_tmp24, __cil_tmp26);
6926      }
6927#line 1352
6928      goto ldv_22613;
6929      case_4: /* CIL Label */ 
6930      {
6931#line 1374
6932      slot_reset(var_group1, var_slot_reset_22_p1);
6933      }
6934#line 1389
6935      goto ldv_22613;
6936      case_5: /* CIL Label */ 
6937      {
6938#line 1422
6939      slot_shutdown(var_group1, var_slot_shutdown_23_p1);
6940      }
6941#line 1437
6942      goto ldv_22613;
6943      case_6: /* CIL Label */ 
6944      {
6945#line 1470
6946      slot_ts_enable(var_group1, var_slot_ts_enable_24_p1);
6947      }
6948#line 1483
6949      goto ldv_22613;
6950      case_7: /* CIL Label */ 
6951      {
6952#line 1518
6953      poll_slot_status(var_group1, var_poll_slot_status_26_p1, var_poll_slot_status_26_p2);
6954      }
6955#line 1531
6956      goto ldv_22613;
6957      case_8: /* CIL Label */ ;
6958#line 1579
6959      goto ldv_22613;
6960      case_9: /* CIL Label */ ;
6961#line 1627
6962      goto ldv_22613;
6963      switch_default: /* CIL Label */ ;
6964#line 1628
6965      goto ldv_22613;
6966    } else {
6967      switch_break: /* CIL Label */ ;
6968    }
6969    }
6970  }
6971  ldv_22613: ;
6972  ldv_22625: 
6973  {
6974#line 1159
6975  tmp___0 = __VERIFIER_nondet_int();
6976  }
6977#line 1159
6978  if (tmp___0 != 0) {
6979#line 1160
6980    goto ldv_22624;
6981  } else {
6982#line 1162
6983    goto ldv_22626;
6984  }
6985  ldv_22626: ;
6986
6987  {
6988#line 1637
6989  ldv_check_final_state();
6990  }
6991#line 1640
6992  return;
6993}
6994}
6995#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6996void ldv_blast_assert(void) 
6997{ 
6998
6999  {
7000  ERROR: ;
7001#line 6
7002  goto ERROR;
7003}
7004}
7005#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7006extern int __VERIFIER_nondet_int(void) ;
7007#line 1661 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
7008int ldv_spin  =    0;
7009#line 1665 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
7010void ldv_check_alloc_flags(gfp_t flags ) 
7011{ 
7012
7013  {
7014#line 1668
7015  if (ldv_spin != 0) {
7016#line 1668
7017    if (flags != 32U) {
7018      {
7019#line 1668
7020      ldv_blast_assert();
7021      }
702