Showing error 1095

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