Showing error 135

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