Showing error 83

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