Showing error 205

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