Showing error 173

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.c
Line in file: 7923
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

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