Showing error 518

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--tests--mtd_oobtest.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 6297
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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