Showing error 1306

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