Showing error 508

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