Showing error 517

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


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 20 "include/asm-generic/int-ll64.h"
   5typedef unsigned char __u8;
   6#line 23 "include/asm-generic/int-ll64.h"
   7typedef unsigned short __u16;
   8#line 25 "include/asm-generic/int-ll64.h"
   9typedef int __s32;
  10#line 26 "include/asm-generic/int-ll64.h"
  11typedef unsigned int __u32;
  12#line 30 "include/asm-generic/int-ll64.h"
  13typedef unsigned long long __u64;
  14#line 43 "include/asm-generic/int-ll64.h"
  15typedef unsigned char u8;
  16#line 45 "include/asm-generic/int-ll64.h"
  17typedef short s16;
  18#line 46 "include/asm-generic/int-ll64.h"
  19typedef unsigned short u16;
  20#line 49 "include/asm-generic/int-ll64.h"
  21typedef unsigned int u32;
  22#line 51 "include/asm-generic/int-ll64.h"
  23typedef long long s64;
  24#line 52 "include/asm-generic/int-ll64.h"
  25typedef unsigned long long u64;
  26#line 14 "include/asm-generic/posix_types.h"
  27typedef long __kernel_long_t;
  28#line 15 "include/asm-generic/posix_types.h"
  29typedef unsigned long __kernel_ulong_t;
  30#line 31 "include/asm-generic/posix_types.h"
  31typedef int __kernel_pid_t;
  32#line 52 "include/asm-generic/posix_types.h"
  33typedef unsigned int __kernel_uid32_t;
  34#line 53 "include/asm-generic/posix_types.h"
  35typedef unsigned int __kernel_gid32_t;
  36#line 75 "include/asm-generic/posix_types.h"
  37typedef __kernel_ulong_t __kernel_size_t;
  38#line 76 "include/asm-generic/posix_types.h"
  39typedef __kernel_long_t __kernel_ssize_t;
  40#line 91 "include/asm-generic/posix_types.h"
  41typedef long long __kernel_loff_t;
  42#line 92 "include/asm-generic/posix_types.h"
  43typedef __kernel_long_t __kernel_time_t;
  44#line 93 "include/asm-generic/posix_types.h"
  45typedef __kernel_long_t __kernel_clock_t;
  46#line 94 "include/asm-generic/posix_types.h"
  47typedef int __kernel_timer_t;
  48#line 95 "include/asm-generic/posix_types.h"
  49typedef int __kernel_clockid_t;
  50#line 21 "include/linux/types.h"
  51typedef __u32 __kernel_dev_t;
  52#line 24 "include/linux/types.h"
  53typedef __kernel_dev_t dev_t;
  54#line 27 "include/linux/types.h"
  55typedef unsigned short umode_t;
  56#line 30 "include/linux/types.h"
  57typedef __kernel_pid_t pid_t;
  58#line 35 "include/linux/types.h"
  59typedef __kernel_clockid_t clockid_t;
  60#line 38 "include/linux/types.h"
  61typedef _Bool bool;
  62#line 40 "include/linux/types.h"
  63typedef __kernel_uid32_t uid_t;
  64#line 41 "include/linux/types.h"
  65typedef __kernel_gid32_t gid_t;
  66#line 54 "include/linux/types.h"
  67typedef __kernel_loff_t loff_t;
  68#line 63 "include/linux/types.h"
  69typedef __kernel_size_t size_t;
  70#line 68 "include/linux/types.h"
  71typedef __kernel_ssize_t ssize_t;
  72#line 78 "include/linux/types.h"
  73typedef __kernel_time_t time_t;
  74#line 92 "include/linux/types.h"
  75typedef unsigned char u_char;
  76#line 95 "include/linux/types.h"
  77typedef unsigned long u_long;
  78#line 111 "include/linux/types.h"
  79typedef __s32 int32_t;
  80#line 115 "include/linux/types.h"
  81typedef __u8 uint8_t;
  82#line 117 "include/linux/types.h"
  83typedef __u32 uint32_t;
  84#line 120 "include/linux/types.h"
  85typedef __u64 uint64_t;
  86#line 202 "include/linux/types.h"
  87typedef unsigned int gfp_t;
  88#line 206 "include/linux/types.h"
  89typedef u64 phys_addr_t;
  90#line 211 "include/linux/types.h"
  91typedef phys_addr_t resource_size_t;
  92#line 219 "include/linux/types.h"
  93struct __anonstruct_atomic_t_7 {
  94   int counter ;
  95};
  96#line 219 "include/linux/types.h"
  97typedef struct __anonstruct_atomic_t_7 atomic_t;
  98#line 224 "include/linux/types.h"
  99struct __anonstruct_atomic64_t_8 {
 100   long counter ;
 101};
 102#line 224 "include/linux/types.h"
 103typedef struct __anonstruct_atomic64_t_8 atomic64_t;
 104#line 229 "include/linux/types.h"
 105struct list_head {
 106   struct list_head *next ;
 107   struct list_head *prev ;
 108};
 109#line 233
 110struct hlist_node;
 111#line 233 "include/linux/types.h"
 112struct hlist_head {
 113   struct hlist_node *first ;
 114};
 115#line 237 "include/linux/types.h"
 116struct hlist_node {
 117   struct hlist_node *next ;
 118   struct hlist_node **pprev ;
 119};
 120#line 253 "include/linux/types.h"
 121struct rcu_head {
 122   struct rcu_head *next ;
 123   void (*func)(struct rcu_head *head ) ;
 124};
 125#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 126struct module;
 127#line 56
 128struct module;
 129#line 146 "include/linux/init.h"
 130typedef void (*ctor_fn_t)(void);
 131#line 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 49 "include/linux/wait.h"
 479struct __wait_queue_head {
 480   spinlock_t lock ;
 481   struct list_head task_list ;
 482};
 483#line 53 "include/linux/wait.h"
 484typedef struct __wait_queue_head wait_queue_head_t;
 485#line 55
 486struct task_struct;
 487#line 119 "include/linux/seqlock.h"
 488struct seqcount {
 489   unsigned int sequence ;
 490};
 491#line 119 "include/linux/seqlock.h"
 492typedef struct seqcount seqcount_t;
 493#line 98 "include/linux/nodemask.h"
 494struct __anonstruct_nodemask_t_42 {
 495   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 496};
 497#line 98 "include/linux/nodemask.h"
 498typedef struct __anonstruct_nodemask_t_42 nodemask_t;
 499#line 60 "include/linux/pageblock-flags.h"
 500struct page;
 501#line 48 "include/linux/mutex.h"
 502struct mutex {
 503   atomic_t count ;
 504   spinlock_t wait_lock ;
 505   struct list_head wait_list ;
 506   struct task_struct *owner ;
 507   char const   *name ;
 508   void *magic ;
 509};
 510#line 69 "include/linux/mutex.h"
 511struct mutex_waiter {
 512   struct list_head list ;
 513   struct task_struct *task ;
 514   void *magic ;
 515};
 516#line 19 "include/linux/rwsem.h"
 517struct rw_semaphore;
 518#line 19
 519struct rw_semaphore;
 520#line 25 "include/linux/rwsem.h"
 521struct rw_semaphore {
 522   long count ;
 523   raw_spinlock_t wait_lock ;
 524   struct list_head wait_list ;
 525};
 526#line 25 "include/linux/completion.h"
 527struct completion {
 528   unsigned int done ;
 529   wait_queue_head_t wait ;
 530};
 531#line 188 "include/linux/rcupdate.h"
 532struct notifier_block;
 533#line 188
 534struct notifier_block;
 535#line 50 "include/linux/notifier.h"
 536struct notifier_block {
 537   int (*notifier_call)(struct notifier_block * , unsigned long  , void * ) ;
 538   struct notifier_block *next ;
 539   int priority ;
 540};
 541#line 9 "include/linux/memory_hotplug.h"
 542struct page;
 543#line 202 "include/linux/ioport.h"
 544struct device;
 545#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 546struct device;
 547#line 14 "include/linux/time.h"
 548struct timespec {
 549   __kernel_time_t tv_sec ;
 550   long tv_nsec ;
 551};
 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 20 "include/linux/kobject_ns.h"
 718struct sock;
 719#line 20
 720struct sock;
 721#line 21
 722struct kobject;
 723#line 21
 724struct kobject;
 725#line 27
 726enum kobj_ns_type {
 727    KOBJ_NS_TYPE_NONE = 0,
 728    KOBJ_NS_TYPE_NET = 1,
 729    KOBJ_NS_TYPES = 2
 730} ;
 731#line 40 "include/linux/kobject_ns.h"
 732struct kobj_ns_type_operations {
 733   enum kobj_ns_type type ;
 734   void *(*grab_current_ns)(void) ;
 735   void const   *(*netlink_ns)(struct sock *sk ) ;
 736   void const   *(*initial_ns)(void) ;
 737   void (*drop_ns)(void * ) ;
 738};
 739#line 22 "include/linux/sysfs.h"
 740struct kobject;
 741#line 23
 742struct module;
 743#line 24
 744enum kobj_ns_type;
 745#line 26 "include/linux/sysfs.h"
 746struct attribute {
 747   char const   *name ;
 748   umode_t mode ;
 749};
 750#line 56 "include/linux/sysfs.h"
 751struct attribute_group {
 752   char const   *name ;
 753   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 754   struct attribute **attrs ;
 755};
 756#line 85
 757struct file;
 758#line 86
 759struct vm_area_struct;
 760#line 88 "include/linux/sysfs.h"
 761struct bin_attribute {
 762   struct attribute attr ;
 763   size_t size ;
 764   void *private ;
 765   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 766                   loff_t  , size_t  ) ;
 767   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 768                    loff_t  , size_t  ) ;
 769   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 770};
 771#line 112 "include/linux/sysfs.h"
 772struct sysfs_ops {
 773   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 774   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 775   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 776};
 777#line 118
 778struct sysfs_dirent;
 779#line 118
 780struct sysfs_dirent;
 781#line 22 "include/linux/kref.h"
 782struct kref {
 783   atomic_t refcount ;
 784};
 785#line 60 "include/linux/kobject.h"
 786struct kset;
 787#line 60
 788struct kobj_type;
 789#line 60 "include/linux/kobject.h"
 790struct kobject {
 791   char const   *name ;
 792   struct list_head entry ;
 793   struct kobject *parent ;
 794   struct kset *kset ;
 795   struct kobj_type *ktype ;
 796   struct sysfs_dirent *sd ;
 797   struct kref kref ;
 798   unsigned int state_initialized : 1 ;
 799   unsigned int state_in_sysfs : 1 ;
 800   unsigned int state_add_uevent_sent : 1 ;
 801   unsigned int state_remove_uevent_sent : 1 ;
 802   unsigned int uevent_suppress : 1 ;
 803};
 804#line 108 "include/linux/kobject.h"
 805struct kobj_type {
 806   void (*release)(struct kobject *kobj ) ;
 807   struct sysfs_ops  const  *sysfs_ops ;
 808   struct attribute **default_attrs ;
 809   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 810   void const   *(*namespace)(struct kobject *kobj ) ;
 811};
 812#line 116 "include/linux/kobject.h"
 813struct kobj_uevent_env {
 814   char *envp[32] ;
 815   int envp_idx ;
 816   char buf[2048] ;
 817   int buflen ;
 818};
 819#line 123 "include/linux/kobject.h"
 820struct kset_uevent_ops {
 821   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 822   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 823   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 824};
 825#line 140
 826struct sock;
 827#line 159 "include/linux/kobject.h"
 828struct kset {
 829   struct list_head list ;
 830   spinlock_t list_lock ;
 831   struct kobject kobj ;
 832   struct kset_uevent_ops  const  *uevent_ops ;
 833};
 834#line 46 "include/linux/slub_def.h"
 835struct kmem_cache_cpu {
 836   void **freelist ;
 837   unsigned long tid ;
 838   struct page *page ;
 839   struct page *partial ;
 840   int node ;
 841   unsigned int stat[26] ;
 842};
 843#line 57 "include/linux/slub_def.h"
 844struct kmem_cache_node {
 845   spinlock_t list_lock ;
 846   unsigned long nr_partial ;
 847   struct list_head partial ;
 848   atomic_long_t nr_slabs ;
 849   atomic_long_t total_objects ;
 850   struct list_head full ;
 851};
 852#line 73 "include/linux/slub_def.h"
 853struct kmem_cache_order_objects {
 854   unsigned long x ;
 855};
 856#line 80 "include/linux/slub_def.h"
 857struct kmem_cache {
 858   struct kmem_cache_cpu *cpu_slab ;
 859   unsigned long flags ;
 860   unsigned long min_partial ;
 861   int size ;
 862   int objsize ;
 863   int offset ;
 864   int cpu_partial ;
 865   struct kmem_cache_order_objects oo ;
 866   struct kmem_cache_order_objects max ;
 867   struct kmem_cache_order_objects min ;
 868   gfp_t allocflags ;
 869   int refcount ;
 870   void (*ctor)(void * ) ;
 871   int inuse ;
 872   int align ;
 873   int reserved ;
 874   char const   *name ;
 875   struct list_head list ;
 876   struct kobject kobj ;
 877   int remote_node_defrag_ratio ;
 878   struct kmem_cache_node *node[1 << 10] ;
 879};
 880#line 29 "include/linux/sysctl.h"
 881struct completion;
 882#line 100 "include/linux/rbtree.h"
 883struct rb_node {
 884   unsigned long rb_parent_color ;
 885   struct rb_node *rb_right ;
 886   struct rb_node *rb_left ;
 887} __attribute__((__aligned__(sizeof(long )))) ;
 888#line 110 "include/linux/rbtree.h"
 889struct rb_root {
 890   struct rb_node *rb_node ;
 891};
 892#line 939 "include/linux/sysctl.h"
 893struct nsproxy;
 894#line 939
 895struct nsproxy;
 896#line 48 "include/linux/kmod.h"
 897struct cred;
 898#line 48
 899struct cred;
 900#line 49
 901struct file;
 902#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 903struct task_struct;
 904#line 18 "include/linux/elf.h"
 905typedef __u64 Elf64_Addr;
 906#line 19 "include/linux/elf.h"
 907typedef __u16 Elf64_Half;
 908#line 23 "include/linux/elf.h"
 909typedef __u32 Elf64_Word;
 910#line 24 "include/linux/elf.h"
 911typedef __u64 Elf64_Xword;
 912#line 194 "include/linux/elf.h"
 913struct elf64_sym {
 914   Elf64_Word st_name ;
 915   unsigned char st_info ;
 916   unsigned char st_other ;
 917   Elf64_Half st_shndx ;
 918   Elf64_Addr st_value ;
 919   Elf64_Xword st_size ;
 920};
 921#line 194 "include/linux/elf.h"
 922typedef struct elf64_sym Elf64_Sym;
 923#line 438
 924struct file;
 925#line 39 "include/linux/moduleparam.h"
 926struct kernel_param;
 927#line 39
 928struct kernel_param;
 929#line 41 "include/linux/moduleparam.h"
 930struct kernel_param_ops {
 931   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 932   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 933   void (*free)(void *arg ) ;
 934};
 935#line 50
 936struct kparam_string;
 937#line 50
 938struct kparam_array;
 939#line 50 "include/linux/moduleparam.h"
 940union __anonunion____missing_field_name_199 {
 941   void *arg ;
 942   struct kparam_string  const  *str ;
 943   struct kparam_array  const  *arr ;
 944};
 945#line 50 "include/linux/moduleparam.h"
 946struct kernel_param {
 947   char const   *name ;
 948   struct kernel_param_ops  const  *ops ;
 949   u16 perm ;
 950   s16 level ;
 951   union __anonunion____missing_field_name_199 __annonCompField32 ;
 952};
 953#line 63 "include/linux/moduleparam.h"
 954struct kparam_string {
 955   unsigned int maxlen ;
 956   char *string ;
 957};
 958#line 69 "include/linux/moduleparam.h"
 959struct kparam_array {
 960   unsigned int max ;
 961   unsigned int elemsize ;
 962   unsigned int *num ;
 963   struct kernel_param_ops  const  *ops ;
 964   void *elem ;
 965};
 966#line 445
 967struct module;
 968#line 80 "include/linux/jump_label.h"
 969struct module;
 970#line 143 "include/linux/jump_label.h"
 971struct static_key {
 972   atomic_t enabled ;
 973};
 974#line 22 "include/linux/tracepoint.h"
 975struct module;
 976#line 23
 977struct tracepoint;
 978#line 23
 979struct tracepoint;
 980#line 25 "include/linux/tracepoint.h"
 981struct tracepoint_func {
 982   void *func ;
 983   void *data ;
 984};
 985#line 30 "include/linux/tracepoint.h"
 986struct tracepoint {
 987   char const   *name ;
 988   struct static_key key ;
 989   void (*regfunc)(void) ;
 990   void (*unregfunc)(void) ;
 991   struct tracepoint_func *funcs ;
 992};
 993#line 19 "include/linux/export.h"
 994struct kernel_symbol {
 995   unsigned long value ;
 996   char const   *name ;
 997};
 998#line 8 "include/asm-generic/module.h"
 999struct mod_arch_specific {
1000
1001};
1002#line 35 "include/linux/module.h"
1003struct module;
1004#line 37
1005struct module_param_attrs;
1006#line 37 "include/linux/module.h"
1007struct module_kobject {
1008   struct kobject kobj ;
1009   struct module *mod ;
1010   struct kobject *drivers_dir ;
1011   struct module_param_attrs *mp ;
1012};
1013#line 44 "include/linux/module.h"
1014struct module_attribute {
1015   struct attribute attr ;
1016   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
1017   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
1018                    size_t count ) ;
1019   void (*setup)(struct module * , char const   * ) ;
1020   int (*test)(struct module * ) ;
1021   void (*free)(struct module * ) ;
1022};
1023#line 71
1024struct exception_table_entry;
1025#line 71
1026struct exception_table_entry;
1027#line 182
1028struct notifier_block;
1029#line 199
1030enum module_state {
1031    MODULE_STATE_LIVE = 0,
1032    MODULE_STATE_COMING = 1,
1033    MODULE_STATE_GOING = 2
1034} ;
1035#line 215 "include/linux/module.h"
1036struct module_ref {
1037   unsigned long incs ;
1038   unsigned long decs ;
1039} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1040#line 220
1041struct module_sect_attrs;
1042#line 220
1043struct module_notes_attrs;
1044#line 220
1045struct ftrace_event_call;
1046#line 220 "include/linux/module.h"
1047struct module {
1048   enum module_state state ;
1049   struct list_head list ;
1050   char name[64UL - sizeof(unsigned long )] ;
1051   struct module_kobject mkobj ;
1052   struct module_attribute *modinfo_attrs ;
1053   char const   *version ;
1054   char const   *srcversion ;
1055   struct kobject *holders_dir ;
1056   struct kernel_symbol  const  *syms ;
1057   unsigned long const   *crcs ;
1058   unsigned int num_syms ;
1059   struct kernel_param *kp ;
1060   unsigned int num_kp ;
1061   unsigned int num_gpl_syms ;
1062   struct kernel_symbol  const  *gpl_syms ;
1063   unsigned long const   *gpl_crcs ;
1064   struct kernel_symbol  const  *unused_syms ;
1065   unsigned long const   *unused_crcs ;
1066   unsigned int num_unused_syms ;
1067   unsigned int num_unused_gpl_syms ;
1068   struct kernel_symbol  const  *unused_gpl_syms ;
1069   unsigned long const   *unused_gpl_crcs ;
1070   struct kernel_symbol  const  *gpl_future_syms ;
1071   unsigned long const   *gpl_future_crcs ;
1072   unsigned int num_gpl_future_syms ;
1073   unsigned int num_exentries ;
1074   struct exception_table_entry *extable ;
1075   int (*init)(void) ;
1076   void *module_init ;
1077   void *module_core ;
1078   unsigned int init_size ;
1079   unsigned int core_size ;
1080   unsigned int init_text_size ;
1081   unsigned int core_text_size ;
1082   unsigned int init_ro_size ;
1083   unsigned int core_ro_size ;
1084   struct mod_arch_specific arch ;
1085   unsigned int taints ;
1086   unsigned int num_bugs ;
1087   struct list_head bug_list ;
1088   struct bug_entry *bug_table ;
1089   Elf64_Sym *symtab ;
1090   Elf64_Sym *core_symtab ;
1091   unsigned int num_symtab ;
1092   unsigned int core_num_syms ;
1093   char *strtab ;
1094   char *core_strtab ;
1095   struct module_sect_attrs *sect_attrs ;
1096   struct module_notes_attrs *notes_attrs ;
1097   char *args ;
1098   void *percpu ;
1099   unsigned int percpu_size ;
1100   unsigned int num_tracepoints ;
1101   struct tracepoint * const  *tracepoints_ptrs ;
1102   unsigned int num_trace_bprintk_fmt ;
1103   char const   **trace_bprintk_fmt_start ;
1104   struct ftrace_event_call **trace_events ;
1105   unsigned int num_trace_events ;
1106   struct list_head source_list ;
1107   struct list_head target_list ;
1108   struct task_struct *waiter ;
1109   void (*exit)(void) ;
1110   struct module_ref *refptr ;
1111   ctor_fn_t *ctors ;
1112   unsigned int num_ctors ;
1113};
1114#line 31 "include/linux/uio.h"
1115struct kvec {
1116   void *iov_base ;
1117   size_t iov_len ;
1118};
1119#line 19 "include/linux/klist.h"
1120struct klist_node;
1121#line 19
1122struct klist_node;
1123#line 39 "include/linux/klist.h"
1124struct klist_node {
1125   void *n_klist ;
1126   struct list_head n_node ;
1127   struct kref n_ref ;
1128};
1129#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1130struct dma_map_ops;
1131#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1132struct dev_archdata {
1133   void *acpi_handle ;
1134   struct dma_map_ops *dma_ops ;
1135   void *iommu ;
1136};
1137#line 28 "include/linux/device.h"
1138struct device;
1139#line 29
1140struct device_private;
1141#line 29
1142struct device_private;
1143#line 30
1144struct device_driver;
1145#line 30
1146struct device_driver;
1147#line 31
1148struct driver_private;
1149#line 31
1150struct driver_private;
1151#line 32
1152struct module;
1153#line 33
1154struct class;
1155#line 33
1156struct class;
1157#line 34
1158struct subsys_private;
1159#line 34
1160struct subsys_private;
1161#line 35
1162struct bus_type;
1163#line 35
1164struct bus_type;
1165#line 36
1166struct device_node;
1167#line 36
1168struct device_node;
1169#line 37
1170struct iommu_ops;
1171#line 37
1172struct iommu_ops;
1173#line 39 "include/linux/device.h"
1174struct bus_attribute {
1175   struct attribute attr ;
1176   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
1177   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
1178};
1179#line 89
1180struct device_attribute;
1181#line 89
1182struct driver_attribute;
1183#line 89 "include/linux/device.h"
1184struct bus_type {
1185   char const   *name ;
1186   char const   *dev_name ;
1187   struct device *dev_root ;
1188   struct bus_attribute *bus_attrs ;
1189   struct device_attribute *dev_attrs ;
1190   struct driver_attribute *drv_attrs ;
1191   int (*match)(struct device *dev , struct device_driver *drv ) ;
1192   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1193   int (*probe)(struct device *dev ) ;
1194   int (*remove)(struct device *dev ) ;
1195   void (*shutdown)(struct device *dev ) ;
1196   int (*suspend)(struct device *dev , pm_message_t state ) ;
1197   int (*resume)(struct device *dev ) ;
1198   struct dev_pm_ops  const  *pm ;
1199   struct iommu_ops *iommu_ops ;
1200   struct subsys_private *p ;
1201};
1202#line 127
1203struct device_type;
1204#line 159
1205struct notifier_block;
1206#line 214
1207struct of_device_id;
1208#line 214 "include/linux/device.h"
1209struct device_driver {
1210   char const   *name ;
1211   struct bus_type *bus ;
1212   struct module *owner ;
1213   char const   *mod_name ;
1214   bool suppress_bind_attrs ;
1215   struct of_device_id  const  *of_match_table ;
1216   int (*probe)(struct device *dev ) ;
1217   int (*remove)(struct device *dev ) ;
1218   void (*shutdown)(struct device *dev ) ;
1219   int (*suspend)(struct device *dev , pm_message_t state ) ;
1220   int (*resume)(struct device *dev ) ;
1221   struct attribute_group  const  **groups ;
1222   struct dev_pm_ops  const  *pm ;
1223   struct driver_private *p ;
1224};
1225#line 249 "include/linux/device.h"
1226struct driver_attribute {
1227   struct attribute attr ;
1228   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1229   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
1230};
1231#line 330
1232struct class_attribute;
1233#line 330 "include/linux/device.h"
1234struct class {
1235   char const   *name ;
1236   struct module *owner ;
1237   struct class_attribute *class_attrs ;
1238   struct device_attribute *dev_attrs ;
1239   struct bin_attribute *dev_bin_attrs ;
1240   struct kobject *dev_kobj ;
1241   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1242   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1243   void (*class_release)(struct class *class ) ;
1244   void (*dev_release)(struct device *dev ) ;
1245   int (*suspend)(struct device *dev , pm_message_t state ) ;
1246   int (*resume)(struct device *dev ) ;
1247   struct kobj_ns_type_operations  const  *ns_type ;
1248   void const   *(*namespace)(struct device *dev ) ;
1249   struct dev_pm_ops  const  *pm ;
1250   struct subsys_private *p ;
1251};
1252#line 397 "include/linux/device.h"
1253struct class_attribute {
1254   struct attribute attr ;
1255   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1256   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
1257                    size_t count ) ;
1258   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
1259};
1260#line 465 "include/linux/device.h"
1261struct device_type {
1262   char const   *name ;
1263   struct attribute_group  const  **groups ;
1264   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1265   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1266   void (*release)(struct device *dev ) ;
1267   struct dev_pm_ops  const  *pm ;
1268};
1269#line 476 "include/linux/device.h"
1270struct device_attribute {
1271   struct attribute attr ;
1272   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1273   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
1274                    size_t count ) ;
1275};
1276#line 559 "include/linux/device.h"
1277struct device_dma_parameters {
1278   unsigned int max_segment_size ;
1279   unsigned long segment_boundary_mask ;
1280};
1281#line 627
1282struct dma_coherent_mem;
1283#line 627 "include/linux/device.h"
1284struct device {
1285   struct device *parent ;
1286   struct device_private *p ;
1287   struct kobject kobj ;
1288   char const   *init_name ;
1289   struct device_type  const  *type ;
1290   struct mutex mutex ;
1291   struct bus_type *bus ;
1292   struct device_driver *driver ;
1293   void *platform_data ;
1294   struct dev_pm_info power ;
1295   struct dev_pm_domain *pm_domain ;
1296   int numa_node ;
1297   u64 *dma_mask ;
1298   u64 coherent_dma_mask ;
1299   struct device_dma_parameters *dma_parms ;
1300   struct list_head dma_pools ;
1301   struct dma_coherent_mem *dma_mem ;
1302   struct dev_archdata archdata ;
1303   struct device_node *of_node ;
1304   dev_t devt ;
1305   u32 id ;
1306   spinlock_t devres_lock ;
1307   struct list_head devres_head ;
1308   struct klist_node knode_class ;
1309   struct class *class ;
1310   struct attribute_group  const  **groups ;
1311   void (*release)(struct device *dev ) ;
1312};
1313#line 43 "include/linux/pm_wakeup.h"
1314struct wakeup_source {
1315   char const   *name ;
1316   struct list_head entry ;
1317   spinlock_t lock ;
1318   struct timer_list timer ;
1319   unsigned long timer_expires ;
1320   ktime_t total_time ;
1321   ktime_t max_time ;
1322   ktime_t last_time ;
1323   unsigned long event_count ;
1324   unsigned long active_count ;
1325   unsigned long relax_count ;
1326   unsigned long hit_count ;
1327   unsigned int active : 1 ;
1328};
1329#line 143 "include/mtd/mtd-abi.h"
1330struct otp_info {
1331   __u32 start ;
1332   __u32 length ;
1333   __u32 locked ;
1334};
1335#line 217 "include/mtd/mtd-abi.h"
1336struct nand_oobfree {
1337   __u32 offset ;
1338   __u32 length ;
1339};
1340#line 247 "include/mtd/mtd-abi.h"
1341struct mtd_ecc_stats {
1342   __u32 corrected ;
1343   __u32 failed ;
1344   __u32 badblocks ;
1345   __u32 bbtblocks ;
1346};
1347#line 48 "include/linux/mtd/mtd.h"
1348struct mtd_info;
1349#line 48 "include/linux/mtd/mtd.h"
1350struct erase_info {
1351   struct mtd_info *mtd ;
1352   uint64_t addr ;
1353   uint64_t len ;
1354   uint64_t fail_addr ;
1355   u_long time ;
1356   u_long retries ;
1357   unsigned int dev ;
1358   unsigned int cell ;
1359   void (*callback)(struct erase_info *self ) ;
1360   u_long priv ;
1361   u_char state ;
1362   struct erase_info *next ;
1363};
1364#line 63 "include/linux/mtd/mtd.h"
1365struct mtd_erase_region_info {
1366   uint64_t offset ;
1367   uint32_t erasesize ;
1368   uint32_t numblocks ;
1369   unsigned long *lockmap ;
1370};
1371#line 89 "include/linux/mtd/mtd.h"
1372struct mtd_oob_ops {
1373   unsigned int mode ;
1374   size_t len ;
1375   size_t retlen ;
1376   size_t ooblen ;
1377   size_t oobretlen ;
1378   uint32_t ooboffs ;
1379   uint8_t *datbuf ;
1380   uint8_t *oobbuf ;
1381};
1382#line 108 "include/linux/mtd/mtd.h"
1383struct nand_ecclayout {
1384   __u32 eccbytes ;
1385   __u32 eccpos[448] ;
1386   __u32 oobavail ;
1387   struct nand_oobfree oobfree[32] ;
1388};
1389#line 115
1390struct module;
1391#line 117
1392struct backing_dev_info;
1393#line 117 "include/linux/mtd/mtd.h"
1394struct mtd_info {
1395   u_char type ;
1396   uint32_t flags ;
1397   uint64_t size ;
1398   uint32_t erasesize ;
1399   uint32_t writesize ;
1400   uint32_t writebufsize ;
1401   uint32_t oobsize ;
1402   uint32_t oobavail ;
1403   unsigned int erasesize_shift ;
1404   unsigned int writesize_shift ;
1405   unsigned int erasesize_mask ;
1406   unsigned int writesize_mask ;
1407   char const   *name ;
1408   int index ;
1409   struct nand_ecclayout *ecclayout ;
1410   unsigned int ecc_strength ;
1411   int numeraseregions ;
1412   struct mtd_erase_region_info *eraseregions ;
1413   int (*_erase)(struct mtd_info *mtd , struct erase_info *instr ) ;
1414   int (*_point)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1415                 void **virt , resource_size_t *phys ) ;
1416   int (*_unpoint)(struct mtd_info *mtd , loff_t from , size_t len ) ;
1417   unsigned long (*_get_unmapped_area)(struct mtd_info *mtd , unsigned long len ,
1418                                       unsigned long offset , unsigned long flags ) ;
1419   int (*_read)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1420                u_char *buf ) ;
1421   int (*_write)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1422                 u_char const   *buf ) ;
1423   int (*_panic_write)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1424                       u_char const   *buf ) ;
1425   int (*_read_oob)(struct mtd_info *mtd , loff_t from , struct mtd_oob_ops *ops ) ;
1426   int (*_write_oob)(struct mtd_info *mtd , loff_t to , struct mtd_oob_ops *ops ) ;
1427   int (*_get_fact_prot_info)(struct mtd_info *mtd , struct otp_info *buf , size_t len ) ;
1428   int (*_read_fact_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1429                              u_char *buf ) ;
1430   int (*_get_user_prot_info)(struct mtd_info *mtd , struct otp_info *buf , size_t len ) ;
1431   int (*_read_user_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1432                              u_char *buf ) ;
1433   int (*_write_user_prot_reg)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1434                               u_char *buf ) ;
1435   int (*_lock_user_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len ) ;
1436   int (*_writev)(struct mtd_info *mtd , struct kvec  const  *vecs , unsigned long count ,
1437                  loff_t to , size_t *retlen ) ;
1438   void (*_sync)(struct mtd_info *mtd ) ;
1439   int (*_lock)(struct mtd_info *mtd , loff_t ofs , uint64_t len ) ;
1440   int (*_unlock)(struct mtd_info *mtd , loff_t ofs , uint64_t len ) ;
1441   int (*_is_locked)(struct mtd_info *mtd , loff_t ofs , uint64_t len ) ;
1442   int (*_block_isbad)(struct mtd_info *mtd , loff_t ofs ) ;
1443   int (*_block_markbad)(struct mtd_info *mtd , loff_t ofs ) ;
1444   int (*_suspend)(struct mtd_info *mtd ) ;
1445   void (*_resume)(struct mtd_info *mtd ) ;
1446   int (*_get_device)(struct mtd_info *mtd ) ;
1447   void (*_put_device)(struct mtd_info *mtd ) ;
1448   struct backing_dev_info *backing_dev_info ;
1449   struct notifier_block reboot_notifier ;
1450   struct mtd_ecc_stats ecc_stats ;
1451   int subpage_sft ;
1452   void *priv ;
1453   struct module *owner ;
1454   struct device dev ;
1455   int usecount ;
1456};
1457#line 359
1458struct mtd_partition;
1459#line 359
1460struct mtd_partition;
1461#line 360
1462struct mtd_part_parser_data;
1463#line 360
1464struct mtd_part_parser_data;
1465#line 39 "include/linux/mtd/partitions.h"
1466struct mtd_partition {
1467   char *name ;
1468   uint64_t size ;
1469   uint64_t offset ;
1470   uint32_t mask_flags ;
1471   struct nand_ecclayout *ecclayout ;
1472};
1473#line 53
1474struct mtd_info;
1475#line 54
1476struct device_node;
1477#line 61 "include/linux/mtd/partitions.h"
1478struct mtd_part_parser_data {
1479   unsigned long origin ;
1480   struct device_node *of_node ;
1481};
1482#line 18 "include/linux/capability.h"
1483struct task_struct;
1484#line 94 "include/linux/capability.h"
1485struct kernel_cap_struct {
1486   __u32 cap[2] ;
1487};
1488#line 94 "include/linux/capability.h"
1489typedef struct kernel_cap_struct kernel_cap_t;
1490#line 378
1491struct user_namespace;
1492#line 378
1493struct user_namespace;
1494#line 14 "include/linux/prio_tree.h"
1495struct prio_tree_node;
1496#line 14 "include/linux/prio_tree.h"
1497struct raw_prio_tree_node {
1498   struct prio_tree_node *left ;
1499   struct prio_tree_node *right ;
1500   struct prio_tree_node *parent ;
1501};
1502#line 20 "include/linux/prio_tree.h"
1503struct prio_tree_node {
1504   struct prio_tree_node *left ;
1505   struct prio_tree_node *right ;
1506   struct prio_tree_node *parent ;
1507   unsigned long start ;
1508   unsigned long last ;
1509};
1510#line 23 "include/linux/mm_types.h"
1511struct address_space;
1512#line 23
1513struct address_space;
1514#line 40 "include/linux/mm_types.h"
1515union __anonunion____missing_field_name_204 {
1516   unsigned long index ;
1517   void *freelist ;
1518};
1519#line 40 "include/linux/mm_types.h"
1520struct __anonstruct____missing_field_name_208 {
1521   unsigned int inuse : 16 ;
1522   unsigned int objects : 15 ;
1523   unsigned int frozen : 1 ;
1524};
1525#line 40 "include/linux/mm_types.h"
1526union __anonunion____missing_field_name_207 {
1527   atomic_t _mapcount ;
1528   struct __anonstruct____missing_field_name_208 __annonCompField34 ;
1529};
1530#line 40 "include/linux/mm_types.h"
1531struct __anonstruct____missing_field_name_206 {
1532   union __anonunion____missing_field_name_207 __annonCompField35 ;
1533   atomic_t _count ;
1534};
1535#line 40 "include/linux/mm_types.h"
1536union __anonunion____missing_field_name_205 {
1537   unsigned long counters ;
1538   struct __anonstruct____missing_field_name_206 __annonCompField36 ;
1539};
1540#line 40 "include/linux/mm_types.h"
1541struct __anonstruct____missing_field_name_203 {
1542   union __anonunion____missing_field_name_204 __annonCompField33 ;
1543   union __anonunion____missing_field_name_205 __annonCompField37 ;
1544};
1545#line 40 "include/linux/mm_types.h"
1546struct __anonstruct____missing_field_name_210 {
1547   struct page *next ;
1548   int pages ;
1549   int pobjects ;
1550};
1551#line 40 "include/linux/mm_types.h"
1552union __anonunion____missing_field_name_209 {
1553   struct list_head lru ;
1554   struct __anonstruct____missing_field_name_210 __annonCompField39 ;
1555};
1556#line 40 "include/linux/mm_types.h"
1557union __anonunion____missing_field_name_211 {
1558   unsigned long private ;
1559   struct kmem_cache *slab ;
1560   struct page *first_page ;
1561};
1562#line 40 "include/linux/mm_types.h"
1563struct page {
1564   unsigned long flags ;
1565   struct address_space *mapping ;
1566   struct __anonstruct____missing_field_name_203 __annonCompField38 ;
1567   union __anonunion____missing_field_name_209 __annonCompField40 ;
1568   union __anonunion____missing_field_name_211 __annonCompField41 ;
1569   unsigned long debug_flags ;
1570} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1571#line 200 "include/linux/mm_types.h"
1572struct __anonstruct_vm_set_213 {
1573   struct list_head list ;
1574   void *parent ;
1575   struct vm_area_struct *head ;
1576};
1577#line 200 "include/linux/mm_types.h"
1578union __anonunion_shared_212 {
1579   struct __anonstruct_vm_set_213 vm_set ;
1580   struct raw_prio_tree_node prio_tree_node ;
1581};
1582#line 200
1583struct anon_vma;
1584#line 200
1585struct vm_operations_struct;
1586#line 200
1587struct mempolicy;
1588#line 200 "include/linux/mm_types.h"
1589struct vm_area_struct {
1590   struct mm_struct *vm_mm ;
1591   unsigned long vm_start ;
1592   unsigned long vm_end ;
1593   struct vm_area_struct *vm_next ;
1594   struct vm_area_struct *vm_prev ;
1595   pgprot_t vm_page_prot ;
1596   unsigned long vm_flags ;
1597   struct rb_node vm_rb ;
1598   union __anonunion_shared_212 shared ;
1599   struct list_head anon_vma_chain ;
1600   struct anon_vma *anon_vma ;
1601   struct vm_operations_struct  const  *vm_ops ;
1602   unsigned long vm_pgoff ;
1603   struct file *vm_file ;
1604   void *vm_private_data ;
1605   struct mempolicy *vm_policy ;
1606};
1607#line 257 "include/linux/mm_types.h"
1608struct core_thread {
1609   struct task_struct *task ;
1610   struct core_thread *next ;
1611};
1612#line 262 "include/linux/mm_types.h"
1613struct core_state {
1614   atomic_t nr_threads ;
1615   struct core_thread dumper ;
1616   struct completion startup ;
1617};
1618#line 284 "include/linux/mm_types.h"
1619struct mm_rss_stat {
1620   atomic_long_t count[3] ;
1621};
1622#line 288
1623struct linux_binfmt;
1624#line 288
1625struct mmu_notifier_mm;
1626#line 288 "include/linux/mm_types.h"
1627struct mm_struct {
1628   struct vm_area_struct *mmap ;
1629   struct rb_root mm_rb ;
1630   struct vm_area_struct *mmap_cache ;
1631   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
1632                                      unsigned long pgoff , unsigned long flags ) ;
1633   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
1634   unsigned long mmap_base ;
1635   unsigned long task_size ;
1636   unsigned long cached_hole_size ;
1637   unsigned long free_area_cache ;
1638   pgd_t *pgd ;
1639   atomic_t mm_users ;
1640   atomic_t mm_count ;
1641   int map_count ;
1642   spinlock_t page_table_lock ;
1643   struct rw_semaphore mmap_sem ;
1644   struct list_head mmlist ;
1645   unsigned long hiwater_rss ;
1646   unsigned long hiwater_vm ;
1647   unsigned long total_vm ;
1648   unsigned long locked_vm ;
1649   unsigned long pinned_vm ;
1650   unsigned long shared_vm ;
1651   unsigned long exec_vm ;
1652   unsigned long stack_vm ;
1653   unsigned long reserved_vm ;
1654   unsigned long def_flags ;
1655   unsigned long nr_ptes ;
1656   unsigned long start_code ;
1657   unsigned long end_code ;
1658   unsigned long start_data ;
1659   unsigned long end_data ;
1660   unsigned long start_brk ;
1661   unsigned long brk ;
1662   unsigned long start_stack ;
1663   unsigned long arg_start ;
1664   unsigned long arg_end ;
1665   unsigned long env_start ;
1666   unsigned long env_end ;
1667   unsigned long saved_auxv[44] ;
1668   struct mm_rss_stat rss_stat ;
1669   struct linux_binfmt *binfmt ;
1670   cpumask_var_t cpu_vm_mask_var ;
1671   mm_context_t context ;
1672   unsigned int faultstamp ;
1673   unsigned int token_priority ;
1674   unsigned int last_interval ;
1675   unsigned long flags ;
1676   struct core_state *core_state ;
1677   spinlock_t ioctx_lock ;
1678   struct hlist_head ioctx_list ;
1679   struct task_struct *owner ;
1680   struct file *exe_file ;
1681   unsigned long num_exe_file_vmas ;
1682   struct mmu_notifier_mm *mmu_notifier_mm ;
1683   pgtable_t pmd_huge_pte ;
1684   struct cpumask cpumask_allocation ;
1685};
1686#line 7 "include/asm-generic/cputime.h"
1687typedef unsigned long cputime_t;
1688#line 84 "include/linux/sem.h"
1689struct task_struct;
1690#line 101
1691struct sem_undo_list;
1692#line 101 "include/linux/sem.h"
1693struct sysv_sem {
1694   struct sem_undo_list *undo_list ;
1695};
1696#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1697struct siginfo;
1698#line 10
1699struct siginfo;
1700#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1701struct __anonstruct_sigset_t_215 {
1702   unsigned long sig[1] ;
1703};
1704#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1705typedef struct __anonstruct_sigset_t_215 sigset_t;
1706#line 17 "include/asm-generic/signal-defs.h"
1707typedef void __signalfn_t(int  );
1708#line 18 "include/asm-generic/signal-defs.h"
1709typedef __signalfn_t *__sighandler_t;
1710#line 20 "include/asm-generic/signal-defs.h"
1711typedef void __restorefn_t(void);
1712#line 21 "include/asm-generic/signal-defs.h"
1713typedef __restorefn_t *__sigrestore_t;
1714#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1715struct sigaction {
1716   __sighandler_t sa_handler ;
1717   unsigned long sa_flags ;
1718   __sigrestore_t sa_restorer ;
1719   sigset_t sa_mask ;
1720};
1721#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1722struct k_sigaction {
1723   struct sigaction sa ;
1724};
1725#line 7 "include/asm-generic/siginfo.h"
1726union sigval {
1727   int sival_int ;
1728   void *sival_ptr ;
1729};
1730#line 7 "include/asm-generic/siginfo.h"
1731typedef union sigval sigval_t;
1732#line 48 "include/asm-generic/siginfo.h"
1733struct __anonstruct__kill_217 {
1734   __kernel_pid_t _pid ;
1735   __kernel_uid32_t _uid ;
1736};
1737#line 48 "include/asm-generic/siginfo.h"
1738struct __anonstruct__timer_218 {
1739   __kernel_timer_t _tid ;
1740   int _overrun ;
1741   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
1742   sigval_t _sigval ;
1743   int _sys_private ;
1744};
1745#line 48 "include/asm-generic/siginfo.h"
1746struct __anonstruct__rt_219 {
1747   __kernel_pid_t _pid ;
1748   __kernel_uid32_t _uid ;
1749   sigval_t _sigval ;
1750};
1751#line 48 "include/asm-generic/siginfo.h"
1752struct __anonstruct__sigchld_220 {
1753   __kernel_pid_t _pid ;
1754   __kernel_uid32_t _uid ;
1755   int _status ;
1756   __kernel_clock_t _utime ;
1757   __kernel_clock_t _stime ;
1758};
1759#line 48 "include/asm-generic/siginfo.h"
1760struct __anonstruct__sigfault_221 {
1761   void *_addr ;
1762   short _addr_lsb ;
1763};
1764#line 48 "include/asm-generic/siginfo.h"
1765struct __anonstruct__sigpoll_222 {
1766   long _band ;
1767   int _fd ;
1768};
1769#line 48 "include/asm-generic/siginfo.h"
1770union __anonunion__sifields_216 {
1771   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
1772   struct __anonstruct__kill_217 _kill ;
1773   struct __anonstruct__timer_218 _timer ;
1774   struct __anonstruct__rt_219 _rt ;
1775   struct __anonstruct__sigchld_220 _sigchld ;
1776   struct __anonstruct__sigfault_221 _sigfault ;
1777   struct __anonstruct__sigpoll_222 _sigpoll ;
1778};
1779#line 48 "include/asm-generic/siginfo.h"
1780struct siginfo {
1781   int si_signo ;
1782   int si_errno ;
1783   int si_code ;
1784   union __anonunion__sifields_216 _sifields ;
1785};
1786#line 48 "include/asm-generic/siginfo.h"
1787typedef struct siginfo siginfo_t;
1788#line 288
1789struct siginfo;
1790#line 10 "include/linux/signal.h"
1791struct task_struct;
1792#line 18
1793struct user_struct;
1794#line 28 "include/linux/signal.h"
1795struct sigpending {
1796   struct list_head list ;
1797   sigset_t signal ;
1798};
1799#line 239
1800struct timespec;
1801#line 240
1802struct pt_regs;
1803#line 50 "include/linux/pid.h"
1804struct pid_namespace;
1805#line 50 "include/linux/pid.h"
1806struct upid {
1807   int nr ;
1808   struct pid_namespace *ns ;
1809   struct hlist_node pid_chain ;
1810};
1811#line 57 "include/linux/pid.h"
1812struct pid {
1813   atomic_t count ;
1814   unsigned int level ;
1815   struct hlist_head tasks[3] ;
1816   struct rcu_head rcu ;
1817   struct upid numbers[1] ;
1818};
1819#line 69 "include/linux/pid.h"
1820struct pid_link {
1821   struct hlist_node node ;
1822   struct pid *pid ;
1823};
1824#line 100
1825struct pid_namespace;
1826#line 10 "include/linux/seccomp.h"
1827struct __anonstruct_seccomp_t_225 {
1828   int mode ;
1829};
1830#line 10 "include/linux/seccomp.h"
1831typedef struct __anonstruct_seccomp_t_225 seccomp_t;
1832#line 81 "include/linux/plist.h"
1833struct plist_head {
1834   struct list_head node_list ;
1835};
1836#line 85 "include/linux/plist.h"
1837struct plist_node {
1838   int prio ;
1839   struct list_head prio_list ;
1840   struct list_head node_list ;
1841};
1842#line 40 "include/linux/rtmutex.h"
1843struct rt_mutex_waiter;
1844#line 40
1845struct rt_mutex_waiter;
1846#line 42 "include/linux/resource.h"
1847struct rlimit {
1848   unsigned long rlim_cur ;
1849   unsigned long rlim_max ;
1850};
1851#line 81
1852struct task_struct;
1853#line 8 "include/linux/timerqueue.h"
1854struct timerqueue_node {
1855   struct rb_node node ;
1856   ktime_t expires ;
1857};
1858#line 13 "include/linux/timerqueue.h"
1859struct timerqueue_head {
1860   struct rb_root head ;
1861   struct timerqueue_node *next ;
1862};
1863#line 27 "include/linux/hrtimer.h"
1864struct hrtimer_clock_base;
1865#line 27
1866struct hrtimer_clock_base;
1867#line 28
1868struct hrtimer_cpu_base;
1869#line 28
1870struct hrtimer_cpu_base;
1871#line 44
1872enum hrtimer_restart {
1873    HRTIMER_NORESTART = 0,
1874    HRTIMER_RESTART = 1
1875} ;
1876#line 108 "include/linux/hrtimer.h"
1877struct hrtimer {
1878   struct timerqueue_node node ;
1879   ktime_t _softexpires ;
1880   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1881   struct hrtimer_clock_base *base ;
1882   unsigned long state ;
1883   int start_pid ;
1884   void *start_site ;
1885   char start_comm[16] ;
1886};
1887#line 145 "include/linux/hrtimer.h"
1888struct hrtimer_clock_base {
1889   struct hrtimer_cpu_base *cpu_base ;
1890   int index ;
1891   clockid_t clockid ;
1892   struct timerqueue_head active ;
1893   ktime_t resolution ;
1894   ktime_t (*get_time)(void) ;
1895   ktime_t softirq_time ;
1896   ktime_t offset ;
1897};
1898#line 178 "include/linux/hrtimer.h"
1899struct hrtimer_cpu_base {
1900   raw_spinlock_t lock ;
1901   unsigned long active_bases ;
1902   ktime_t expires_next ;
1903   int hres_active ;
1904   int hang_detected ;
1905   unsigned long nr_events ;
1906   unsigned long nr_retries ;
1907   unsigned long nr_hangs ;
1908   ktime_t max_hang_time ;
1909   struct hrtimer_clock_base clock_base[3] ;
1910};
1911#line 11 "include/linux/task_io_accounting.h"
1912struct task_io_accounting {
1913   u64 rchar ;
1914   u64 wchar ;
1915   u64 syscr ;
1916   u64 syscw ;
1917   u64 read_bytes ;
1918   u64 write_bytes ;
1919   u64 cancelled_write_bytes ;
1920};
1921#line 13 "include/linux/latencytop.h"
1922struct task_struct;
1923#line 20 "include/linux/latencytop.h"
1924struct latency_record {
1925   unsigned long backtrace[12] ;
1926   unsigned int count ;
1927   unsigned long time ;
1928   unsigned long max ;
1929};
1930#line 29 "include/linux/key.h"
1931typedef int32_t key_serial_t;
1932#line 32 "include/linux/key.h"
1933typedef uint32_t key_perm_t;
1934#line 34
1935struct key;
1936#line 34
1937struct key;
1938#line 75
1939struct user_struct;
1940#line 76
1941struct signal_struct;
1942#line 76
1943struct signal_struct;
1944#line 77
1945struct cred;
1946#line 79
1947struct key_type;
1948#line 79
1949struct key_type;
1950#line 81
1951struct keyring_list;
1952#line 81
1953struct keyring_list;
1954#line 124
1955struct key_user;
1956#line 124 "include/linux/key.h"
1957union __anonunion____missing_field_name_226 {
1958   time_t expiry ;
1959   time_t revoked_at ;
1960};
1961#line 124 "include/linux/key.h"
1962union __anonunion_type_data_227 {
1963   struct list_head link ;
1964   unsigned long x[2] ;
1965   void *p[2] ;
1966   int reject_error ;
1967};
1968#line 124 "include/linux/key.h"
1969union __anonunion_payload_228 {
1970   unsigned long value ;
1971   void *rcudata ;
1972   void *data ;
1973   struct keyring_list *subscriptions ;
1974};
1975#line 124 "include/linux/key.h"
1976struct key {
1977   atomic_t usage ;
1978   key_serial_t serial ;
1979   struct rb_node serial_node ;
1980   struct key_type *type ;
1981   struct rw_semaphore sem ;
1982   struct key_user *user ;
1983   void *security ;
1984   union __anonunion____missing_field_name_226 __annonCompField42 ;
1985   uid_t uid ;
1986   gid_t gid ;
1987   key_perm_t perm ;
1988   unsigned short quotalen ;
1989   unsigned short datalen ;
1990   unsigned long flags ;
1991   char *description ;
1992   union __anonunion_type_data_227 type_data ;
1993   union __anonunion_payload_228 payload ;
1994};
1995#line 18 "include/linux/selinux.h"
1996struct audit_context;
1997#line 18
1998struct audit_context;
1999#line 21 "include/linux/cred.h"
2000struct user_struct;
2001#line 22
2002struct cred;
2003#line 31 "include/linux/cred.h"
2004struct group_info {
2005   atomic_t usage ;
2006   int ngroups ;
2007   int nblocks ;
2008   gid_t small_block[32] ;
2009   gid_t *blocks[0] ;
2010};
2011#line 83 "include/linux/cred.h"
2012struct thread_group_cred {
2013   atomic_t usage ;
2014   pid_t tgid ;
2015   spinlock_t lock ;
2016   struct key *session_keyring ;
2017   struct key *process_keyring ;
2018   struct rcu_head rcu ;
2019};
2020#line 116 "include/linux/cred.h"
2021struct cred {
2022   atomic_t usage ;
2023   atomic_t subscribers ;
2024   void *put_addr ;
2025   unsigned int magic ;
2026   uid_t uid ;
2027   gid_t gid ;
2028   uid_t suid ;
2029   gid_t sgid ;
2030   uid_t euid ;
2031   gid_t egid ;
2032   uid_t fsuid ;
2033   gid_t fsgid ;
2034   unsigned int securebits ;
2035   kernel_cap_t cap_inheritable ;
2036   kernel_cap_t cap_permitted ;
2037   kernel_cap_t cap_effective ;
2038   kernel_cap_t cap_bset ;
2039   unsigned char jit_keyring ;
2040   struct key *thread_keyring ;
2041   struct key *request_key_auth ;
2042   struct thread_group_cred *tgcred ;
2043   void *security ;
2044   struct user_struct *user ;
2045   struct user_namespace *user_ns ;
2046   struct group_info *group_info ;
2047   struct rcu_head rcu ;
2048};
2049#line 61 "include/linux/llist.h"
2050struct llist_node;
2051#line 65 "include/linux/llist.h"
2052struct llist_node {
2053   struct llist_node *next ;
2054};
2055#line 97 "include/linux/sched.h"
2056struct futex_pi_state;
2057#line 97
2058struct futex_pi_state;
2059#line 98
2060struct robust_list_head;
2061#line 98
2062struct robust_list_head;
2063#line 99
2064struct bio_list;
2065#line 99
2066struct bio_list;
2067#line 100
2068struct fs_struct;
2069#line 100
2070struct fs_struct;
2071#line 101
2072struct perf_event_context;
2073#line 101
2074struct perf_event_context;
2075#line 102
2076struct blk_plug;
2077#line 102
2078struct blk_plug;
2079#line 151
2080struct cfs_rq;
2081#line 151
2082struct cfs_rq;
2083#line 259
2084struct task_struct;
2085#line 366
2086struct nsproxy;
2087#line 367
2088struct user_namespace;
2089#line 214 "include/linux/aio.h"
2090struct mm_struct;
2091#line 443 "include/linux/sched.h"
2092struct sighand_struct {
2093   atomic_t count ;
2094   struct k_sigaction action[64] ;
2095   spinlock_t siglock ;
2096   wait_queue_head_t signalfd_wqh ;
2097};
2098#line 450 "include/linux/sched.h"
2099struct pacct_struct {
2100   int ac_flag ;
2101   long ac_exitcode ;
2102   unsigned long ac_mem ;
2103   cputime_t ac_utime ;
2104   cputime_t ac_stime ;
2105   unsigned long ac_minflt ;
2106   unsigned long ac_majflt ;
2107};
2108#line 458 "include/linux/sched.h"
2109struct cpu_itimer {
2110   cputime_t expires ;
2111   cputime_t incr ;
2112   u32 error ;
2113   u32 incr_error ;
2114};
2115#line 476 "include/linux/sched.h"
2116struct task_cputime {
2117   cputime_t utime ;
2118   cputime_t stime ;
2119   unsigned long long sum_exec_runtime ;
2120};
2121#line 512 "include/linux/sched.h"
2122struct thread_group_cputimer {
2123   struct task_cputime cputime ;
2124   int running ;
2125   raw_spinlock_t lock ;
2126};
2127#line 519
2128struct autogroup;
2129#line 519
2130struct autogroup;
2131#line 528
2132struct tty_struct;
2133#line 528
2134struct taskstats;
2135#line 528
2136struct tty_audit_buf;
2137#line 528 "include/linux/sched.h"
2138struct signal_struct {
2139   atomic_t sigcnt ;
2140   atomic_t live ;
2141   int nr_threads ;
2142   wait_queue_head_t wait_chldexit ;
2143   struct task_struct *curr_target ;
2144   struct sigpending shared_pending ;
2145   int group_exit_code ;
2146   int notify_count ;
2147   struct task_struct *group_exit_task ;
2148   int group_stop_count ;
2149   unsigned int flags ;
2150   unsigned int is_child_subreaper : 1 ;
2151   unsigned int has_child_subreaper : 1 ;
2152   struct list_head posix_timers ;
2153   struct hrtimer real_timer ;
2154   struct pid *leader_pid ;
2155   ktime_t it_real_incr ;
2156   struct cpu_itimer it[2] ;
2157   struct thread_group_cputimer cputimer ;
2158   struct task_cputime cputime_expires ;
2159   struct list_head cpu_timers[3] ;
2160   struct pid *tty_old_pgrp ;
2161   int leader ;
2162   struct tty_struct *tty ;
2163   struct autogroup *autogroup ;
2164   cputime_t utime ;
2165   cputime_t stime ;
2166   cputime_t cutime ;
2167   cputime_t cstime ;
2168   cputime_t gtime ;
2169   cputime_t cgtime ;
2170   cputime_t prev_utime ;
2171   cputime_t prev_stime ;
2172   unsigned long nvcsw ;
2173   unsigned long nivcsw ;
2174   unsigned long cnvcsw ;
2175   unsigned long cnivcsw ;
2176   unsigned long min_flt ;
2177   unsigned long maj_flt ;
2178   unsigned long cmin_flt ;
2179   unsigned long cmaj_flt ;
2180   unsigned long inblock ;
2181   unsigned long oublock ;
2182   unsigned long cinblock ;
2183   unsigned long coublock ;
2184   unsigned long maxrss ;
2185   unsigned long cmaxrss ;
2186   struct task_io_accounting ioac ;
2187   unsigned long long sum_sched_runtime ;
2188   struct rlimit rlim[16] ;
2189   struct pacct_struct pacct ;
2190   struct taskstats *stats ;
2191   unsigned int audit_tty ;
2192   struct tty_audit_buf *tty_audit_buf ;
2193   struct rw_semaphore group_rwsem ;
2194   int oom_adj ;
2195   int oom_score_adj ;
2196   int oom_score_adj_min ;
2197   struct mutex cred_guard_mutex ;
2198};
2199#line 703 "include/linux/sched.h"
2200struct user_struct {
2201   atomic_t __count ;
2202   atomic_t processes ;
2203   atomic_t files ;
2204   atomic_t sigpending ;
2205   atomic_t inotify_watches ;
2206   atomic_t inotify_devs ;
2207   atomic_t fanotify_listeners ;
2208   atomic_long_t epoll_watches ;
2209   unsigned long mq_bytes ;
2210   unsigned long locked_shm ;
2211   struct key *uid_keyring ;
2212   struct key *session_keyring ;
2213   struct hlist_node uidhash_node ;
2214   uid_t uid ;
2215   struct user_namespace *user_ns ;
2216   atomic_long_t locked_vm ;
2217};
2218#line 747
2219struct backing_dev_info;
2220#line 748
2221struct reclaim_state;
2222#line 748
2223struct reclaim_state;
2224#line 751 "include/linux/sched.h"
2225struct sched_info {
2226   unsigned long pcount ;
2227   unsigned long long run_delay ;
2228   unsigned long long last_arrival ;
2229   unsigned long long last_queued ;
2230};
2231#line 763 "include/linux/sched.h"
2232struct task_delay_info {
2233   spinlock_t lock ;
2234   unsigned int flags ;
2235   struct timespec blkio_start ;
2236   struct timespec blkio_end ;
2237   u64 blkio_delay ;
2238   u64 swapin_delay ;
2239   u32 blkio_count ;
2240   u32 swapin_count ;
2241   struct timespec freepages_start ;
2242   struct timespec freepages_end ;
2243   u64 freepages_delay ;
2244   u32 freepages_count ;
2245};
2246#line 1088
2247struct io_context;
2248#line 1088
2249struct io_context;
2250#line 1097
2251struct audit_context;
2252#line 1098
2253struct mempolicy;
2254#line 1099
2255struct pipe_inode_info;
2256#line 1099
2257struct pipe_inode_info;
2258#line 1102
2259struct rq;
2260#line 1102
2261struct rq;
2262#line 1122 "include/linux/sched.h"
2263struct sched_class {
2264   struct sched_class  const  *next ;
2265   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2266   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2267   void (*yield_task)(struct rq *rq ) ;
2268   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
2269   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
2270   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
2271   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
2272   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
2273   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
2274   void (*post_schedule)(struct rq *this_rq ) ;
2275   void (*task_waking)(struct task_struct *task ) ;
2276   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
2277   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
2278   void (*rq_online)(struct rq *rq ) ;
2279   void (*rq_offline)(struct rq *rq ) ;
2280   void (*set_curr_task)(struct rq *rq ) ;
2281   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
2282   void (*task_fork)(struct task_struct *p ) ;
2283   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
2284   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
2285   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
2286   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
2287   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
2288};
2289#line 1167 "include/linux/sched.h"
2290struct load_weight {
2291   unsigned long weight ;
2292   unsigned long inv_weight ;
2293};
2294#line 1172 "include/linux/sched.h"
2295struct sched_statistics {
2296   u64 wait_start ;
2297   u64 wait_max ;
2298   u64 wait_count ;
2299   u64 wait_sum ;
2300   u64 iowait_count ;
2301   u64 iowait_sum ;
2302   u64 sleep_start ;
2303   u64 sleep_max ;
2304   s64 sum_sleep_runtime ;
2305   u64 block_start ;
2306   u64 block_max ;
2307   u64 exec_max ;
2308   u64 slice_max ;
2309   u64 nr_migrations_cold ;
2310   u64 nr_failed_migrations_affine ;
2311   u64 nr_failed_migrations_running ;
2312   u64 nr_failed_migrations_hot ;
2313   u64 nr_forced_migrations ;
2314   u64 nr_wakeups ;
2315   u64 nr_wakeups_sync ;
2316   u64 nr_wakeups_migrate ;
2317   u64 nr_wakeups_local ;
2318   u64 nr_wakeups_remote ;
2319   u64 nr_wakeups_affine ;
2320   u64 nr_wakeups_affine_attempts ;
2321   u64 nr_wakeups_passive ;
2322   u64 nr_wakeups_idle ;
2323};
2324#line 1207 "include/linux/sched.h"
2325struct sched_entity {
2326   struct load_weight load ;
2327   struct rb_node run_node ;
2328   struct list_head group_node ;
2329   unsigned int on_rq ;
2330   u64 exec_start ;
2331   u64 sum_exec_runtime ;
2332   u64 vruntime ;
2333   u64 prev_sum_exec_runtime ;
2334   u64 nr_migrations ;
2335   struct sched_statistics statistics ;
2336   struct sched_entity *parent ;
2337   struct cfs_rq *cfs_rq ;
2338   struct cfs_rq *my_q ;
2339};
2340#line 1233
2341struct rt_rq;
2342#line 1233 "include/linux/sched.h"
2343struct sched_rt_entity {
2344   struct list_head run_list ;
2345   unsigned long timeout ;
2346   unsigned int time_slice ;
2347   int nr_cpus_allowed ;
2348   struct sched_rt_entity *back ;
2349   struct sched_rt_entity *parent ;
2350   struct rt_rq *rt_rq ;
2351   struct rt_rq *my_q ;
2352};
2353#line 1264
2354struct files_struct;
2355#line 1264
2356struct css_set;
2357#line 1264
2358struct compat_robust_list_head;
2359#line 1264
2360struct mem_cgroup;
2361#line 1264 "include/linux/sched.h"
2362struct memcg_batch_info {
2363   int do_batch ;
2364   struct mem_cgroup *memcg ;
2365   unsigned long nr_pages ;
2366   unsigned long memsw_nr_pages ;
2367};
2368#line 1264 "include/linux/sched.h"
2369struct task_struct {
2370   long volatile   state ;
2371   void *stack ;
2372   atomic_t usage ;
2373   unsigned int flags ;
2374   unsigned int ptrace ;
2375   struct llist_node wake_entry ;
2376   int on_cpu ;
2377   int on_rq ;
2378   int prio ;
2379   int static_prio ;
2380   int normal_prio ;
2381   unsigned int rt_priority ;
2382   struct sched_class  const  *sched_class ;
2383   struct sched_entity se ;
2384   struct sched_rt_entity rt ;
2385   struct hlist_head preempt_notifiers ;
2386   unsigned char fpu_counter ;
2387   unsigned int policy ;
2388   cpumask_t cpus_allowed ;
2389   struct sched_info sched_info ;
2390   struct list_head tasks ;
2391   struct plist_node pushable_tasks ;
2392   struct mm_struct *mm ;
2393   struct mm_struct *active_mm ;
2394   unsigned int brk_randomized : 1 ;
2395   int exit_state ;
2396   int exit_code ;
2397   int exit_signal ;
2398   int pdeath_signal ;
2399   unsigned int jobctl ;
2400   unsigned int personality ;
2401   unsigned int did_exec : 1 ;
2402   unsigned int in_execve : 1 ;
2403   unsigned int in_iowait : 1 ;
2404   unsigned int sched_reset_on_fork : 1 ;
2405   unsigned int sched_contributes_to_load : 1 ;
2406   unsigned int irq_thread : 1 ;
2407   pid_t pid ;
2408   pid_t tgid ;
2409   unsigned long stack_canary ;
2410   struct task_struct *real_parent ;
2411   struct task_struct *parent ;
2412   struct list_head children ;
2413   struct list_head sibling ;
2414   struct task_struct *group_leader ;
2415   struct list_head ptraced ;
2416   struct list_head ptrace_entry ;
2417   struct pid_link pids[3] ;
2418   struct list_head thread_group ;
2419   struct completion *vfork_done ;
2420   int *set_child_tid ;
2421   int *clear_child_tid ;
2422   cputime_t utime ;
2423   cputime_t stime ;
2424   cputime_t utimescaled ;
2425   cputime_t stimescaled ;
2426   cputime_t gtime ;
2427   cputime_t prev_utime ;
2428   cputime_t prev_stime ;
2429   unsigned long nvcsw ;
2430   unsigned long nivcsw ;
2431   struct timespec start_time ;
2432   struct timespec real_start_time ;
2433   unsigned long min_flt ;
2434   unsigned long maj_flt ;
2435   struct task_cputime cputime_expires ;
2436   struct list_head cpu_timers[3] ;
2437   struct cred  const  *real_cred ;
2438   struct cred  const  *cred ;
2439   struct cred *replacement_session_keyring ;
2440   char comm[16] ;
2441   int link_count ;
2442   int total_link_count ;
2443   struct sysv_sem sysvsem ;
2444   unsigned long last_switch_count ;
2445   struct thread_struct thread ;
2446   struct fs_struct *fs ;
2447   struct files_struct *files ;
2448   struct nsproxy *nsproxy ;
2449   struct signal_struct *signal ;
2450   struct sighand_struct *sighand ;
2451   sigset_t blocked ;
2452   sigset_t real_blocked ;
2453   sigset_t saved_sigmask ;
2454   struct sigpending pending ;
2455   unsigned long sas_ss_sp ;
2456   size_t sas_ss_size ;
2457   int (*notifier)(void *priv ) ;
2458   void *notifier_data ;
2459   sigset_t *notifier_mask ;
2460   struct audit_context *audit_context ;
2461   uid_t loginuid ;
2462   unsigned int sessionid ;
2463   seccomp_t seccomp ;
2464   u32 parent_exec_id ;
2465   u32 self_exec_id ;
2466   spinlock_t alloc_lock ;
2467   raw_spinlock_t pi_lock ;
2468   struct plist_head pi_waiters ;
2469   struct rt_mutex_waiter *pi_blocked_on ;
2470   struct mutex_waiter *blocked_on ;
2471   unsigned int irq_events ;
2472   unsigned long hardirq_enable_ip ;
2473   unsigned long hardirq_disable_ip ;
2474   unsigned int hardirq_enable_event ;
2475   unsigned int hardirq_disable_event ;
2476   int hardirqs_enabled ;
2477   int hardirq_context ;
2478   unsigned long softirq_disable_ip ;
2479   unsigned long softirq_enable_ip ;
2480   unsigned int softirq_disable_event ;
2481   unsigned int softirq_enable_event ;
2482   int softirqs_enabled ;
2483   int softirq_context ;
2484   void *journal_info ;
2485   struct bio_list *bio_list ;
2486   struct blk_plug *plug ;
2487   struct reclaim_state *reclaim_state ;
2488   struct backing_dev_info *backing_dev_info ;
2489   struct io_context *io_context ;
2490   unsigned long ptrace_message ;
2491   siginfo_t *last_siginfo ;
2492   struct task_io_accounting ioac ;
2493   u64 acct_rss_mem1 ;
2494   u64 acct_vm_mem1 ;
2495   cputime_t acct_timexpd ;
2496   nodemask_t mems_allowed ;
2497   seqcount_t mems_allowed_seq ;
2498   int cpuset_mem_spread_rotor ;
2499   int cpuset_slab_spread_rotor ;
2500   struct css_set *cgroups ;
2501   struct list_head cg_list ;
2502   struct robust_list_head *robust_list ;
2503   struct compat_robust_list_head *compat_robust_list ;
2504   struct list_head pi_state_list ;
2505   struct futex_pi_state *pi_state_cache ;
2506   struct perf_event_context *perf_event_ctxp[2] ;
2507   struct mutex perf_event_mutex ;
2508   struct list_head perf_event_list ;
2509   struct mempolicy *mempolicy ;
2510   short il_next ;
2511   short pref_node_fork ;
2512   struct rcu_head rcu ;
2513   struct pipe_inode_info *splice_pipe ;
2514   struct task_delay_info *delays ;
2515   int make_it_fail ;
2516   int nr_dirtied ;
2517   int nr_dirtied_pause ;
2518   unsigned long dirty_paused_when ;
2519   int latency_record_count ;
2520   struct latency_record latency_record[32] ;
2521   unsigned long timer_slack_ns ;
2522   unsigned long default_timer_slack_ns ;
2523   struct list_head *scm_work_list ;
2524   unsigned long trace ;
2525   unsigned long trace_recursion ;
2526   struct memcg_batch_info memcg_batch ;
2527   atomic_t ptrace_bp_refcnt ;
2528};
2529#line 1681
2530struct pid_namespace;
2531#line 31 "include/linux/mtd/flashchip.h"
2532enum __anonenum_flstate_t_232 {
2533    FL_READY = 0,
2534    FL_STATUS = 1,
2535    FL_CFI_QUERY = 2,
2536    FL_JEDEC_QUERY = 3,
2537    FL_ERASING = 4,
2538    FL_ERASE_SUSPENDING = 5,
2539    FL_ERASE_SUSPENDED = 6,
2540    FL_WRITING = 7,
2541    FL_WRITING_TO_BUFFER = 8,
2542    FL_OTP_WRITE = 9,
2543    FL_WRITE_SUSPENDING = 10,
2544    FL_WRITE_SUSPENDED = 11,
2545    FL_PM_SUSPENDED = 12,
2546    FL_SYNCING = 13,
2547    FL_UNLOADING = 14,
2548    FL_LOCKING = 15,
2549    FL_UNLOCKING = 16,
2550    FL_POINT = 17,
2551    FL_XIP_WHILE_ERASING = 18,
2552    FL_XIP_WHILE_WRITING = 19,
2553    FL_SHUTDOWN = 20,
2554    FL_READING = 21,
2555    FL_CACHEDPRG = 22,
2556    FL_RESETING = 23,
2557    FL_OTPING = 24,
2558    FL_PREPARING_ERASE = 25,
2559    FL_VERIFYING_ERASE = 26,
2560    FL_UNKNOWN = 27
2561} ;
2562#line 31 "include/linux/mtd/flashchip.h"
2563typedef enum __anonenum_flstate_t_232 flstate_t;
2564#line 33 "include/linux/mtd/onenand.h"
2565struct onenand_bufferram {
2566   int blockpage ;
2567};
2568#line 87 "include/linux/mtd/onenand.h"
2569struct onenand_chip {
2570   void *base ;
2571   unsigned int dies ;
2572   unsigned int boundary[2] ;
2573   loff_t diesize[2] ;
2574   unsigned int chipsize ;
2575   unsigned int device_id ;
2576   unsigned int version_id ;
2577   unsigned int technology ;
2578   unsigned int density_mask ;
2579   unsigned int options ;
2580   unsigned int erase_shift ;
2581   unsigned int page_shift ;
2582   unsigned int page_mask ;
2583   unsigned int writesize ;
2584   unsigned int bufferram_index ;
2585   struct onenand_bufferram bufferram[2] ;
2586   int (*command)(struct mtd_info *mtd , int cmd , loff_t address , size_t len ) ;
2587   int (*wait)(struct mtd_info *mtd , int state ) ;
2588   int (*bbt_wait)(struct mtd_info *mtd , int state ) ;
2589   void (*unlock_all)(struct mtd_info *mtd ) ;
2590   int (*read_bufferram)(struct mtd_info *mtd , int area , unsigned char *buffer ,
2591                         int offset , size_t count ) ;
2592   int (*write_bufferram)(struct mtd_info *mtd , int area , unsigned char const   *buffer ,
2593                          int offset , size_t count ) ;
2594   unsigned short (*read_word)(void *addr ) ;
2595   void (*write_word)(unsigned short value , void *addr ) ;
2596   void (*mmcontrol)(struct mtd_info *mtd , int sync_read ) ;
2597   int (*chip_probe)(struct mtd_info *mtd ) ;
2598   int (*block_markbad)(struct mtd_info *mtd , loff_t ofs ) ;
2599   int (*scan_bbt)(struct mtd_info *mtd ) ;
2600   int (*enable)(struct mtd_info *mtd ) ;
2601   int (*disable)(struct mtd_info *mtd ) ;
2602   struct completion complete ;
2603   int irq ;
2604   spinlock_t chip_lock ;
2605   wait_queue_head_t wq ;
2606   flstate_t state ;
2607   unsigned char *page_buf ;
2608   unsigned char *oob_buf ;
2609   unsigned char *verify_buf ;
2610   int subpagesize ;
2611   struct nand_ecclayout *ecclayout ;
2612   void *bbm ;
2613   void *priv ;
2614   unsigned int ongoing ;
2615};
2616#line 232
2617struct mtd_partition;
2618#line 25 "include/linux/io.h"
2619struct device;
2620#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2621struct onenand_flash {
2622   void *base ;
2623   void *data ;
2624};
2625#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2626struct onenand_info {
2627   struct mtd_info mtd ;
2628   struct mtd_partition *parts ;
2629   struct onenand_chip onenand ;
2630   struct onenand_flash flash ;
2631};
2632#line 543 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2633struct __anonstruct_233 {
2634   int  : 0 ;
2635};
2636#line 1 "<compiler builtins>"
2637
2638#line 1
2639long __builtin_expect(long val , long res ) ;
2640#line 100 "include/linux/printk.h"
2641extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
2642#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
2643extern void *memset(void *s , int c , size_t n ) ;
2644#line 60
2645extern int memcmp(void const   *cs , void const   *ct , unsigned long count ) ;
2646#line 152 "include/linux/mutex.h"
2647void mutex_lock(struct mutex *lock ) ;
2648#line 153
2649int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2650#line 154
2651int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2652#line 168
2653int mutex_trylock(struct mutex *lock ) ;
2654#line 169
2655void mutex_unlock(struct mutex *lock ) ;
2656#line 170
2657int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2658#line 54 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
2659__inline static unsigned short readw(void const volatile   *addr )  __attribute__((__no_instrument_function__)) ;
2660#line 54 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
2661__inline static unsigned short readw(void const volatile   *addr ) 
2662{ unsigned short ret ;
2663  unsigned short volatile   *__cil_tmp3 ;
2664
2665  {
2666#line 54
2667  __cil_tmp3 = (unsigned short volatile   *)addr;
2668#line 54
2669  __asm__  volatile   ("mov"
2670                       "w"
2671                       " %1,%0": "=r" (ret): "m" (*__cil_tmp3): "memory");
2672#line 54
2673  return (ret);
2674}
2675}
2676#line 62
2677__inline static void writew(unsigned short val , void volatile   *addr )  __attribute__((__no_instrument_function__)) ;
2678#line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
2679__inline static void writew(unsigned short val , void volatile   *addr ) 
2680{ unsigned short volatile   *__cil_tmp3 ;
2681
2682  {
2683#line 62
2684  __cil_tmp3 = (unsigned short volatile   *)addr;
2685#line 62
2686  __asm__  volatile   ("mov"
2687                       "w"
2688                       " %0,%1": : "r" (val), "m" (*__cil_tmp3): "memory");
2689#line 62
2690  return;
2691}
2692}
2693#line 54 "include/linux/vmalloc.h"
2694extern void *vmalloc(unsigned long size ) ;
2695#line 66
2696extern void vfree(void const   *addr ) ;
2697#line 161 "include/linux/slab.h"
2698extern void kfree(void const   * ) ;
2699#line 221 "include/linux/slub_def.h"
2700extern void *__kmalloc(size_t size , gfp_t flags ) ;
2701#line 268
2702__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2703                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2704#line 268 "include/linux/slub_def.h"
2705__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2706                                                                    gfp_t flags ) 
2707{ void *tmp___2 ;
2708
2709  {
2710  {
2711#line 283
2712  tmp___2 = __kmalloc(size, flags);
2713  }
2714#line 283
2715  return (tmp___2);
2716}
2717}
2718#line 349 "include/linux/slab.h"
2719__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2720#line 349 "include/linux/slab.h"
2721__inline static void *kzalloc(size_t size , gfp_t flags ) 
2722{ void *tmp ;
2723  unsigned int __cil_tmp4 ;
2724
2725  {
2726  {
2727#line 351
2728  __cil_tmp4 = flags | 32768U;
2729#line 351
2730  tmp = kmalloc(size, __cil_tmp4);
2731  }
2732#line 351
2733  return (tmp);
2734}
2735}
2736#line 26 "include/linux/export.h"
2737extern struct module __this_module ;
2738#line 67 "include/linux/module.h"
2739int init_module(void) ;
2740#line 68
2741void cleanup_module(void) ;
2742#line 362 "include/linux/mtd/mtd.h"
2743extern int mtd_device_parse_register(struct mtd_info *mtd , char const   **part_probe_types ,
2744                                     struct mtd_part_parser_data *parser_data , struct mtd_partition  const  *defparts ,
2745                                     int defnr_parts ) ;
2746#line 25 "include/linux/mtd/onenand.h"
2747extern int onenand_scan(struct mtd_info *mtd , int max_chips ) ;
2748#line 27
2749extern void onenand_release(struct mtd_info *mtd ) ;
2750#line 229
2751extern loff_t onenand_addr(struct onenand_chip *this , int block ) ;
2752#line 230
2753extern int flexonenand_region(struct mtd_info *mtd , loff_t addr ) ;
2754#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2755static int manuf_id  =    236;
2756#line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2757static int device_id  =    4;
2758#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2759static int version_id  =    30;
2760#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2761static int technology_id  =    (4 >> 9) & 1;
2762#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2763static int boundary[2]  = {      1,      1};
2764#line 89 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2765static unsigned char *ffchars  ;
2766#line 97 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2767static struct mtd_partition os_partitions[1]  = {      {(char *)"OneNAND simulator partition", (uint64_t )0, (uint64_t )0, 0U, (struct nand_ecclayout *)0}};
2768#line 115 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2769static struct onenand_info *info  ;
2770#line 131 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
2771static void onenand_lock_handle(struct onenand_chip *this , int cmd ) 
2772{ int block_lock_scheme ;
2773  int status ;
2774  unsigned short tmp___7 ;
2775  int __cil_tmp6 ;
2776  void *__cil_tmp7 ;
2777  void *__cil_tmp8 ;
2778  void const volatile   *__cil_tmp9 ;
2779  unsigned long __cil_tmp10 ;
2780  unsigned long __cil_tmp11 ;
2781  unsigned int __cil_tmp12 ;
2782  unsigned int __cil_tmp13 ;
2783  int __cil_tmp14 ;
2784  unsigned short __cil_tmp15 ;
2785  int __cil_tmp16 ;
2786  void *__cil_tmp17 ;
2787  void *__cil_tmp18 ;
2788  void volatile   *__cil_tmp19 ;
2789  int __cil_tmp20 ;
2790  int __cil_tmp21 ;
2791  unsigned short __cil_tmp22 ;
2792  int __cil_tmp23 ;
2793  void *__cil_tmp24 ;
2794  void *__cil_tmp25 ;
2795  void volatile   *__cil_tmp26 ;
2796  int __cil_tmp27 ;
2797  unsigned short __cil_tmp28 ;
2798  int __cil_tmp29 ;
2799  void *__cil_tmp30 ;
2800  void *__cil_tmp31 ;
2801  void volatile   *__cil_tmp32 ;
2802  int __cil_tmp33 ;
2803  int __cil_tmp34 ;
2804  unsigned short __cil_tmp35 ;
2805  int __cil_tmp36 ;
2806  void *__cil_tmp37 ;
2807  void *__cil_tmp38 ;
2808  void volatile   *__cil_tmp39 ;
2809  int __cil_tmp40 ;
2810  void *__cil_tmp41 ;
2811  void *__cil_tmp42 ;
2812  void volatile   *__cil_tmp43 ;
2813  int __cil_tmp44 ;
2814  unsigned short __cil_tmp45 ;
2815  int __cil_tmp46 ;
2816  void *__cil_tmp47 ;
2817  void *__cil_tmp48 ;
2818  void volatile   *__cil_tmp49 ;
2819
2820  {
2821  {
2822#line 136
2823  __cil_tmp6 = 62030 << 1;
2824#line 136
2825  __cil_tmp7 = *((void **)this);
2826#line 136
2827  __cil_tmp8 = __cil_tmp7 + __cil_tmp6;
2828#line 136
2829  __cil_tmp9 = (void const volatile   *)__cil_tmp8;
2830#line 136
2831  tmp___7 = readw(__cil_tmp9);
2832#line 136
2833  status = (int )tmp___7;
2834#line 137
2835  __cil_tmp10 = (unsigned long )this;
2836#line 137
2837  __cil_tmp11 = __cil_tmp10 + 60;
2838#line 137
2839  __cil_tmp12 = *((unsigned int *)__cil_tmp11);
2840#line 137
2841  __cil_tmp13 = __cil_tmp12 & 1U;
2842#line 137
2843  block_lock_scheme = ! __cil_tmp13;
2844  }
2845#line 140
2846  if (cmd == 35) {
2847#line 140
2848    goto case_35;
2849  } else
2850#line 141
2851  if (cmd == 39) {
2852#line 141
2853    goto case_35;
2854  } else
2855#line 148
2856  if (cmd == 42) {
2857#line 148
2858    goto case_42;
2859  } else
2860#line 155
2861  if (cmd == 44) {
2862#line 155
2863    goto case_44;
2864  } else {
2865    {
2866#line 162
2867    goto switch_default;
2868#line 139
2869    if (0) {
2870      case_35: /* CIL Label */ 
2871      case_39: /* CIL Label */ 
2872#line 142
2873      if (block_lock_scheme) {
2874        {
2875#line 143
2876        __cil_tmp14 = 1 << 2;
2877#line 143
2878        __cil_tmp15 = (unsigned short )__cil_tmp14;
2879#line 143
2880        __cil_tmp16 = 62030 << 1;
2881#line 143
2882        __cil_tmp17 = *((void **)this);
2883#line 143
2884        __cil_tmp18 = __cil_tmp17 + __cil_tmp16;
2885#line 143
2886        __cil_tmp19 = (void volatile   *)__cil_tmp18;
2887#line 143
2888        writew(__cil_tmp15, __cil_tmp19);
2889        }
2890      } else {
2891        {
2892#line 145
2893        __cil_tmp20 = 1 << 2;
2894#line 145
2895        __cil_tmp21 = status | __cil_tmp20;
2896#line 145
2897        __cil_tmp22 = (unsigned short )__cil_tmp21;
2898#line 145
2899        __cil_tmp23 = 62030 << 1;
2900#line 145
2901        __cil_tmp24 = *((void **)this);
2902#line 145
2903        __cil_tmp25 = __cil_tmp24 + __cil_tmp23;
2904#line 145
2905        __cil_tmp26 = (void volatile   *)__cil_tmp25;
2906#line 145
2907        writew(__cil_tmp22, __cil_tmp26);
2908        }
2909      }
2910#line 146
2911      goto switch_break;
2912      case_42: /* CIL Label */ 
2913#line 149
2914      if (block_lock_scheme) {
2915        {
2916#line 150
2917        __cil_tmp27 = 1 << 1;
2918#line 150
2919        __cil_tmp28 = (unsigned short )__cil_tmp27;
2920#line 150
2921        __cil_tmp29 = 62030 << 1;
2922#line 150
2923        __cil_tmp30 = *((void **)this);
2924#line 150
2925        __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
2926#line 150
2927        __cil_tmp32 = (void volatile   *)__cil_tmp31;
2928#line 150
2929        writew(__cil_tmp28, __cil_tmp32);
2930        }
2931      } else {
2932        {
2933#line 152
2934        __cil_tmp33 = 1 << 1;
2935#line 152
2936        __cil_tmp34 = status | __cil_tmp33;
2937#line 152
2938        __cil_tmp35 = (unsigned short )__cil_tmp34;
2939#line 152
2940        __cil_tmp36 = 62030 << 1;
2941#line 152
2942        __cil_tmp37 = *((void **)this);
2943#line 152
2944        __cil_tmp38 = __cil_tmp37 + __cil_tmp36;
2945#line 152
2946        __cil_tmp39 = (void volatile   *)__cil_tmp38;
2947#line 152
2948        writew(__cil_tmp35, __cil_tmp39);
2949        }
2950      }
2951#line 153
2952      goto switch_break;
2953      case_44: /* CIL Label */ 
2954#line 156
2955      if (block_lock_scheme) {
2956        {
2957#line 157
2958        __cil_tmp40 = 62030 << 1;
2959#line 157
2960        __cil_tmp41 = *((void **)this);
2961#line 157
2962        __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
2963#line 157
2964        __cil_tmp43 = (void volatile   *)__cil_tmp42;
2965#line 157
2966        writew((unsigned short)1, __cil_tmp43);
2967        }
2968      } else {
2969        {
2970#line 159
2971        __cil_tmp44 = status | 1;
2972#line 159
2973        __cil_tmp45 = (unsigned short )__cil_tmp44;
2974#line 159
2975        __cil_tmp46 = 62030 << 1;
2976#line 159
2977        __cil_tmp47 = *((void **)this);
2978#line 159
2979        __cil_tmp48 = __cil_tmp47 + __cil_tmp46;
2980#line 159
2981        __cil_tmp49 = (void volatile   *)__cil_tmp48;
2982#line 159
2983        writew(__cil_tmp45, __cil_tmp49);
2984        }
2985      }
2986#line 160
2987      goto switch_break;
2988      switch_default: /* CIL Label */ 
2989#line 163
2990      goto switch_break;
2991    } else {
2992      switch_break: /* CIL Label */ ;
2993    }
2994    }
2995  }
2996#line 165
2997  return;
2998}
2999}
3000#line 174 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
3001static void onenand_bootram_handle(struct onenand_chip *this , int cmd ) 
3002{ unsigned short __cil_tmp3 ;
3003  void *__cil_tmp4 ;
3004  void volatile   *__cil_tmp5 ;
3005  unsigned short __cil_tmp6 ;
3006  void *__cil_tmp7 ;
3007  void *__cil_tmp8 ;
3008  void volatile   *__cil_tmp9 ;
3009  unsigned short __cil_tmp10 ;
3010  void *__cil_tmp11 ;
3011  void *__cil_tmp12 ;
3012  void volatile   *__cil_tmp13 ;
3013
3014  {
3015#line 177
3016  if (cmd == 144) {
3017#line 177
3018    goto case_144;
3019  } else {
3020    {
3021#line 183
3022    goto switch_default;
3023#line 176
3024    if (0) {
3025      case_144: /* CIL Label */ 
3026      {
3027#line 178
3028      __cil_tmp3 = (unsigned short )manuf_id;
3029#line 178
3030      __cil_tmp4 = *((void **)this);
3031#line 178
3032      __cil_tmp5 = (void volatile   *)__cil_tmp4;
3033#line 178
3034      writew(__cil_tmp3, __cil_tmp5);
3035#line 179
3036      __cil_tmp6 = (unsigned short )device_id;
3037#line 179
3038      __cil_tmp7 = *((void **)this);
3039#line 179
3040      __cil_tmp8 = __cil_tmp7 + 2;
3041#line 179
3042      __cil_tmp9 = (void volatile   *)__cil_tmp8;
3043#line 179
3044      writew(__cil_tmp6, __cil_tmp9);
3045#line 180
3046      __cil_tmp10 = (unsigned short )version_id;
3047#line 180
3048      __cil_tmp11 = *((void **)this);
3049#line 180
3050      __cil_tmp12 = __cil_tmp11 + 4;
3051#line 180
3052      __cil_tmp13 = (void volatile   *)__cil_tmp12;
3053#line 180
3054      writew(__cil_tmp10, __cil_tmp13);
3055      }
3056#line 181
3057      goto switch_break;
3058      switch_default: /* CIL Label */ 
3059#line 185
3060      goto switch_break;
3061    } else {
3062      switch_break: /* CIL Label */ ;
3063    }
3064    }
3065  }
3066#line 187
3067  return;
3068}
3069}
3070#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
3071static void onenand_update_interrupt(struct onenand_chip *this , int cmd ) 
3072{ int interrupt ;
3073  int __cil_tmp4 ;
3074  int __cil_tmp5 ;
3075  int __cil_tmp6 ;
3076  int __cil_tmp7 ;
3077  unsigned short __cil_tmp8 ;
3078  int __cil_tmp9 ;
3079  void *__cil_tmp10 ;
3080  void *__cil_tmp11 ;
3081  void volatile   *__cil_tmp12 ;
3082
3083  {
3084#line 198
3085  interrupt = 1 << 15;
3086#line 201
3087  if (cmd == 0) {
3088#line 201
3089    goto case_0;
3090  } else
3091#line 202
3092  if (cmd == 19) {
3093#line 202
3094    goto case_0;
3095  } else
3096#line 206
3097  if (cmd == 128) {
3098#line 206
3099    goto case_128;
3100  } else
3101#line 207
3102  if (cmd == 26) {
3103#line 207
3104    goto case_128;
3105  } else
3106#line 211
3107  if (cmd == 148) {
3108#line 211
3109    goto case_148;
3110  } else
3111#line 215
3112  if (cmd == 240) {
3113#line 215
3114    goto case_240;
3115  } else {
3116    {
3117#line 219
3118    goto switch_default;
3119#line 200
3120    if (0) {
3121      case_0: /* CIL Label */ 
3122      case_19: /* CIL Label */ 
3123#line 203
3124      __cil_tmp4 = 1 << 7;
3125#line 203
3126      interrupt = interrupt | __cil_tmp4;
3127#line 204
3128      goto switch_break;
3129      case_128: /* CIL Label */ 
3130      case_26: /* CIL Label */ 
3131#line 208
3132      __cil_tmp5 = 1 << 6;
3133#line 208
3134      interrupt = interrupt | __cil_tmp5;
3135#line 209
3136      goto switch_break;
3137      case_148: /* CIL Label */ 
3138#line 212
3139      __cil_tmp6 = 1 << 5;
3140#line 212
3141      interrupt = interrupt | __cil_tmp6;
3142#line 213
3143      goto switch_break;
3144      case_240: /* CIL Label */ 
3145#line 216
3146      __cil_tmp7 = 1 << 4;
3147#line 216
3148      interrupt = interrupt | __cil_tmp7;
3149#line 217
3150      goto switch_break;
3151      switch_default: /* CIL Label */ 
3152#line 220
3153      goto switch_break;
3154    } else {
3155      switch_break: /* CIL Label */ ;
3156    }
3157    }
3158  }
3159  {
3160#line 223
3161  __cil_tmp8 = (unsigned short )interrupt;
3162#line 223
3163  __cil_tmp9 = 62017 << 1;
3164#line 223
3165  __cil_tmp10 = *((void **)this);
3166#line 223
3167  __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
3168#line 223
3169  __cil_tmp12 = (void volatile   *)__cil_tmp11;
3170#line 223
3171  writew(__cil_tmp8, __cil_tmp12);
3172  }
3173#line 224
3174  return;
3175}
3176}
3177#line 236 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
3178static int onenand_check_overwrite(void *dest , void *src , size_t count ) 
3179{ unsigned int *s ;
3180  unsigned int *d ;
3181  int i ;
3182  unsigned int *tmp___7 ;
3183  unsigned int *tmp___8 ;
3184  size_t __cil_tmp9 ;
3185  unsigned int __cil_tmp10 ;
3186  unsigned int __cil_tmp11 ;
3187  unsigned int __cil_tmp12 ;
3188
3189  {
3190#line 238
3191  s = (unsigned int *)src;
3192#line 239
3193  d = (unsigned int *)dest;
3194#line 242
3195  count = count >> 2;
3196#line 243
3197  i = 0;
3198  {
3199#line 243
3200  while (1) {
3201    while_continue: /* CIL Label */ ;
3202    {
3203#line 243
3204    __cil_tmp9 = (size_t )i;
3205#line 243
3206    if (__cil_tmp9 < count) {
3207
3208    } else {
3209#line 243
3210      goto while_break;
3211    }
3212    }
3213#line 244
3214    tmp___7 = s;
3215#line 244
3216    s = s + 1;
3217#line 244
3218    tmp___8 = d;
3219#line 244
3220    d = d + 1;
3221    {
3222#line 244
3223    __cil_tmp10 = *tmp___8;
3224#line 244
3225    __cil_tmp11 = *tmp___7;
3226#line 244
3227    __cil_tmp12 = __cil_tmp11 ^ __cil_tmp10;
3228#line 244
3229    if (__cil_tmp12 != 0U) {
3230#line 245
3231      return (1);
3232    } else {
3233
3234    }
3235    }
3236#line 243
3237    i = i + 1;
3238  }
3239  while_break: /* CIL Label */ ;
3240  }
3241#line 247
3242  return (0);
3243}
3244}
3245#line 270 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
3246static int pi_operation  ;
3247#line 261 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
3248static void onenand_data_handle(struct onenand_chip *this , int cmd , int dataram ,
3249                                unsigned int offset ) 
3250{ struct mtd_info *mtd ;
3251  struct onenand_flash *flash ;
3252  int main_offset ;
3253  int spare_offset ;
3254  int die ;
3255  void *src ;
3256  void *dest ;
3257  unsigned int i ;
3258  int erasesize ;
3259  int rgn ;
3260  unsigned short tmp___7 ;
3261  size_t __len ;
3262  void *__ret ;
3263  size_t __len___0 ;
3264  void *__ret___0 ;
3265  unsigned short tmp___8 ;
3266  int off ;
3267  int tmp___9 ;
3268  int tmp___10 ;
3269  int tmp___11 ;
3270  size_t __len___1 ;
3271  void *__ret___1 ;
3272  int tmp___12 ;
3273  int tmp___13 ;
3274  int tmp___14 ;
3275  size_t __len___2 ;
3276  void *__ret___2 ;
3277  unsigned long __cil_tmp32 ;
3278  unsigned long __cil_tmp33 ;
3279  void *__cil_tmp34 ;
3280  unsigned long __cil_tmp35 ;
3281  unsigned long __cil_tmp36 ;
3282  uint32_t __cil_tmp37 ;
3283  unsigned long __cil_tmp38 ;
3284  unsigned long __cil_tmp39 ;
3285  uint32_t __cil_tmp40 ;
3286  int __cil_tmp41 ;
3287  void *__cil_tmp42 ;
3288  void *__cil_tmp43 ;
3289  void const volatile   *__cil_tmp44 ;
3290  unsigned long __cil_tmp45 ;
3291  unsigned long __cil_tmp46 ;
3292  void *__cil_tmp47 ;
3293  int __cil_tmp48 ;
3294  void *__cil_tmp49 ;
3295  void *__cil_tmp50 ;
3296  unsigned long __cil_tmp51 ;
3297  unsigned long __cil_tmp52 ;
3298  int __cil_tmp53 ;
3299  unsigned short __cil_tmp54 ;
3300  int __cil_tmp55 ;
3301  void *__cil_tmp56 ;
3302  void *__cil_tmp57 ;
3303  void volatile   *__cil_tmp58 ;
3304  unsigned long __cil_tmp59 ;
3305  unsigned long __cil_tmp60 ;
3306  uint32_t __cil_tmp61 ;
3307  void const   *__cil_tmp62 ;
3308  unsigned int __cil_tmp63 ;
3309  unsigned long __cil_tmp64 ;
3310  unsigned long __cil_tmp65 ;
3311  unsigned int __cil_tmp66 ;
3312  unsigned long __cil_tmp67 ;
3313  unsigned long __cil_tmp68 ;
3314  void *__cil_tmp69 ;
3315  void *__cil_tmp70 ;
3316  int __cil_tmp71 ;
3317  void *__cil_tmp72 ;
3318  void *__cil_tmp73 ;
3319  unsigned long __cil_tmp74 ;
3320  unsigned long __cil_tmp75 ;
3321  uint32_t __cil_tmp76 ;
3322  void const   *__cil_tmp77 ;
3323  int __cil_tmp78 ;
3324  void *__cil_tmp79 ;
3325  void *__cil_tmp80 ;
3326  unsigned long __cil_tmp81 ;
3327  unsigned long __cil_tmp82 ;
3328  void *__cil_tmp83 ;
3329  int __cil_tmp84 ;
3330  void *__cil_tmp85 ;
3331  void *__cil_tmp86 ;
3332  void const volatile   *__cil_tmp87 ;
3333  unsigned long __cil_tmp88 ;
3334  unsigned long __cil_tmp89 ;
3335  unsigned long __cil_tmp90 ;
3336  unsigned long __cil_tmp91 ;
3337  int __cil_tmp92 ;
3338  int __cil_tmp93 ;
3339  unsigned int __cil_tmp94 ;
3340  unsigned long __cil_tmp95 ;
3341  unsigned long __cil_tmp96 ;
3342  int __cil_tmp97 ;
3343  unsigned int __cil_tmp98 ;
3344  unsigned int __cil_tmp99 ;
3345  void *__cil_tmp100 ;
3346  void const   *__cil_tmp101 ;
3347  void const   *__cil_tmp102 ;
3348  unsigned long __cil_tmp103 ;
3349  unsigned long __cil_tmp104 ;
3350  int __cil_tmp105 ;
3351  unsigned long __cil_tmp106 ;
3352  void *__cil_tmp107 ;
3353  void const   *__cil_tmp108 ;
3354  void const   *__cil_tmp109 ;
3355  unsigned long __cil_tmp110 ;
3356  unsigned long __cil_tmp111 ;
3357  int __cil_tmp112 ;
3358  unsigned long __cil_tmp113 ;
3359  void *__cil_tmp114 ;
3360  void *__cil_tmp115 ;
3361  unsigned long __cil_tmp116 ;
3362  unsigned long __cil_tmp117 ;
3363  int __cil_tmp118 ;
3364  size_t __cil_tmp119 ;
3365  unsigned long __cil_tmp120 ;
3366  unsigned long __cil_tmp121 ;
3367  int __cil_tmp122 ;
3368  void *__cil_tmp123 ;
3369  void *__cil_tmp124 ;
3370  void const   *__cil_tmp125 ;
3371  int __cil_tmp126 ;
3372  void *__cil_tmp127 ;
3373  void *__cil_tmp128 ;
3374  void const   *__cil_tmp129 ;
3375  void const   *__cil_tmp130 ;
3376  unsigned long __cil_tmp131 ;
3377  unsigned long __cil_tmp132 ;
3378  uint32_t __cil_tmp133 ;
3379  unsigned long __cil_tmp134 ;
3380  unsigned int __cil_tmp135 ;
3381  unsigned long __cil_tmp136 ;
3382  unsigned long __cil_tmp137 ;
3383  unsigned int __cil_tmp138 ;
3384  unsigned long __cil_tmp139 ;
3385  unsigned long __cil_tmp140 ;
3386  void *__cil_tmp141 ;
3387  void *__cil_tmp142 ;
3388  void const   *__cil_tmp143 ;
3389  void const   *__cil_tmp144 ;
3390  unsigned long __cil_tmp145 ;
3391  unsigned long __cil_tmp146 ;
3392  uint32_t __cil_tmp147 ;
3393  unsigned long __cil_tmp148 ;
3394  unsigned long __cil_tmp149 ;
3395  unsigned long __cil_tmp150 ;
3396  uint32_t __cil_tmp151 ;
3397  size_t __cil_tmp152 ;
3398  unsigned long __cil_tmp153 ;
3399  unsigned long __cil_tmp154 ;
3400  uint32_t __cil_tmp155 ;
3401  void const   *__cil_tmp156 ;
3402  int __cil_tmp157 ;
3403  unsigned int __cil_tmp158 ;
3404  unsigned long __cil_tmp159 ;
3405  unsigned long __cil_tmp160 ;
3406  unsigned int __cil_tmp161 ;
3407  loff_t __cil_tmp162 ;
3408  unsigned long __cil_tmp163 ;
3409  unsigned long __cil_tmp164 ;
3410  struct mtd_erase_region_info *__cil_tmp165 ;
3411  struct mtd_erase_region_info *__cil_tmp166 ;
3412  unsigned long __cil_tmp167 ;
3413  unsigned long __cil_tmp168 ;
3414  uint32_t __cil_tmp169 ;
3415  unsigned long __cil_tmp170 ;
3416  unsigned long __cil_tmp171 ;
3417  uint32_t __cil_tmp172 ;
3418  unsigned long __cil_tmp173 ;
3419  unsigned long __cil_tmp174 ;
3420  void *__cil_tmp175 ;
3421  void *__cil_tmp176 ;
3422  size_t __cil_tmp177 ;
3423  unsigned int __cil_tmp178 ;
3424  unsigned long __cil_tmp179 ;
3425  unsigned long __cil_tmp180 ;
3426  unsigned int __cil_tmp181 ;
3427  unsigned long __cil_tmp182 ;
3428  unsigned long __cil_tmp183 ;
3429  void *__cil_tmp184 ;
3430  void *__cil_tmp185 ;
3431  void *__cil_tmp186 ;
3432  int __cil_tmp187 ;
3433  size_t __cil_tmp188 ;
3434
3435  {
3436#line 264
3437  mtd = (struct mtd_info *)info;
3438#line 265
3439  __cil_tmp32 = (unsigned long )this;
3440#line 265
3441  __cil_tmp33 = __cil_tmp32 + 384;
3442#line 265
3443  __cil_tmp34 = *((void **)__cil_tmp33);
3444#line 265
3445  flash = (struct onenand_flash *)__cil_tmp34;
3446#line 266
3447  die = 0;
3448#line 273
3449  if (dataram) {
3450#line 274
3451    __cil_tmp35 = (unsigned long )mtd;
3452#line 274
3453    __cil_tmp36 = __cil_tmp35 + 20;
3454#line 274
3455    __cil_tmp37 = *((uint32_t *)__cil_tmp36);
3456#line 274
3457    main_offset = (int )__cil_tmp37;
3458#line 275
3459    __cil_tmp38 = (unsigned long )mtd;
3460#line 275
3461    __cil_tmp39 = __cil_tmp38 + 28;
3462#line 275
3463    __cil_tmp40 = *((uint32_t *)__cil_tmp39);
3464#line 275
3465    spare_offset = (int )__cil_tmp40;
3466  } else {
3467#line 277
3468    main_offset = 0;
3469#line 278
3470    spare_offset = 0;
3471  }
3472#line 281
3473  if (pi_operation) {
3474    {
3475#line 282
3476    __cil_tmp41 = 61697 << 1;
3477#line 282
3478    __cil_tmp42 = *((void **)this);
3479#line 282
3480    __cil_tmp43 = __cil_tmp42 + __cil_tmp41;
3481#line 282
3482    __cil_tmp44 = (void const volatile   *)__cil_tmp43;
3483#line 282
3484    tmp___7 = readw(__cil_tmp44);
3485#line 282
3486    die = (int )tmp___7;
3487#line 283
3488    die = die >> 15;
3489    }
3490  } else {
3491
3492  }
3493#line 287
3494  if (cmd == 102) {
3495#line 287
3496    goto case_102;
3497  } else
3498#line 291
3499  if (cmd == 240) {
3500#line 291
3501    goto case_240;
3502  } else
3503#line 295
3504  if (cmd == 0) {
3505#line 295
3506    goto case_0;
3507  } else
3508#line 305
3509  if (cmd == 19) {
3510#line 305
3511    goto case_19;
3512  } else
3513#line 311
3514  if (cmd == 128) {
3515#line 311
3516    goto case_128;
3517  } else
3518#line 330
3519  if (cmd == 26) {
3520#line 330
3521    goto case_26;
3522  } else
3523#line 344
3524  if (cmd == 148) {
3525#line 344
3526    goto case_148;
3527  } else {
3528    {
3529#line 359
3530    goto switch_default;
3531#line 286
3532    if (0) {
3533      case_102: /* CIL Label */ 
3534#line 288
3535      pi_operation = 1;
3536#line 289
3537      goto switch_break;
3538      case_240: /* CIL Label */ 
3539#line 292
3540      pi_operation = 0;
3541#line 293
3542      goto switch_break;
3543      case_0: /* CIL Label */ 
3544#line 296
3545      __cil_tmp45 = (unsigned long )flash;
3546#line 296
3547      __cil_tmp46 = __cil_tmp45 + 8;
3548#line 296
3549      __cil_tmp47 = *((void **)__cil_tmp46);
3550#line 296
3551      src = __cil_tmp47 + offset;
3552#line 297
3553      __cil_tmp48 = 512 << 1;
3554#line 297
3555      __cil_tmp49 = *((void **)this);
3556#line 297
3557      __cil_tmp50 = __cil_tmp49 + __cil_tmp48;
3558#line 297
3559      dest = __cil_tmp50 + main_offset;
3560#line 298
3561      if (pi_operation) {
3562        {
3563#line 299
3564        __cil_tmp51 = die * 4UL;
3565#line 299
3566        __cil_tmp52 = (unsigned long )(boundary) + __cil_tmp51;
3567#line 299
3568        __cil_tmp53 = *((int *)__cil_tmp52);
3569#line 299
3570        __cil_tmp54 = (unsigned short )__cil_tmp53;
3571#line 299
3572        __cil_tmp55 = 512 << 1;
3573#line 299
3574        __cil_tmp56 = *((void **)this);
3575#line 299
3576        __cil_tmp57 = __cil_tmp56 + __cil_tmp55;
3577#line 299
3578        __cil_tmp58 = (void volatile   *)__cil_tmp57;
3579#line 299
3580        writew(__cil_tmp54, __cil_tmp58);
3581        }
3582#line 300
3583        goto switch_break;
3584      } else {
3585
3586      }
3587      {
3588#line 302
3589      __cil_tmp59 = (unsigned long )mtd;
3590#line 302
3591      __cil_tmp60 = __cil_tmp59 + 20;
3592#line 302
3593      __cil_tmp61 = *((uint32_t *)__cil_tmp60);
3594#line 302
3595      __len = (size_t )__cil_tmp61;
3596#line 302
3597      __cil_tmp62 = (void const   *)src;
3598#line 302
3599      __ret = __builtin_memcpy(dest, __cil_tmp62, __len);
3600      }
3601      case_19: /* CIL Label */ 
3602      {
3603#line 306
3604      __cil_tmp63 = offset >> 5;
3605#line 306
3606      __cil_tmp64 = (unsigned long )this;
3607#line 306
3608      __cil_tmp65 = __cil_tmp64 + 40;
3609#line 306
3610      __cil_tmp66 = *((unsigned int *)__cil_tmp65);
3611#line 306
3612      __cil_tmp67 = (unsigned long )flash;
3613#line 306
3614      __cil_tmp68 = __cil_tmp67 + 8;
3615#line 306
3616      __cil_tmp69 = *((void **)__cil_tmp68);
3617#line 306
3618      __cil_tmp70 = __cil_tmp69 + __cil_tmp66;
3619#line 306
3620      src = __cil_tmp70 + __cil_tmp63;
3621#line 307
3622      __cil_tmp71 = 32784 << 1;
3623#line 307
3624      __cil_tmp72 = *((void **)this);
3625#line 307
3626      __cil_tmp73 = __cil_tmp72 + __cil_tmp71;
3627#line 307
3628      dest = __cil_tmp73 + spare_offset;
3629#line 308
3630      __cil_tmp74 = (unsigned long )mtd;
3631#line 308
3632      __cil_tmp75 = __cil_tmp74 + 28;
3633#line 308
3634      __cil_tmp76 = *((uint32_t *)__cil_tmp75);
3635#line 308
3636      __len___0 = (size_t )__cil_tmp76;
3637#line 308
3638      __cil_tmp77 = (void const   *)src;
3639#line 308
3640      __ret___0 = __builtin_memcpy(dest, __cil_tmp77, __len___0);
3641      }
3642#line 309
3643      goto switch_break;
3644      case_128: /* CIL Label */ 
3645#line 312
3646      __cil_tmp78 = 512 << 1;
3647#line 312
3648      __cil_tmp79 = *((void **)this);
3649#line 312
3650      __cil_tmp80 = __cil_tmp79 + __cil_tmp78;
3651#line 312
3652      src = __cil_tmp80 + main_offset;
3653#line 313
3654      __cil_tmp81 = (unsigned long )flash;
3655#line 313
3656      __cil_tmp82 = __cil_tmp81 + 8;
3657#line 313
3658      __cil_tmp83 = *((void **)__cil_tmp82);
3659#line 313
3660      dest = __cil_tmp83 + offset;
3661#line 314
3662      if (pi_operation) {
3663        {
3664#line 315
3665        __cil_tmp84 = 512 << 1;
3666#line 315
3667        __cil_tmp85 = *((void **)this);
3668#line 315
3669        __cil_tmp86 = __cil_tmp85 + __cil_tmp84;
3670#line 315
3671        __cil_tmp87 = (void const volatile   *)__cil_tmp86;
3672#line 315
3673        tmp___8 = readw(__cil_tmp87);
3674#line 315
3675        __cil_tmp88 = die * 4UL;
3676#line 315
3677        __cil_tmp89 = (unsigned long )(boundary) + __cil_tmp88;
3678#line 315
3679        *((int *)__cil_tmp89) = (int )tmp___8;
3680        }
3681#line 316
3682        goto switch_break;
3683      } else {
3684
3685      }
3686#line 319
3687      i = 0U;
3688      {
3689#line 319
3690      while (1) {
3691        while_continue: /* CIL Label */ ;
3692        {
3693#line 319
3694        __cil_tmp90 = (unsigned long )mtd;
3695#line 319
3696        __cil_tmp91 = __cil_tmp90 + 352;
3697#line 319
3698        __cil_tmp92 = *((int *)__cil_tmp91);
3699#line 319
3700        __cil_tmp93 = 1 << __cil_tmp92;
3701#line 319
3702        __cil_tmp94 = (unsigned int )__cil_tmp93;
3703#line 319
3704        if (i < __cil_tmp94) {
3705
3706        } else {
3707#line 319
3708          goto while_break;
3709        }
3710        }
3711        {
3712#line 320
3713        __cil_tmp95 = (unsigned long )this;
3714#line 320
3715        __cil_tmp96 = __cil_tmp95 + 360;
3716#line 320
3717        __cil_tmp97 = *((int *)__cil_tmp96);
3718#line 320
3719        __cil_tmp98 = (unsigned int )__cil_tmp97;
3720#line 320
3721        __cil_tmp99 = i * __cil_tmp98;
3722#line 320
3723        off = (int )__cil_tmp99;
3724#line 321
3725        __cil_tmp100 = src + off;
3726#line 321
3727        __cil_tmp101 = (void const   *)__cil_tmp100;
3728#line 321
3729        __cil_tmp102 = (void const   *)ffchars;
3730#line 321
3731        __cil_tmp103 = (unsigned long )this;
3732#line 321
3733        __cil_tmp104 = __cil_tmp103 + 360;
3734#line 321
3735        __cil_tmp105 = *((int *)__cil_tmp104);
3736#line 321
3737        __cil_tmp106 = (unsigned long )__cil_tmp105;
3738#line 321
3739        tmp___9 = memcmp(__cil_tmp101, __cil_tmp102, __cil_tmp106);
3740        }
3741#line 321
3742        if (tmp___9) {
3743
3744        } else {
3745#line 322
3746          goto __Cont;
3747        }
3748        {
3749#line 323
3750        __cil_tmp107 = dest + off;
3751#line 323
3752        __cil_tmp108 = (void const   *)__cil_tmp107;
3753#line 323
3754        __cil_tmp109 = (void const   *)ffchars;
3755#line 323
3756        __cil_tmp110 = (unsigned long )this;
3757#line 323
3758        __cil_tmp111 = __cil_tmp110 + 360;
3759#line 323
3760        __cil_tmp112 = *((int *)__cil_tmp111);
3761#line 323
3762        __cil_tmp113 = (unsigned long )__cil_tmp112;
3763#line 323
3764        tmp___10 = memcmp(__cil_tmp108, __cil_tmp109, __cil_tmp113);
3765        }
3766#line 323
3767        if (tmp___10) {
3768          {
3769#line 323
3770          __cil_tmp114 = dest + off;
3771#line 323
3772          __cil_tmp115 = src + off;
3773#line 323
3774          __cil_tmp116 = (unsigned long )this;
3775#line 323
3776          __cil_tmp117 = __cil_tmp116 + 360;
3777#line 323
3778          __cil_tmp118 = *((int *)__cil_tmp117);
3779#line 323
3780          __cil_tmp119 = (size_t )__cil_tmp118;
3781#line 323
3782          tmp___11 = onenand_check_overwrite(__cil_tmp114, __cil_tmp115, __cil_tmp119);
3783          }
3784#line 323
3785          if (tmp___11) {
3786            {
3787#line 325
3788            printk("<3>over-write happened at 0x%08x\n", offset);
3789            }
3790          } else {
3791
3792          }
3793        } else {
3794
3795        }
3796        {
3797#line 326
3798        __cil_tmp120 = (unsigned long )this;
3799#line 326
3800        __cil_tmp121 = __cil_tmp120 + 360;
3801#line 326
3802        __cil_tmp122 = *((int *)__cil_tmp121);
3803#line 326
3804        __len___1 = (size_t )__cil_tmp122;
3805#line 326
3806        __cil_tmp123 = dest + off;
3807#line 326
3808        __cil_tmp124 = src + off;
3809#line 326
3810        __cil_tmp125 = (void const   *)__cil_tmp124;
3811#line 326
3812        __ret___1 = __builtin_memcpy(__cil_tmp123, __cil_tmp125, __len___1);
3813        }
3814        __Cont: /* CIL Label */ 
3815#line 319
3816        i = i + 1U;
3817      }
3818      while_break: /* CIL Label */ ;
3819      }
3820      case_26: /* CIL Label */ 
3821      {
3822#line 331
3823      __cil_tmp126 = 32784 << 1;
3824#line 331
3825      __cil_tmp127 = *((void **)this);
3826#line 331
3827      __cil_tmp128 = __cil_tmp127 + __cil_tmp126;
3828#line 331
3829      src = __cil_tmp128 + spare_offset;
3830#line 333
3831      __cil_tmp129 = (void const   *)src;
3832#line 333
3833      __cil_tmp130 = (void const   *)ffchars;
3834#line 333
3835      __cil_tmp131 = (unsigned long )mtd;
3836#line 333
3837      __cil_tmp132 = __cil_tmp131 + 28;
3838#line 333
3839      __cil_tmp133 = *((uint32_t *)__cil_tmp132);
3840#line 333
3841      __cil_tmp134 = (unsigned long )__cil_tmp133;
3842#line 333
3843      tmp___12 = memcmp(__cil_tmp129, __cil_tmp130, __cil_tmp134);
3844      }
3845#line 333
3846      if (tmp___12) {
3847
3848      } else {
3849#line 334
3850        goto switch_break;
3851      }
3852      {
3853#line 336
3854      __cil_tmp135 = offset >> 5;
3855#line 336
3856      __cil_tmp136 = (unsigned long )this;
3857#line 336
3858      __cil_tmp137 = __cil_tmp136 + 40;
3859#line 336
3860      __cil_tmp138 = *((unsigned int *)__cil_tmp137);
3861#line 336
3862      __cil_tmp139 = (unsigned long )flash;
3863#line 336
3864      __cil_tmp140 = __cil_tmp139 + 8;
3865#line 336
3866      __cil_tmp141 = *((void **)__cil_tmp140);
3867#line 336
3868      __cil_tmp142 = __cil_tmp141 + __cil_tmp138;
3869#line 336
3870      dest = __cil_tmp142 + __cil_tmp135;
3871#line 337
3872      __cil_tmp143 = (void const   *)dest;
3873#line 337
3874      __cil_tmp144 = (void const   *)ffchars;
3875#line 337
3876      __cil_tmp145 = (unsigned long )mtd;
3877#line 337
3878      __cil_tmp146 = __cil_tmp145 + 28;
3879#line 337
3880      __cil_tmp147 = *((uint32_t *)__cil_tmp146);
3881#line 337
3882      __cil_tmp148 = (unsigned long )__cil_tmp147;
3883#line 337
3884      tmp___13 = memcmp(__cil_tmp143, __cil_tmp144, __cil_tmp148);
3885      }
3886#line 337
3887      if (tmp___13) {
3888        {
3889#line 337
3890        __cil_tmp149 = (unsigned long )mtd;
3891#line 337
3892        __cil_tmp150 = __cil_tmp149 + 28;
3893#line 337
3894        __cil_tmp151 = *((uint32_t *)__cil_tmp150);
3895#line 337
3896        __cil_tmp152 = (size_t )__cil_tmp151;
3897#line 337
3898        tmp___14 = onenand_check_overwrite(dest, src, __cil_tmp152);
3899        }
3900#line 337
3901        if (tmp___14) {
3902          {
3903#line 339
3904          printk("<3>OOB: over-write happened at 0x%08x\n", offset);
3905          }
3906        } else {
3907
3908        }
3909      } else {
3910
3911      }
3912      {
3913#line 341
3914      __cil_tmp153 = (unsigned long )mtd;
3915#line 341
3916      __cil_tmp154 = __cil_tmp153 + 28;
3917#line 341
3918      __cil_tmp155 = *((uint32_t *)__cil_tmp154);
3919#line 341
3920      __len___2 = (size_t )__cil_tmp155;
3921#line 341
3922      __cil_tmp156 = (void const   *)src;
3923#line 341
3924      __ret___2 = __builtin_memcpy(dest, __cil_tmp156, __len___2);
3925      }
3926#line 342
3927      goto switch_break;
3928      case_148: /* CIL Label */ 
3929#line 345
3930      if (pi_operation) {
3931#line 346
3932        goto switch_break;
3933      } else {
3934
3935      }
3936      {
3937#line 348
3938      __cil_tmp157 = 1 << 9;
3939#line 348
3940      __cil_tmp158 = (unsigned int )__cil_tmp157;
3941#line 348
3942      __cil_tmp159 = (unsigned long )this;
3943#line 348
3944      __cil_tmp160 = __cil_tmp159 + 44;
3945#line 348
3946      __cil_tmp161 = *((unsigned int *)__cil_tmp160);
3947#line 348
3948      if (__cil_tmp161 & __cil_tmp158) {
3949        {
3950#line 349
3951        __cil_tmp162 = (loff_t )offset;
3952#line 349
3953        rgn = flexonenand_region(mtd, __cil_tmp162);
3954#line 350
3955        __cil_tmp163 = (unsigned long )mtd;
3956#line 350
3957        __cil_tmp164 = __cil_tmp163 + 88;
3958#line 350
3959        __cil_tmp165 = *((struct mtd_erase_region_info **)__cil_tmp164);
3960#line 350
3961        __cil_tmp166 = __cil_tmp165 + rgn;
3962#line 350
3963        __cil_tmp167 = (unsigned long )__cil_tmp166;
3964#line 350
3965        __cil_tmp168 = __cil_tmp167 + 8;
3966#line 350
3967        __cil_tmp169 = *((uint32_t *)__cil_tmp168);
3968#line 350
3969        erasesize = (int )__cil_tmp169;
3970        }
3971      } else {
3972#line 352
3973        __cil_tmp170 = (unsigned long )mtd;
3974#line 352
3975        __cil_tmp171 = __cil_tmp170 + 16;
3976#line 352
3977        __cil_tmp172 = *((uint32_t *)__cil_tmp171);
3978#line 352
3979        erasesize = (int )__cil_tmp172;
3980      }
3981      }
3982      {
3983#line 354
3984      __cil_tmp173 = (unsigned long )flash;
3985#line 354
3986      __cil_tmp174 = __cil_tmp173 + 8;
3987#line 354
3988      __cil_tmp175 = *((void **)__cil_tmp174);
3989#line 354
3990      __cil_tmp176 = __cil_tmp175 + offset;
3991#line 354
3992      __cil_tmp177 = (size_t )erasesize;
3993#line 354
3994      memset(__cil_tmp176, 255, __cil_tmp177);
3995#line 355
3996      __cil_tmp178 = offset >> 5;
3997#line 355
3998      __cil_tmp179 = (unsigned long )this;
3999#line 355
4000      __cil_tmp180 = __cil_tmp179 + 40;
4001#line 355
4002      __cil_tmp181 = *((unsigned int *)__cil_tmp180);
4003#line 355
4004      __cil_tmp182 = (unsigned long )flash;
4005#line 355
4006      __cil_tmp183 = __cil_tmp182 + 8;
4007#line 355
4008      __cil_tmp184 = *((void **)__cil_tmp183);
4009#line 355
4010      __cil_tmp185 = __cil_tmp184 + __cil_tmp181;
4011#line 355
4012      __cil_tmp186 = __cil_tmp185 + __cil_tmp178;
4013#line 355
4014      __cil_tmp187 = erasesize >> 5;
4015#line 355
4016      __cil_tmp188 = (size_t )__cil_tmp187;
4017#line 355
4018      memset(__cil_tmp186, 255, __cil_tmp188);
4019      }
4020#line 357
4021      goto switch_break;
4022      switch_default: /* CIL Label */ 
4023#line 360
4024      goto switch_break;
4025    } else {
4026      switch_break: /* CIL Label */ ;
4027    }
4028    }
4029  }
4030#line 362
4031  return;
4032}
4033}
4034#line 371 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4035static void onenand_command_handle(struct onenand_chip *this , int cmd ) 
4036{ unsigned long offset ;
4037  int block ;
4038  int page ;
4039  int bufferram ;
4040  int dataram ;
4041  unsigned short tmp___7 ;
4042  unsigned short tmp___8 ;
4043  unsigned short tmp___9 ;
4044  loff_t tmp___10 ;
4045  int __cil_tmp12 ;
4046  void *__cil_tmp13 ;
4047  void *__cil_tmp14 ;
4048  void const volatile   *__cil_tmp15 ;
4049  int __cil_tmp16 ;
4050  int __cil_tmp17 ;
4051  int __cil_tmp18 ;
4052  unsigned long __cil_tmp19 ;
4053  unsigned long __cil_tmp20 ;
4054  unsigned int __cil_tmp21 ;
4055  unsigned int __cil_tmp22 ;
4056  unsigned long __cil_tmp23 ;
4057  unsigned long __cil_tmp24 ;
4058  unsigned int __cil_tmp25 ;
4059  unsigned int __cil_tmp26 ;
4060  unsigned int __cil_tmp27 ;
4061  unsigned int __cil_tmp28 ;
4062  int __cil_tmp29 ;
4063  void *__cil_tmp30 ;
4064  void *__cil_tmp31 ;
4065  void const volatile   *__cil_tmp32 ;
4066  int __cil_tmp33 ;
4067  void *__cil_tmp34 ;
4068  void *__cil_tmp35 ;
4069  void const volatile   *__cil_tmp36 ;
4070  int __cil_tmp37 ;
4071  int __cil_tmp38 ;
4072  unsigned long __cil_tmp39 ;
4073  unsigned long __cil_tmp40 ;
4074  unsigned int __cil_tmp41 ;
4075  int __cil_tmp42 ;
4076  unsigned long __cil_tmp43 ;
4077  unsigned int __cil_tmp44 ;
4078
4079  {
4080#line 373
4081  offset = 0UL;
4082#line 374
4083  block = -1;
4084#line 374
4085  page = -1;
4086#line 374
4087  bufferram = -1;
4088#line 375
4089  dataram = 0;
4090#line 378
4091  if (cmd == 35) {
4092#line 378
4093    goto case_35;
4094  } else
4095#line 379
4096  if (cmd == 42) {
4097#line 379
4098    goto case_35;
4099  } else
4100#line 380
4101  if (cmd == 44) {
4102#line 380
4103    goto case_35;
4104  } else
4105#line 381
4106  if (cmd == 39) {
4107#line 381
4108    goto case_35;
4109  } else
4110#line 385
4111  if (cmd == 6520) {
4112#line 385
4113    goto case_6520;
4114  } else {
4115    {
4116#line 389
4117    goto switch_default;
4118#line 377
4119    if (0) {
4120      case_35: /* CIL Label */ 
4121      case_42: /* CIL Label */ 
4122      case_44: /* CIL Label */ 
4123      case_39: /* CIL Label */ 
4124      {
4125#line 382
4126      onenand_lock_handle(this, cmd);
4127      }
4128#line 383
4129      goto switch_break;
4130      case_6520: /* CIL Label */ 
4131#line 387
4132      return;
4133      switch_default: /* CIL Label */ 
4134      {
4135#line 390
4136      __cil_tmp12 = 61696 << 1;
4137#line 390
4138      __cil_tmp13 = *((void **)this);
4139#line 390
4140      __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
4141#line 390
4142      __cil_tmp15 = (void const volatile   *)__cil_tmp14;
4143#line 390
4144      tmp___7 = readw(__cil_tmp15);
4145#line 390
4146      block = (int )tmp___7;
4147      }
4148      {
4149#line 391
4150      __cil_tmp16 = 1 << 15;
4151#line 391
4152      if (block & __cil_tmp16) {
4153#line 392
4154        __cil_tmp17 = 1 << 15;
4155#line 392
4156        __cil_tmp18 = ~ __cil_tmp17;
4157#line 392
4158        block = block & __cil_tmp18;
4159#line 394
4160        __cil_tmp19 = (unsigned long )this;
4161#line 394
4162        __cil_tmp20 = __cil_tmp19 + 64;
4163#line 394
4164        __cil_tmp21 = *((unsigned int *)__cil_tmp20);
4165#line 394
4166        __cil_tmp22 = __cil_tmp21 + 1U;
4167#line 394
4168        __cil_tmp23 = (unsigned long )this;
4169#line 394
4170        __cil_tmp24 = __cil_tmp23 + 40;
4171#line 394
4172        __cil_tmp25 = *((unsigned int *)__cil_tmp24);
4173#line 394
4174        __cil_tmp26 = __cil_tmp25 >> __cil_tmp22;
4175#line 394
4176        __cil_tmp27 = (unsigned int )block;
4177#line 394
4178        __cil_tmp28 = __cil_tmp27 + __cil_tmp26;
4179#line 394
4180        block = (int )__cil_tmp28;
4181      } else {
4182
4183      }
4184      }
4185#line 396
4186      if (cmd == 148) {
4187#line 397
4188        goto switch_break;
4189      } else {
4190
4191      }
4192      {
4193#line 399
4194      __cil_tmp29 = 61703 << 1;
4195#line 399
4196      __cil_tmp30 = *((void **)this);
4197#line 399
4198      __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
4199#line 399
4200      __cil_tmp32 = (void const volatile   *)__cil_tmp31;
4201#line 399
4202      tmp___8 = readw(__cil_tmp32);
4203#line 399
4204      page = (int )tmp___8;
4205#line 400
4206      page = page >> 2;
4207#line 401
4208      __cil_tmp33 = 61952 << 1;
4209#line 401
4210      __cil_tmp34 = *((void **)this);
4211#line 401
4212      __cil_tmp35 = __cil_tmp34 + __cil_tmp33;
4213#line 401
4214      __cil_tmp36 = (void const volatile   *)__cil_tmp35;
4215#line 401
4216      tmp___9 = readw(__cil_tmp36);
4217#line 401
4218      bufferram = (int )tmp___9;
4219#line 402
4220      bufferram = bufferram >> 8;
4221#line 403
4222      __cil_tmp37 = 3 << 2;
4223#line 403
4224      bufferram = bufferram & __cil_tmp37;
4225      }
4226      {
4227#line 404
4228      __cil_tmp38 = 3 << 2;
4229#line 404
4230      if (bufferram == __cil_tmp38) {
4231#line 404
4232        dataram = 1;
4233      } else {
4234#line 404
4235        dataram = 0;
4236      }
4237      }
4238#line 405
4239      goto switch_break;
4240    } else {
4241      switch_break: /* CIL Label */ ;
4242    }
4243    }
4244  }
4245#line 408
4246  if (block != -1) {
4247    {
4248#line 409
4249    tmp___10 = onenand_addr(this, block);
4250#line 409
4251    offset = (unsigned long )tmp___10;
4252    }
4253  } else {
4254
4255  }
4256#line 411
4257  if (page != -1) {
4258#line 412
4259    __cil_tmp39 = (unsigned long )this;
4260#line 412
4261    __cil_tmp40 = __cil_tmp39 + 68;
4262#line 412
4263    __cil_tmp41 = *((unsigned int *)__cil_tmp40);
4264#line 412
4265    __cil_tmp42 = page << __cil_tmp41;
4266#line 412
4267    __cil_tmp43 = (unsigned long )__cil_tmp42;
4268#line 412
4269    offset = offset + __cil_tmp43;
4270  } else {
4271
4272  }
4273  {
4274#line 414
4275  __cil_tmp44 = (unsigned int )offset;
4276#line 414
4277  onenand_data_handle(this, cmd, dataram, __cil_tmp44);
4278#line 416
4279  onenand_update_interrupt(this, cmd);
4280  }
4281#line 417
4282  return;
4283}
4284}
4285#line 426 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4286static void onenand_writew(unsigned short value , void *addr ) 
4287{ struct onenand_chip *this ;
4288  unsigned long __cil_tmp4 ;
4289  unsigned long __cil_tmp5 ;
4290  unsigned long __cil_tmp6 ;
4291  void *__cil_tmp7 ;
4292  int __cil_tmp8 ;
4293  void *__cil_tmp9 ;
4294  void *__cil_tmp10 ;
4295  unsigned long __cil_tmp11 ;
4296  unsigned long __cil_tmp12 ;
4297  int __cil_tmp13 ;
4298  int __cil_tmp14 ;
4299  void *__cil_tmp15 ;
4300  void *__cil_tmp16 ;
4301  unsigned long __cil_tmp17 ;
4302  unsigned long __cil_tmp18 ;
4303  int __cil_tmp19 ;
4304  void volatile   *__cil_tmp20 ;
4305
4306  {
4307#line 428
4308  __cil_tmp4 = 0 + 360;
4309#line 428
4310  __cil_tmp5 = (unsigned long )info;
4311#line 428
4312  __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
4313#line 428
4314  __cil_tmp7 = *((void **)__cil_tmp6);
4315#line 428
4316  this = (struct onenand_chip *)__cil_tmp7;
4317  {
4318#line 431
4319  __cil_tmp8 = 512 << 1;
4320#line 431
4321  __cil_tmp9 = *((void **)this);
4322#line 431
4323  __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
4324#line 431
4325  __cil_tmp11 = (unsigned long )__cil_tmp10;
4326#line 431
4327  __cil_tmp12 = (unsigned long )addr;
4328#line 431
4329  if (__cil_tmp12 < __cil_tmp11) {
4330    {
4331#line 432
4332    __cil_tmp13 = (int )value;
4333#line 432
4334    onenand_bootram_handle(this, __cil_tmp13);
4335    }
4336#line 433
4337    return;
4338  } else {
4339
4340  }
4341  }
4342  {
4343#line 436
4344  __cil_tmp14 = 61984 << 1;
4345#line 436
4346  __cil_tmp15 = *((void **)this);
4347#line 436
4348  __cil_tmp16 = __cil_tmp15 + __cil_tmp14;
4349#line 436
4350  __cil_tmp17 = (unsigned long )__cil_tmp16;
4351#line 436
4352  __cil_tmp18 = (unsigned long )addr;
4353#line 436
4354  if (__cil_tmp18 == __cil_tmp17) {
4355    {
4356#line 437
4357    __cil_tmp19 = (int )value;
4358#line 437
4359    onenand_command_handle(this, __cil_tmp19);
4360    }
4361  } else {
4362
4363  }
4364  }
4365  {
4366#line 439
4367  __cil_tmp20 = (void volatile   *)addr;
4368#line 439
4369  writew(value, __cil_tmp20);
4370  }
4371#line 440
4372  return;
4373}
4374}
4375#line 448
4376static int flash_init(struct onenand_flash *flash )  __attribute__((__section__(".init.text"),
4377__no_instrument_function__)) ;
4378#line 448 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4379static int flash_init(struct onenand_flash *flash ) 
4380{ int density ;
4381  int size ;
4382  int buffer_size ;
4383  size_t __cil_tmp5 ;
4384  void *__cil_tmp6 ;
4385  int __cil_tmp7 ;
4386  unsigned long __cil_tmp8 ;
4387  unsigned long __cil_tmp9 ;
4388  int __cil_tmp10 ;
4389  int __cil_tmp11 ;
4390  unsigned long __cil_tmp12 ;
4391  unsigned long __cil_tmp13 ;
4392  unsigned long __cil_tmp14 ;
4393  void *__cil_tmp15 ;
4394  void *__cil_tmp16 ;
4395  void const   *__cil_tmp17 ;
4396  unsigned long __cil_tmp18 ;
4397  unsigned long __cil_tmp19 ;
4398  void *__cil_tmp20 ;
4399  int __cil_tmp21 ;
4400  int __cil_tmp22 ;
4401  size_t __cil_tmp23 ;
4402  unsigned short __cil_tmp24 ;
4403  int __cil_tmp25 ;
4404  void *__cil_tmp26 ;
4405  void *__cil_tmp27 ;
4406  void volatile   *__cil_tmp28 ;
4407  unsigned short __cil_tmp29 ;
4408  int __cil_tmp30 ;
4409  void *__cil_tmp31 ;
4410  void *__cil_tmp32 ;
4411  void volatile   *__cil_tmp33 ;
4412  unsigned short __cil_tmp34 ;
4413  int __cil_tmp35 ;
4414  void *__cil_tmp36 ;
4415  void *__cil_tmp37 ;
4416  void volatile   *__cil_tmp38 ;
4417  unsigned short __cil_tmp39 ;
4418  int __cil_tmp40 ;
4419  void *__cil_tmp41 ;
4420  void *__cil_tmp42 ;
4421  void volatile   *__cil_tmp43 ;
4422  int __cil_tmp44 ;
4423  int __cil_tmp45 ;
4424  unsigned short __cil_tmp46 ;
4425  int __cil_tmp47 ;
4426  void *__cil_tmp48 ;
4427  void *__cil_tmp49 ;
4428  void volatile   *__cil_tmp50 ;
4429
4430  {
4431  {
4432#line 453
4433  __cil_tmp5 = (size_t )131072;
4434#line 453
4435  *((void **)flash) = kzalloc(__cil_tmp5, 208U);
4436  }
4437  {
4438#line 454
4439  __cil_tmp6 = *((void **)flash);
4440#line 454
4441  if (! __cil_tmp6) {
4442    {
4443#line 455
4444    printk("<3>Unable to allocate base address.\n");
4445    }
4446#line 456
4447    return (-12);
4448  } else {
4449
4450  }
4451  }
4452  {
4453#line 459
4454  density = device_id >> 4;
4455#line 460
4456  density = density & 15;
4457#line 461
4458  __cil_tmp7 = 16 << 20;
4459#line 461
4460  size = __cil_tmp7 << density;
4461#line 463
4462  __cil_tmp8 = (unsigned long )flash;
4463#line 463
4464  __cil_tmp9 = __cil_tmp8 + 8;
4465#line 463
4466  __cil_tmp10 = size >> 5;
4467#line 463
4468  __cil_tmp11 = size + __cil_tmp10;
4469#line 463
4470  __cil_tmp12 = (unsigned long )__cil_tmp11;
4471#line 463
4472  *((void **)__cil_tmp9) = vmalloc(__cil_tmp12);
4473  }
4474  {
4475#line 464
4476  __cil_tmp13 = (unsigned long )flash;
4477#line 464
4478  __cil_tmp14 = __cil_tmp13 + 8;
4479#line 464
4480  __cil_tmp15 = *((void **)__cil_tmp14);
4481#line 464
4482  if (! __cil_tmp15) {
4483    {
4484#line 465
4485    printk("<3>Unable to allocate nand core address.\n");
4486#line 466
4487    __cil_tmp16 = *((void **)flash);
4488#line 466
4489    __cil_tmp17 = (void const   *)__cil_tmp16;
4490#line 466
4491    kfree(__cil_tmp17);
4492    }
4493#line 467
4494    return (-12);
4495  } else {
4496
4497  }
4498  }
4499  {
4500#line 470
4501  __cil_tmp18 = (unsigned long )flash;
4502#line 470
4503  __cil_tmp19 = __cil_tmp18 + 8;
4504#line 470
4505  __cil_tmp20 = *((void **)__cil_tmp19);
4506#line 470
4507  __cil_tmp21 = size >> 5;
4508#line 470
4509  __cil_tmp22 = size + __cil_tmp21;
4510#line 470
4511  __cil_tmp23 = (size_t )__cil_tmp22;
4512#line 470
4513  memset(__cil_tmp20, 255, __cil_tmp23);
4514#line 473
4515  __cil_tmp24 = (unsigned short )manuf_id;
4516#line 473
4517  __cil_tmp25 = 61440 << 1;
4518#line 473
4519  __cil_tmp26 = *((void **)flash);
4520#line 473
4521  __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
4522#line 473
4523  __cil_tmp28 = (void volatile   *)__cil_tmp27;
4524#line 473
4525  writew(__cil_tmp24, __cil_tmp28);
4526#line 474
4527  __cil_tmp29 = (unsigned short )device_id;
4528#line 474
4529  __cil_tmp30 = 61441 << 1;
4530#line 474
4531  __cil_tmp31 = *((void **)flash);
4532#line 474
4533  __cil_tmp32 = __cil_tmp31 + __cil_tmp30;
4534#line 474
4535  __cil_tmp33 = (void volatile   *)__cil_tmp32;
4536#line 474
4537  writew(__cil_tmp29, __cil_tmp33);
4538#line 475
4539  __cil_tmp34 = (unsigned short )version_id;
4540#line 475
4541  __cil_tmp35 = 61442 << 1;
4542#line 475
4543  __cil_tmp36 = *((void **)flash);
4544#line 475
4545  __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
4546#line 475
4547  __cil_tmp38 = (void volatile   *)__cil_tmp37;
4548#line 475
4549  writew(__cil_tmp34, __cil_tmp38);
4550#line 476
4551  __cil_tmp39 = (unsigned short )technology_id;
4552#line 476
4553  __cil_tmp40 = 61446 << 1;
4554#line 476
4555  __cil_tmp41 = *((void **)flash);
4556#line 476
4557  __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
4558#line 476
4559  __cil_tmp43 = (void volatile   *)__cil_tmp42;
4560#line 476
4561  writew(__cil_tmp39, __cil_tmp43);
4562  }
4563#line 478
4564  if (density < 2) {
4565    {
4566#line 478
4567    __cil_tmp44 = 4 >> 9;
4568#line 478
4569    __cil_tmp45 = __cil_tmp44 & 1;
4570#line 478
4571    if (! __cil_tmp45) {
4572#line 479
4573      buffer_size = 1024;
4574    } else {
4575#line 481
4576      buffer_size = 2048;
4577    }
4578    }
4579  } else {
4580#line 481
4581    buffer_size = 2048;
4582  }
4583  {
4584#line 482
4585  __cil_tmp46 = (unsigned short )buffer_size;
4586#line 482
4587  __cil_tmp47 = 61443 << 1;
4588#line 482
4589  __cil_tmp48 = *((void **)flash);
4590#line 482
4591  __cil_tmp49 = __cil_tmp48 + __cil_tmp47;
4592#line 482
4593  __cil_tmp50 = (void volatile   *)__cil_tmp49;
4594#line 482
4595  writew(__cil_tmp46, __cil_tmp50);
4596  }
4597#line 484
4598  return (0);
4599}
4600}
4601#line 493 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4602static void flash_exit(struct onenand_flash *flash ) 
4603{ unsigned long __cil_tmp2 ;
4604  unsigned long __cil_tmp3 ;
4605  void *__cil_tmp4 ;
4606  void const   *__cil_tmp5 ;
4607  void *__cil_tmp6 ;
4608  void const   *__cil_tmp7 ;
4609
4610  {
4611  {
4612#line 495
4613  __cil_tmp2 = (unsigned long )flash;
4614#line 495
4615  __cil_tmp3 = __cil_tmp2 + 8;
4616#line 495
4617  __cil_tmp4 = *((void **)__cil_tmp3);
4618#line 495
4619  __cil_tmp5 = (void const   *)__cil_tmp4;
4620#line 495
4621  vfree(__cil_tmp5);
4622#line 496
4623  __cil_tmp6 = *((void **)flash);
4624#line 496
4625  __cil_tmp7 = (void const   *)__cil_tmp6;
4626#line 496
4627  kfree(__cil_tmp7);
4628  }
4629#line 497
4630  return;
4631}
4632}
4633#line 499
4634static int onenand_sim_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
4635#line 499 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4636static int onenand_sim_init(void) 
4637{ void *tmp___7 ;
4638  void *tmp___8 ;
4639  int tmp___9 ;
4640  int tmp___10 ;
4641  size_t __cil_tmp5 ;
4642  void *__cil_tmp6 ;
4643  size_t __cil_tmp7 ;
4644  void const   *__cil_tmp8 ;
4645  unsigned long __cil_tmp9 ;
4646  unsigned long __cil_tmp10 ;
4647  unsigned long __cil_tmp11 ;
4648  unsigned long __cil_tmp12 ;
4649  unsigned long __cil_tmp13 ;
4650  struct onenand_flash *__cil_tmp14 ;
4651  void const   *__cil_tmp15 ;
4652  void const   *__cil_tmp16 ;
4653  unsigned long __cil_tmp17 ;
4654  unsigned long __cil_tmp18 ;
4655  unsigned long __cil_tmp19 ;
4656  unsigned long __cil_tmp20 ;
4657  unsigned long __cil_tmp21 ;
4658  unsigned long __cil_tmp22 ;
4659  unsigned long __cil_tmp23 ;
4660  unsigned long __cil_tmp24 ;
4661  unsigned long __cil_tmp25 ;
4662  unsigned long __cil_tmp26 ;
4663  unsigned long __cil_tmp27 ;
4664  unsigned long __cil_tmp28 ;
4665  unsigned long __cil_tmp29 ;
4666  struct onenand_flash *__cil_tmp30 ;
4667  unsigned long __cil_tmp31 ;
4668  unsigned long __cil_tmp32 ;
4669  unsigned long __cil_tmp33 ;
4670  unsigned long __cil_tmp34 ;
4671  unsigned long __cil_tmp35 ;
4672  unsigned long __cil_tmp36 ;
4673  unsigned long __cil_tmp37 ;
4674  unsigned long __cil_tmp38 ;
4675  struct onenand_chip *__cil_tmp39 ;
4676  unsigned long __cil_tmp40 ;
4677  unsigned long __cil_tmp41 ;
4678  unsigned long __cil_tmp42 ;
4679  struct mtd_info *__cil_tmp43 ;
4680  unsigned long __cil_tmp44 ;
4681  unsigned long __cil_tmp45 ;
4682  struct onenand_flash *__cil_tmp46 ;
4683  void const   *__cil_tmp47 ;
4684  void const   *__cil_tmp48 ;
4685  struct mtd_info *__cil_tmp49 ;
4686  void *__cil_tmp50 ;
4687  char const   **__cil_tmp51 ;
4688  void *__cil_tmp52 ;
4689  struct mtd_part_parser_data *__cil_tmp53 ;
4690  unsigned long __cil_tmp54 ;
4691  unsigned long __cil_tmp55 ;
4692  struct mtd_partition *__cil_tmp56 ;
4693  struct mtd_partition  const  *__cil_tmp57 ;
4694  unsigned long __cil_tmp58 ;
4695  unsigned long __cil_tmp59 ;
4696  int __cil_tmp60 ;
4697
4698  {
4699  {
4700#line 502
4701  __cil_tmp5 = (size_t )4224;
4702#line 502
4703  tmp___7 = kmalloc(__cil_tmp5, 208U);
4704#line 502
4705  ffchars = (unsigned char *)tmp___7;
4706  }
4707#line 503
4708  if (! ffchars) {
4709    {
4710#line 504
4711    printk("<3>Unable to allocate ff chars.\n");
4712    }
4713#line 505
4714    return (-12);
4715  } else {
4716
4717  }
4718  {
4719#line 507
4720  __cil_tmp6 = (void *)ffchars;
4721#line 507
4722  __cil_tmp7 = (size_t )4224;
4723#line 507
4724  memset(__cil_tmp6, 255, __cil_tmp7);
4725#line 510
4726  tmp___8 = kzalloc(1576UL, 208U);
4727#line 510
4728  info = (struct onenand_info *)tmp___8;
4729  }
4730#line 511
4731  if (! info) {
4732    {
4733#line 512
4734    printk("<3>Unable to allocate core structures.\n");
4735#line 513
4736    __cil_tmp8 = (void const   *)ffchars;
4737#line 513
4738    kfree(__cil_tmp8);
4739    }
4740#line 514
4741    return (-12);
4742  } else {
4743
4744  }
4745  {
4746#line 518
4747  __cil_tmp9 = 1160 + 152;
4748#line 518
4749  __cil_tmp10 = (unsigned long )info;
4750#line 518
4751  __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
4752#line 518
4753  *((void (**)(unsigned short value , void *addr ))__cil_tmp11) = & onenand_writew;
4754#line 520
4755  __cil_tmp12 = (unsigned long )info;
4756#line 520
4757  __cil_tmp13 = __cil_tmp12 + 1560;
4758#line 520
4759  __cil_tmp14 = (struct onenand_flash *)__cil_tmp13;
4760#line 520
4761  tmp___9 = flash_init(__cil_tmp14);
4762  }
4763#line 520
4764  if (tmp___9) {
4765    {
4766#line 521
4767    printk("<3>Unable to allocate flash.\n");
4768#line 522
4769    __cil_tmp15 = (void const   *)ffchars;
4770#line 522
4771    kfree(__cil_tmp15);
4772#line 523
4773    __cil_tmp16 = (void const   *)info;
4774#line 523
4775    kfree(__cil_tmp16);
4776    }
4777#line 524
4778    return (-12);
4779  } else {
4780
4781  }
4782  {
4783#line 527
4784  __cil_tmp17 = (unsigned long )info;
4785#line 527
4786  __cil_tmp18 = __cil_tmp17 + 1152;
4787#line 527
4788  __cil_tmp19 = 0 * 40UL;
4789#line 527
4790  __cil_tmp20 = (unsigned long )(os_partitions) + __cil_tmp19;
4791#line 527
4792  *((struct mtd_partition **)__cil_tmp18) = (struct mtd_partition *)__cil_tmp20;
4793#line 529
4794  __cil_tmp21 = (unsigned long )info;
4795#line 529
4796  __cil_tmp22 = __cil_tmp21 + 1160;
4797#line 529
4798  __cil_tmp23 = (unsigned long )info;
4799#line 529
4800  __cil_tmp24 = __cil_tmp23 + 1560;
4801#line 529
4802  *((void **)__cil_tmp22) = *((void **)__cil_tmp24);
4803#line 530
4804  __cil_tmp25 = 1160 + 384;
4805#line 530
4806  __cil_tmp26 = (unsigned long )info;
4807#line 530
4808  __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
4809#line 530
4810  __cil_tmp28 = (unsigned long )info;
4811#line 530
4812  __cil_tmp29 = __cil_tmp28 + 1560;
4813#line 530
4814  __cil_tmp30 = (struct onenand_flash *)__cil_tmp29;
4815#line 530
4816  *((void **)__cil_tmp27) = (void *)__cil_tmp30;
4817#line 532
4818  __cil_tmp31 = 0 + 56;
4819#line 532
4820  __cil_tmp32 = (unsigned long )info;
4821#line 532
4822  __cil_tmp33 = __cil_tmp32 + __cil_tmp31;
4823#line 532
4824  *((char const   **)__cil_tmp33) = "OneNAND simulator";
4825#line 533
4826  __cil_tmp34 = 0 + 360;
4827#line 533
4828  __cil_tmp35 = (unsigned long )info;
4829#line 533
4830  __cil_tmp36 = __cil_tmp35 + __cil_tmp34;
4831#line 533
4832  __cil_tmp37 = (unsigned long )info;
4833#line 533
4834  __cil_tmp38 = __cil_tmp37 + 1160;
4835#line 533
4836  __cil_tmp39 = (struct onenand_chip *)__cil_tmp38;
4837#line 533
4838  *((void **)__cil_tmp36) = (void *)__cil_tmp39;
4839#line 534
4840  __cil_tmp40 = 0 + 368;
4841#line 534
4842  __cil_tmp41 = (unsigned long )info;
4843#line 534
4844  __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
4845#line 534
4846  *((struct module **)__cil_tmp42) = & __this_module;
4847#line 536
4848  __cil_tmp43 = (struct mtd_info *)info;
4849#line 536
4850  tmp___10 = onenand_scan(__cil_tmp43, 1);
4851  }
4852#line 536
4853  if (tmp___10) {
4854    {
4855#line 537
4856    __cil_tmp44 = (unsigned long )info;
4857#line 537
4858    __cil_tmp45 = __cil_tmp44 + 1560;
4859#line 537
4860    __cil_tmp46 = (struct onenand_flash *)__cil_tmp45;
4861#line 537
4862    flash_exit(__cil_tmp46);
4863#line 538
4864    __cil_tmp47 = (void const   *)ffchars;
4865#line 538
4866    kfree(__cil_tmp47);
4867#line 539
4868    __cil_tmp48 = (void const   *)info;
4869#line 539
4870    kfree(__cil_tmp48);
4871    }
4872#line 540
4873    return (-6);
4874  } else {
4875
4876  }
4877  {
4878#line 543
4879  __cil_tmp49 = (struct mtd_info *)info;
4880#line 543
4881  __cil_tmp50 = (void *)0;
4882#line 543
4883  __cil_tmp51 = (char const   **)__cil_tmp50;
4884#line 543
4885  __cil_tmp52 = (void *)0;
4886#line 543
4887  __cil_tmp53 = (struct mtd_part_parser_data *)__cil_tmp52;
4888#line 543
4889  __cil_tmp54 = (unsigned long )info;
4890#line 543
4891  __cil_tmp55 = __cil_tmp54 + 1152;
4892#line 543
4893  __cil_tmp56 = *((struct mtd_partition **)__cil_tmp55);
4894#line 543
4895  __cil_tmp57 = (struct mtd_partition  const  *)__cil_tmp56;
4896#line 543
4897  __cil_tmp58 = 40UL / 40UL;
4898#line 543
4899  __cil_tmp59 = __cil_tmp58 + 0UL;
4900#line 543
4901  __cil_tmp60 = (int )__cil_tmp59;
4902#line 543
4903  mtd_device_parse_register(__cil_tmp49, __cil_tmp51, __cil_tmp53, __cil_tmp57, __cil_tmp60);
4904  }
4905#line 546
4906  return (0);
4907}
4908}
4909#line 549
4910static void onenand_sim_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
4911#line 549 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4912static void onenand_sim_exit(void) 
4913{ struct onenand_chip *this ;
4914  struct onenand_flash *flash ;
4915  unsigned long __cil_tmp3 ;
4916  unsigned long __cil_tmp4 ;
4917  unsigned long __cil_tmp5 ;
4918  void *__cil_tmp6 ;
4919  unsigned long __cil_tmp7 ;
4920  unsigned long __cil_tmp8 ;
4921  void *__cil_tmp9 ;
4922  struct mtd_info *__cil_tmp10 ;
4923  void const   *__cil_tmp11 ;
4924  void const   *__cil_tmp12 ;
4925
4926  {
4927  {
4928#line 551
4929  __cil_tmp3 = 0 + 360;
4930#line 551
4931  __cil_tmp4 = (unsigned long )info;
4932#line 551
4933  __cil_tmp5 = __cil_tmp4 + __cil_tmp3;
4934#line 551
4935  __cil_tmp6 = *((void **)__cil_tmp5);
4936#line 551
4937  this = (struct onenand_chip *)__cil_tmp6;
4938#line 552
4939  __cil_tmp7 = (unsigned long )this;
4940#line 552
4941  __cil_tmp8 = __cil_tmp7 + 384;
4942#line 552
4943  __cil_tmp9 = *((void **)__cil_tmp8);
4944#line 552
4945  flash = (struct onenand_flash *)__cil_tmp9;
4946#line 554
4947  __cil_tmp10 = (struct mtd_info *)info;
4948#line 554
4949  onenand_release(__cil_tmp10);
4950#line 555
4951  flash_exit(flash);
4952#line 556
4953  __cil_tmp11 = (void const   *)ffchars;
4954#line 556
4955  kfree(__cil_tmp11);
4956#line 557
4957  __cil_tmp12 = (void const   *)info;
4958#line 557
4959  kfree(__cil_tmp12);
4960  }
4961#line 558
4962  return;
4963}
4964}
4965#line 560 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4966int init_module(void) 
4967{ int tmp___7 ;
4968
4969  {
4970  {
4971#line 560
4972  tmp___7 = onenand_sim_init();
4973  }
4974#line 560
4975  return (tmp___7);
4976}
4977}
4978#line 561 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4979void cleanup_module(void) 
4980{ 
4981
4982  {
4983  {
4984#line 561
4985  onenand_sim_exit();
4986  }
4987#line 561
4988  return;
4989}
4990}
4991#line 563 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
4992static char const   __mod_author563[49]  __attribute__((__used__, __unused__, __section__(".modinfo"),
4993__aligned__(1)))  = 
4994#line 563
4995  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
4996        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'K', 
4997        (char const   )'y',      (char const   )'u',      (char const   )'n',      (char const   )'g', 
4998        (char const   )'m',      (char const   )'i',      (char const   )'n',      (char const   )' ', 
4999        (char const   )'P',      (char const   )'a',      (char const   )'r',      (char const   )'k', 
5000        (char const   )' ',      (char const   )'<',      (char const   )'k',      (char const   )'y', 
5001        (char const   )'u',      (char const   )'n',      (char const   )'g',      (char const   )'m', 
5002        (char const   )'i',      (char const   )'n',      (char const   )'.',      (char const   )'p', 
5003        (char const   )'a',      (char const   )'r',      (char const   )'k',      (char const   )'@', 
5004        (char const   )'s',      (char const   )'a',      (char const   )'m',      (char const   )'s', 
5005        (char const   )'u',      (char const   )'n',      (char const   )'g',      (char const   )'.', 
5006        (char const   )'c',      (char const   )'o',      (char const   )'m',      (char const   )'>', 
5007        (char const   )'\000'};
5008#line 564 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
5009static char const   __mod_description564[40]  __attribute__((__used__, __unused__,
5010__section__(".modinfo"), __aligned__(1)))  = 
5011#line 564
5012  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
5013        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
5014        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
5015        (char const   )'T',      (char const   )'h',      (char const   )'e',      (char const   )' ', 
5016        (char const   )'O',      (char const   )'n',      (char const   )'e',      (char const   )'N', 
5017        (char const   )'A',      (char const   )'N',      (char const   )'D',      (char const   )' ', 
5018        (char const   )'f',      (char const   )'l',      (char const   )'a',      (char const   )'s', 
5019        (char const   )'h',      (char const   )' ',      (char const   )'s',      (char const   )'i', 
5020        (char const   )'m',      (char const   )'u',      (char const   )'l',      (char const   )'a', 
5021        (char const   )'t',      (char const   )'o',      (char const   )'r',      (char const   )'\000'};
5022#line 565 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
5023static char const   __mod_license565[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
5024__aligned__(1)))  = 
5025#line 565
5026  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
5027        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
5028        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
5029#line 583
5030void ldv_check_final_state(void) ;
5031#line 589
5032extern void ldv_initialize(void) ;
5033#line 592
5034extern int __VERIFIER_nondet_int(void) ;
5035#line 595 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
5036int LDV_IN_INTERRUPT  ;
5037#line 598 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
5038void main(void) 
5039{ int tmp___7 ;
5040  int tmp___8 ;
5041  int tmp___9 ;
5042
5043  {
5044  {
5045#line 610
5046  LDV_IN_INTERRUPT = 1;
5047#line 619
5048  ldv_initialize();
5049#line 667
5050  tmp___7 = onenand_sim_init();
5051  }
5052#line 667
5053  if (tmp___7) {
5054#line 668
5055    goto ldv_final;
5056  } else {
5057
5058  }
5059  {
5060#line 670
5061  while (1) {
5062    while_continue: /* CIL Label */ ;
5063    {
5064#line 670
5065    tmp___9 = __VERIFIER_nondet_int();
5066    }
5067#line 670
5068    if (tmp___9) {
5069
5070    } else {
5071#line 670
5072      goto while_break;
5073    }
5074    {
5075#line 673
5076    tmp___8 = __VERIFIER_nondet_int();
5077    }
5078    {
5079#line 675
5080    goto switch_default;
5081#line 673
5082    if (0) {
5083      switch_default: /* CIL Label */ 
5084#line 675
5085      goto switch_break;
5086    } else {
5087      switch_break: /* CIL Label */ ;
5088    }
5089    }
5090  }
5091  while_break: /* CIL Label */ ;
5092  }
5093  {
5094#line 729
5095  onenand_sim_exit();
5096  }
5097  ldv_final: 
5098  {
5099#line 732
5100  ldv_check_final_state();
5101  }
5102#line 735
5103  return;
5104}
5105}
5106#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5107void ldv_blast_assert(void) 
5108{ 
5109
5110  {
5111  ERROR: 
5112#line 6
5113  goto ERROR;
5114}
5115}
5116#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5117extern int __VERIFIER_nondet_int(void) ;
5118#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5119int ldv_mutex  =    1;
5120#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5121int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
5122{ int nondetermined ;
5123
5124  {
5125#line 29
5126  if (ldv_mutex == 1) {
5127
5128  } else {
5129    {
5130#line 29
5131    ldv_blast_assert();
5132    }
5133  }
5134  {
5135#line 32
5136  nondetermined = __VERIFIER_nondet_int();
5137  }
5138#line 35
5139  if (nondetermined) {
5140#line 38
5141    ldv_mutex = 2;
5142#line 40
5143    return (0);
5144  } else {
5145#line 45
5146    return (-4);
5147  }
5148}
5149}
5150#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5151int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
5152{ int nondetermined ;
5153
5154  {
5155#line 57
5156  if (ldv_mutex == 1) {
5157
5158  } else {
5159    {
5160#line 57
5161    ldv_blast_assert();
5162    }
5163  }
5164  {
5165#line 60
5166  nondetermined = __VERIFIER_nondet_int();
5167  }
5168#line 63
5169  if (nondetermined) {
5170#line 66
5171    ldv_mutex = 2;
5172#line 68
5173    return (0);
5174  } else {
5175#line 73
5176    return (-4);
5177  }
5178}
5179}
5180#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5181int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
5182{ int atomic_value_after_dec ;
5183
5184  {
5185#line 83
5186  if (ldv_mutex == 1) {
5187
5188  } else {
5189    {
5190#line 83
5191    ldv_blast_assert();
5192    }
5193  }
5194  {
5195#line 86
5196  atomic_value_after_dec = __VERIFIER_nondet_int();
5197  }
5198#line 89
5199  if (atomic_value_after_dec == 0) {
5200#line 92
5201    ldv_mutex = 2;
5202#line 94
5203    return (1);
5204  } else {
5205
5206  }
5207#line 98
5208  return (0);
5209}
5210}
5211#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5212void mutex_lock(struct mutex *lock ) 
5213{ 
5214
5215  {
5216#line 108
5217  if (ldv_mutex == 1) {
5218
5219  } else {
5220    {
5221#line 108
5222    ldv_blast_assert();
5223    }
5224  }
5225#line 110
5226  ldv_mutex = 2;
5227#line 111
5228  return;
5229}
5230}
5231#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5232int mutex_trylock(struct mutex *lock ) 
5233{ int nondetermined ;
5234
5235  {
5236#line 121
5237  if (ldv_mutex == 1) {
5238
5239  } else {
5240    {
5241#line 121
5242    ldv_blast_assert();
5243    }
5244  }
5245  {
5246#line 124
5247  nondetermined = __VERIFIER_nondet_int();
5248  }
5249#line 127
5250  if (nondetermined) {
5251#line 130
5252    ldv_mutex = 2;
5253#line 132
5254    return (1);
5255  } else {
5256#line 137
5257    return (0);
5258  }
5259}
5260}
5261#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5262void mutex_unlock(struct mutex *lock ) 
5263{ 
5264
5265  {
5266#line 147
5267  if (ldv_mutex == 2) {
5268
5269  } else {
5270    {
5271#line 147
5272    ldv_blast_assert();
5273    }
5274  }
5275#line 149
5276  ldv_mutex = 1;
5277#line 150
5278  return;
5279}
5280}
5281#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5282void ldv_check_final_state(void) 
5283{ 
5284
5285  {
5286#line 156
5287  if (ldv_mutex == 1) {
5288
5289  } else {
5290    {
5291#line 156
5292    ldv_blast_assert();
5293    }
5294  }
5295#line 157
5296  return;
5297}
5298}
5299#line 744 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/drivers/mtd/onenand/onenand_sim.c.common.c"
5300long s__builtin_expect(long val , long res ) 
5301{ 
5302
5303  {
5304#line 745
5305  return (val);
5306}
5307}