Showing error 191

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-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.c
Line in file: 6860
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

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