Showing error 123

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-input-misc-keyspan_remote.ko_unsafe.cil.out.i.pp.cil.c
Line in file: 7602
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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