Showing error 503

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--doc2001plus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 7750
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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