Showing error 151

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-uwb-i1480-dfu-i1480-dfu-usb.ko_safe.cil.out.i.pp.cil.c
Line in file: 4489
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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