Showing error 515

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