Showing error 197

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3644
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 23 "include/asm-generic/int-ll64.h"
   5typedef unsigned short __u16;
   6#line 25 "include/asm-generic/int-ll64.h"
   7typedef int __s32;
   8#line 26 "include/asm-generic/int-ll64.h"
   9typedef unsigned int __u32;
  10#line 30 "include/asm-generic/int-ll64.h"
  11typedef unsigned long long __u64;
  12#line 43 "include/asm-generic/int-ll64.h"
  13typedef unsigned char u8;
  14#line 45 "include/asm-generic/int-ll64.h"
  15typedef short s16;
  16#line 46 "include/asm-generic/int-ll64.h"
  17typedef unsigned short u16;
  18#line 49 "include/asm-generic/int-ll64.h"
  19typedef unsigned int u32;
  20#line 51 "include/asm-generic/int-ll64.h"
  21typedef long long s64;
  22#line 52 "include/asm-generic/int-ll64.h"
  23typedef unsigned long long u64;
  24#line 14 "include/asm-generic/posix_types.h"
  25typedef long __kernel_long_t;
  26#line 15 "include/asm-generic/posix_types.h"
  27typedef unsigned long __kernel_ulong_t;
  28#line 31 "include/asm-generic/posix_types.h"
  29typedef int __kernel_pid_t;
  30#line 52 "include/asm-generic/posix_types.h"
  31typedef unsigned int __kernel_uid32_t;
  32#line 53 "include/asm-generic/posix_types.h"
  33typedef unsigned int __kernel_gid32_t;
  34#line 75 "include/asm-generic/posix_types.h"
  35typedef __kernel_ulong_t __kernel_size_t;
  36#line 76 "include/asm-generic/posix_types.h"
  37typedef __kernel_long_t __kernel_ssize_t;
  38#line 91 "include/asm-generic/posix_types.h"
  39typedef long long __kernel_loff_t;
  40#line 92 "include/asm-generic/posix_types.h"
  41typedef __kernel_long_t __kernel_time_t;
  42#line 93 "include/asm-generic/posix_types.h"
  43typedef __kernel_long_t __kernel_clock_t;
  44#line 94 "include/asm-generic/posix_types.h"
  45typedef int __kernel_timer_t;
  46#line 95 "include/asm-generic/posix_types.h"
  47typedef int __kernel_clockid_t;
  48#line 21 "include/linux/types.h"
  49typedef __u32 __kernel_dev_t;
  50#line 24 "include/linux/types.h"
  51typedef __kernel_dev_t dev_t;
  52#line 27 "include/linux/types.h"
  53typedef unsigned short umode_t;
  54#line 30 "include/linux/types.h"
  55typedef __kernel_pid_t pid_t;
  56#line 35 "include/linux/types.h"
  57typedef __kernel_clockid_t clockid_t;
  58#line 38 "include/linux/types.h"
  59typedef _Bool bool;
  60#line 40 "include/linux/types.h"
  61typedef __kernel_uid32_t uid_t;
  62#line 41 "include/linux/types.h"
  63typedef __kernel_gid32_t gid_t;
  64#line 54 "include/linux/types.h"
  65typedef __kernel_loff_t loff_t;
  66#line 63 "include/linux/types.h"
  67typedef __kernel_size_t size_t;
  68#line 68 "include/linux/types.h"
  69typedef __kernel_ssize_t ssize_t;
  70#line 78 "include/linux/types.h"
  71typedef __kernel_time_t time_t;
  72#line 111 "include/linux/types.h"
  73typedef __s32 int32_t;
  74#line 117 "include/linux/types.h"
  75typedef __u32 uint32_t;
  76#line 155 "include/linux/types.h"
  77typedef u64 dma_addr_t;
  78#line 202 "include/linux/types.h"
  79typedef unsigned int gfp_t;
  80#line 219 "include/linux/types.h"
  81struct __anonstruct_atomic_t_7 {
  82   int counter ;
  83};
  84#line 219 "include/linux/types.h"
  85typedef struct __anonstruct_atomic_t_7 atomic_t;
  86#line 224 "include/linux/types.h"
  87struct __anonstruct_atomic64_t_8 {
  88   long counter ;
  89};
  90#line 224 "include/linux/types.h"
  91typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  92#line 229 "include/linux/types.h"
  93struct list_head {
  94   struct list_head *next ;
  95   struct list_head *prev ;
  96};
  97#line 233
  98struct hlist_node;
  99#line 233 "include/linux/types.h"
 100struct hlist_head {
 101   struct hlist_node *first ;
 102};
 103#line 237 "include/linux/types.h"
 104struct hlist_node {
 105   struct hlist_node *next ;
 106   struct hlist_node **pprev ;
 107};
 108#line 253 "include/linux/types.h"
 109struct rcu_head {
 110   struct rcu_head *next ;
 111   void (*func)(struct rcu_head *head ) ;
 112};
 113#line 146 "include/linux/init.h"
 114typedef void (*ctor_fn_t)(void);
 115#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 116typedef u16 __ticket_t;
 117#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 118typedef u32 __ticketpair_t;
 119#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 120struct __raw_tickets {
 121   __ticket_t head ;
 122   __ticket_t tail ;
 123};
 124#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 125union __anonunion____missing_field_name_9 {
 126   __ticketpair_t head_tail ;
 127   struct __raw_tickets tickets ;
 128};
 129#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 130struct arch_spinlock {
 131   union __anonunion____missing_field_name_9 __annonCompField4 ;
 132};
 133#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 134typedef struct arch_spinlock arch_spinlock_t;
 135#line 12 "include/linux/lockdep.h"
 136struct task_struct;
 137#line 12
 138struct task_struct;
 139#line 391 "include/linux/lockdep.h"
 140struct lock_class_key {
 141
 142};
 143#line 20 "include/linux/spinlock_types.h"
 144struct raw_spinlock {
 145   arch_spinlock_t raw_lock ;
 146   unsigned int magic ;
 147   unsigned int owner_cpu ;
 148   void *owner ;
 149};
 150#line 20 "include/linux/spinlock_types.h"
 151typedef struct raw_spinlock raw_spinlock_t;
 152#line 64 "include/linux/spinlock_types.h"
 153union __anonunion____missing_field_name_12 {
 154   struct raw_spinlock rlock ;
 155};
 156#line 64 "include/linux/spinlock_types.h"
 157struct spinlock {
 158   union __anonunion____missing_field_name_12 __annonCompField6 ;
 159};
 160#line 64 "include/linux/spinlock_types.h"
 161typedef struct spinlock spinlock_t;
 162#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 163struct task_struct;
 164#line 8
 165struct mm_struct;
 166#line 8
 167struct mm_struct;
 168#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 169struct pt_regs {
 170   unsigned long r15 ;
 171   unsigned long r14 ;
 172   unsigned long r13 ;
 173   unsigned long r12 ;
 174   unsigned long bp ;
 175   unsigned long bx ;
 176   unsigned long r11 ;
 177   unsigned long r10 ;
 178   unsigned long r9 ;
 179   unsigned long r8 ;
 180   unsigned long ax ;
 181   unsigned long cx ;
 182   unsigned long dx ;
 183   unsigned long si ;
 184   unsigned long di ;
 185   unsigned long orig_ax ;
 186   unsigned long ip ;
 187   unsigned long cs ;
 188   unsigned long flags ;
 189   unsigned long sp ;
 190   unsigned long ss ;
 191};
 192#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 193struct __anonstruct____missing_field_name_15 {
 194   unsigned int a ;
 195   unsigned int b ;
 196};
 197#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 198struct __anonstruct____missing_field_name_16 {
 199   u16 limit0 ;
 200   u16 base0 ;
 201   unsigned int base1 : 8 ;
 202   unsigned int type : 4 ;
 203   unsigned int s : 1 ;
 204   unsigned int dpl : 2 ;
 205   unsigned int p : 1 ;
 206   unsigned int limit : 4 ;
 207   unsigned int avl : 1 ;
 208   unsigned int l : 1 ;
 209   unsigned int d : 1 ;
 210   unsigned int g : 1 ;
 211   unsigned int base2 : 8 ;
 212};
 213#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 214union __anonunion____missing_field_name_14 {
 215   struct __anonstruct____missing_field_name_15 __annonCompField7 ;
 216   struct __anonstruct____missing_field_name_16 __annonCompField8 ;
 217};
 218#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 219struct desc_struct {
 220   union __anonunion____missing_field_name_14 __annonCompField9 ;
 221} __attribute__((__packed__)) ;
 222#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 223typedef unsigned long pgdval_t;
 224#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 225typedef unsigned long pgprotval_t;
 226#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 227struct pgprot {
 228   pgprotval_t pgprot ;
 229};
 230#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 231typedef struct pgprot pgprot_t;
 232#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 233struct __anonstruct_pgd_t_20 {
 234   pgdval_t pgd ;
 235};
 236#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 237typedef struct __anonstruct_pgd_t_20 pgd_t;
 238#line 282
 239struct page;
 240#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 241typedef struct page *pgtable_t;
 242#line 295
 243struct file;
 244#line 295
 245struct file;
 246#line 313
 247struct seq_file;
 248#line 313
 249struct seq_file;
 250#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 251struct page;
 252#line 47
 253struct thread_struct;
 254#line 47
 255struct thread_struct;
 256#line 50
 257struct mm_struct;
 258#line 51
 259struct desc_struct;
 260#line 52
 261struct task_struct;
 262#line 53
 263struct cpumask;
 264#line 53
 265struct cpumask;
 266#line 329
 267struct arch_spinlock;
 268#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 269struct task_struct;
 270#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 271struct kernel_vm86_regs {
 272   struct pt_regs pt ;
 273   unsigned short es ;
 274   unsigned short __esh ;
 275   unsigned short ds ;
 276   unsigned short __dsh ;
 277   unsigned short fs ;
 278   unsigned short __fsh ;
 279   unsigned short gs ;
 280   unsigned short __gsh ;
 281};
 282#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 283union __anonunion____missing_field_name_24 {
 284   struct pt_regs *regs ;
 285   struct kernel_vm86_regs *vm86 ;
 286};
 287#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 288struct math_emu_info {
 289   long ___orig_eip ;
 290   union __anonunion____missing_field_name_24 __annonCompField10 ;
 291};
 292#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 293struct module;
 294#line 56
 295struct module;
 296#line 9 "include/linux/dynamic_debug.h"
 297struct _ddebug {
 298   char const   *modname ;
 299   char const   *function ;
 300   char const   *filename ;
 301   char const   *format ;
 302   unsigned int lineno : 18 ;
 303   unsigned int flags : 8 ;
 304} __attribute__((__aligned__(8))) ;
 305#line 47
 306struct device;
 307#line 47
 308struct device;
 309#line 135 "include/linux/kernel.h"
 310struct completion;
 311#line 135
 312struct completion;
 313#line 136
 314struct pt_regs;
 315#line 349
 316struct pid;
 317#line 349
 318struct pid;
 319#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 320struct task_struct;
 321#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 322struct page;
 323#line 10 "include/asm-generic/bug.h"
 324struct bug_entry {
 325   int bug_addr_disp ;
 326   int file_disp ;
 327   unsigned short line ;
 328   unsigned short flags ;
 329};
 330#line 12 "include/linux/bug.h"
 331struct pt_regs;
 332#line 14 "include/linux/cpumask.h"
 333struct cpumask {
 334   unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 335};
 336#line 14 "include/linux/cpumask.h"
 337typedef struct cpumask cpumask_t;
 338#line 637 "include/linux/cpumask.h"
 339typedef struct cpumask *cpumask_var_t;
 340#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 341struct static_key;
 342#line 234
 343struct static_key;
 344#line 11 "include/linux/personality.h"
 345struct pt_regs;
 346#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 347struct i387_fsave_struct {
 348   u32 cwd ;
 349   u32 swd ;
 350   u32 twd ;
 351   u32 fip ;
 352   u32 fcs ;
 353   u32 foo ;
 354   u32 fos ;
 355   u32 st_space[20] ;
 356   u32 status ;
 357};
 358#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 359struct __anonstruct____missing_field_name_32 {
 360   u64 rip ;
 361   u64 rdp ;
 362};
 363#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 364struct __anonstruct____missing_field_name_33 {
 365   u32 fip ;
 366   u32 fcs ;
 367   u32 foo ;
 368   u32 fos ;
 369};
 370#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 371union __anonunion____missing_field_name_31 {
 372   struct __anonstruct____missing_field_name_32 __annonCompField14 ;
 373   struct __anonstruct____missing_field_name_33 __annonCompField15 ;
 374};
 375#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 376union __anonunion____missing_field_name_34 {
 377   u32 padding1[12] ;
 378   u32 sw_reserved[12] ;
 379};
 380#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 381struct i387_fxsave_struct {
 382   u16 cwd ;
 383   u16 swd ;
 384   u16 twd ;
 385   u16 fop ;
 386   union __anonunion____missing_field_name_31 __annonCompField16 ;
 387   u32 mxcsr ;
 388   u32 mxcsr_mask ;
 389   u32 st_space[32] ;
 390   u32 xmm_space[64] ;
 391   u32 padding[12] ;
 392   union __anonunion____missing_field_name_34 __annonCompField17 ;
 393} __attribute__((__aligned__(16))) ;
 394#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 395struct i387_soft_struct {
 396   u32 cwd ;
 397   u32 swd ;
 398   u32 twd ;
 399   u32 fip ;
 400   u32 fcs ;
 401   u32 foo ;
 402   u32 fos ;
 403   u32 st_space[20] ;
 404   u8 ftop ;
 405   u8 changed ;
 406   u8 lookahead ;
 407   u8 no_update ;
 408   u8 rm ;
 409   u8 alimit ;
 410   struct math_emu_info *info ;
 411   u32 entry_eip ;
 412};
 413#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 414struct ymmh_struct {
 415   u32 ymmh_space[64] ;
 416};
 417#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 418struct xsave_hdr_struct {
 419   u64 xstate_bv ;
 420   u64 reserved1[2] ;
 421   u64 reserved2[5] ;
 422} __attribute__((__packed__)) ;
 423#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 424struct xsave_struct {
 425   struct i387_fxsave_struct i387 ;
 426   struct xsave_hdr_struct xsave_hdr ;
 427   struct ymmh_struct ymmh ;
 428} __attribute__((__packed__, __aligned__(64))) ;
 429#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 430union thread_xstate {
 431   struct i387_fsave_struct fsave ;
 432   struct i387_fxsave_struct fxsave ;
 433   struct i387_soft_struct soft ;
 434   struct xsave_struct xsave ;
 435};
 436#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 437struct fpu {
 438   unsigned int last_cpu ;
 439   unsigned int has_fpu ;
 440   union thread_xstate *state ;
 441};
 442#line 433
 443struct kmem_cache;
 444#line 435
 445struct perf_event;
 446#line 435
 447struct perf_event;
 448#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 449struct thread_struct {
 450   struct desc_struct tls_array[3] ;
 451   unsigned long sp0 ;
 452   unsigned long sp ;
 453   unsigned long usersp ;
 454   unsigned short es ;
 455   unsigned short ds ;
 456   unsigned short fsindex ;
 457   unsigned short gsindex ;
 458   unsigned long fs ;
 459   unsigned long gs ;
 460   struct perf_event *ptrace_bps[4] ;
 461   unsigned long debugreg6 ;
 462   unsigned long ptrace_dr7 ;
 463   unsigned long cr2 ;
 464   unsigned long trap_nr ;
 465   unsigned long error_code ;
 466   struct fpu fpu ;
 467   unsigned long *io_bitmap_ptr ;
 468   unsigned long iopl ;
 469   unsigned int io_bitmap_max ;
 470};
 471#line 23 "include/asm-generic/atomic-long.h"
 472typedef atomic64_t atomic_long_t;
 473#line 48 "include/linux/mutex.h"
 474struct mutex {
 475   atomic_t count ;
 476   spinlock_t wait_lock ;
 477   struct list_head wait_list ;
 478   struct task_struct *owner ;
 479   char const   *name ;
 480   void *magic ;
 481};
 482#line 69 "include/linux/mutex.h"
 483struct mutex_waiter {
 484   struct list_head list ;
 485   struct task_struct *task ;
 486   void *magic ;
 487};
 488#line 202 "include/linux/ioport.h"
 489struct device;
 490#line 20 "include/linux/kobject_ns.h"
 491struct sock;
 492#line 20
 493struct sock;
 494#line 21
 495struct kobject;
 496#line 21
 497struct kobject;
 498#line 27
 499enum kobj_ns_type {
 500    KOBJ_NS_TYPE_NONE = 0,
 501    KOBJ_NS_TYPE_NET = 1,
 502    KOBJ_NS_TYPES = 2
 503} ;
 504#line 40 "include/linux/kobject_ns.h"
 505struct kobj_ns_type_operations {
 506   enum kobj_ns_type type ;
 507   void *(*grab_current_ns)(void) ;
 508   void const   *(*netlink_ns)(struct sock *sk ) ;
 509   void const   *(*initial_ns)(void) ;
 510   void (*drop_ns)(void * ) ;
 511};
 512#line 22 "include/linux/sysfs.h"
 513struct kobject;
 514#line 23
 515struct module;
 516#line 24
 517enum kobj_ns_type;
 518#line 26 "include/linux/sysfs.h"
 519struct attribute {
 520   char const   *name ;
 521   umode_t mode ;
 522};
 523#line 56 "include/linux/sysfs.h"
 524struct attribute_group {
 525   char const   *name ;
 526   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 527   struct attribute **attrs ;
 528};
 529#line 85
 530struct file;
 531#line 86
 532struct vm_area_struct;
 533#line 86
 534struct vm_area_struct;
 535#line 88 "include/linux/sysfs.h"
 536struct bin_attribute {
 537   struct attribute attr ;
 538   size_t size ;
 539   void *private ;
 540   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 541                   loff_t  , size_t  ) ;
 542   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 543                    loff_t  , size_t  ) ;
 544   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 545};
 546#line 112 "include/linux/sysfs.h"
 547struct sysfs_ops {
 548   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 549   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 550   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 551};
 552#line 118
 553struct sysfs_dirent;
 554#line 118
 555struct sysfs_dirent;
 556#line 12 "include/linux/thread_info.h"
 557struct timespec;
 558#line 12
 559struct timespec;
 560#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 561struct task_struct;
 562#line 22 "include/linux/kref.h"
 563struct kref {
 564   atomic_t refcount ;
 565};
 566#line 49 "include/linux/wait.h"
 567struct __wait_queue_head {
 568   spinlock_t lock ;
 569   struct list_head task_list ;
 570};
 571#line 53 "include/linux/wait.h"
 572typedef struct __wait_queue_head wait_queue_head_t;
 573#line 55
 574struct task_struct;
 575#line 60 "include/linux/kobject.h"
 576struct kset;
 577#line 60
 578struct kobj_type;
 579#line 60 "include/linux/kobject.h"
 580struct kobject {
 581   char const   *name ;
 582   struct list_head entry ;
 583   struct kobject *parent ;
 584   struct kset *kset ;
 585   struct kobj_type *ktype ;
 586   struct sysfs_dirent *sd ;
 587   struct kref kref ;
 588   unsigned int state_initialized : 1 ;
 589   unsigned int state_in_sysfs : 1 ;
 590   unsigned int state_add_uevent_sent : 1 ;
 591   unsigned int state_remove_uevent_sent : 1 ;
 592   unsigned int uevent_suppress : 1 ;
 593};
 594#line 108 "include/linux/kobject.h"
 595struct kobj_type {
 596   void (*release)(struct kobject *kobj ) ;
 597   struct sysfs_ops  const  *sysfs_ops ;
 598   struct attribute **default_attrs ;
 599   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 600   void const   *(*namespace)(struct kobject *kobj ) ;
 601};
 602#line 116 "include/linux/kobject.h"
 603struct kobj_uevent_env {
 604   char *envp[32] ;
 605   int envp_idx ;
 606   char buf[2048] ;
 607   int buflen ;
 608};
 609#line 123 "include/linux/kobject.h"
 610struct kset_uevent_ops {
 611   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 612   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 613   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 614};
 615#line 140
 616struct sock;
 617#line 159 "include/linux/kobject.h"
 618struct kset {
 619   struct list_head list ;
 620   spinlock_t list_lock ;
 621   struct kobject kobj ;
 622   struct kset_uevent_ops  const  *uevent_ops ;
 623};
 624#line 19 "include/linux/klist.h"
 625struct klist_node;
 626#line 19
 627struct klist_node;
 628#line 39 "include/linux/klist.h"
 629struct klist_node {
 630   void *n_klist ;
 631   struct list_head n_node ;
 632   struct kref n_ref ;
 633};
 634#line 119 "include/linux/seqlock.h"
 635struct seqcount {
 636   unsigned int sequence ;
 637};
 638#line 119 "include/linux/seqlock.h"
 639typedef struct seqcount seqcount_t;
 640#line 14 "include/linux/time.h"
 641struct timespec {
 642   __kernel_time_t tv_sec ;
 643   long tv_nsec ;
 644};
 645#line 46 "include/linux/ktime.h"
 646union ktime {
 647   s64 tv64 ;
 648};
 649#line 59 "include/linux/ktime.h"
 650typedef union ktime ktime_t;
 651#line 10 "include/linux/timer.h"
 652struct tvec_base;
 653#line 10
 654struct tvec_base;
 655#line 12 "include/linux/timer.h"
 656struct timer_list {
 657   struct list_head entry ;
 658   unsigned long expires ;
 659   struct tvec_base *base ;
 660   void (*function)(unsigned long  ) ;
 661   unsigned long data ;
 662   int slack ;
 663   int start_pid ;
 664   void *start_site ;
 665   char start_comm[16] ;
 666};
 667#line 289
 668struct hrtimer;
 669#line 289
 670struct hrtimer;
 671#line 290
 672enum hrtimer_restart;
 673#line 17 "include/linux/workqueue.h"
 674struct work_struct;
 675#line 17
 676struct work_struct;
 677#line 79 "include/linux/workqueue.h"
 678struct work_struct {
 679   atomic_long_t data ;
 680   struct list_head entry ;
 681   void (*func)(struct work_struct *work ) ;
 682};
 683#line 25 "include/linux/completion.h"
 684struct completion {
 685   unsigned int done ;
 686   wait_queue_head_t wait ;
 687};
 688#line 42 "include/linux/pm.h"
 689struct device;
 690#line 50 "include/linux/pm.h"
 691struct pm_message {
 692   int event ;
 693};
 694#line 50 "include/linux/pm.h"
 695typedef struct pm_message pm_message_t;
 696#line 264 "include/linux/pm.h"
 697struct dev_pm_ops {
 698   int (*prepare)(struct device *dev ) ;
 699   void (*complete)(struct device *dev ) ;
 700   int (*suspend)(struct device *dev ) ;
 701   int (*resume)(struct device *dev ) ;
 702   int (*freeze)(struct device *dev ) ;
 703   int (*thaw)(struct device *dev ) ;
 704   int (*poweroff)(struct device *dev ) ;
 705   int (*restore)(struct device *dev ) ;
 706   int (*suspend_late)(struct device *dev ) ;
 707   int (*resume_early)(struct device *dev ) ;
 708   int (*freeze_late)(struct device *dev ) ;
 709   int (*thaw_early)(struct device *dev ) ;
 710   int (*poweroff_late)(struct device *dev ) ;
 711   int (*restore_early)(struct device *dev ) ;
 712   int (*suspend_noirq)(struct device *dev ) ;
 713   int (*resume_noirq)(struct device *dev ) ;
 714   int (*freeze_noirq)(struct device *dev ) ;
 715   int (*thaw_noirq)(struct device *dev ) ;
 716   int (*poweroff_noirq)(struct device *dev ) ;
 717   int (*restore_noirq)(struct device *dev ) ;
 718   int (*runtime_suspend)(struct device *dev ) ;
 719   int (*runtime_resume)(struct device *dev ) ;
 720   int (*runtime_idle)(struct device *dev ) ;
 721};
 722#line 458
 723enum rpm_status {
 724    RPM_ACTIVE = 0,
 725    RPM_RESUMING = 1,
 726    RPM_SUSPENDED = 2,
 727    RPM_SUSPENDING = 3
 728} ;
 729#line 480
 730enum rpm_request {
 731    RPM_REQ_NONE = 0,
 732    RPM_REQ_IDLE = 1,
 733    RPM_REQ_SUSPEND = 2,
 734    RPM_REQ_AUTOSUSPEND = 3,
 735    RPM_REQ_RESUME = 4
 736} ;
 737#line 488
 738struct wakeup_source;
 739#line 488
 740struct wakeup_source;
 741#line 495 "include/linux/pm.h"
 742struct pm_subsys_data {
 743   spinlock_t lock ;
 744   unsigned int refcount ;
 745};
 746#line 506
 747struct dev_pm_qos_request;
 748#line 506
 749struct pm_qos_constraints;
 750#line 506 "include/linux/pm.h"
 751struct dev_pm_info {
 752   pm_message_t power_state ;
 753   unsigned int can_wakeup : 1 ;
 754   unsigned int async_suspend : 1 ;
 755   bool is_prepared : 1 ;
 756   bool is_suspended : 1 ;
 757   bool ignore_children : 1 ;
 758   spinlock_t lock ;
 759   struct list_head entry ;
 760   struct completion completion ;
 761   struct wakeup_source *wakeup ;
 762   bool wakeup_path : 1 ;
 763   struct timer_list suspend_timer ;
 764   unsigned long timer_expires ;
 765   struct work_struct work ;
 766   wait_queue_head_t wait_queue ;
 767   atomic_t usage_count ;
 768   atomic_t child_count ;
 769   unsigned int disable_depth : 3 ;
 770   unsigned int idle_notification : 1 ;
 771   unsigned int request_pending : 1 ;
 772   unsigned int deferred_resume : 1 ;
 773   unsigned int run_wake : 1 ;
 774   unsigned int runtime_auto : 1 ;
 775   unsigned int no_callbacks : 1 ;
 776   unsigned int irq_safe : 1 ;
 777   unsigned int use_autosuspend : 1 ;
 778   unsigned int timer_autosuspends : 1 ;
 779   enum rpm_request request ;
 780   enum rpm_status runtime_status ;
 781   int runtime_error ;
 782   int autosuspend_delay ;
 783   unsigned long last_busy ;
 784   unsigned long active_jiffies ;
 785   unsigned long suspended_jiffies ;
 786   unsigned long accounting_timestamp ;
 787   ktime_t suspend_time ;
 788   s64 max_time_suspended_ns ;
 789   struct dev_pm_qos_request *pq_req ;
 790   struct pm_subsys_data *subsys_data ;
 791   struct pm_qos_constraints *constraints ;
 792};
 793#line 564 "include/linux/pm.h"
 794struct dev_pm_domain {
 795   struct dev_pm_ops ops ;
 796};
 797#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 798struct dma_map_ops;
 799#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 800struct dev_archdata {
 801   void *acpi_handle ;
 802   struct dma_map_ops *dma_ops ;
 803   void *iommu ;
 804};
 805#line 28 "include/linux/device.h"
 806struct device;
 807#line 29
 808struct device_private;
 809#line 29
 810struct device_private;
 811#line 30
 812struct device_driver;
 813#line 30
 814struct device_driver;
 815#line 31
 816struct driver_private;
 817#line 31
 818struct driver_private;
 819#line 32
 820struct module;
 821#line 33
 822struct class;
 823#line 33
 824struct class;
 825#line 34
 826struct subsys_private;
 827#line 34
 828struct subsys_private;
 829#line 35
 830struct bus_type;
 831#line 35
 832struct bus_type;
 833#line 36
 834struct device_node;
 835#line 36
 836struct device_node;
 837#line 37
 838struct iommu_ops;
 839#line 37
 840struct iommu_ops;
 841#line 39 "include/linux/device.h"
 842struct bus_attribute {
 843   struct attribute attr ;
 844   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
 845   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 846};
 847#line 89
 848struct device_attribute;
 849#line 89
 850struct driver_attribute;
 851#line 89 "include/linux/device.h"
 852struct bus_type {
 853   char const   *name ;
 854   char const   *dev_name ;
 855   struct device *dev_root ;
 856   struct bus_attribute *bus_attrs ;
 857   struct device_attribute *dev_attrs ;
 858   struct driver_attribute *drv_attrs ;
 859   int (*match)(struct device *dev , struct device_driver *drv ) ;
 860   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 861   int (*probe)(struct device *dev ) ;
 862   int (*remove)(struct device *dev ) ;
 863   void (*shutdown)(struct device *dev ) ;
 864   int (*suspend)(struct device *dev , pm_message_t state ) ;
 865   int (*resume)(struct device *dev ) ;
 866   struct dev_pm_ops  const  *pm ;
 867   struct iommu_ops *iommu_ops ;
 868   struct subsys_private *p ;
 869};
 870#line 127
 871struct device_type;
 872#line 214
 873struct of_device_id;
 874#line 214 "include/linux/device.h"
 875struct device_driver {
 876   char const   *name ;
 877   struct bus_type *bus ;
 878   struct module *owner ;
 879   char const   *mod_name ;
 880   bool suppress_bind_attrs ;
 881   struct of_device_id  const  *of_match_table ;
 882   int (*probe)(struct device *dev ) ;
 883   int (*remove)(struct device *dev ) ;
 884   void (*shutdown)(struct device *dev ) ;
 885   int (*suspend)(struct device *dev , pm_message_t state ) ;
 886   int (*resume)(struct device *dev ) ;
 887   struct attribute_group  const  **groups ;
 888   struct dev_pm_ops  const  *pm ;
 889   struct driver_private *p ;
 890};
 891#line 249 "include/linux/device.h"
 892struct driver_attribute {
 893   struct attribute attr ;
 894   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
 895   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
 896};
 897#line 330
 898struct class_attribute;
 899#line 330 "include/linux/device.h"
 900struct class {
 901   char const   *name ;
 902   struct module *owner ;
 903   struct class_attribute *class_attrs ;
 904   struct device_attribute *dev_attrs ;
 905   struct bin_attribute *dev_bin_attrs ;
 906   struct kobject *dev_kobj ;
 907   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 908   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 909   void (*class_release)(struct class *class ) ;
 910   void (*dev_release)(struct device *dev ) ;
 911   int (*suspend)(struct device *dev , pm_message_t state ) ;
 912   int (*resume)(struct device *dev ) ;
 913   struct kobj_ns_type_operations  const  *ns_type ;
 914   void const   *(*namespace)(struct device *dev ) ;
 915   struct dev_pm_ops  const  *pm ;
 916   struct subsys_private *p ;
 917};
 918#line 397 "include/linux/device.h"
 919struct class_attribute {
 920   struct attribute attr ;
 921   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
 922   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
 923                    size_t count ) ;
 924   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
 925};
 926#line 465 "include/linux/device.h"
 927struct device_type {
 928   char const   *name ;
 929   struct attribute_group  const  **groups ;
 930   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 931   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 932   void (*release)(struct device *dev ) ;
 933   struct dev_pm_ops  const  *pm ;
 934};
 935#line 476 "include/linux/device.h"
 936struct device_attribute {
 937   struct attribute attr ;
 938   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
 939   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
 940                    size_t count ) ;
 941};
 942#line 559 "include/linux/device.h"
 943struct device_dma_parameters {
 944   unsigned int max_segment_size ;
 945   unsigned long segment_boundary_mask ;
 946};
 947#line 627
 948struct dma_coherent_mem;
 949#line 627 "include/linux/device.h"
 950struct device {
 951   struct device *parent ;
 952   struct device_private *p ;
 953   struct kobject kobj ;
 954   char const   *init_name ;
 955   struct device_type  const  *type ;
 956   struct mutex mutex ;
 957   struct bus_type *bus ;
 958   struct device_driver *driver ;
 959   void *platform_data ;
 960   struct dev_pm_info power ;
 961   struct dev_pm_domain *pm_domain ;
 962   int numa_node ;
 963   u64 *dma_mask ;
 964   u64 coherent_dma_mask ;
 965   struct device_dma_parameters *dma_parms ;
 966   struct list_head dma_pools ;
 967   struct dma_coherent_mem *dma_mem ;
 968   struct dev_archdata archdata ;
 969   struct device_node *of_node ;
 970   dev_t devt ;
 971   u32 id ;
 972   spinlock_t devres_lock ;
 973   struct list_head devres_head ;
 974   struct klist_node knode_class ;
 975   struct class *class ;
 976   struct attribute_group  const  **groups ;
 977   void (*release)(struct device *dev ) ;
 978};
 979#line 43 "include/linux/pm_wakeup.h"
 980struct wakeup_source {
 981   char const   *name ;
 982   struct list_head entry ;
 983   spinlock_t lock ;
 984   struct timer_list timer ;
 985   unsigned long timer_expires ;
 986   ktime_t total_time ;
 987   ktime_t max_time ;
 988   ktime_t last_time ;
 989   unsigned long event_count ;
 990   unsigned long active_count ;
 991   unsigned long relax_count ;
 992   unsigned long hit_count ;
 993   unsigned int active : 1 ;
 994};
 995#line 12 "include/linux/mod_devicetable.h"
 996typedef unsigned long kernel_ulong_t;
 997#line 219 "include/linux/mod_devicetable.h"
 998struct of_device_id {
 999   char name[32] ;
1000   char type[32] ;
1001   char compatible[128] ;
1002   void *data ;
1003};
1004#line 442 "include/linux/mod_devicetable.h"
1005struct spi_device_id {
1006   char name[32] ;
1007   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
1008};
1009#line 98 "include/linux/nodemask.h"
1010struct __anonstruct_nodemask_t_45 {
1011   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1012};
1013#line 98 "include/linux/nodemask.h"
1014typedef struct __anonstruct_nodemask_t_45 nodemask_t;
1015#line 60 "include/linux/pageblock-flags.h"
1016struct page;
1017#line 19 "include/linux/rwsem.h"
1018struct rw_semaphore;
1019#line 19
1020struct rw_semaphore;
1021#line 25 "include/linux/rwsem.h"
1022struct rw_semaphore {
1023   long count ;
1024   raw_spinlock_t wait_lock ;
1025   struct list_head wait_list ;
1026};
1027#line 9 "include/linux/memory_hotplug.h"
1028struct page;
1029#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
1030struct device;
1031#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
1032struct __anonstruct_mm_context_t_113 {
1033   void *ldt ;
1034   int size ;
1035   unsigned short ia32_compat ;
1036   struct mutex lock ;
1037   void *vdso ;
1038};
1039#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
1040typedef struct __anonstruct_mm_context_t_113 mm_context_t;
1041#line 8 "include/linux/vmalloc.h"
1042struct vm_area_struct;
1043#line 994 "include/linux/mmzone.h"
1044struct page;
1045#line 10 "include/linux/gfp.h"
1046struct vm_area_struct;
1047#line 46 "include/linux/slub_def.h"
1048struct kmem_cache_cpu {
1049   void **freelist ;
1050   unsigned long tid ;
1051   struct page *page ;
1052   struct page *partial ;
1053   int node ;
1054   unsigned int stat[26] ;
1055};
1056#line 57 "include/linux/slub_def.h"
1057struct kmem_cache_node {
1058   spinlock_t list_lock ;
1059   unsigned long nr_partial ;
1060   struct list_head partial ;
1061   atomic_long_t nr_slabs ;
1062   atomic_long_t total_objects ;
1063   struct list_head full ;
1064};
1065#line 73 "include/linux/slub_def.h"
1066struct kmem_cache_order_objects {
1067   unsigned long x ;
1068};
1069#line 80 "include/linux/slub_def.h"
1070struct kmem_cache {
1071   struct kmem_cache_cpu *cpu_slab ;
1072   unsigned long flags ;
1073   unsigned long min_partial ;
1074   int size ;
1075   int objsize ;
1076   int offset ;
1077   int cpu_partial ;
1078   struct kmem_cache_order_objects oo ;
1079   struct kmem_cache_order_objects max ;
1080   struct kmem_cache_order_objects min ;
1081   gfp_t allocflags ;
1082   int refcount ;
1083   void (*ctor)(void * ) ;
1084   int inuse ;
1085   int align ;
1086   int reserved ;
1087   char const   *name ;
1088   struct list_head list ;
1089   struct kobject kobj ;
1090   int remote_node_defrag_ratio ;
1091   struct kmem_cache_node *node[1 << 10] ;
1092};
1093#line 18 "include/linux/capability.h"
1094struct task_struct;
1095#line 94 "include/linux/capability.h"
1096struct kernel_cap_struct {
1097   __u32 cap[2] ;
1098};
1099#line 94 "include/linux/capability.h"
1100typedef struct kernel_cap_struct kernel_cap_t;
1101#line 378
1102struct user_namespace;
1103#line 378
1104struct user_namespace;
1105#line 100 "include/linux/rbtree.h"
1106struct rb_node {
1107   unsigned long rb_parent_color ;
1108   struct rb_node *rb_right ;
1109   struct rb_node *rb_left ;
1110} __attribute__((__aligned__(sizeof(long )))) ;
1111#line 110 "include/linux/rbtree.h"
1112struct rb_root {
1113   struct rb_node *rb_node ;
1114};
1115#line 14 "include/linux/prio_tree.h"
1116struct prio_tree_node;
1117#line 14 "include/linux/prio_tree.h"
1118struct raw_prio_tree_node {
1119   struct prio_tree_node *left ;
1120   struct prio_tree_node *right ;
1121   struct prio_tree_node *parent ;
1122};
1123#line 20 "include/linux/prio_tree.h"
1124struct prio_tree_node {
1125   struct prio_tree_node *left ;
1126   struct prio_tree_node *right ;
1127   struct prio_tree_node *parent ;
1128   unsigned long start ;
1129   unsigned long last ;
1130};
1131#line 23 "include/linux/mm_types.h"
1132struct address_space;
1133#line 23
1134struct address_space;
1135#line 40 "include/linux/mm_types.h"
1136union __anonunion____missing_field_name_142 {
1137   unsigned long index ;
1138   void *freelist ;
1139};
1140#line 40 "include/linux/mm_types.h"
1141struct __anonstruct____missing_field_name_146 {
1142   unsigned int inuse : 16 ;
1143   unsigned int objects : 15 ;
1144   unsigned int frozen : 1 ;
1145};
1146#line 40 "include/linux/mm_types.h"
1147union __anonunion____missing_field_name_145 {
1148   atomic_t _mapcount ;
1149   struct __anonstruct____missing_field_name_146 __annonCompField31 ;
1150};
1151#line 40 "include/linux/mm_types.h"
1152struct __anonstruct____missing_field_name_144 {
1153   union __anonunion____missing_field_name_145 __annonCompField32 ;
1154   atomic_t _count ;
1155};
1156#line 40 "include/linux/mm_types.h"
1157union __anonunion____missing_field_name_143 {
1158   unsigned long counters ;
1159   struct __anonstruct____missing_field_name_144 __annonCompField33 ;
1160};
1161#line 40 "include/linux/mm_types.h"
1162struct __anonstruct____missing_field_name_141 {
1163   union __anonunion____missing_field_name_142 __annonCompField30 ;
1164   union __anonunion____missing_field_name_143 __annonCompField34 ;
1165};
1166#line 40 "include/linux/mm_types.h"
1167struct __anonstruct____missing_field_name_148 {
1168   struct page *next ;
1169   int pages ;
1170   int pobjects ;
1171};
1172#line 40 "include/linux/mm_types.h"
1173union __anonunion____missing_field_name_147 {
1174   struct list_head lru ;
1175   struct __anonstruct____missing_field_name_148 __annonCompField36 ;
1176};
1177#line 40 "include/linux/mm_types.h"
1178union __anonunion____missing_field_name_149 {
1179   unsigned long private ;
1180   struct kmem_cache *slab ;
1181   struct page *first_page ;
1182};
1183#line 40 "include/linux/mm_types.h"
1184struct page {
1185   unsigned long flags ;
1186   struct address_space *mapping ;
1187   struct __anonstruct____missing_field_name_141 __annonCompField35 ;
1188   union __anonunion____missing_field_name_147 __annonCompField37 ;
1189   union __anonunion____missing_field_name_149 __annonCompField38 ;
1190   unsigned long debug_flags ;
1191} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1192#line 200 "include/linux/mm_types.h"
1193struct __anonstruct_vm_set_151 {
1194   struct list_head list ;
1195   void *parent ;
1196   struct vm_area_struct *head ;
1197};
1198#line 200 "include/linux/mm_types.h"
1199union __anonunion_shared_150 {
1200   struct __anonstruct_vm_set_151 vm_set ;
1201   struct raw_prio_tree_node prio_tree_node ;
1202};
1203#line 200
1204struct anon_vma;
1205#line 200
1206struct vm_operations_struct;
1207#line 200
1208struct mempolicy;
1209#line 200 "include/linux/mm_types.h"
1210struct vm_area_struct {
1211   struct mm_struct *vm_mm ;
1212   unsigned long vm_start ;
1213   unsigned long vm_end ;
1214   struct vm_area_struct *vm_next ;
1215   struct vm_area_struct *vm_prev ;
1216   pgprot_t vm_page_prot ;
1217   unsigned long vm_flags ;
1218   struct rb_node vm_rb ;
1219   union __anonunion_shared_150 shared ;
1220   struct list_head anon_vma_chain ;
1221   struct anon_vma *anon_vma ;
1222   struct vm_operations_struct  const  *vm_ops ;
1223   unsigned long vm_pgoff ;
1224   struct file *vm_file ;
1225   void *vm_private_data ;
1226   struct mempolicy *vm_policy ;
1227};
1228#line 257 "include/linux/mm_types.h"
1229struct core_thread {
1230   struct task_struct *task ;
1231   struct core_thread *next ;
1232};
1233#line 262 "include/linux/mm_types.h"
1234struct core_state {
1235   atomic_t nr_threads ;
1236   struct core_thread dumper ;
1237   struct completion startup ;
1238};
1239#line 284 "include/linux/mm_types.h"
1240struct mm_rss_stat {
1241   atomic_long_t count[3] ;
1242};
1243#line 288
1244struct linux_binfmt;
1245#line 288
1246struct mmu_notifier_mm;
1247#line 288 "include/linux/mm_types.h"
1248struct mm_struct {
1249   struct vm_area_struct *mmap ;
1250   struct rb_root mm_rb ;
1251   struct vm_area_struct *mmap_cache ;
1252   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
1253                                      unsigned long pgoff , unsigned long flags ) ;
1254   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
1255   unsigned long mmap_base ;
1256   unsigned long task_size ;
1257   unsigned long cached_hole_size ;
1258   unsigned long free_area_cache ;
1259   pgd_t *pgd ;
1260   atomic_t mm_users ;
1261   atomic_t mm_count ;
1262   int map_count ;
1263   spinlock_t page_table_lock ;
1264   struct rw_semaphore mmap_sem ;
1265   struct list_head mmlist ;
1266   unsigned long hiwater_rss ;
1267   unsigned long hiwater_vm ;
1268   unsigned long total_vm ;
1269   unsigned long locked_vm ;
1270   unsigned long pinned_vm ;
1271   unsigned long shared_vm ;
1272   unsigned long exec_vm ;
1273   unsigned long stack_vm ;
1274   unsigned long reserved_vm ;
1275   unsigned long def_flags ;
1276   unsigned long nr_ptes ;
1277   unsigned long start_code ;
1278   unsigned long end_code ;
1279   unsigned long start_data ;
1280   unsigned long end_data ;
1281   unsigned long start_brk ;
1282   unsigned long brk ;
1283   unsigned long start_stack ;
1284   unsigned long arg_start ;
1285   unsigned long arg_end ;
1286   unsigned long env_start ;
1287   unsigned long env_end ;
1288   unsigned long saved_auxv[44] ;
1289   struct mm_rss_stat rss_stat ;
1290   struct linux_binfmt *binfmt ;
1291   cpumask_var_t cpu_vm_mask_var ;
1292   mm_context_t context ;
1293   unsigned int faultstamp ;
1294   unsigned int token_priority ;
1295   unsigned int last_interval ;
1296   unsigned long flags ;
1297   struct core_state *core_state ;
1298   spinlock_t ioctx_lock ;
1299   struct hlist_head ioctx_list ;
1300   struct task_struct *owner ;
1301   struct file *exe_file ;
1302   unsigned long num_exe_file_vmas ;
1303   struct mmu_notifier_mm *mmu_notifier_mm ;
1304   pgtable_t pmd_huge_pte ;
1305   struct cpumask cpumask_allocation ;
1306};
1307#line 7 "include/asm-generic/cputime.h"
1308typedef unsigned long cputime_t;
1309#line 84 "include/linux/sem.h"
1310struct task_struct;
1311#line 101
1312struct sem_undo_list;
1313#line 101 "include/linux/sem.h"
1314struct sysv_sem {
1315   struct sem_undo_list *undo_list ;
1316};
1317#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1318struct siginfo;
1319#line 10
1320struct siginfo;
1321#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1322struct __anonstruct_sigset_t_153 {
1323   unsigned long sig[1] ;
1324};
1325#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1326typedef struct __anonstruct_sigset_t_153 sigset_t;
1327#line 17 "include/asm-generic/signal-defs.h"
1328typedef void __signalfn_t(int  );
1329#line 18 "include/asm-generic/signal-defs.h"
1330typedef __signalfn_t *__sighandler_t;
1331#line 20 "include/asm-generic/signal-defs.h"
1332typedef void __restorefn_t(void);
1333#line 21 "include/asm-generic/signal-defs.h"
1334typedef __restorefn_t *__sigrestore_t;
1335#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1336struct sigaction {
1337   __sighandler_t sa_handler ;
1338   unsigned long sa_flags ;
1339   __sigrestore_t sa_restorer ;
1340   sigset_t sa_mask ;
1341};
1342#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1343struct k_sigaction {
1344   struct sigaction sa ;
1345};
1346#line 7 "include/asm-generic/siginfo.h"
1347union sigval {
1348   int sival_int ;
1349   void *sival_ptr ;
1350};
1351#line 7 "include/asm-generic/siginfo.h"
1352typedef union sigval sigval_t;
1353#line 48 "include/asm-generic/siginfo.h"
1354struct __anonstruct__kill_155 {
1355   __kernel_pid_t _pid ;
1356   __kernel_uid32_t _uid ;
1357};
1358#line 48 "include/asm-generic/siginfo.h"
1359struct __anonstruct__timer_156 {
1360   __kernel_timer_t _tid ;
1361   int _overrun ;
1362   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
1363   sigval_t _sigval ;
1364   int _sys_private ;
1365};
1366#line 48 "include/asm-generic/siginfo.h"
1367struct __anonstruct__rt_157 {
1368   __kernel_pid_t _pid ;
1369   __kernel_uid32_t _uid ;
1370   sigval_t _sigval ;
1371};
1372#line 48 "include/asm-generic/siginfo.h"
1373struct __anonstruct__sigchld_158 {
1374   __kernel_pid_t _pid ;
1375   __kernel_uid32_t _uid ;
1376   int _status ;
1377   __kernel_clock_t _utime ;
1378   __kernel_clock_t _stime ;
1379};
1380#line 48 "include/asm-generic/siginfo.h"
1381struct __anonstruct__sigfault_159 {
1382   void *_addr ;
1383   short _addr_lsb ;
1384};
1385#line 48 "include/asm-generic/siginfo.h"
1386struct __anonstruct__sigpoll_160 {
1387   long _band ;
1388   int _fd ;
1389};
1390#line 48 "include/asm-generic/siginfo.h"
1391union __anonunion__sifields_154 {
1392   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
1393   struct __anonstruct__kill_155 _kill ;
1394   struct __anonstruct__timer_156 _timer ;
1395   struct __anonstruct__rt_157 _rt ;
1396   struct __anonstruct__sigchld_158 _sigchld ;
1397   struct __anonstruct__sigfault_159 _sigfault ;
1398   struct __anonstruct__sigpoll_160 _sigpoll ;
1399};
1400#line 48 "include/asm-generic/siginfo.h"
1401struct siginfo {
1402   int si_signo ;
1403   int si_errno ;
1404   int si_code ;
1405   union __anonunion__sifields_154 _sifields ;
1406};
1407#line 48 "include/asm-generic/siginfo.h"
1408typedef struct siginfo siginfo_t;
1409#line 288
1410struct siginfo;
1411#line 10 "include/linux/signal.h"
1412struct task_struct;
1413#line 18
1414struct user_struct;
1415#line 28 "include/linux/signal.h"
1416struct sigpending {
1417   struct list_head list ;
1418   sigset_t signal ;
1419};
1420#line 239
1421struct timespec;
1422#line 240
1423struct pt_regs;
1424#line 50 "include/linux/pid.h"
1425struct pid_namespace;
1426#line 50 "include/linux/pid.h"
1427struct upid {
1428   int nr ;
1429   struct pid_namespace *ns ;
1430   struct hlist_node pid_chain ;
1431};
1432#line 57 "include/linux/pid.h"
1433struct pid {
1434   atomic_t count ;
1435   unsigned int level ;
1436   struct hlist_head tasks[3] ;
1437   struct rcu_head rcu ;
1438   struct upid numbers[1] ;
1439};
1440#line 69 "include/linux/pid.h"
1441struct pid_link {
1442   struct hlist_node node ;
1443   struct pid *pid ;
1444};
1445#line 100
1446struct pid_namespace;
1447#line 10 "include/linux/seccomp.h"
1448struct __anonstruct_seccomp_t_163 {
1449   int mode ;
1450};
1451#line 10 "include/linux/seccomp.h"
1452typedef struct __anonstruct_seccomp_t_163 seccomp_t;
1453#line 81 "include/linux/plist.h"
1454struct plist_head {
1455   struct list_head node_list ;
1456};
1457#line 85 "include/linux/plist.h"
1458struct plist_node {
1459   int prio ;
1460   struct list_head prio_list ;
1461   struct list_head node_list ;
1462};
1463#line 40 "include/linux/rtmutex.h"
1464struct rt_mutex_waiter;
1465#line 40
1466struct rt_mutex_waiter;
1467#line 42 "include/linux/resource.h"
1468struct rlimit {
1469   unsigned long rlim_cur ;
1470   unsigned long rlim_max ;
1471};
1472#line 81
1473struct task_struct;
1474#line 8 "include/linux/timerqueue.h"
1475struct timerqueue_node {
1476   struct rb_node node ;
1477   ktime_t expires ;
1478};
1479#line 13 "include/linux/timerqueue.h"
1480struct timerqueue_head {
1481   struct rb_root head ;
1482   struct timerqueue_node *next ;
1483};
1484#line 27 "include/linux/hrtimer.h"
1485struct hrtimer_clock_base;
1486#line 27
1487struct hrtimer_clock_base;
1488#line 28
1489struct hrtimer_cpu_base;
1490#line 28
1491struct hrtimer_cpu_base;
1492#line 44
1493enum hrtimer_restart {
1494    HRTIMER_NORESTART = 0,
1495    HRTIMER_RESTART = 1
1496} ;
1497#line 108 "include/linux/hrtimer.h"
1498struct hrtimer {
1499   struct timerqueue_node node ;
1500   ktime_t _softexpires ;
1501   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1502   struct hrtimer_clock_base *base ;
1503   unsigned long state ;
1504   int start_pid ;
1505   void *start_site ;
1506   char start_comm[16] ;
1507};
1508#line 145 "include/linux/hrtimer.h"
1509struct hrtimer_clock_base {
1510   struct hrtimer_cpu_base *cpu_base ;
1511   int index ;
1512   clockid_t clockid ;
1513   struct timerqueue_head active ;
1514   ktime_t resolution ;
1515   ktime_t (*get_time)(void) ;
1516   ktime_t softirq_time ;
1517   ktime_t offset ;
1518};
1519#line 178 "include/linux/hrtimer.h"
1520struct hrtimer_cpu_base {
1521   raw_spinlock_t lock ;
1522   unsigned long active_bases ;
1523   ktime_t expires_next ;
1524   int hres_active ;
1525   int hang_detected ;
1526   unsigned long nr_events ;
1527   unsigned long nr_retries ;
1528   unsigned long nr_hangs ;
1529   ktime_t max_hang_time ;
1530   struct hrtimer_clock_base clock_base[3] ;
1531};
1532#line 11 "include/linux/task_io_accounting.h"
1533struct task_io_accounting {
1534   u64 rchar ;
1535   u64 wchar ;
1536   u64 syscr ;
1537   u64 syscw ;
1538   u64 read_bytes ;
1539   u64 write_bytes ;
1540   u64 cancelled_write_bytes ;
1541};
1542#line 13 "include/linux/latencytop.h"
1543struct task_struct;
1544#line 20 "include/linux/latencytop.h"
1545struct latency_record {
1546   unsigned long backtrace[12] ;
1547   unsigned int count ;
1548   unsigned long time ;
1549   unsigned long max ;
1550};
1551#line 29 "include/linux/sysctl.h"
1552struct completion;
1553#line 939
1554struct nsproxy;
1555#line 939
1556struct nsproxy;
1557#line 29 "include/linux/key.h"
1558typedef int32_t key_serial_t;
1559#line 32 "include/linux/key.h"
1560typedef uint32_t key_perm_t;
1561#line 34
1562struct key;
1563#line 34
1564struct key;
1565#line 74
1566struct seq_file;
1567#line 75
1568struct user_struct;
1569#line 76
1570struct signal_struct;
1571#line 76
1572struct signal_struct;
1573#line 77
1574struct cred;
1575#line 77
1576struct cred;
1577#line 79
1578struct key_type;
1579#line 79
1580struct key_type;
1581#line 81
1582struct keyring_list;
1583#line 81
1584struct keyring_list;
1585#line 124
1586struct key_user;
1587#line 124 "include/linux/key.h"
1588union __anonunion____missing_field_name_220 {
1589   time_t expiry ;
1590   time_t revoked_at ;
1591};
1592#line 124 "include/linux/key.h"
1593union __anonunion_type_data_221 {
1594   struct list_head link ;
1595   unsigned long x[2] ;
1596   void *p[2] ;
1597   int reject_error ;
1598};
1599#line 124 "include/linux/key.h"
1600union __anonunion_payload_222 {
1601   unsigned long value ;
1602   void *rcudata ;
1603   void *data ;
1604   struct keyring_list *subscriptions ;
1605};
1606#line 124 "include/linux/key.h"
1607struct key {
1608   atomic_t usage ;
1609   key_serial_t serial ;
1610   struct rb_node serial_node ;
1611   struct key_type *type ;
1612   struct rw_semaphore sem ;
1613   struct key_user *user ;
1614   void *security ;
1615   union __anonunion____missing_field_name_220 __annonCompField41 ;
1616   uid_t uid ;
1617   gid_t gid ;
1618   key_perm_t perm ;
1619   unsigned short quotalen ;
1620   unsigned short datalen ;
1621   unsigned long flags ;
1622   char *description ;
1623   union __anonunion_type_data_221 type_data ;
1624   union __anonunion_payload_222 payload ;
1625};
1626#line 18 "include/linux/selinux.h"
1627struct audit_context;
1628#line 18
1629struct audit_context;
1630#line 21 "include/linux/cred.h"
1631struct user_struct;
1632#line 22
1633struct cred;
1634#line 31 "include/linux/cred.h"
1635struct group_info {
1636   atomic_t usage ;
1637   int ngroups ;
1638   int nblocks ;
1639   gid_t small_block[32] ;
1640   gid_t *blocks[0] ;
1641};
1642#line 83 "include/linux/cred.h"
1643struct thread_group_cred {
1644   atomic_t usage ;
1645   pid_t tgid ;
1646   spinlock_t lock ;
1647   struct key *session_keyring ;
1648   struct key *process_keyring ;
1649   struct rcu_head rcu ;
1650};
1651#line 116 "include/linux/cred.h"
1652struct cred {
1653   atomic_t usage ;
1654   atomic_t subscribers ;
1655   void *put_addr ;
1656   unsigned int magic ;
1657   uid_t uid ;
1658   gid_t gid ;
1659   uid_t suid ;
1660   gid_t sgid ;
1661   uid_t euid ;
1662   gid_t egid ;
1663   uid_t fsuid ;
1664   gid_t fsgid ;
1665   unsigned int securebits ;
1666   kernel_cap_t cap_inheritable ;
1667   kernel_cap_t cap_permitted ;
1668   kernel_cap_t cap_effective ;
1669   kernel_cap_t cap_bset ;
1670   unsigned char jit_keyring ;
1671   struct key *thread_keyring ;
1672   struct key *request_key_auth ;
1673   struct thread_group_cred *tgcred ;
1674   void *security ;
1675   struct user_struct *user ;
1676   struct user_namespace *user_ns ;
1677   struct group_info *group_info ;
1678   struct rcu_head rcu ;
1679};
1680#line 61 "include/linux/llist.h"
1681struct llist_node;
1682#line 65 "include/linux/llist.h"
1683struct llist_node {
1684   struct llist_node *next ;
1685};
1686#line 97 "include/linux/sched.h"
1687struct futex_pi_state;
1688#line 97
1689struct futex_pi_state;
1690#line 98
1691struct robust_list_head;
1692#line 98
1693struct robust_list_head;
1694#line 99
1695struct bio_list;
1696#line 99
1697struct bio_list;
1698#line 100
1699struct fs_struct;
1700#line 100
1701struct fs_struct;
1702#line 101
1703struct perf_event_context;
1704#line 101
1705struct perf_event_context;
1706#line 102
1707struct blk_plug;
1708#line 102
1709struct blk_plug;
1710#line 150
1711struct seq_file;
1712#line 151
1713struct cfs_rq;
1714#line 151
1715struct cfs_rq;
1716#line 259
1717struct task_struct;
1718#line 366
1719struct nsproxy;
1720#line 367
1721struct user_namespace;
1722#line 214 "include/linux/aio.h"
1723struct mm_struct;
1724#line 443 "include/linux/sched.h"
1725struct sighand_struct {
1726   atomic_t count ;
1727   struct k_sigaction action[64] ;
1728   spinlock_t siglock ;
1729   wait_queue_head_t signalfd_wqh ;
1730};
1731#line 450 "include/linux/sched.h"
1732struct pacct_struct {
1733   int ac_flag ;
1734   long ac_exitcode ;
1735   unsigned long ac_mem ;
1736   cputime_t ac_utime ;
1737   cputime_t ac_stime ;
1738   unsigned long ac_minflt ;
1739   unsigned long ac_majflt ;
1740};
1741#line 458 "include/linux/sched.h"
1742struct cpu_itimer {
1743   cputime_t expires ;
1744   cputime_t incr ;
1745   u32 error ;
1746   u32 incr_error ;
1747};
1748#line 476 "include/linux/sched.h"
1749struct task_cputime {
1750   cputime_t utime ;
1751   cputime_t stime ;
1752   unsigned long long sum_exec_runtime ;
1753};
1754#line 512 "include/linux/sched.h"
1755struct thread_group_cputimer {
1756   struct task_cputime cputime ;
1757   int running ;
1758   raw_spinlock_t lock ;
1759};
1760#line 519
1761struct autogroup;
1762#line 519
1763struct autogroup;
1764#line 528
1765struct tty_struct;
1766#line 528
1767struct taskstats;
1768#line 528
1769struct tty_audit_buf;
1770#line 528 "include/linux/sched.h"
1771struct signal_struct {
1772   atomic_t sigcnt ;
1773   atomic_t live ;
1774   int nr_threads ;
1775   wait_queue_head_t wait_chldexit ;
1776   struct task_struct *curr_target ;
1777   struct sigpending shared_pending ;
1778   int group_exit_code ;
1779   int notify_count ;
1780   struct task_struct *group_exit_task ;
1781   int group_stop_count ;
1782   unsigned int flags ;
1783   unsigned int is_child_subreaper : 1 ;
1784   unsigned int has_child_subreaper : 1 ;
1785   struct list_head posix_timers ;
1786   struct hrtimer real_timer ;
1787   struct pid *leader_pid ;
1788   ktime_t it_real_incr ;
1789   struct cpu_itimer it[2] ;
1790   struct thread_group_cputimer cputimer ;
1791   struct task_cputime cputime_expires ;
1792   struct list_head cpu_timers[3] ;
1793   struct pid *tty_old_pgrp ;
1794   int leader ;
1795   struct tty_struct *tty ;
1796   struct autogroup *autogroup ;
1797   cputime_t utime ;
1798   cputime_t stime ;
1799   cputime_t cutime ;
1800   cputime_t cstime ;
1801   cputime_t gtime ;
1802   cputime_t cgtime ;
1803   cputime_t prev_utime ;
1804   cputime_t prev_stime ;
1805   unsigned long nvcsw ;
1806   unsigned long nivcsw ;
1807   unsigned long cnvcsw ;
1808   unsigned long cnivcsw ;
1809   unsigned long min_flt ;
1810   unsigned long maj_flt ;
1811   unsigned long cmin_flt ;
1812   unsigned long cmaj_flt ;
1813   unsigned long inblock ;
1814   unsigned long oublock ;
1815   unsigned long cinblock ;
1816   unsigned long coublock ;
1817   unsigned long maxrss ;
1818   unsigned long cmaxrss ;
1819   struct task_io_accounting ioac ;
1820   unsigned long long sum_sched_runtime ;
1821   struct rlimit rlim[16] ;
1822   struct pacct_struct pacct ;
1823   struct taskstats *stats ;
1824   unsigned int audit_tty ;
1825   struct tty_audit_buf *tty_audit_buf ;
1826   struct rw_semaphore group_rwsem ;
1827   int oom_adj ;
1828   int oom_score_adj ;
1829   int oom_score_adj_min ;
1830   struct mutex cred_guard_mutex ;
1831};
1832#line 703 "include/linux/sched.h"
1833struct user_struct {
1834   atomic_t __count ;
1835   atomic_t processes ;
1836   atomic_t files ;
1837   atomic_t sigpending ;
1838   atomic_t inotify_watches ;
1839   atomic_t inotify_devs ;
1840   atomic_t fanotify_listeners ;
1841   atomic_long_t epoll_watches ;
1842   unsigned long mq_bytes ;
1843   unsigned long locked_shm ;
1844   struct key *uid_keyring ;
1845   struct key *session_keyring ;
1846   struct hlist_node uidhash_node ;
1847   uid_t uid ;
1848   struct user_namespace *user_ns ;
1849   atomic_long_t locked_vm ;
1850};
1851#line 747
1852struct backing_dev_info;
1853#line 747
1854struct backing_dev_info;
1855#line 748
1856struct reclaim_state;
1857#line 748
1858struct reclaim_state;
1859#line 751 "include/linux/sched.h"
1860struct sched_info {
1861   unsigned long pcount ;
1862   unsigned long long run_delay ;
1863   unsigned long long last_arrival ;
1864   unsigned long long last_queued ;
1865};
1866#line 763 "include/linux/sched.h"
1867struct task_delay_info {
1868   spinlock_t lock ;
1869   unsigned int flags ;
1870   struct timespec blkio_start ;
1871   struct timespec blkio_end ;
1872   u64 blkio_delay ;
1873   u64 swapin_delay ;
1874   u32 blkio_count ;
1875   u32 swapin_count ;
1876   struct timespec freepages_start ;
1877   struct timespec freepages_end ;
1878   u64 freepages_delay ;
1879   u32 freepages_count ;
1880};
1881#line 1088
1882struct io_context;
1883#line 1088
1884struct io_context;
1885#line 1097
1886struct audit_context;
1887#line 1098
1888struct mempolicy;
1889#line 1099
1890struct pipe_inode_info;
1891#line 1099
1892struct pipe_inode_info;
1893#line 1102
1894struct rq;
1895#line 1102
1896struct rq;
1897#line 1122 "include/linux/sched.h"
1898struct sched_class {
1899   struct sched_class  const  *next ;
1900   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
1901   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
1902   void (*yield_task)(struct rq *rq ) ;
1903   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
1904   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
1905   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
1906   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
1907   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
1908   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
1909   void (*post_schedule)(struct rq *this_rq ) ;
1910   void (*task_waking)(struct task_struct *task ) ;
1911   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
1912   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
1913   void (*rq_online)(struct rq *rq ) ;
1914   void (*rq_offline)(struct rq *rq ) ;
1915   void (*set_curr_task)(struct rq *rq ) ;
1916   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
1917   void (*task_fork)(struct task_struct *p ) ;
1918   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
1919   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
1920   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
1921   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
1922   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
1923};
1924#line 1167 "include/linux/sched.h"
1925struct load_weight {
1926   unsigned long weight ;
1927   unsigned long inv_weight ;
1928};
1929#line 1172 "include/linux/sched.h"
1930struct sched_statistics {
1931   u64 wait_start ;
1932   u64 wait_max ;
1933   u64 wait_count ;
1934   u64 wait_sum ;
1935   u64 iowait_count ;
1936   u64 iowait_sum ;
1937   u64 sleep_start ;
1938   u64 sleep_max ;
1939   s64 sum_sleep_runtime ;
1940   u64 block_start ;
1941   u64 block_max ;
1942   u64 exec_max ;
1943   u64 slice_max ;
1944   u64 nr_migrations_cold ;
1945   u64 nr_failed_migrations_affine ;
1946   u64 nr_failed_migrations_running ;
1947   u64 nr_failed_migrations_hot ;
1948   u64 nr_forced_migrations ;
1949   u64 nr_wakeups ;
1950   u64 nr_wakeups_sync ;
1951   u64 nr_wakeups_migrate ;
1952   u64 nr_wakeups_local ;
1953   u64 nr_wakeups_remote ;
1954   u64 nr_wakeups_affine ;
1955   u64 nr_wakeups_affine_attempts ;
1956   u64 nr_wakeups_passive ;
1957   u64 nr_wakeups_idle ;
1958};
1959#line 1207 "include/linux/sched.h"
1960struct sched_entity {
1961   struct load_weight load ;
1962   struct rb_node run_node ;
1963   struct list_head group_node ;
1964   unsigned int on_rq ;
1965   u64 exec_start ;
1966   u64 sum_exec_runtime ;
1967   u64 vruntime ;
1968   u64 prev_sum_exec_runtime ;
1969   u64 nr_migrations ;
1970   struct sched_statistics statistics ;
1971   struct sched_entity *parent ;
1972   struct cfs_rq *cfs_rq ;
1973   struct cfs_rq *my_q ;
1974};
1975#line 1233
1976struct rt_rq;
1977#line 1233 "include/linux/sched.h"
1978struct sched_rt_entity {
1979   struct list_head run_list ;
1980   unsigned long timeout ;
1981   unsigned int time_slice ;
1982   int nr_cpus_allowed ;
1983   struct sched_rt_entity *back ;
1984   struct sched_rt_entity *parent ;
1985   struct rt_rq *rt_rq ;
1986   struct rt_rq *my_q ;
1987};
1988#line 1264
1989struct files_struct;
1990#line 1264
1991struct css_set;
1992#line 1264
1993struct compat_robust_list_head;
1994#line 1264
1995struct mem_cgroup;
1996#line 1264 "include/linux/sched.h"
1997struct memcg_batch_info {
1998   int do_batch ;
1999   struct mem_cgroup *memcg ;
2000   unsigned long nr_pages ;
2001   unsigned long memsw_nr_pages ;
2002};
2003#line 1264 "include/linux/sched.h"
2004struct task_struct {
2005   long volatile   state ;
2006   void *stack ;
2007   atomic_t usage ;
2008   unsigned int flags ;
2009   unsigned int ptrace ;
2010   struct llist_node wake_entry ;
2011   int on_cpu ;
2012   int on_rq ;
2013   int prio ;
2014   int static_prio ;
2015   int normal_prio ;
2016   unsigned int rt_priority ;
2017   struct sched_class  const  *sched_class ;
2018   struct sched_entity se ;
2019   struct sched_rt_entity rt ;
2020   struct hlist_head preempt_notifiers ;
2021   unsigned char fpu_counter ;
2022   unsigned int policy ;
2023   cpumask_t cpus_allowed ;
2024   struct sched_info sched_info ;
2025   struct list_head tasks ;
2026   struct plist_node pushable_tasks ;
2027   struct mm_struct *mm ;
2028   struct mm_struct *active_mm ;
2029   unsigned int brk_randomized : 1 ;
2030   int exit_state ;
2031   int exit_code ;
2032   int exit_signal ;
2033   int pdeath_signal ;
2034   unsigned int jobctl ;
2035   unsigned int personality ;
2036   unsigned int did_exec : 1 ;
2037   unsigned int in_execve : 1 ;
2038   unsigned int in_iowait : 1 ;
2039   unsigned int sched_reset_on_fork : 1 ;
2040   unsigned int sched_contributes_to_load : 1 ;
2041   unsigned int irq_thread : 1 ;
2042   pid_t pid ;
2043   pid_t tgid ;
2044   unsigned long stack_canary ;
2045   struct task_struct *real_parent ;
2046   struct task_struct *parent ;
2047   struct list_head children ;
2048   struct list_head sibling ;
2049   struct task_struct *group_leader ;
2050   struct list_head ptraced ;
2051   struct list_head ptrace_entry ;
2052   struct pid_link pids[3] ;
2053   struct list_head thread_group ;
2054   struct completion *vfork_done ;
2055   int *set_child_tid ;
2056   int *clear_child_tid ;
2057   cputime_t utime ;
2058   cputime_t stime ;
2059   cputime_t utimescaled ;
2060   cputime_t stimescaled ;
2061   cputime_t gtime ;
2062   cputime_t prev_utime ;
2063   cputime_t prev_stime ;
2064   unsigned long nvcsw ;
2065   unsigned long nivcsw ;
2066   struct timespec start_time ;
2067   struct timespec real_start_time ;
2068   unsigned long min_flt ;
2069   unsigned long maj_flt ;
2070   struct task_cputime cputime_expires ;
2071   struct list_head cpu_timers[3] ;
2072   struct cred  const  *real_cred ;
2073   struct cred  const  *cred ;
2074   struct cred *replacement_session_keyring ;
2075   char comm[16] ;
2076   int link_count ;
2077   int total_link_count ;
2078   struct sysv_sem sysvsem ;
2079   unsigned long last_switch_count ;
2080   struct thread_struct thread ;
2081   struct fs_struct *fs ;
2082   struct files_struct *files ;
2083   struct nsproxy *nsproxy ;
2084   struct signal_struct *signal ;
2085   struct sighand_struct *sighand ;
2086   sigset_t blocked ;
2087   sigset_t real_blocked ;
2088   sigset_t saved_sigmask ;
2089   struct sigpending pending ;
2090   unsigned long sas_ss_sp ;
2091   size_t sas_ss_size ;
2092   int (*notifier)(void *priv ) ;
2093   void *notifier_data ;
2094   sigset_t *notifier_mask ;
2095   struct audit_context *audit_context ;
2096   uid_t loginuid ;
2097   unsigned int sessionid ;
2098   seccomp_t seccomp ;
2099   u32 parent_exec_id ;
2100   u32 self_exec_id ;
2101   spinlock_t alloc_lock ;
2102   raw_spinlock_t pi_lock ;
2103   struct plist_head pi_waiters ;
2104   struct rt_mutex_waiter *pi_blocked_on ;
2105   struct mutex_waiter *blocked_on ;
2106   unsigned int irq_events ;
2107   unsigned long hardirq_enable_ip ;
2108   unsigned long hardirq_disable_ip ;
2109   unsigned int hardirq_enable_event ;
2110   unsigned int hardirq_disable_event ;
2111   int hardirqs_enabled ;
2112   int hardirq_context ;
2113   unsigned long softirq_disable_ip ;
2114   unsigned long softirq_enable_ip ;
2115   unsigned int softirq_disable_event ;
2116   unsigned int softirq_enable_event ;
2117   int softirqs_enabled ;
2118   int softirq_context ;
2119   void *journal_info ;
2120   struct bio_list *bio_list ;
2121   struct blk_plug *plug ;
2122   struct reclaim_state *reclaim_state ;
2123   struct backing_dev_info *backing_dev_info ;
2124   struct io_context *io_context ;
2125   unsigned long ptrace_message ;
2126   siginfo_t *last_siginfo ;
2127   struct task_io_accounting ioac ;
2128   u64 acct_rss_mem1 ;
2129   u64 acct_vm_mem1 ;
2130   cputime_t acct_timexpd ;
2131   nodemask_t mems_allowed ;
2132   seqcount_t mems_allowed_seq ;
2133   int cpuset_mem_spread_rotor ;
2134   int cpuset_slab_spread_rotor ;
2135   struct css_set *cgroups ;
2136   struct list_head cg_list ;
2137   struct robust_list_head *robust_list ;
2138   struct compat_robust_list_head *compat_robust_list ;
2139   struct list_head pi_state_list ;
2140   struct futex_pi_state *pi_state_cache ;
2141   struct perf_event_context *perf_event_ctxp[2] ;
2142   struct mutex perf_event_mutex ;
2143   struct list_head perf_event_list ;
2144   struct mempolicy *mempolicy ;
2145   short il_next ;
2146   short pref_node_fork ;
2147   struct rcu_head rcu ;
2148   struct pipe_inode_info *splice_pipe ;
2149   struct task_delay_info *delays ;
2150   int make_it_fail ;
2151   int nr_dirtied ;
2152   int nr_dirtied_pause ;
2153   unsigned long dirty_paused_when ;
2154   int latency_record_count ;
2155   struct latency_record latency_record[32] ;
2156   unsigned long timer_slack_ns ;
2157   unsigned long default_timer_slack_ns ;
2158   struct list_head *scm_work_list ;
2159   unsigned long trace ;
2160   unsigned long trace_recursion ;
2161   struct memcg_batch_info memcg_batch ;
2162   atomic_t ptrace_bp_refcnt ;
2163};
2164#line 1681
2165struct pid_namespace;
2166#line 55 "include/linux/kthread.h"
2167struct kthread_work;
2168#line 55
2169struct kthread_work;
2170#line 58 "include/linux/kthread.h"
2171struct kthread_worker {
2172   spinlock_t lock ;
2173   struct list_head work_list ;
2174   struct task_struct *task ;
2175};
2176#line 64 "include/linux/kthread.h"
2177struct kthread_work {
2178   struct list_head node ;
2179   void (*func)(struct kthread_work *work ) ;
2180   wait_queue_head_t done ;
2181   atomic_t flushing ;
2182   int queue_seq ;
2183   int done_seq ;
2184};
2185#line 70 "include/linux/spi/spi.h"
2186struct spi_master;
2187#line 70 "include/linux/spi/spi.h"
2188struct spi_device {
2189   struct device dev ;
2190   struct spi_master *master ;
2191   u32 max_speed_hz ;
2192   u8 chip_select ;
2193   u8 mode ;
2194   u8 bits_per_word ;
2195   int irq ;
2196   void *controller_state ;
2197   void *controller_data ;
2198   char modalias[32] ;
2199};
2200#line 145
2201struct spi_message;
2202#line 145
2203struct spi_message;
2204#line 176 "include/linux/spi/spi.h"
2205struct spi_driver {
2206   struct spi_device_id  const  *id_table ;
2207   int (*probe)(struct spi_device *spi ) ;
2208   int (*remove)(struct spi_device *spi ) ;
2209   void (*shutdown)(struct spi_device *spi ) ;
2210   int (*suspend)(struct spi_device *spi , pm_message_t mesg ) ;
2211   int (*resume)(struct spi_device *spi ) ;
2212   struct device_driver driver ;
2213};
2214#line 272 "include/linux/spi/spi.h"
2215struct spi_master {
2216   struct device dev ;
2217   struct list_head list ;
2218   s16 bus_num ;
2219   u16 num_chipselect ;
2220   u16 dma_alignment ;
2221   u16 mode_bits ;
2222   u16 flags ;
2223   spinlock_t bus_lock_spinlock ;
2224   struct mutex bus_lock_mutex ;
2225   bool bus_lock_flag ;
2226   int (*setup)(struct spi_device *spi ) ;
2227   int (*transfer)(struct spi_device *spi , struct spi_message *mesg ) ;
2228   void (*cleanup)(struct spi_device *spi ) ;
2229   bool queued ;
2230   struct kthread_worker kworker ;
2231   struct task_struct *kworker_task ;
2232   struct kthread_work pump_messages ;
2233   spinlock_t queue_lock ;
2234   struct list_head queue ;
2235   struct spi_message *cur_msg ;
2236   bool busy ;
2237   bool running ;
2238   bool rt ;
2239   int (*prepare_transfer_hardware)(struct spi_master *master ) ;
2240   int (*transfer_one_message)(struct spi_master *master , struct spi_message *mesg ) ;
2241   int (*unprepare_transfer_hardware)(struct spi_master *master ) ;
2242};
2243#line 492 "include/linux/spi/spi.h"
2244struct spi_transfer {
2245   void const   *tx_buf ;
2246   void *rx_buf ;
2247   unsigned int len ;
2248   dma_addr_t tx_dma ;
2249   dma_addr_t rx_dma ;
2250   unsigned int cs_change : 1 ;
2251   u8 bits_per_word ;
2252   u16 delay_usecs ;
2253   u32 speed_hz ;
2254   struct list_head transfer_list ;
2255};
2256#line 541 "include/linux/spi/spi.h"
2257struct spi_message {
2258   struct list_head transfers ;
2259   struct spi_device *spi ;
2260   unsigned int is_dma_mapped : 1 ;
2261   void (*complete)(void *context ) ;
2262   void *context ;
2263   unsigned int actual_length ;
2264   int status ;
2265   struct list_head queue ;
2266   void *state ;
2267};
2268#line 4 "include/linux/spi/mc33880.h"
2269struct mc33880_platform_data {
2270   unsigned int base ;
2271};
2272#line 28 "include/linux/of.h"
2273typedef u32 phandle;
2274#line 31 "include/linux/of.h"
2275struct property {
2276   char *name ;
2277   int length ;
2278   void *value ;
2279   struct property *next ;
2280   unsigned long _flags ;
2281   unsigned int unique_id ;
2282};
2283#line 44
2284struct proc_dir_entry;
2285#line 44 "include/linux/of.h"
2286struct device_node {
2287   char const   *name ;
2288   char const   *type ;
2289   phandle phandle ;
2290   char *full_name ;
2291   struct property *properties ;
2292   struct property *deadprops ;
2293   struct device_node *parent ;
2294   struct device_node *child ;
2295   struct device_node *sibling ;
2296   struct device_node *next ;
2297   struct device_node *allnext ;
2298   struct proc_dir_entry *pde ;
2299   struct kref kref ;
2300   unsigned long _flags ;
2301   void *data ;
2302};
2303#line 44 "include/asm-generic/gpio.h"
2304struct device;
2305#line 46
2306struct seq_file;
2307#line 47
2308struct module;
2309#line 48
2310struct device_node;
2311#line 92 "include/asm-generic/gpio.h"
2312struct gpio_chip {
2313   char const   *label ;
2314   struct device *dev ;
2315   struct module *owner ;
2316   int (*request)(struct gpio_chip *chip , unsigned int offset ) ;
2317   void (*free)(struct gpio_chip *chip , unsigned int offset ) ;
2318   int (*direction_input)(struct gpio_chip *chip , unsigned int offset ) ;
2319   int (*get)(struct gpio_chip *chip , unsigned int offset ) ;
2320   int (*direction_output)(struct gpio_chip *chip , unsigned int offset , int value ) ;
2321   int (*set_debounce)(struct gpio_chip *chip , unsigned int offset , unsigned int debounce ) ;
2322   void (*set)(struct gpio_chip *chip , unsigned int offset , int value ) ;
2323   int (*to_irq)(struct gpio_chip *chip , unsigned int offset ) ;
2324   void (*dbg_show)(struct seq_file *s , struct gpio_chip *chip ) ;
2325   int base ;
2326   u16 ngpio ;
2327   char const   * const  *names ;
2328   unsigned int can_sleep : 1 ;
2329   unsigned int exported : 1 ;
2330};
2331#line 48 "include/linux/kmod.h"
2332struct cred;
2333#line 49
2334struct file;
2335#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
2336struct task_struct;
2337#line 18 "include/linux/elf.h"
2338typedef __u64 Elf64_Addr;
2339#line 19 "include/linux/elf.h"
2340typedef __u16 Elf64_Half;
2341#line 23 "include/linux/elf.h"
2342typedef __u32 Elf64_Word;
2343#line 24 "include/linux/elf.h"
2344typedef __u64 Elf64_Xword;
2345#line 194 "include/linux/elf.h"
2346struct elf64_sym {
2347   Elf64_Word st_name ;
2348   unsigned char st_info ;
2349   unsigned char st_other ;
2350   Elf64_Half st_shndx ;
2351   Elf64_Addr st_value ;
2352   Elf64_Xword st_size ;
2353};
2354#line 194 "include/linux/elf.h"
2355typedef struct elf64_sym Elf64_Sym;
2356#line 438
2357struct file;
2358#line 39 "include/linux/moduleparam.h"
2359struct kernel_param;
2360#line 39
2361struct kernel_param;
2362#line 41 "include/linux/moduleparam.h"
2363struct kernel_param_ops {
2364   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
2365   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
2366   void (*free)(void *arg ) ;
2367};
2368#line 50
2369struct kparam_string;
2370#line 50
2371struct kparam_array;
2372#line 50 "include/linux/moduleparam.h"
2373union __anonunion____missing_field_name_230 {
2374   void *arg ;
2375   struct kparam_string  const  *str ;
2376   struct kparam_array  const  *arr ;
2377};
2378#line 50 "include/linux/moduleparam.h"
2379struct kernel_param {
2380   char const   *name ;
2381   struct kernel_param_ops  const  *ops ;
2382   u16 perm ;
2383   s16 level ;
2384   union __anonunion____missing_field_name_230 __annonCompField43 ;
2385};
2386#line 63 "include/linux/moduleparam.h"
2387struct kparam_string {
2388   unsigned int maxlen ;
2389   char *string ;
2390};
2391#line 69 "include/linux/moduleparam.h"
2392struct kparam_array {
2393   unsigned int max ;
2394   unsigned int elemsize ;
2395   unsigned int *num ;
2396   struct kernel_param_ops  const  *ops ;
2397   void *elem ;
2398};
2399#line 445
2400struct module;
2401#line 80 "include/linux/jump_label.h"
2402struct module;
2403#line 143 "include/linux/jump_label.h"
2404struct static_key {
2405   atomic_t enabled ;
2406};
2407#line 22 "include/linux/tracepoint.h"
2408struct module;
2409#line 23
2410struct tracepoint;
2411#line 23
2412struct tracepoint;
2413#line 25 "include/linux/tracepoint.h"
2414struct tracepoint_func {
2415   void *func ;
2416   void *data ;
2417};
2418#line 30 "include/linux/tracepoint.h"
2419struct tracepoint {
2420   char const   *name ;
2421   struct static_key key ;
2422   void (*regfunc)(void) ;
2423   void (*unregfunc)(void) ;
2424   struct tracepoint_func *funcs ;
2425};
2426#line 19 "include/linux/export.h"
2427struct kernel_symbol {
2428   unsigned long value ;
2429   char const   *name ;
2430};
2431#line 8 "include/asm-generic/module.h"
2432struct mod_arch_specific {
2433
2434};
2435#line 35 "include/linux/module.h"
2436struct module;
2437#line 37
2438struct module_param_attrs;
2439#line 37 "include/linux/module.h"
2440struct module_kobject {
2441   struct kobject kobj ;
2442   struct module *mod ;
2443   struct kobject *drivers_dir ;
2444   struct module_param_attrs *mp ;
2445};
2446#line 44 "include/linux/module.h"
2447struct module_attribute {
2448   struct attribute attr ;
2449   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
2450   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
2451                    size_t count ) ;
2452   void (*setup)(struct module * , char const   * ) ;
2453   int (*test)(struct module * ) ;
2454   void (*free)(struct module * ) ;
2455};
2456#line 71
2457struct exception_table_entry;
2458#line 71
2459struct exception_table_entry;
2460#line 199
2461enum module_state {
2462    MODULE_STATE_LIVE = 0,
2463    MODULE_STATE_COMING = 1,
2464    MODULE_STATE_GOING = 2
2465} ;
2466#line 215 "include/linux/module.h"
2467struct module_ref {
2468   unsigned long incs ;
2469   unsigned long decs ;
2470} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
2471#line 220
2472struct module_sect_attrs;
2473#line 220
2474struct module_notes_attrs;
2475#line 220
2476struct ftrace_event_call;
2477#line 220 "include/linux/module.h"
2478struct module {
2479   enum module_state state ;
2480   struct list_head list ;
2481   char name[64UL - sizeof(unsigned long )] ;
2482   struct module_kobject mkobj ;
2483   struct module_attribute *modinfo_attrs ;
2484   char const   *version ;
2485   char const   *srcversion ;
2486   struct kobject *holders_dir ;
2487   struct kernel_symbol  const  *syms ;
2488   unsigned long const   *crcs ;
2489   unsigned int num_syms ;
2490   struct kernel_param *kp ;
2491   unsigned int num_kp ;
2492   unsigned int num_gpl_syms ;
2493   struct kernel_symbol  const  *gpl_syms ;
2494   unsigned long const   *gpl_crcs ;
2495   struct kernel_symbol  const  *unused_syms ;
2496   unsigned long const   *unused_crcs ;
2497   unsigned int num_unused_syms ;
2498   unsigned int num_unused_gpl_syms ;
2499   struct kernel_symbol  const  *unused_gpl_syms ;
2500   unsigned long const   *unused_gpl_crcs ;
2501   struct kernel_symbol  const  *gpl_future_syms ;
2502   unsigned long const   *gpl_future_crcs ;
2503   unsigned int num_gpl_future_syms ;
2504   unsigned int num_exentries ;
2505   struct exception_table_entry *extable ;
2506   int (*init)(void) ;
2507   void *module_init ;
2508   void *module_core ;
2509   unsigned int init_size ;
2510   unsigned int core_size ;
2511   unsigned int init_text_size ;
2512   unsigned int core_text_size ;
2513   unsigned int init_ro_size ;
2514   unsigned int core_ro_size ;
2515   struct mod_arch_specific arch ;
2516   unsigned int taints ;
2517   unsigned int num_bugs ;
2518   struct list_head bug_list ;
2519   struct bug_entry *bug_table ;
2520   Elf64_Sym *symtab ;
2521   Elf64_Sym *core_symtab ;
2522   unsigned int num_symtab ;
2523   unsigned int core_num_syms ;
2524   char *strtab ;
2525   char *core_strtab ;
2526   struct module_sect_attrs *sect_attrs ;
2527   struct module_notes_attrs *notes_attrs ;
2528   char *args ;
2529   void *percpu ;
2530   unsigned int percpu_size ;
2531   unsigned int num_tracepoints ;
2532   struct tracepoint * const  *tracepoints_ptrs ;
2533   unsigned int num_trace_bprintk_fmt ;
2534   char const   **trace_bprintk_fmt_start ;
2535   struct ftrace_event_call **trace_events ;
2536   unsigned int num_trace_events ;
2537   struct list_head source_list ;
2538   struct list_head target_list ;
2539   struct task_struct *waiter ;
2540   void (*exit)(void) ;
2541   struct module_ref *refptr ;
2542   ctor_fn_t *ctors ;
2543   unsigned int num_ctors ;
2544};
2545#line 49 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
2546struct mc33880 {
2547   struct mutex lock ;
2548   u8 port_config ;
2549   struct gpio_chip chip ;
2550   struct spi_device *spi ;
2551};
2552#line 1 "<compiler builtins>"
2553long __builtin_expect(long val , long res ) ;
2554#line 24 "include/linux/list.h"
2555__inline static void INIT_LIST_HEAD(struct list_head *list )  __attribute__((__no_instrument_function__)) ;
2556#line 24 "include/linux/list.h"
2557__inline static void INIT_LIST_HEAD(struct list_head *list ) 
2558{ unsigned long __cil_tmp2 ;
2559  unsigned long __cil_tmp3 ;
2560
2561  {
2562#line 26
2563  *((struct list_head **)list) = list;
2564#line 27
2565  __cil_tmp2 = (unsigned long )list;
2566#line 27
2567  __cil_tmp3 = __cil_tmp2 + 8;
2568#line 27
2569  *((struct list_head **)__cil_tmp3) = list;
2570#line 28
2571  return;
2572}
2573}
2574#line 47
2575extern void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next ) ;
2576#line 74
2577__inline static void list_add_tail(struct list_head *new , struct list_head *head )  __attribute__((__no_instrument_function__)) ;
2578#line 74 "include/linux/list.h"
2579__inline static void list_add_tail(struct list_head *new , struct list_head *head ) 
2580{ unsigned long __cil_tmp3 ;
2581  unsigned long __cil_tmp4 ;
2582  struct list_head *__cil_tmp5 ;
2583
2584  {
2585  {
2586#line 76
2587  __cil_tmp3 = (unsigned long )head;
2588#line 76
2589  __cil_tmp4 = __cil_tmp3 + 8;
2590#line 76
2591  __cil_tmp5 = *((struct list_head **)__cil_tmp4);
2592#line 76
2593  __list_add(new, __cil_tmp5, head);
2594  }
2595#line 77
2596  return;
2597}
2598}
2599#line 100 "include/linux/printk.h"
2600extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
2601#line 49 "include/linux/dynamic_debug.h"
2602extern int ( /* format attribute */  __dynamic_dev_dbg)(struct _ddebug *descriptor ,
2603                                                        struct device  const  *dev ,
2604                                                        char const   *fmt  , ...) ;
2605#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
2606extern void *memset(void *s , int c , size_t n ) ;
2607#line 21 "include/linux/mutex-debug.h"
2608extern void mutex_destroy(struct mutex *lock ) ;
2609#line 115 "include/linux/mutex.h"
2610extern void __mutex_init(struct mutex *lock , char const   *name , struct lock_class_key *key ) ;
2611#line 152
2612void mutex_lock(struct mutex *lock ) ;
2613#line 153
2614int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2615#line 154
2616int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2617#line 168
2618int mutex_trylock(struct mutex *lock ) ;
2619#line 169
2620void mutex_unlock(struct mutex *lock ) ;
2621#line 170
2622int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2623#line 239 "include/linux/device.h"
2624extern void driver_unregister(struct device_driver *drv ) ;
2625#line 792
2626extern void *dev_get_drvdata(struct device  const  *dev ) ;
2627#line 793
2628extern int dev_set_drvdata(struct device *dev , void *data ) ;
2629#line 891
2630extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
2631                                              , ...) ;
2632#line 161 "include/linux/slab.h"
2633extern void kfree(void const   * ) ;
2634#line 221 "include/linux/slub_def.h"
2635extern void *__kmalloc(size_t size , gfp_t flags ) ;
2636#line 268
2637__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2638                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2639#line 268 "include/linux/slub_def.h"
2640__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2641                                                                    gfp_t flags ) 
2642{ void *tmp___2 ;
2643
2644  {
2645  {
2646#line 283
2647  tmp___2 = __kmalloc(size, flags);
2648  }
2649#line 283
2650  return (tmp___2);
2651}
2652}
2653#line 349 "include/linux/slab.h"
2654__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2655#line 349 "include/linux/slab.h"
2656__inline static void *kzalloc(size_t size , gfp_t flags ) 
2657{ void *tmp ;
2658  unsigned int __cil_tmp4 ;
2659
2660  {
2661  {
2662#line 351
2663  __cil_tmp4 = flags | 32768U;
2664#line 351
2665  tmp = kmalloc(size, __cil_tmp4);
2666  }
2667#line 351
2668  return (tmp);
2669}
2670}
2671#line 191 "include/linux/spi/spi.h"
2672extern int spi_register_driver(struct spi_driver *sdrv ) ;
2673#line 198
2674__inline static void spi_unregister_driver(struct spi_driver *sdrv )  __attribute__((__no_instrument_function__)) ;
2675#line 198 "include/linux/spi/spi.h"
2676__inline static void spi_unregister_driver(struct spi_driver *sdrv ) 
2677{ unsigned long __cil_tmp2 ;
2678  unsigned long __cil_tmp3 ;
2679  struct device_driver *__cil_tmp4 ;
2680
2681  {
2682#line 200
2683  if (sdrv) {
2684    {
2685#line 201
2686    __cil_tmp2 = (unsigned long )sdrv;
2687#line 201
2688    __cil_tmp3 = __cil_tmp2 + 48;
2689#line 201
2690    __cil_tmp4 = (struct device_driver *)__cil_tmp3;
2691#line 201
2692    driver_unregister(__cil_tmp4);
2693    }
2694  } else {
2695
2696  }
2697#line 202
2698  return;
2699}
2700}
2701#line 573
2702__inline static void spi_message_init(struct spi_message *m )  __attribute__((__no_instrument_function__)) ;
2703#line 573 "include/linux/spi/spi.h"
2704__inline static void spi_message_init(struct spi_message *m ) 
2705{ void *__cil_tmp2 ;
2706  struct list_head *__cil_tmp3 ;
2707
2708  {
2709  {
2710#line 575
2711  __cil_tmp2 = (void *)m;
2712#line 575
2713  memset(__cil_tmp2, 0, 80UL);
2714#line 576
2715  __cil_tmp3 = (struct list_head *)m;
2716#line 576
2717  INIT_LIST_HEAD(__cil_tmp3);
2718  }
2719#line 577
2720  return;
2721}
2722}
2723#line 579
2724__inline static void spi_message_add_tail(struct spi_transfer *t , struct spi_message *m )  __attribute__((__no_instrument_function__)) ;
2725#line 579 "include/linux/spi/spi.h"
2726__inline static void spi_message_add_tail(struct spi_transfer *t , struct spi_message *m ) 
2727{ unsigned long __cil_tmp3 ;
2728  unsigned long __cil_tmp4 ;
2729  struct list_head *__cil_tmp5 ;
2730  struct list_head *__cil_tmp6 ;
2731
2732  {
2733  {
2734#line 582
2735  __cil_tmp3 = (unsigned long )t;
2736#line 582
2737  __cil_tmp4 = __cil_tmp3 + 48;
2738#line 582
2739  __cil_tmp5 = (struct list_head *)__cil_tmp4;
2740#line 582
2741  __cil_tmp6 = (struct list_head *)m;
2742#line 582
2743  list_add_tail(__cil_tmp5, __cil_tmp6);
2744  }
2745#line 583
2746  return;
2747}
2748}
2749#line 618
2750extern int spi_setup(struct spi_device *spi ) ;
2751#line 630
2752extern int spi_sync(struct spi_device *spi , struct spi_message *message ) ;
2753#line 645
2754__inline static int spi_write(struct spi_device *spi , void const   *buf , size_t len )  __attribute__((__no_instrument_function__)) ;
2755#line 645 "include/linux/spi/spi.h"
2756__inline static int spi_write(struct spi_device *spi , void const   *buf , size_t len ) 
2757{ struct spi_transfer t ;
2758  struct spi_message m ;
2759  int tmp___7 ;
2760  struct spi_transfer *__cil_tmp7 ;
2761  unsigned long __cil_tmp8 ;
2762  unsigned long __cil_tmp9 ;
2763  unsigned long __cil_tmp10 ;
2764  unsigned long __cil_tmp11 ;
2765  unsigned long __cil_tmp12 ;
2766  unsigned long __cil_tmp13 ;
2767  unsigned long __cil_tmp14 ;
2768  unsigned long __cil_tmp15 ;
2769  unsigned long __cil_tmp16 ;
2770  unsigned long __cil_tmp17 ;
2771  unsigned long __cil_tmp18 ;
2772
2773  {
2774  {
2775#line 648
2776  __cil_tmp7 = & t;
2777#line 648
2778  *((void const   **)__cil_tmp7) = buf;
2779#line 648
2780  __cil_tmp8 = (unsigned long )(& t) + 8;
2781#line 648
2782  *((void **)__cil_tmp8) = (void *)0;
2783#line 648
2784  __cil_tmp9 = (unsigned long )(& t) + 16;
2785#line 648
2786  *((unsigned int *)__cil_tmp9) = (unsigned int )len;
2787#line 648
2788  __cil_tmp10 = (unsigned long )(& t) + 24;
2789#line 648
2790  *((dma_addr_t *)__cil_tmp10) = 0ULL;
2791#line 648
2792  __cil_tmp11 = (unsigned long )(& t) + 32;
2793#line 648
2794  *((dma_addr_t *)__cil_tmp11) = 0ULL;
2795#line 648
2796  __cil_tmp12 = (unsigned long )(& t) + 40;
2797#line 648
2798  *((unsigned int *)__cil_tmp12) = 0U;
2799#line 648
2800  __cil_tmp13 = (unsigned long )(& t) + 41;
2801#line 648
2802  *((u8 *)__cil_tmp13) = (unsigned char)0;
2803#line 648
2804  __cil_tmp14 = (unsigned long )(& t) + 42;
2805#line 648
2806  *((u16 *)__cil_tmp14) = (unsigned short)0;
2807#line 648
2808  __cil_tmp15 = (unsigned long )(& t) + 44;
2809#line 648
2810  *((u32 *)__cil_tmp15) = 0U;
2811#line 648
2812  __cil_tmp16 = (unsigned long )(& t) + 48;
2813#line 648
2814  *((struct list_head **)__cil_tmp16) = (struct list_head *)0;
2815#line 648
2816  __cil_tmp17 = 48 + 8;
2817#line 648
2818  __cil_tmp18 = (unsigned long )(& t) + __cil_tmp17;
2819#line 648
2820  *((struct list_head **)__cil_tmp18) = (struct list_head *)0;
2821#line 654
2822  spi_message_init(& m);
2823#line 655
2824  spi_message_add_tail(& t, & m);
2825#line 656
2826  tmp___7 = spi_sync(spi, & m);
2827  }
2828#line 656
2829  return (tmp___7);
2830}
2831}
2832#line 143 "include/asm-generic/gpio.h"
2833extern int gpiochip_add(struct gpio_chip *chip ) ;
2834#line 144
2835extern int __attribute__((__warn_unused_result__))  gpiochip_remove(struct gpio_chip *chip ) ;
2836#line 26 "include/linux/export.h"
2837extern struct module __this_module ;
2838#line 67 "include/linux/module.h"
2839int init_module(void) ;
2840#line 68
2841void cleanup_module(void) ;
2842#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
2843static int mc33880_write_config(struct mc33880 *mc ) 
2844{ int tmp___7 ;
2845  unsigned long __cil_tmp3 ;
2846  unsigned long __cil_tmp4 ;
2847  struct spi_device *__cil_tmp5 ;
2848  unsigned long __cil_tmp6 ;
2849  unsigned long __cil_tmp7 ;
2850  u8 *__cil_tmp8 ;
2851  void const   *__cil_tmp9 ;
2852
2853  {
2854  {
2855#line 58
2856  __cil_tmp3 = (unsigned long )mc;
2857#line 58
2858  __cil_tmp4 = __cil_tmp3 + 200;
2859#line 58
2860  __cil_tmp5 = *((struct spi_device **)__cil_tmp4);
2861#line 58
2862  __cil_tmp6 = (unsigned long )mc;
2863#line 58
2864  __cil_tmp7 = __cil_tmp6 + 72;
2865#line 58
2866  __cil_tmp8 = (u8 *)__cil_tmp7;
2867#line 58
2868  __cil_tmp9 = (void const   *)__cil_tmp8;
2869#line 58
2870  tmp___7 = spi_write(__cil_tmp5, __cil_tmp9, 1UL);
2871  }
2872#line 58
2873  return (tmp___7);
2874}
2875}
2876#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
2877static int __mc33880_set(struct mc33880 *mc , unsigned int offset , int value ) 
2878{ int tmp___7 ;
2879  unsigned long __cil_tmp5 ;
2880  unsigned long __cil_tmp6 ;
2881  int __cil_tmp7 ;
2882  unsigned long __cil_tmp8 ;
2883  unsigned long __cil_tmp9 ;
2884  u8 __cil_tmp10 ;
2885  int __cil_tmp11 ;
2886  int __cil_tmp12 ;
2887  unsigned long __cil_tmp13 ;
2888  unsigned long __cil_tmp14 ;
2889  int __cil_tmp15 ;
2890  int __cil_tmp16 ;
2891  unsigned long __cil_tmp17 ;
2892  unsigned long __cil_tmp18 ;
2893  u8 __cil_tmp19 ;
2894  int __cil_tmp20 ;
2895  int __cil_tmp21 ;
2896
2897  {
2898#line 64
2899  if (value) {
2900#line 65
2901    __cil_tmp5 = (unsigned long )mc;
2902#line 65
2903    __cil_tmp6 = __cil_tmp5 + 72;
2904#line 65
2905    __cil_tmp7 = 1 << offset;
2906#line 65
2907    __cil_tmp8 = (unsigned long )mc;
2908#line 65
2909    __cil_tmp9 = __cil_tmp8 + 72;
2910#line 65
2911    __cil_tmp10 = *((u8 *)__cil_tmp9);
2912#line 65
2913    __cil_tmp11 = (int )__cil_tmp10;
2914#line 65
2915    __cil_tmp12 = __cil_tmp11 | __cil_tmp7;
2916#line 65
2917    *((u8 *)__cil_tmp6) = (u8 )__cil_tmp12;
2918  } else {
2919#line 67
2920    __cil_tmp13 = (unsigned long )mc;
2921#line 67
2922    __cil_tmp14 = __cil_tmp13 + 72;
2923#line 67
2924    __cil_tmp15 = 1 << offset;
2925#line 67
2926    __cil_tmp16 = ~ __cil_tmp15;
2927#line 67
2928    __cil_tmp17 = (unsigned long )mc;
2929#line 67
2930    __cil_tmp18 = __cil_tmp17 + 72;
2931#line 67
2932    __cil_tmp19 = *((u8 *)__cil_tmp18);
2933#line 67
2934    __cil_tmp20 = (int )__cil_tmp19;
2935#line 67
2936    __cil_tmp21 = __cil_tmp20 & __cil_tmp16;
2937#line 67
2938    *((u8 *)__cil_tmp14) = (u8 )__cil_tmp21;
2939  }
2940  {
2941#line 69
2942  tmp___7 = mc33880_write_config(mc);
2943  }
2944#line 69
2945  return (tmp___7);
2946}
2947}
2948#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
2949static void mc33880_set(struct gpio_chip *chip , unsigned int offset , int value ) 
2950{ struct mc33880 *mc ;
2951  struct gpio_chip  const  *__mptr ;
2952  struct mc33880 *__cil_tmp6 ;
2953  unsigned long __cil_tmp7 ;
2954  unsigned long __cil_tmp8 ;
2955  struct gpio_chip *__cil_tmp9 ;
2956  unsigned int __cil_tmp10 ;
2957  char *__cil_tmp11 ;
2958  char *__cil_tmp12 ;
2959  struct mutex *__cil_tmp13 ;
2960  struct mutex *__cil_tmp14 ;
2961
2962  {
2963  {
2964#line 75
2965  __mptr = (struct gpio_chip  const  *)chip;
2966#line 75
2967  __cil_tmp6 = (struct mc33880 *)0;
2968#line 75
2969  __cil_tmp7 = (unsigned long )__cil_tmp6;
2970#line 75
2971  __cil_tmp8 = __cil_tmp7 + 80;
2972#line 75
2973  __cil_tmp9 = (struct gpio_chip *)__cil_tmp8;
2974#line 75
2975  __cil_tmp10 = (unsigned int )__cil_tmp9;
2976#line 75
2977  __cil_tmp11 = (char *)__mptr;
2978#line 75
2979  __cil_tmp12 = __cil_tmp11 - __cil_tmp10;
2980#line 75
2981  mc = (struct mc33880 *)__cil_tmp12;
2982#line 77
2983  __cil_tmp13 = (struct mutex *)mc;
2984#line 77
2985  mutex_lock(__cil_tmp13);
2986#line 79
2987  __mc33880_set(mc, offset, value);
2988#line 81
2989  __cil_tmp14 = (struct mutex *)mc;
2990#line 81
2991  mutex_unlock(__cil_tmp14);
2992  }
2993#line 82
2994  return;
2995}
2996}
2997#line 92
2998static int mc33880_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
2999__no_instrument_function__)) ;
3000#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3001static struct _ddebug  __attribute__((__aligned__(8))) descriptor  __attribute__((__used__,
3002__section__("__verbose")))  =    {"gpio_mc33880", "mc33880_probe", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c",
3003    "incorrect or missing platform data\n", 92U, 1U};
3004#line 109 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3005static struct lock_class_key __key___3  ;
3006#line 84
3007static int mc33880_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
3008__no_instrument_function__)) ;
3009#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3010static int mc33880_probe(struct spi_device *spi ) 
3011{ struct mc33880 *mc ;
3012  struct mc33880_platform_data *pdata ;
3013  int ret ;
3014  long tmp___7 ;
3015  void *tmp___8 ;
3016  unsigned long __cil_tmp7 ;
3017  unsigned long __cil_tmp8 ;
3018  unsigned long __cil_tmp9 ;
3019  void *__cil_tmp10 ;
3020  unsigned int __cil_tmp11 ;
3021  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp12 ;
3022  unsigned int __cil_tmp13 ;
3023  unsigned int __cil_tmp14 ;
3024  int __cil_tmp15 ;
3025  int __cil_tmp16 ;
3026  long __cil_tmp17 ;
3027  struct device *__cil_tmp18 ;
3028  struct device  const  *__cil_tmp19 ;
3029  unsigned long __cil_tmp20 ;
3030  unsigned long __cil_tmp21 ;
3031  struct mutex *__cil_tmp22 ;
3032  struct device *__cil_tmp23 ;
3033  void *__cil_tmp24 ;
3034  unsigned long __cil_tmp25 ;
3035  unsigned long __cil_tmp26 ;
3036  unsigned long __cil_tmp27 ;
3037  unsigned long __cil_tmp28 ;
3038  unsigned long __cil_tmp29 ;
3039  unsigned long __cil_tmp30 ;
3040  unsigned long __cil_tmp31 ;
3041  unsigned long __cil_tmp32 ;
3042  unsigned long __cil_tmp33 ;
3043  unsigned long __cil_tmp34 ;
3044  unsigned int __cil_tmp35 ;
3045  unsigned long __cil_tmp36 ;
3046  unsigned long __cil_tmp37 ;
3047  unsigned long __cil_tmp38 ;
3048  unsigned long __cil_tmp39 ;
3049  unsigned long __cil_tmp40 ;
3050  unsigned long __cil_tmp41 ;
3051  unsigned long __cil_tmp42 ;
3052  unsigned long __cil_tmp43 ;
3053  unsigned long __cil_tmp44 ;
3054  unsigned long __cil_tmp45 ;
3055  unsigned long __cil_tmp46 ;
3056  unsigned long __cil_tmp47 ;
3057  unsigned long __cil_tmp48 ;
3058  unsigned long __cil_tmp49 ;
3059  unsigned long __cil_tmp50 ;
3060  unsigned long __cil_tmp51 ;
3061  unsigned long __cil_tmp52 ;
3062  unsigned long __cil_tmp53 ;
3063  struct gpio_chip *__cil_tmp54 ;
3064  struct device *__cil_tmp55 ;
3065  void *__cil_tmp56 ;
3066  struct mutex *__cil_tmp57 ;
3067  void const   *__cil_tmp58 ;
3068
3069  {
3070#line 90
3071  __cil_tmp7 = 0 + 184;
3072#line 90
3073  __cil_tmp8 = (unsigned long )spi;
3074#line 90
3075  __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
3076#line 90
3077  __cil_tmp10 = *((void **)__cil_tmp9);
3078#line 90
3079  pdata = (struct mc33880_platform_data *)__cil_tmp10;
3080#line 91
3081  if (! pdata) {
3082#line 91
3083    goto _L;
3084  } else {
3085    {
3086#line 91
3087    __cil_tmp11 = *((unsigned int *)pdata);
3088#line 91
3089    if (! __cil_tmp11) {
3090      _L: /* CIL Label */ 
3091      {
3092#line 92
3093      while (1) {
3094        while_continue: /* CIL Label */ ;
3095        {
3096#line 92
3097        while (1) {
3098          while_continue___0: /* CIL Label */ ;
3099          {
3100#line 92
3101          __cil_tmp12 = & descriptor;
3102#line 92
3103          __cil_tmp13 = __cil_tmp12->flags;
3104#line 92
3105          __cil_tmp14 = __cil_tmp13 & 1U;
3106#line 92
3107          __cil_tmp15 = ! __cil_tmp14;
3108#line 92
3109          __cil_tmp16 = ! __cil_tmp15;
3110#line 92
3111          __cil_tmp17 = (long )__cil_tmp16;
3112#line 92
3113          tmp___7 = __builtin_expect(__cil_tmp17, 0L);
3114          }
3115#line 92
3116          if (tmp___7) {
3117            {
3118#line 92
3119            __cil_tmp18 = (struct device *)spi;
3120#line 92
3121            __cil_tmp19 = (struct device  const  *)__cil_tmp18;
3122#line 92
3123            __dynamic_dev_dbg(& descriptor, __cil_tmp19, "incorrect or missing platform data\n");
3124            }
3125          } else {
3126
3127          }
3128#line 92
3129          goto while_break___0;
3130        }
3131        while_break___0: /* CIL Label */ ;
3132        }
3133#line 92
3134        goto while_break;
3135      }
3136      while_break: /* CIL Label */ ;
3137      }
3138#line 93
3139      return (-22);
3140    } else {
3141
3142    }
3143    }
3144  }
3145  {
3146#line 99
3147  __cil_tmp20 = (unsigned long )spi;
3148#line 99
3149  __cil_tmp21 = __cil_tmp20 + 782;
3150#line 99
3151  *((u8 *)__cil_tmp21) = (u8 )8;
3152#line 101
3153  ret = spi_setup(spi);
3154  }
3155#line 102
3156  if (ret < 0) {
3157#line 103
3158    return (ret);
3159  } else {
3160
3161  }
3162  {
3163#line 105
3164  tmp___8 = kzalloc(208UL, 208U);
3165#line 105
3166  mc = (struct mc33880 *)tmp___8;
3167  }
3168#line 106
3169  if (! mc) {
3170#line 107
3171    return (-12);
3172  } else {
3173
3174  }
3175  {
3176#line 109
3177  while (1) {
3178    while_continue___1: /* CIL Label */ ;
3179    {
3180#line 109
3181    __cil_tmp22 = (struct mutex *)mc;
3182#line 109
3183    __mutex_init(__cil_tmp22, "&mc->lock", & __key___3);
3184    }
3185#line 109
3186    goto while_break___1;
3187  }
3188  while_break___1: /* CIL Label */ ;
3189  }
3190  {
3191#line 111
3192  __cil_tmp23 = (struct device *)spi;
3193#line 111
3194  __cil_tmp24 = (void *)mc;
3195#line 111
3196  dev_set_drvdata(__cil_tmp23, __cil_tmp24);
3197#line 113
3198  __cil_tmp25 = (unsigned long )mc;
3199#line 113
3200  __cil_tmp26 = __cil_tmp25 + 200;
3201#line 113
3202  *((struct spi_device **)__cil_tmp26) = spi;
3203#line 115
3204  __cil_tmp27 = (unsigned long )mc;
3205#line 115
3206  __cil_tmp28 = __cil_tmp27 + 80;
3207#line 115
3208  *((char const   **)__cil_tmp28) = "mc33880";
3209#line 115
3210  __cil_tmp29 = 80 + 72;
3211#line 115
3212  __cil_tmp30 = (unsigned long )mc;
3213#line 115
3214  __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
3215#line 115
3216  *((void (**)(struct gpio_chip *chip , unsigned int offset , int value ))__cil_tmp31) = & mc33880_set;
3217#line 117
3218  __cil_tmp32 = 80 + 96;
3219#line 117
3220  __cil_tmp33 = (unsigned long )mc;
3221#line 117
3222  __cil_tmp34 = __cil_tmp33 + __cil_tmp32;
3223#line 117
3224  __cil_tmp35 = *((unsigned int *)pdata);
3225#line 117
3226  *((int *)__cil_tmp34) = (int )__cil_tmp35;
3227#line 118
3228  __cil_tmp36 = 80 + 100;
3229#line 118
3230  __cil_tmp37 = (unsigned long )mc;
3231#line 118
3232  __cil_tmp38 = __cil_tmp37 + __cil_tmp36;
3233#line 118
3234  *((u16 *)__cil_tmp38) = (u16 )8;
3235#line 119
3236  __cil_tmp39 = 80 + 112;
3237#line 119
3238  __cil_tmp40 = (unsigned long )mc;
3239#line 119
3240  __cil_tmp41 = __cil_tmp40 + __cil_tmp39;
3241#line 119
3242  *((unsigned int *)__cil_tmp41) = 1U;
3243#line 120
3244  __cil_tmp42 = 80 + 8;
3245#line 120
3246  __cil_tmp43 = (unsigned long )mc;
3247#line 120
3248  __cil_tmp44 = __cil_tmp43 + __cil_tmp42;
3249#line 120
3250  *((struct device **)__cil_tmp44) = (struct device *)spi;
3251#line 121
3252  __cil_tmp45 = 80 + 16;
3253#line 121
3254  __cil_tmp46 = (unsigned long )mc;
3255#line 121
3256  __cil_tmp47 = __cil_tmp46 + __cil_tmp45;
3257#line 121
3258  *((struct module **)__cil_tmp47) = & __this_module;
3259#line 123
3260  __cil_tmp48 = (unsigned long )mc;
3261#line 123
3262  __cil_tmp49 = __cil_tmp48 + 72;
3263#line 123
3264  *((u8 *)__cil_tmp49) = (u8 )0;
3265#line 128
3266  ret = mc33880_write_config(mc);
3267#line 129
3268  __cil_tmp50 = (unsigned long )mc;
3269#line 129
3270  __cil_tmp51 = __cil_tmp50 + 72;
3271#line 129
3272  *((u8 *)__cil_tmp51) = (u8 )0;
3273  }
3274#line 130
3275  if (! ret) {
3276    {
3277#line 131
3278    ret = mc33880_write_config(mc);
3279    }
3280  } else {
3281
3282  }
3283#line 133
3284  if (ret) {
3285    {
3286#line 134
3287    printk("<3>Failed writing to mc33880: %d\n", ret);
3288    }
3289#line 135
3290    goto exit_destroy;
3291  } else {
3292
3293  }
3294  {
3295#line 138
3296  __cil_tmp52 = (unsigned long )mc;
3297#line 138
3298  __cil_tmp53 = __cil_tmp52 + 80;
3299#line 138
3300  __cil_tmp54 = (struct gpio_chip *)__cil_tmp53;
3301#line 138
3302  ret = gpiochip_add(__cil_tmp54);
3303  }
3304#line 139
3305  if (ret) {
3306#line 140
3307    goto exit_destroy;
3308  } else {
3309
3310  }
3311#line 142
3312  return (ret);
3313  exit_destroy: 
3314  {
3315#line 145
3316  __cil_tmp55 = (struct device *)spi;
3317#line 145
3318  __cil_tmp56 = (void *)0;
3319#line 145
3320  dev_set_drvdata(__cil_tmp55, __cil_tmp56);
3321#line 146
3322  __cil_tmp57 = (struct mutex *)mc;
3323#line 146
3324  mutex_destroy(__cil_tmp57);
3325#line 147
3326  __cil_tmp58 = (void const   *)mc;
3327#line 147
3328  kfree(__cil_tmp58);
3329  }
3330#line 148
3331  return (ret);
3332}
3333}
3334#line 151
3335static int mc33880_remove(struct spi_device *spi )  __attribute__((__section__(".devexit.text"),
3336__no_instrument_function__)) ;
3337#line 151 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3338static int mc33880_remove(struct spi_device *spi ) 
3339{ struct mc33880 *mc ;
3340  int ret ;
3341  void *tmp___7 ;
3342  struct device *__cil_tmp5 ;
3343  struct device  const  *__cil_tmp6 ;
3344  void *__cil_tmp7 ;
3345  unsigned long __cil_tmp8 ;
3346  unsigned long __cil_tmp9 ;
3347  struct device *__cil_tmp10 ;
3348  void *__cil_tmp11 ;
3349  unsigned long __cil_tmp12 ;
3350  unsigned long __cil_tmp13 ;
3351  struct gpio_chip *__cil_tmp14 ;
3352  struct mutex *__cil_tmp15 ;
3353  void const   *__cil_tmp16 ;
3354  struct device *__cil_tmp17 ;
3355  struct device  const  *__cil_tmp18 ;
3356
3357  {
3358  {
3359#line 156
3360  __cil_tmp5 = (struct device *)spi;
3361#line 156
3362  __cil_tmp6 = (struct device  const  *)__cil_tmp5;
3363#line 156
3364  tmp___7 = dev_get_drvdata(__cil_tmp6);
3365#line 156
3366  mc = (struct mc33880 *)tmp___7;
3367  }
3368  {
3369#line 157
3370  __cil_tmp7 = (void *)0;
3371#line 157
3372  __cil_tmp8 = (unsigned long )__cil_tmp7;
3373#line 157
3374  __cil_tmp9 = (unsigned long )mc;
3375#line 157
3376  if (__cil_tmp9 == __cil_tmp8) {
3377#line 158
3378    return (-19);
3379  } else {
3380
3381  }
3382  }
3383  {
3384#line 160
3385  __cil_tmp10 = (struct device *)spi;
3386#line 160
3387  __cil_tmp11 = (void *)0;
3388#line 160
3389  dev_set_drvdata(__cil_tmp10, __cil_tmp11);
3390#line 162
3391  __cil_tmp12 = (unsigned long )mc;
3392#line 162
3393  __cil_tmp13 = __cil_tmp12 + 80;
3394#line 162
3395  __cil_tmp14 = (struct gpio_chip *)__cil_tmp13;
3396#line 162
3397  ret = (int )gpiochip_remove(__cil_tmp14);
3398  }
3399#line 163
3400  if (! ret) {
3401    {
3402#line 164
3403    __cil_tmp15 = (struct mutex *)mc;
3404#line 164
3405    mutex_destroy(__cil_tmp15);
3406#line 165
3407    __cil_tmp16 = (void const   *)mc;
3408#line 165
3409    kfree(__cil_tmp16);
3410    }
3411  } else {
3412    {
3413#line 167
3414    __cil_tmp17 = (struct device *)spi;
3415#line 167
3416    __cil_tmp18 = (struct device  const  *)__cil_tmp17;
3417#line 167
3418    dev_err(__cil_tmp18, "Failed to remove the GPIO controller: %d\n", ret);
3419    }
3420  }
3421#line 170
3422  return (ret);
3423}
3424}
3425#line 173 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3426static struct spi_driver mc33880_driver  =    {(struct spi_device_id  const  *)0, & mc33880_probe, & mc33880_remove, (void (*)(struct spi_device *spi ))0,
3427    (int (*)(struct spi_device *spi , pm_message_t mesg ))0, (int (*)(struct spi_device *spi ))0,
3428    {"mc33880", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
3429     (struct of_device_id  const  *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3430     (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
3431     (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
3432     (struct driver_private *)0}};
3433#line 182
3434static int mc33880_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
3435#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3436static int mc33880_init(void) 
3437{ int tmp___7 ;
3438
3439  {
3440  {
3441#line 184
3442  tmp___7 = spi_register_driver(& mc33880_driver);
3443  }
3444#line 184
3445  return (tmp___7);
3446}
3447}
3448#line 189 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3449int init_module(void) 
3450{ int tmp___7 ;
3451
3452  {
3453  {
3454#line 189
3455  tmp___7 = mc33880_init();
3456  }
3457#line 189
3458  return (tmp___7);
3459}
3460}
3461#line 191
3462static void mc33880_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
3463#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3464static void mc33880_exit(void) 
3465{ 
3466
3467  {
3468  {
3469#line 193
3470  spi_unregister_driver(& mc33880_driver);
3471  }
3472#line 194
3473  return;
3474}
3475}
3476#line 195 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3477void cleanup_module(void) 
3478{ 
3479
3480  {
3481  {
3482#line 195
3483  mc33880_exit();
3484  }
3485#line 195
3486  return;
3487}
3488}
3489#line 197 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3490static char const   __mod_author197[50]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3491__aligned__(1)))  = 
3492#line 197
3493  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
3494        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'M', 
3495        (char const   )'o',      (char const   )'c',      (char const   )'e',      (char const   )'a', 
3496        (char const   )'n',      (char const   )' ',      (char const   )'L',      (char const   )'a', 
3497        (char const   )'b',      (char const   )'o',      (char const   )'r',      (char const   )'a', 
3498        (char const   )'t',      (char const   )'o',      (char const   )'r',      (char const   )'i', 
3499        (char const   )'e',      (char const   )'s',      (char const   )' ',      (char const   )'<', 
3500        (char const   )'i',      (char const   )'n',      (char const   )'f',      (char const   )'o', 
3501        (char const   )'@',      (char const   )'m',      (char const   )'o',      (char const   )'c', 
3502        (char const   )'e',      (char const   )'a',      (char const   )'n',      (char const   )'-', 
3503        (char const   )'l',      (char const   )'a',      (char const   )'b',      (char const   )'s', 
3504        (char const   )'.',      (char const   )'c',      (char const   )'o',      (char const   )'m', 
3505        (char const   )'>',      (char const   )'\000'};
3506#line 198 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3507static char const   __mod_license198[15]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3508__aligned__(1)))  = 
3509#line 198
3510  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
3511        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
3512        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )' ', 
3513        (char const   )'v',      (char const   )'2',      (char const   )'\000'};
3514#line 217
3515void ldv_check_final_state(void) ;
3516#line 220
3517extern void ldv_check_return_value(int res ) ;
3518#line 223
3519extern void ldv_initialize(void) ;
3520#line 226
3521extern int __VERIFIER_nondet_int(void) ;
3522#line 229 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3523int LDV_IN_INTERRUPT  ;
3524#line 251 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3525static int res_mc33880_probe_3  ;
3526#line 232 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3527void main(void) 
3528{ struct spi_device *var_group1 ;
3529  int tmp___7 ;
3530  int ldv_s_mc33880_driver_spi_driver ;
3531  int tmp___8 ;
3532  int tmp___9 ;
3533  int __cil_tmp6 ;
3534
3535  {
3536  {
3537#line 259
3538  LDV_IN_INTERRUPT = 1;
3539#line 268
3540  ldv_initialize();
3541#line 281
3542  tmp___7 = mc33880_init();
3543  }
3544#line 281
3545  if (tmp___7) {
3546#line 282
3547    goto ldv_final;
3548  } else {
3549
3550  }
3551#line 283
3552  ldv_s_mc33880_driver_spi_driver = 0;
3553  {
3554#line 286
3555  while (1) {
3556    while_continue: /* CIL Label */ ;
3557    {
3558#line 286
3559    tmp___9 = __VERIFIER_nondet_int();
3560    }
3561#line 286
3562    if (tmp___9) {
3563
3564    } else {
3565      {
3566#line 286
3567      __cil_tmp6 = ldv_s_mc33880_driver_spi_driver == 0;
3568#line 286
3569      if (! __cil_tmp6) {
3570
3571      } else {
3572#line 286
3573        goto while_break;
3574      }
3575      }
3576    }
3577    {
3578#line 290
3579    tmp___8 = __VERIFIER_nondet_int();
3580    }
3581#line 292
3582    if (tmp___8 == 0) {
3583#line 292
3584      goto case_0;
3585    } else {
3586      {
3587#line 318
3588      goto switch_default;
3589#line 290
3590      if (0) {
3591        case_0: /* CIL Label */ 
3592#line 295
3593        if (ldv_s_mc33880_driver_spi_driver == 0) {
3594          {
3595#line 307
3596          res_mc33880_probe_3 = mc33880_probe(var_group1);
3597#line 308
3598          ldv_check_return_value(res_mc33880_probe_3);
3599          }
3600#line 309
3601          if (res_mc33880_probe_3) {
3602#line 310
3603            goto ldv_module_exit;
3604          } else {
3605
3606          }
3607#line 311
3608          ldv_s_mc33880_driver_spi_driver = 0;
3609        } else {
3610
3611        }
3612#line 317
3613        goto switch_break;
3614        switch_default: /* CIL Label */ 
3615#line 318
3616        goto switch_break;
3617      } else {
3618        switch_break: /* CIL Label */ ;
3619      }
3620      }
3621    }
3622  }
3623  while_break: /* CIL Label */ ;
3624  }
3625  ldv_module_exit: 
3626  {
3627#line 337
3628  mc33880_exit();
3629  }
3630  ldv_final: 
3631  {
3632#line 340
3633  ldv_check_final_state();
3634  }
3635#line 343
3636  return;
3637}
3638}
3639#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3640void ldv_blast_assert(void) 
3641{ 
3642
3643  {
3644  ERROR: 
3645#line 6
3646  goto ERROR;
3647}
3648}
3649#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3650extern int __VERIFIER_nondet_int(void) ;
3651#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3652int ldv_mutex  =    1;
3653#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3654int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
3655{ int nondetermined ;
3656
3657  {
3658#line 29
3659  if (ldv_mutex == 1) {
3660
3661  } else {
3662    {
3663#line 29
3664    ldv_blast_assert();
3665    }
3666  }
3667  {
3668#line 32
3669  nondetermined = __VERIFIER_nondet_int();
3670  }
3671#line 35
3672  if (nondetermined) {
3673#line 38
3674    ldv_mutex = 2;
3675#line 40
3676    return (0);
3677  } else {
3678#line 45
3679    return (-4);
3680  }
3681}
3682}
3683#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3684int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
3685{ int nondetermined ;
3686
3687  {
3688#line 57
3689  if (ldv_mutex == 1) {
3690
3691  } else {
3692    {
3693#line 57
3694    ldv_blast_assert();
3695    }
3696  }
3697  {
3698#line 60
3699  nondetermined = __VERIFIER_nondet_int();
3700  }
3701#line 63
3702  if (nondetermined) {
3703#line 66
3704    ldv_mutex = 2;
3705#line 68
3706    return (0);
3707  } else {
3708#line 73
3709    return (-4);
3710  }
3711}
3712}
3713#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3714int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
3715{ int atomic_value_after_dec ;
3716
3717  {
3718#line 83
3719  if (ldv_mutex == 1) {
3720
3721  } else {
3722    {
3723#line 83
3724    ldv_blast_assert();
3725    }
3726  }
3727  {
3728#line 86
3729  atomic_value_after_dec = __VERIFIER_nondet_int();
3730  }
3731#line 89
3732  if (atomic_value_after_dec == 0) {
3733#line 92
3734    ldv_mutex = 2;
3735#line 94
3736    return (1);
3737  } else {
3738
3739  }
3740#line 98
3741  return (0);
3742}
3743}
3744#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3745void mutex_lock(struct mutex *lock ) 
3746{ 
3747
3748  {
3749#line 108
3750  if (ldv_mutex == 1) {
3751
3752  } else {
3753    {
3754#line 108
3755    ldv_blast_assert();
3756    }
3757  }
3758#line 110
3759  ldv_mutex = 2;
3760#line 111
3761  return;
3762}
3763}
3764#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3765int mutex_trylock(struct mutex *lock ) 
3766{ int nondetermined ;
3767
3768  {
3769#line 121
3770  if (ldv_mutex == 1) {
3771
3772  } else {
3773    {
3774#line 121
3775    ldv_blast_assert();
3776    }
3777  }
3778  {
3779#line 124
3780  nondetermined = __VERIFIER_nondet_int();
3781  }
3782#line 127
3783  if (nondetermined) {
3784#line 130
3785    ldv_mutex = 2;
3786#line 132
3787    return (1);
3788  } else {
3789#line 137
3790    return (0);
3791  }
3792}
3793}
3794#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3795void mutex_unlock(struct mutex *lock ) 
3796{ 
3797
3798  {
3799#line 147
3800  if (ldv_mutex == 2) {
3801
3802  } else {
3803    {
3804#line 147
3805    ldv_blast_assert();
3806    }
3807  }
3808#line 149
3809  ldv_mutex = 1;
3810#line 150
3811  return;
3812}
3813}
3814#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3815void ldv_check_final_state(void) 
3816{ 
3817
3818  {
3819#line 156
3820  if (ldv_mutex == 1) {
3821
3822  } else {
3823    {
3824#line 156
3825    ldv_blast_assert();
3826    }
3827  }
3828#line 157
3829  return;
3830}
3831}
3832#line 352 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5850/dscv_tempdir/dscv/ri/32_1/drivers/gpio/gpio-mc33880.c.common.c"
3833long s__builtin_expect(long val , long res ) 
3834{ 
3835
3836  {
3837#line 353
3838  return (val);
3839}
3840}