Showing error 204

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


Source:

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